diff --git a/benches/fibonacci.rs b/benches/fibonacci.rs index 0d665a4c85..a27d2c508c 100644 --- a/benches/fibonacci.rs +++ b/benches/fibonacci.rs @@ -38,7 +38,7 @@ fn fib(store: &Store, state: Rc>, _a: u64) -> Pt // nth Fibonacci number to `a`. // means of computing it.] fn fib_frame(n: usize) -> usize { - 11 + 16 * n + 11 + 10 * n } // Set the limit so the last step will be filled exactly, since Lurk currently only pads terminal/error continuations. diff --git a/examples/fibonacci.rs b/examples/fibonacci.rs index 2a41ae5bad..a9d1f29c75 100644 --- a/examples/fibonacci.rs +++ b/examples/fibonacci.rs @@ -18,7 +18,7 @@ fn fib_expr(store: &Store) -> Ptr { // The env output in the `fib_frame`th frame of the above, infinite Fibonacci computation contains a binding of the // nth Fibonacci number to `a`. fn fib_frame(n: usize) -> usize { - 11 + 16 * n + 11 + 10 * n } // Set the limit so the last step will be filled exactly, since Lurk currently only pads terminal/error continuations. diff --git a/src/lem/eval.rs b/src/lem/eval.rs index b63a0e3e7e..869bee6b4e 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -674,20 +674,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let env: Expr::Cons = cons2(smaller_rec_env, smaller_env); return (env) }); - let extract_arg = func!(extract_arg(args): 2 => { - match args.tag { - Expr::Nil => { - let dummy = Symbol("dummy"); - let nil = Symbol("nil"); - let nil = cast(nil, Expr::Nil); - return (dummy, nil) - } - Expr::Cons => { - let (arg, rest) = decons2(args); - return (arg, rest) - } - } - }); let expand_bindings = func!(expand_bindings(head, body, body1, rest_bindings): 1 => { match rest_bindings.tag { Expr::Nil => { @@ -824,31 +810,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { }; return (nil) }); - let make_call = func!(make_call(head, rest, env, cont): 4 => { - let ret = Symbol("return"); - let foo: Expr::Nil; - match rest.tag { - Expr::Nil => { - let cont: Cont::Call0 = cons4(env, cont, foo, foo); - return (head, env, cont, ret) - } - Expr::Cons => { - let (arg, more_args) = decons2(rest); - match more_args.tag { - Expr::Nil => { - let cont: Cont::Call = cons4(arg, env, cont, foo); - return (head, env, cont, ret) - } - }; - let nil = Symbol("nil"); - let nil = cast(nil, Expr::Nil); - let expanded_inner0: Expr::Cons = cons2(arg, nil); - let expanded_inner: Expr::Cons = cons2(head, expanded_inner0); - let expanded: Expr::Cons = cons2(expanded_inner, more_args); - return (expanded, env, cont, ret) - } - } - }); let is_potentially_fun = func!(is_potentially_fun(head): 1 => { let fun: Expr::Fun; let cons: Expr::Cons; @@ -935,12 +896,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { if eq_val { return (val_or_more_rec_env, env, cont, apply) } - match cont.tag { - Cont::Lookup => { - return (expr, smaller_env, cont, ret) - } - }; - let cont: Cont::Lookup = cons4(env, cont, foo, foo); return (expr, smaller_env, cont, ret) } Expr::Cons => { @@ -951,10 +906,10 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { match val2.tag { Expr::Fun => { // if `val2` is a closure, then extend its environment - let (arg, body, closed_env) = decons3(val2); + let (arg, body, closed_env, _foo) = decons4(val2); let extended: Expr::Cons = cons2(binding, closed_env); // and return the extended closure - let fun: Expr::Fun = cons3(arg, body, extended); + let fun: Expr::Fun = cons4(arg, body, extended, foo); return (fun, env, cont, apply) } }; @@ -962,13 +917,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (val2, env, cont, apply) } let (env_to_use) = env_to_use(smaller_env, val_or_more_rec_env); - - match cont.tag { - Cont::Lookup => { - return (expr, env_to_use, cont, ret) - } - }; - let cont: Cont::Lookup = cons4(env, cont, foo, foo); return (expr, env_to_use, cont, ret) } }; @@ -1029,22 +977,30 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { } match symbol head { "lambda" => { - let (args, body) = car_cdr(rest); - let (arg, cdr_args) = extract_arg(args); - - match arg.tag { - Expr::Sym => { - match cdr_args.tag { - Expr::Nil => { - let function: Expr::Fun = cons3(arg, body, env); - return (function, env, cont, apply) + let (vars, rest) = car_cdr(rest); + let rest_nil = eq_tag(rest, nil); + if rest_nil { + return (expr, env, err, errctrl) + } + let (body, end) = car_cdr(rest); + let end_nil = eq_tag(end, nil); + if !end_nil { + return (expr, env, err, errctrl) + } + match vars.tag { + Expr::Cons => { + let (var, _rest_vars) = decons2(vars); + match var.tag { + Expr::Sym => { + let fun: Expr::Fun = cons4(vars, body, env, foo); + return (fun, env, cont, apply) } }; - let inner: Expr::Cons = cons2(cdr_args, body); - let l: Expr::Cons = cons2(head, inner); - let inner_body: Expr::Cons = cons2(l, nil); - let function: Expr::Fun = cons3(arg, inner_body, env); - return (function, env, cont, apply) + return (expr, env, err, errctrl) + } + Expr::Nil => { + let fun: Expr::Fun = cons4(vars, body, env, foo); + return (fun, env, cont, apply) } }; return (expr, env, err, errctrl) @@ -1095,7 +1051,7 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (expr, env, err, errctrl) } }; - let cont: Cont::If = cons4(more, cont, foo, foo); + let cont: Cont::If = cons4(more, env, cont, foo); return (condition, env, cont, ret) } "current-env" => { @@ -1142,16 +1098,18 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let is_cproc_is_t = eq_val(is_cproc, t); if is_cproc_is_t { if rest_is_nil { - let cont: Cont::Cproc = cons4(head, nil, nil, cont); + let args: Expr::Cons = cons2(nil, nil); + let cont: Cont::Cproc = cons4(head, args, env, cont); return (nil, env, cont, apply); } let (arg, unevaled_args) = car_cdr(rest); - let cont: Cont::Cproc = cons4(head, unevaled_args, nil, cont); + let args: Expr::Cons = cons2(unevaled_args, nil); + let cont: Cont::Cproc = cons4(head, args, env, cont); return (arg, env, cont, ret); } // just call assuming that the symbol is bound to a function - let (fun, env, cont, ret) = make_call(head, rest, env, cont); - return (fun, env, cont, ret); + let cont: Cont::Call = cons4(rest, env, cont, foo); + return (head, env, cont, ret); } }; @@ -1159,8 +1117,8 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let (potentially_fun) = is_potentially_fun(head); let eq_val = eq_val(potentially_fun, t); if eq_val { - let (fun, env, cont, ret) = make_call(head, rest, env, cont); - return (fun, env, cont, ret); + let cont: Cont::Call = cons4(rest, env, cont, foo); + return (head, env, cont, ret); } return (expr, env, err, errctrl) } @@ -1200,17 +1158,6 @@ fn choose_cproc_call(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { let car_cdr = car_cdr(); - let make_tail_continuation = func!(make_tail_continuation(env, continuation): 1 => { - match continuation.tag { - Cont::Tail => { - return (continuation); - } - }; - let foo: Expr::Nil; - let tail_continuation: Cont::Tail = cons4(env, continuation, foo, foo); - return (tail_continuation); - }); - let extend_rec = func!(extend_rec(env, var, result): 1 => { let nil = Symbol("nil"); let nil = cast(nil, Expr::Nil); @@ -1272,15 +1219,6 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { match symbol ctrl { "apply-continuation" => { let makethunk = Symbol("make-thunk"); - let lookup: Cont::Lookup; - let tail: Cont::Tail; - let cont_is_lookup = eq_tag(cont, lookup); - let cont_is_tail = eq_tag(cont, tail); - let cont_is_tail_or_lookup = or(cont_is_lookup, cont_is_tail); - if cont_is_tail_or_lookup { - let (saved_env, continuation, _foo, _foo) = decons4(cont); - return (result, saved_env, continuation, makethunk) - } let errctrl = Symbol("error"); let ret = Symbol("return"); @@ -1296,71 +1234,79 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { let term: Cont::Terminal = HASH_8_ZEROS; match cont.tag { Cont::Outermost => { - return (result, env, term, ret) + // We erase the environment as to not leak any information about internal variables. + return (result, nil, term, ret) } Cont::Emit => { let (cont, _rest, _foo, _foo) = decons4(cont); return (result, env, cont, makethunk) } - Cont::Call0 => { - let (saved_env, continuation, _foo, _foo) = decons4(cont); + Cont::Call => { match result.tag { Expr::Fun => { - let (arg, body, closed_env) = decons3(result); - match symbol arg { - "dummy" => { - match body.tag { + let (args, args_env, continuation, _foo) = decons4(cont); + let (vars, body, fun_env, _foo) = decons4(result); + match args.tag { + Expr::Cons => { + match vars.tag { Expr::Nil => { + // Cannot apply non-zero number of arguments to a zero argument function return (result, env, err, errctrl) } - }; - let (body_form, end) = car_cdr(body); - match end.tag { + Expr::Cons => { + let (arg, rest_args) = decons2(args); + let newer_cont: Cont::Call2 = cons4(result, rest_args, args_env, continuation); + return (arg, args_env, newer_cont, ret) + } + } + } + Expr::Nil => { + match vars.tag { Expr::Nil => { - let (cont) = make_tail_continuation(saved_env, continuation); - return (body_form, closed_env, cont, ret) + return (body, fun_env, continuation, ret) } - }; - return (result, env, err, errctrl) + Expr::Cons => { + // TODO should we not fail here in an analogous way to the non-zero application + // on a zero argument function case? + return (result, env, continuation, ret) + } + } } - }; - return (result, env, continuation, ret) - } - }; - return (result, env, err, errctrl) - } - Cont::Call => { - match result.tag { - Expr::Fun => { - let (unevaled_arg, saved_env, continuation, _foo) = decons4(cont); - let newer_cont: Cont::Call2 = cons4(result, saved_env, continuation, foo); - return (unevaled_arg, env, newer_cont, ret) + } } }; return (result, env, err, errctrl) } Cont::Call2 => { - let (function, saved_env, continuation, _foo) = decons4(cont); + let (function, args, args_env, continuation) = decons4(cont); match function.tag { Expr::Fun => { - let (arg, body, closed_env) = decons3(function); - match symbol arg { - "dummy" => { - return (result, env, err, errctrl) - } - }; - match body.tag { - Expr::Nil => { - return (result, env, err, errctrl) + let (vars, body, fun_env, _foo) = decons4(function); + // vars must be non-empty, so: + let (var, rest_vars) = decons2(vars); + let binding: Expr::Cons = cons2(var, result); + let ext_env: Expr::Cons = cons2(binding, fun_env); + let rest_vars_empty = eq_tag(rest_vars, nil); + let args_empty = eq_tag(args, nil); + if rest_vars_empty { + if args_empty { + return (body, ext_env, continuation, ret) } - }; - let (body_form, end) = decons2(body); - match end.tag { - Expr::Nil => { - let binding: Expr::Cons = cons2(arg, result); - let newer_env: Expr::Cons = cons2(binding, closed_env); - let (cont) = make_tail_continuation(saved_env, continuation); - return (body_form, newer_env, cont, ret) + // Oversaturated call + let cont: Cont::Call = cons4(args, args_env, continuation, foo); + return (body, ext_env, cont, ret) + } + let ext_function: Expr::Fun = cons4(rest_vars, body, ext_env, foo); + let (var, _rest_vars) = car_cdr(rest_vars); + match var.tag { + Expr::Sym => { + if args_empty { + // Undersaturated call + return (ext_function, ext_env, continuation, ret) + } + let (arg, rest_args) = decons2(args); + let cont: Cont::Call2 = cons4(ext_function, rest_args, args_env, continuation); + return (arg, args_env, cont, ret) } }; return (result, env, err, errctrl) @@ -1371,14 +1317,12 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { Cont::Let => { let (var, saved_env, body, cont) = decons4(cont); let binding: Expr::Cons = cons2(var, result); - let extended_env: Expr::Cons = cons2(binding, env); - let (cont) = make_tail_continuation(saved_env, cont); + let extended_env: Expr::Cons = cons2(binding, saved_env); return (body, extended_env, cont, ret) } Cont::LetRec => { let (var, saved_env, body, cont) = decons4(cont); - let (extended_env) = extend_rec(env, var, result); - let (cont) = make_tail_continuation(saved_env, cont); + let (extended_env) = extend_rec(saved_env, var, result); return (body, extended_env, cont, ret) } Cont::Unop => { @@ -1721,41 +1665,43 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { return (result, env, err, errctrl) } Cont::If => { - let (unevaled_args, continuation, _foo, _foo) = decons4(cont); + let (unevaled_args, args_env, continuation, _foo) = decons4(cont); let (arg1, more) = car_cdr(unevaled_args); let (arg2, end) = car_cdr(more); match end.tag { Expr::Nil => { match result.tag { Expr::Nil => { - return (arg2, env, continuation, ret) + return (arg2, args_env, continuation, ret) } }; - return (arg1, env, continuation, ret) + return (arg1, args_env, continuation, ret) } }; return (arg1, env, err, errctrl) } Cont::Cproc => { - let (cproc_name, unevaled_args, evaluated_args, cont) = decons4(cont); + let (cproc_name, args, saved_env, cont) = decons4(cont); + let (unevaled_args, evaluated_args) = decons2(args); // accumulate the evaluated arg (`result`) let evaluated_args: Expr::Cons = cons2(result, evaluated_args); match unevaled_args.tag { Expr::Nil => { // nothing else to evaluate - let (expr, env, cont, ctrl) = choose_cproc_call(cproc_name, evaluated_args, env, cont); + let (expr, env, cont, ctrl) = choose_cproc_call(cproc_name, evaluated_args, saved_env, cont); return (expr, env, cont, ctrl); } Expr::Cons => { // pop the next argument that needs to be evaluated let (arg, unevaled_args) = decons2(unevaled_args); + let args: Expr::Cons = cons2(unevaled_args, evaluated_args); let cont: Cont::Cproc = cons4( cproc_name, - unevaled_args, - evaluated_args, + args, + saved_env, cont ); - return (arg, env, cont, ret); + return (arg, saved_env, cont, ret); } } } @@ -1771,15 +1717,11 @@ fn make_thunk() -> Func { match symbol ctrl { "make-thunk" => { match cont.tag { - Cont::Tail => { - let (saved_env, saved_cont, _foo, _foo) = decons4(cont); - let thunk: Expr::Thunk = cons2(expr, saved_cont); - let cont: Cont::Dummy = HASH_8_ZEROS; - return (thunk, saved_env, cont) - } Cont::Outermost => { + let nil = Symbol("nil"); + let nil = cast(nil, Expr::Nil); let cont: Cont::Terminal = HASH_8_ZEROS; - return (expr, env, cont) + return (expr, nil, cont) } }; let thunk: Expr::Thunk = cons2(expr, cont); @@ -1814,8 +1756,8 @@ mod tests { func.slots_count, SlotsCounter { hash4: 14, - hash6: 3, - hash8: 4, + hash6: 0, + hash8: 6, commitment: 1, bit_decomp: 3, } @@ -1824,8 +1766,8 @@ mod tests { expected.assert_eq(&computed.to_string()); }; expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["9118"]); - expect_eq(cs.num_constraints(), expect!["11064"]); + expect_eq(cs.aux().len(), expect!["8823"]); + expect_eq(cs.num_constraints(), expect!["10628"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/lem/store.rs b/src/lem/store.rs index 378481f36f..acb504d97a 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -535,7 +535,7 @@ impl Store { #[inline] pub fn intern_fun(&self, arg: Ptr, body: Ptr, env: Ptr) -> Ptr { - self.intern_3_ptrs(Tag::Expr(Fun), arg, body, env) + self.intern_4_ptrs(Tag::Expr(Fun), arg, body, env, self.dummy()) } #[inline] @@ -1007,32 +1007,20 @@ impl Ptr { "".into() } } - Fun => match self.get_index3() { + Fun => match self.get_index4() { None => "".into(), Some(idx) => { - if let Some((arg, bod, _)) = store.fetch_3_ptrs(idx) { - match bod.tag() { + if let Some((vars, body, ..)) = store.fetch_4_ptrs(idx) { + match vars.tag() { Tag::Expr(Nil) => { - format!( - "", - arg.fmt_to_string(store, state), - bod.fmt_to_string(store, state) - ) + format!("", body.fmt_to_string(store, state)) } Tag::Expr(Cons) => { - if let Some(idx) = bod.get_index2() { - if let Some((bod, _)) = store.fetch_2_ptrs(idx) { - format!( - "", - arg.fmt_to_string(store, state), - bod.fmt_to_string(store, state) - ) - } else { - "".into() - } - } else { - "".into() - } + format!( + "", + vars.fmt_to_string(store, state), + body.fmt_to_string(store, state) + ) } _ => "".into(), } diff --git a/src/lem/tests/eval_tests.rs b/src/lem/tests/eval_tests.rs index 84c1c52a16..83e752eb6f 100644 --- a/src/lem/tests/eval_tests.rs +++ b/src/lem/tests/eval_tests.rs @@ -278,7 +278,7 @@ fn evaluate_lambda2() { None, Some(terminal), None, - &expect!["9"], + &expect!["8"], &None, ); } @@ -339,7 +339,7 @@ fn evaluate_lambda5() { None, Some(terminal), None, - &expect!["13"], + &expect!["11"], &None, ); } @@ -481,7 +481,7 @@ fn evaluate_adder1() { None, Some(terminal), None, - &expect!["13"], + &expect!["10"], &None, ); } @@ -502,7 +502,7 @@ fn evaluate_adder2() { None, Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -561,7 +561,7 @@ fn evaluate_let() { None, Some(terminal), None, - &expect!["10"], + &expect!["8"], &None, ); } @@ -658,7 +658,7 @@ fn evaluate_arithmetic_let() { Some(new_env), Some(terminal), None, - &expect!["18"], + &expect!["15"], &None, ); } @@ -689,7 +689,7 @@ fn evaluate_fundamental_conditional() { None, Some(terminal), None, - &expect!["35"], + &expect!["28"], &None, ); } @@ -716,7 +716,7 @@ fn evaluate_fundamental_conditional() { None, Some(terminal), None, - &expect!["32"], + &expect!["26"], &None, ); } @@ -800,7 +800,7 @@ fn evaluate_recursion1() { None, Some(terminal), None, - &expect!["91"], + &expect!["76"], &None, ); } @@ -825,7 +825,7 @@ fn evaluate_recursion2() { None, Some(terminal), None, - &expect!["201"], + &expect!["163"], &None, ); } @@ -848,7 +848,7 @@ fn evaluate_recursion_multiarg() { None, Some(terminal), None, - &expect!["95"], + &expect!["68"], &None, ); } @@ -874,7 +874,7 @@ fn evaluate_recursion_optimized() { None, Some(terminal), None, - &expect!["75"], + &expect!["66"], &None, ); } @@ -899,7 +899,7 @@ fn evaluate_tail_recursion() { None, Some(terminal), None, - &expect!["129"], + &expect!["105"], &None, ); } @@ -927,7 +927,7 @@ fn evaluate_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["110"], + &expect!["92"], &None, ); } @@ -948,7 +948,7 @@ fn evaluate_multiple_letrec_bindings() { None, Some(terminal), None, - &expect!["22"], + &expect!["20"], &None, ); } @@ -969,7 +969,7 @@ fn evaluate_multiple_letrec_bindings_referencing() { None, Some(terminal), None, - &expect!["31"], + &expect!["28"], &None, ); } @@ -1001,7 +1001,7 @@ fn evaluate_multiple_letrec_bindings_recursive() { None, Some(terminal), None, - &expect!["242"], + &expect!["175"], &None, ); } @@ -1025,7 +1025,7 @@ fn nested_let_closure_regression() { None, Some(terminal), None, - &expect!["13"], + &expect!["11"], &None, ); } @@ -1042,7 +1042,7 @@ fn nested_let_closure_regression() { None, Some(terminal), None, - &expect!["14"], + &expect!["11"], &None, ); } @@ -1142,11 +1142,10 @@ fn evaluate_zero_arg_lambda() { } { let expected = { - let arg = s.intern_user_symbol("x"); + let args = s.list(vec![s.intern_user_symbol("x")]); let num = s.num_u64(123); - let body = s.list(vec![num]); let env = s.intern_nil(); - s.intern_fun(arg, body, env) + s.intern_fun(args, num, env) }; // One arg expected but zero supplied. @@ -1173,7 +1172,7 @@ fn evaluate_zero_arg_lambda() { None, Some(terminal), None, - &expect!["12"], + &expect!["10"], &None, ); } @@ -1186,7 +1185,7 @@ fn evaluate_zero_arg_lambda_variants() { let expr = "((lambda () 123) 1)"; let error = s.cont_error(); - test_aux::>(s, expr, None, None, Some(error), None, &expect!["3"], &None); + test_aux::>(s, expr, None, None, Some(error), None, &expect!["2"], &None); } { let s = &Store::::default(); @@ -1236,7 +1235,7 @@ fn evaluate_make_tree() { None, Some(terminal), None, - &expect!["493"], + &expect!["445"], &None, ); } @@ -1282,7 +1281,7 @@ fn evaluate_map_tree_bug() { None, Some(terminal), None, - &expect!["170"], + &expect!["125"], &None, ); } @@ -1309,7 +1308,7 @@ fn evaluate_map_tree_numequal_bug() { None, Some(error), None, - &expect!["169"], + &expect!["125"], &None, ); } @@ -1344,7 +1343,7 @@ fn env_lost_bug() { None, Some(terminal), None, - &expect!["25"], + &expect!["22"], &None, ); } @@ -1369,7 +1368,7 @@ fn dont_discard_rest_env() { None, Some(terminal), None, - &expect!["22"], + &expect!["20"], &None, ); } @@ -1675,7 +1674,7 @@ fn go_translate() { None, None, None, - &expect!["1114"], + &expect!["840"], &None, ); } @@ -2389,7 +2388,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["19"], + &expect!["17"], &None, ); } @@ -2408,7 +2407,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["24"], + &expect!["22"], &None, ); } @@ -2432,7 +2431,7 @@ fn test_num_syntax_implications() { None, Some(terminal), None, - &expect!["10"], + &expect!["8"], &None, ); } @@ -2565,7 +2564,7 @@ fn test_quoted_symbols() { None, Some(terminal), None, - &expect!["13"], + &expect!["11"], &None, ); } @@ -3338,7 +3337,7 @@ fn test_fold_cons_regression() { None, Some(terminal), None, - &expect!["152"], + &expect!["92"], &None, ); } @@ -3551,7 +3550,7 @@ fn test_eval_lambda_body_syntax() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); test_aux::>( @@ -3561,7 +3560,7 @@ fn test_eval_lambda_body_syntax() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); } @@ -3671,7 +3670,7 @@ fn test_dumb_lang() { None, Some(terminal), None, - &expect!["6"], + &expect!["5"], &Some(&lang), ); test_aux( diff --git a/src/proof/tests/nova_tests_lem.rs b/src/proof/tests/nova_tests_lem.rs index 9fa63e514d..8867f589fd 100644 --- a/src/proof/tests/nova_tests_lem.rs +++ b/src/proof/tests/nova_tests_lem.rs @@ -123,7 +123,7 @@ fn test_prove_arithmetic_let() { None, Some(terminal), None, - &expect!["18"], + &expect!["15"], &None, ); } @@ -357,7 +357,7 @@ fn test_prove_recursion1() { None, Some(terminal), None, - &expect!["66"], + &expect!["55"], &None, ); } @@ -381,7 +381,7 @@ fn test_prove_recursion2() { None, Some(terminal), None, - &expect!["93"], + &expect!["76"], &None, ); } @@ -511,7 +511,7 @@ fn test_prove_evaluate2() { None, Some(terminal), None, - &expect!["9"], + &expect!["8"], &None, ); } @@ -579,7 +579,7 @@ fn test_prove_evaluate5() { None, Some(terminal), None, - &expect!["13"], + &expect!["11"], &None, ); } @@ -811,7 +811,7 @@ fn test_prove_adder() { None, Some(terminal), None, - &expect!["13"], + &expect!["10"], &None, ); } @@ -912,7 +912,7 @@ fn test_prove_lambda_empty_error() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); } @@ -1081,7 +1081,7 @@ fn test_prove_let() { None, Some(terminal), None, - &expect!["18"], + &expect!["15"], &None, ); } @@ -1106,7 +1106,7 @@ fn test_prove_arithmetic() { None, Some(terminal), None, - &expect!["23"], + &expect!["18"], &None, ); } @@ -1128,7 +1128,7 @@ fn test_prove_comparison() { None, Some(terminal), None, - &expect!["21"], + &expect!["18"], &None, ); } @@ -1157,7 +1157,7 @@ fn test_prove_conditional() { None, Some(terminal), None, - &expect!["35"], + &expect!["28"], &None, ); } @@ -1186,7 +1186,7 @@ fn test_prove_conditional2() { None, Some(terminal), None, - &expect!["32"], + &expect!["26"], &None, ); } @@ -1212,7 +1212,7 @@ fn test_prove_fundamental_conditional_bug() { None, Some(terminal), None, - &expect!["32"], + &expect!["25"], &None, ); } @@ -1253,7 +1253,7 @@ fn test_prove_recursion() { None, Some(terminal), None, - &expect!["66"], + &expect!["55"], &None, ); } @@ -1275,7 +1275,7 @@ fn test_prove_recursion_multiarg() { None, Some(terminal), None, - &expect!["69"], + &expect!["49"], &None, ); } @@ -1300,7 +1300,7 @@ fn test_prove_recursion_optimized() { None, Some(terminal), None, - &expect!["56"], + &expect!["49"], &None, ); } @@ -1324,7 +1324,7 @@ fn test_prove_tail_recursion() { None, Some(terminal), None, - &expect!["93"], + &expect!["76"], &None, ); } @@ -1350,7 +1350,7 @@ fn test_prove_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["81"], &None + &expect!["68"], &None ); } @@ -1375,7 +1375,7 @@ fn test_prove_no_mutual_recursion() { None, Some(terminal), None, - &expect!["22"], + &expect!["21"], &None, ); } @@ -1400,7 +1400,7 @@ fn test_prove_no_mutual_recursion_error() { None, Some(error), None, - &expect!["25"], + &expect!["24"], &None, ); } @@ -1533,7 +1533,7 @@ fn test_prove_zero_arg_lambda2() { None, Some(terminal), None, - &expect!["10"], + &expect!["9"], &None, ); } @@ -1542,11 +1542,10 @@ fn test_prove_zero_arg_lambda2() { fn test_prove_zero_arg_lambda3() { let s = &Store::::default(); let expected = { - let arg = s.intern_user_symbol("x"); + let args = s.list(vec![s.intern_user_symbol("x")]); let num = s.num_u64(123); - let body = s.list(vec![num]); let env = s.intern_nil(); - s.intern_fun(arg, body, env) + s.intern_fun(args, num, env) }; let terminal = s.cont_terminal(); nova_test_full_aux::<_, _, M1<'_, _>>( @@ -1575,7 +1574,7 @@ fn test_prove_zero_arg_lambda4() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); } @@ -1630,7 +1629,7 @@ fn test_prove_nested_let_closure_regression() { None, Some(terminal), None, - &expect!["14"], + &expect!["11"], &None, ); } @@ -1653,7 +1652,7 @@ fn test_prove_minimal_tail_call() { None, Some(terminal), None, - &expect!["50"], + &expect!["47"], &None, ); } @@ -1675,7 +1674,7 @@ fn test_prove_cons_in_function1() { None, Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -1697,7 +1696,7 @@ fn test_prove_cons_in_function2() { None, Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -1739,7 +1738,7 @@ fn test_prove_multiple_letrec_bindings() { None, Some(terminal), None, - &expect!["78"], + &expect!["73"], &None, ); } @@ -1763,7 +1762,7 @@ fn test_prove_tail_call2() { None, Some(terminal), None, - &expect!["84"], + &expect!["78"], &None, ); } @@ -1783,7 +1782,7 @@ fn test_prove_multiple_letrecstar_bindings() { None, Some(terminal), None, - &expect!["22"], + &expect!["20"], &None, ); } @@ -1803,7 +1802,7 @@ fn test_prove_multiple_letrecstar_bindings_referencing() { None, Some(terminal), None, - &expect!["31"], + &expect!["28"], &None, ); } @@ -1834,7 +1833,7 @@ fn test_prove_multiple_letrecstar_bindings_recursive() { None, Some(terminal), None, - &expect!["242"], + &expect!["175"], &None, ); } @@ -1856,7 +1855,7 @@ fn test_prove_dont_discard_rest_env() { None, Some(terminal), None, - &expect!["22"], + &expect!["20"], &None, ); } @@ -1882,7 +1881,7 @@ fn test_prove_fibonacci() { None, Some(terminal), None, - &expect!["89"], + &expect!["60"], 5, false, None, @@ -1925,7 +1924,7 @@ fn test_prove_terminal_continuation_regression() { None, Some(terminal), None, - &expect!["9"], + &expect!["8"], &None, ); } @@ -1946,7 +1945,7 @@ fn test_prove_chained_functional_commitment() { None, Some(terminal), None, - &expect!["39"], + &expect!["30"], &None, ); } @@ -3001,7 +3000,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["19"], + &expect!["17"], &None, ); } @@ -3102,7 +3101,7 @@ fn test_prove_functional_commitment() { None, Some(terminal), None, - &expect!["25"], + &expect!["21"], &None, ); } @@ -3132,7 +3131,7 @@ fn test_prove_complicated_functional_commitment() { None, Some(terminal), None, - &expect!["108"], + &expect!["83"], &None, ); } @@ -3155,7 +3154,7 @@ fn test_prove_test_fold_cons_regression() { None, Some(terminal), None, - &expect!["152"], + &expect!["92"], &None, ); } @@ -3785,9 +3784,9 @@ fn test_prove_dotted_syntax_error() { fn test_prove_call_literal_fun() { let s = &Store::::default(); let empty_env = s.intern_nil(); - let arg = s.intern_user_symbol("x"); - let body = s.read_with_default_state("((+ x 1))").unwrap(); - let fun = s.intern_3_ptrs(Tag::Expr(ExprTag::Fun), arg, body, empty_env); + let args = s.list(vec![s.intern_user_symbol("x")]); + let body = s.read_with_default_state("(+ x 1)").unwrap(); + let fun = s.intern_4_ptrs(Tag::Expr(ExprTag::Fun), args, body, empty_env, s.dummy()); let input = s.num_u64(9); let expr = s.list(vec![fun, input]); let res = s.num_u64(10); @@ -3801,7 +3800,7 @@ fn test_prove_call_literal_fun() { None, Some(terminal), None, - &expect!["7"], + &expect!["6"], DEFAULT_REDUCTION_COUNT, false, None, @@ -3841,7 +3840,7 @@ fn test_prove_lambda_body_syntax() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); test_aux::<_, _, M1<'_, _>>( @@ -3851,7 +3850,7 @@ fn test_prove_lambda_body_syntax() { None, Some(error), None, - &expect!["3"], + &expect!["2"], &None, ); } @@ -4077,7 +4076,7 @@ fn test_dumb_lang() { None, Some(terminal), None, - &expect!["6"], + &expect!["5"], &Some(lang.clone()), ); test_aux::<_, _, C1LEM<'_, _, DumbCoprocessor<_>>>( @@ -4336,7 +4335,7 @@ fn test_letrec_let_nesting() { None, Some(terminal), None, - &expect!["6"], + &expect!["5"], &None, ); } @@ -4368,7 +4367,7 @@ fn test_letrec_sequencing() { None, Some(terminal), None, - &expect!["8"], + &expect!["7"], &None, ); } diff --git a/src/state.rs b/src/state.rs index b99b2278e3..1eef65c247 100644 --- a/src/state.rs +++ b/src/state.rs @@ -215,7 +215,7 @@ const LURK_PACKAGE_SYMBOL_NAME: &str = "lurk"; const USER_PACKAGE_SYMBOL_NAME: &str = "user"; const META_PACKAGE_SYMBOL_NAME: &str = "meta"; -const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 36] = [ +const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 35] = [ "atom", "begin", "car", @@ -251,7 +251,6 @@ const LURK_PACKAGE_SYMBOLS_NAMES: [&str; 36] = [ ">", "<=", ">=", - "_", ]; const META_PACKAGE_SYMBOLS_NAMES: [&str; 28] = [