chore: fill in machine todos and cost model for case and constr

This allows for several more tests to pass
**Had to remove case-7 since it was incorrectly passing before**
This commit is contained in:
microproofs 2023-11-17 19:52:03 -05:00
parent 0382e5ce12
commit 1567e42875
24 changed files with 60 additions and 12 deletions

View File

@ -240,9 +240,12 @@ impl Machine {
env, env,
t.clone(), t.clone(),
)), )),
None => todo!(), None => Err(Error::MissingCaseBranch(
branches,
Value::Constr { tag, fields },
)),
}, },
_ => todo!("return a proper evaluation error"), v => Err(Error::NonConstrScrutinized(v)),
}, },
} }
} }

View File

@ -186,12 +186,12 @@ impl Default for MachineCosts {
}, },
// Placeholder values // Placeholder values
constr: ExBudget { constr: ExBudget {
mem: 30000000000, mem: 100,
cpu: 30000000000, cpu: 23000,
}, },
case: ExBudget { case: ExBudget {
mem: 30000000000, mem: 100,
cpu: 30000000000, cpu: 23000,
}, },
} }
} }

View File

@ -20,6 +20,10 @@ pub enum Error {
NonPolymorphicInstantiation(Value), NonPolymorphicInstantiation(Value),
#[error("Attempted to apply a non-function:\n\n{0:#?} to argument:\n\n{1:#?}")] #[error("Attempted to apply a non-function:\n\n{0:#?} to argument:\n\n{1:#?}")]
NonFunctionalApplication(Value, Value), 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}'")] #[error("Type mismatch expected '{0}' got '{1}'")]
TypeMismatch(Type, Type), TypeMismatch(Type, Type),
#[error("Type mismatch expected '(list a)' got '{0}'")] #[error("Type mismatch expected '(list a)' got '{0}'")]
@ -36,6 +40,7 @@ pub enum Error {
NotAConstant(Value), NotAConstant(Value),
#[error("The evaluation never reached a final state")] #[error("The evaluation never reached a final state")]
MachineNeverReachedDone, MachineNeverReachedDone,
#[error("Decoding utf8")] #[error("Decoding utf8")]
Utf8(#[from] FromUtf8Error), Utf8(#[from] FromUtf8Error),
#[error("Out of Bounds\n\nindex: {}\nbytestring: {}\npossible: 0 - {}", .0, hex::encode(.1), .1.len() - 1)] #[error("Out of Bounds\n\nindex: {}\nbytestring: {}\npossible: 0 - {}", .0, hex::encode(.1), .1.len() - 1)]

View File

@ -145,7 +145,7 @@ peg::parser! {
} }
rule case(interner: &mut Interner) -> Term<Name> 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 } Term::Case { constr: constr.into(), branches }
} }

View File

@ -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)))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (con integer 1))

View File

@ -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)))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (con integer 2))

View File

@ -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])))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (con integer 5))

View File

@ -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])))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (con integer 1))

View File

@ -0,0 +1,4 @@
-- case of non-constr
(program 1.1.0
(case (con integer 1) (lam x x) (lam x x))
)

View File

@ -0,0 +1 @@
evaluation failure

View File

@ -1,4 +0,0 @@
-- case can't be used before 1.1.0
(program 1.0.0
(case (con integer 1))
)

View File

@ -0,0 +1,4 @@
-- nullary case
(program 1.1.0
(case (constr 0) (con integer 1) (con integer 2))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (con integer 1))

View File

@ -0,0 +1,4 @@
-- empty case, aka -XEmptyCase
(program 1.1.0
(case (constr 0))
)

View File

@ -0,0 +1 @@
evaluation failure

View File

@ -0,0 +1,4 @@
-- empty constr
(program 1.1.0
(constr 0 )
)

View File

@ -0,0 +1 @@
(program 1.1.0 (constr 0))

View File

@ -0,0 +1,4 @@
-- constr with an argument
(program 1.1.0
(constr 0 (con integer 1))
)

View File

@ -0,0 +1 @@
(program 1.1.0 (constr 0 (con integer 1)))