Skip to content

Commit

Permalink
chore: fill in machine todos and cost model for case and constr
Browse files Browse the repository at this point in the history
This allows for several more tests to pass
**Had to remove case-7 since it was incorrectly passing before**
  • Loading branch information
MicroProofs committed Nov 18, 2023
1 parent 0382e5c commit 1567e42
Show file tree
Hide file tree
Showing 24 changed files with 60 additions and 12 deletions.
7 changes: 5 additions & 2 deletions crates/uplc/src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -240,9 +240,12 @@ impl Machine {
env,
t.clone(),
)),
None => todo!(),
None => Err(Error::MissingCaseBranch(
branches,
Value::Constr { tag, fields },
)),
},
_ => todo!("return a proper evaluation error"),
v => Err(Error::NonConstrScrutinized(v)),
},
}
}
Expand Down
8 changes: 4 additions & 4 deletions crates/uplc/src/machine/cost_model.rs
Original file line number Diff line number Diff line change
Expand Up @@ -186,12 +186,12 @@ impl Default for MachineCosts {
},
// Placeholder values
constr: ExBudget {
mem: 30000000000,
cpu: 30000000000,
mem: 100,
cpu: 23000,
},
case: ExBudget {
mem: 30000000000,
cpu: 30000000000,
mem: 100,
cpu: 23000,
},
}
}
Expand Down
5 changes: 5 additions & 0 deletions crates/uplc/src/machine/error.rs
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,10 @@ pub enum Error {
NonPolymorphicInstantiation(Value),
#[error("Attempted to apply a non-function:\n\n{0:#?} to argument:\n\n{1:#?}")]
NonFunctionalApplication(Value, Value),
#[error("Attempted to case a non-const:\n\n{0:#?}")]
NonConstrScrutinized(Value),
#[error("Cases: {0:#?}\n\n are missing branch for constr:\n\n{1:#?}")]
MissingCaseBranch(Vec<Term<NamedDeBruijn>>, Value),
#[error("Type mismatch expected '{0}' got '{1}'")]
TypeMismatch(Type, Type),
#[error("Type mismatch expected '(list a)' got '{0}'")]
Expand All @@ -36,6 +40,7 @@ pub enum Error {
NotAConstant(Value),
#[error("The evaluation never reached a final state")]
MachineNeverReachedDone,

#[error("Decoding utf8")]
Utf8(#[from] FromUtf8Error),
#[error("Out of Bounds\n\nindex: {}\nbytestring: {}\npossible: 0 - {}", .0, hex::encode(.1), .1.len() - 1)]
Expand Down
2 changes: 1 addition & 1 deletion crates/uplc/src/parser.rs
Original file line number Diff line number Diff line change
Expand Up @@ -145,7 +145,7 @@ peg::parser! {
}

rule case(interner: &mut Interner) -> Term<Name>
= "(" _* "case" _+ constr:term(interner) _* branches:(t:term(interner) _* { t })+ _* ")" {
= "(" _* "case" _+ constr:term(interner) _* branches:(t:term(interner) _* { t })* _* ")" {
Term::Case { constr: constr.into(), branches }
}

Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- select first branch
(program 1.1.0
(case (constr 0 (con integer 0)) (lam x (con integer 1)) (lam x (con integer 2)))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (con integer 1))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- select second branch
(program 1.1.0
(case (constr 1 (con integer 0)) (lam x (con integer 1)) (lam x (con integer 2)))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (con integer 2))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- select first branch and do computation with the args
(program 1.1.0
(case (constr 0 (con integer 3) (con integer 2)) (lam x (lam y [(builtin addInteger) x y])) (lam x (lam y [(builtin subtractInteger) x y])))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (con integer 5))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- select second branch and do computation with the args
(program 1.1.0
(case (constr 1 (con integer 3) (con integer 2)) (lam x (lam y [(builtin addInteger) x y])) (lam x (lam y [(builtin subtractInteger) x y])))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (con integer 1))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- case of non-constr
(program 1.1.0
(case (con integer 1) (lam x x) (lam x x))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
evaluation failure

This file was deleted.

This file was deleted.

Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- nullary case
(program 1.1.0
(case (constr 0) (con integer 1) (con integer 2))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (con integer 1))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- empty case, aka -XEmptyCase
(program 1.1.0
(case (constr 0))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
evaluation failure
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- empty constr
(program 1.1.0
(constr 0 )
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (constr 0))
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
-- constr with an argument
(program 1.1.0
(constr 0 (con integer 1))
)
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
(program 1.1.0 (constr 0 (con integer 1)))

0 comments on commit 1567e42

Please sign in to comment.