diff --git a/benches/common/fib.rs b/benches/common/fib.rs index 60ece870d4..a403b14f9f 100644 --- a/benches/common/fib.rs +++ b/benches/common/fib.rs @@ -23,7 +23,7 @@ pub(crate) fn fib_expr(store: &Store) -> Ptr { } const LIN_COEF: usize = 7; -const ANG_COEF: usize = 10; +const ANG_COEF: usize = 7; // 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`. diff --git a/demo/bank.lurk b/demo/bank.lurk index 1b6cac8e74..6fabcd133d 100644 --- a/demo/bank.lurk +++ b/demo/bank.lurk @@ -192,7 +192,7 @@ ledger2 ;; Now we can open the committed ledger transfer function on a transaction. -!(call 0x30ee7657cfa11c0dc69160195540297c50176a27baf2b407d6bf16d6284abaea '(1 0 2)) +!(call 0x3be53fdb5946af9449e4f7063fd8d60a6acc7ccdea8da8b575facedcb2b1291d '(1 0 2)) ;; And the record reflects that Church sent one unit to Satoshi. @@ -202,7 +202,7 @@ ledger2 ;; We can verify the proof.. -!(verify "Nova_Pallas_10_39457589f3ffd148aadaba23819641cdd914ab291a3c77d20dcb65f757c08925") +!(verify "Nova_Pallas_10_0bac4e49ef06a34fd1a6a18d6d7bff8770e6acbf6a4624783af29ad8cd780b14") ;; Unfortunately, this functional commitment doesn't let us maintain state. ;; Let's turn our single-transaction function into a chained function. @@ -219,24 +219,24 @@ ledger2 ;; Now we can transfer one unit from Church to Satoshi like before. -!(chain 0x1aaf63ef4f853b935df9aad04424e0a8ba1e5bfd7220e5de842eca9d6e608f36 '(1 0 2)) +!(chain 0x01ad5587273aed89dca2527f7a9a235e1ee74ba2519d39adc7b4c521c66f9dbb '(1 0 2)) !(prove) -!(verify "Nova_Pallas_10_27cf734c3a663d0c09a62e4150fe4813ebd7db2fb038589facd7e48ba6c76e1e") +!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a") ;; Then we can transfer 5 more, proceeding from the new head of the chain. -!(chain 0x242e4fb1434ce1f6b4a19d8e96651e36ca5f7daa2fa2796f6f5924f66c35cd31 '(5 0 2)) +!(chain 0x07172fda01948387c25038beb5738a12bf88cfb3317180cf5894319c16276c78 '(5 0 2)) !(prove) -!(verify "Nova_Pallas_10_14a98bfb5ee8451accb717eca8dadaaeb1c21f95e7890d53bcd733b73224e0fc") +!(verify "Nova_Pallas_10_2def0d8894789eda3fdbafe6216b9d38c1d73c39964780fff407596dca93535a") ;; And once more, this time we'll transfer 20 from Turing to Church. -!(chain 0x0f7247de19a2f52890cb4f165aaebe40934c09cc3466ab9ce2e03a8c21a32c7a '(20 1 0)) +!(chain 0x261e0afd81be78f88bc638c79d6530f341517ff5fdb368e575407bd701c712cc '(20 1 0)) !(prove) -!(verify "Nova_Pallas_10_21832c545de0ab0111c9006728ab9a1d4550d044b21c73f3076f60256a732db9") +!(verify "Nova_Pallas_10_2d3c73be45dce3971cf9208a6ec538238fc4a01328342d2b3aa501e5709ea2c5") diff --git a/demo/chained-functional-commitment.lurk b/demo/chained-functional-commitment.lurk index cba7746e18..86ce3510ec 100644 --- a/demo/chained-functional-commitment.lurk +++ b/demo/chained-functional-commitment.lurk @@ -9,7 +9,7 @@ ;; We chain a next commitment by applying the committed function to a value of 9. -!(chain 0x14cb06e2d3c594af90d5b670e73595791d7462b20442c24cd56ba2919947d769 9) +!(chain 0x07978f48203798156497b7fdef995301644c10b16de71c98a9c3c5d5c80e5cb9 9) ;; The new counter value is 9, and the function returns a new functional commitment. @@ -21,11 +21,11 @@ ;; We can verify the proof. -!(verify "Nova_Pallas_10_38f55f6f5c92197e331c92971ba13514f621cf1e0de66133574fe3c1d2d71114") +!(verify "Nova_Pallas_10_29077a93c626166dfe527acb4665eeaa0a2945965db1d984d111fdb04d7f6cb4") ;; Now let's chain another call to the new head, adding 12 to the counter. -!(chain 0x26f9a6e61ea91163545a0472304d5ad42825ce1f6873ea10301e26dfd84f3ea6 12) +!(chain 0x09d46102bcc9faaf2d8dbfabe72b5142a1788538129e4826e0e30015f594e035 12) ;; Now the counter is 21, and we have a new head commitment. @@ -35,11 +35,11 @@ ;; And verify. -!(verify "Nova_Pallas_10_141e90709e746411b9d0b3557758fe7543aafc33ed9cc25ee22606adab7d8e6f") +!(verify "Nova_Pallas_10_18beccbc88887d27b074b782525d2c3d5cfafb7f553877513b167b8bb45017e4") ;; One more time, we'll add 14 to the head commitment's internal state. -!(chain 0x2adacaf2ae7983d45e6855fa6c6577e73ca4657c33e45286cbfb8e44d68e351c 14) +!(chain 0x3b0ed1000667da8ce73779a52e4dfe17638f359fcb77f0aad1a6322c1fcef599 14) ;; 21 + 14 = 35, as expected. @@ -49,7 +49,7 @@ ;; Verify. -!(verify "Nova_Pallas_10_3fe9b0d562d982f0614cb96e4cbb88f56733442524f6c42a29ef8cf5ab8a6c7e") +!(verify "Nova_Pallas_10_034258d4a0c61bc5fff43cc2e912a88f341abca00c4149c0ed85ab02b33d45dc") ;; Repeat indefinitely. diff --git a/demo/vdf.lurk b/demo/vdf.lurk index ae99938fd7..f339e8000e 100644 --- a/demo/vdf.lurk +++ b/demo/vdf.lurk @@ -51,7 +51,7 @@ !(prove) -!(verify "Nova_Pallas_10_1955d9399a7174ffb6ecd9b558e260c746e42456018246335de9c22811282119") +!(verify "Nova_Pallas_10_04ebf402c8345327dbb271b393325f4d360372784e4d1e625e707235a8736dad") !(def timelock-encrypt (lambda (secret-key plaintext rounds) (let ((ciphertext (+ secret-key plaintext)) diff --git a/lurk-lib b/lurk-lib index 6c9bfb76ac..845c7fced5 160000 --- a/lurk-lib +++ b/lurk-lib @@ -1 +1 @@ -Subproject commit 6c9bfb76acdf45906c6baa9a963de9d27b3863dc +Subproject commit 845c7fced5e102dd6884bae8c3114ab679a4e73e diff --git a/src/lem/eval.rs b/src/lem/eval.rs index 0510eec5e5..ea5d8e8e24 100644 --- a/src/lem/eval.rs +++ b/src/lem/eval.rs @@ -660,15 +660,6 @@ fn match_and_run_cproc(cprocs: &[(&Symbol, usize)]) -> Func { fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { // Auxiliary functions let car_cdr = car_cdr(); - let env_to_use = func!(env_to_use(smaller_env, smaller_rec_env): 1 => { - match smaller_rec_env.tag { - Expr::Nil => { - return (smaller_env) - } - }; - let env: Expr::Cons = cons2(smaller_rec_env, smaller_env); - return (env) - }); let expand_bindings = func!(expand_bindings(head, body, body1, rest_bindings): 1 => { match rest_bindings.tag { Expr::Nil => { @@ -679,18 +670,6 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { let expanded: Expr::Cons = cons2(head, expanded_0); return (expanded) }); - let choose_let_cont = func!(choose_let_cont(head, var, env, expanded, cont): 1 => { - match symbol head { - "let" => { - let cont: Cont::Let = cons4(var, env, expanded, cont); - return (cont) - } - "letrec" => { - let cont: Cont::LetRec = cons4(var, env, expanded, cont); - return (cont) - } - } - }); let get_unop = func!(get_unop(head): 1 => { let nil = Symbol("nil"); let nil = cast(nil, Expr::Nil); @@ -823,6 +802,45 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { return (nil) }); let is_cproc = is_cproc(cprocs); + let lookup = func!(lookup(expr, env, found, binding): 4 => { + let rec = Symbol("rec"); + let non_rec = Symbol("non_rec"); + let error = Symbol("error"); + let not_found = Symbol("not_found"); + let continue = eq_val(not_found, found); + if !continue { + return (expr, env, found, binding) + } + match env.tag { + Expr::Nil => { + return (expr, env, error, binding) + } + }; + let (binding, smaller_env) = car_cdr(env); + match binding.tag { + Expr::Nil => { + return (expr, env, error, binding) + } + }; + let (var, val) = decons2(binding); + match var.tag { + Expr::Sym => { + let eq_val = eq_val(var, expr); + if eq_val { + return (val, env, non_rec, binding) + } + return (expr, smaller_env, not_found, binding) + } + Expr::RecVar => { + let eq_val = eq_val(var, expr); + if eq_val { + return (val, env, rec, binding) + } + return (expr, smaller_env, not_found, binding) + } + }; + return (expr, env, error, binding) + }); func!(reduce(expr, env, cont): 4 => { let ret = Symbol("return"); @@ -869,53 +887,34 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { if expr_is_nil_or_t { return (expr, env, cont, apply) } - - match env.tag { - Expr::Nil => { + let not_found = Symbol("not_found"); + let (expr, env, found, binding) = lookup(expr, env, not_found, nil); + let (expr, env, found, binding) = lookup(expr, env, found, binding); + let (expr, env, found, binding) = lookup(expr, env, found, binding); + match symbol found { + "error" => { return (expr, env, err, errctrl) } - }; - - let (binding, smaller_env) = car_cdr(env); - match binding.tag { - Expr::Nil => { - return (expr, env, err, errctrl) + "non_rec" => { + return (expr, env, cont, apply) } - }; - - let (var_or_rec_binding, val_or_more_rec_env) = - car_cdr(binding); - match var_or_rec_binding.tag { - Expr::Sym => { - let eq_val = eq_val(var_or_rec_binding, expr); - if eq_val { - return (val_or_more_rec_env, env, cont, apply) - } - return (expr, smaller_env, cont, ret) + "rec" => { + match expr.tag { + Expr::Fun => { + // if `val2` is a closure, then extend its environment + let (arg, body, closed_env, _foo) = decons4(expr); + let extended: Expr::Cons = cons2(binding, closed_env); + // and return the extended closure + let fun: Expr::Fun = cons4(arg, body, extended, foo); + return (fun, env, cont, apply) + } + }; + return (expr, env, cont, apply) } - Expr::Cons => { - let (v2, val2) = decons2(var_or_rec_binding); - - let eq_val = eq_val(v2, expr); - if eq_val { - match val2.tag { - Expr::Fun => { - // if `val2` is a closure, then extend its environment - 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 = cons4(arg, body, extended, foo); - return (fun, env, cont, apply) - } - }; - // otherwise return `val2` - return (val2, env, cont, apply) - } - let (env_to_use) = env_to_use(smaller_env, val_or_more_rec_env); - return (expr, env_to_use, cont, ret) + "not_found" => { + return (expr, env, cont, ret) } - }; - return (expr, env, err, errctrl) + } } Expr::Cons => { // No need for `car_cdr` since the expression is already a `Cons` @@ -955,14 +954,17 @@ fn reduce(cprocs: &[(&Symbol, usize)]) -> Func { match var.tag { Expr::Sym => { let (val, end) = car_cdr(vals); - match end.tag { - Expr::Nil => { - let (expanded) = expand_bindings(head, body, body1, rest_bindings); - let (cont) = choose_let_cont(head, var, env, expanded, cont); - return (val, env, cont, ret) - } - }; - return (expr, env, err, errctrl) + let end_is_nil = eq_tag(end, nil); + if !end_is_nil { + return (expr, env, err, errctrl) + } + let (expanded) = expand_bindings(head, body, body1, rest_bindings); + if head_is_let_sym { + let cont: Cont::Let = cons4(var, env, expanded, cont); + return (val, env, cont, ret) + } + let cont: Cont::LetRec = cons4(var, env, expanded, cont); + return (val, env, cont, ret) } }; return (expr, env, err, errctrl) @@ -1153,27 +1155,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 extend_rec = func!(extend_rec(env, var, result): 1 => { - let nil = Symbol("nil"); - let nil = cast(nil, Expr::Nil); - let sym: Expr::Sym; - let (binding_or_env, rest) = car_cdr(env); - let (var_or_binding, _val_or_more_bindings) = car_cdr(binding_or_env); - let binding: Expr::Cons = cons2(var, result); - let var_or_binding_is_sym = eq_tag(var_or_binding, sym); - let var_or_binding_is_nil = eq_tag(var_or_binding, nil); - let var_or_binding_is_sym_or_nil = or(var_or_binding_is_sym, var_or_binding_is_nil); - if var_or_binding_is_sym_or_nil { - // It's a var, so we are extending a simple env with a recursive env. - let list: Expr::Cons = cons2(binding, nil); - let res: Expr::Cons = cons2(list, env); - return (res) - } - // It's a binding, so we are extending a recursive env. - let cons2: Expr::Cons = cons2(binding, binding_or_env); - let res: Expr::Cons = cons2(cons2, rest); - return (res) - }); // Returns 0u64 if both arguments are U64, 0 (num) if the arguments are some kind of number (either U64 or Num), // and nil otherwise let args_num_type = func!(args_num_type(arg1, arg2): 1 => { @@ -1317,7 +1298,10 @@ fn apply_cont(cprocs: &[(&Symbol, usize)], ivc: bool) -> Func { } Cont::LetRec => { let (var, saved_env, body, cont) = decons4(cont); - let (extended_env) = extend_rec(saved_env, var, result); + // Since the variable came from a letrec, it is a recursive variable + let var = cast(var, Expr::RecVar); + let binding: Expr::Cons = cons2(var, result); + let extended_env: Expr::Cons = cons2(binding, saved_env); return (body, extended_env, cont, ret) } Cont::Unop => { @@ -1761,8 +1745,8 @@ mod tests { expected.assert_eq(&computed.to_string()); }; expect_eq(cs.num_inputs(), expect!["1"]); - expect_eq(cs.aux().len(), expect!["8823"]); - expect_eq(cs.num_constraints(), expect!["10628"]); + expect_eq(cs.aux().len(), expect!["8884"]); + expect_eq(cs.num_constraints(), expect!["10831"]); assert_eq!(func.num_constraints(&store), cs.num_constraints()); } } diff --git a/src/lem/store.rs b/src/lem/store.rs index 9f732f2efc..dd29c05e1a 100644 --- a/src/lem/store.rs +++ b/src/lem/store.rs @@ -23,7 +23,7 @@ use crate::{ self, Binop, Binop2, Call, Call0, Call2, Dummy, Emit, If, Let, LetRec, Lookup, Outermost, Tail, Terminal, Unop, }, - tag::ExprTag::{Char, Comm, Cons, Cproc, Fun, Key, Nil, Num, Str, Sym, Thunk, U64}, + tag::ExprTag::{Char, Comm, Cons, Cproc, Fun, Key, Nil, Num, RecVar, Str, Sym, Thunk, U64}, }; use super::pointers::{Ptr, RawPtr, ZPtr}; @@ -1004,6 +1004,13 @@ impl Ptr { "".into() } } + RecVar => { + if let Some(sym) = store.fetch_sym(&self.cast(Tag::Expr(Sym))) { + state.fmt_to_string(&sym.into()) + } else { + "".into() + } + } Key => { if let Some(key) = store.fetch_key(self) { state.fmt_to_string(&key.into()) diff --git a/src/lem/tests/eval_tests.rs b/src/lem/tests/eval_tests.rs index 311f614891..63f494bc4c 100644 --- a/src/lem/tests/eval_tests.rs +++ b/src/lem/tests/eval_tests.rs @@ -281,7 +281,7 @@ fn evaluate_lambda2() { None, Some(terminal), None, - &expect!["8"], + &expect!["7"], &None, ); } @@ -342,7 +342,7 @@ fn evaluate_lambda5() { None, Some(terminal), None, - &expect!["11"], + &expect!["10"], &None, ); } @@ -484,7 +484,7 @@ fn evaluate_adder1() { None, Some(terminal), None, - &expect!["10"], + &expect!["9"], &None, ); } @@ -505,7 +505,7 @@ fn evaluate_adder2() { None, Some(terminal), None, - &expect!["12"], + &expect!["11"], &None, ); } @@ -564,7 +564,7 @@ fn evaluate_let() { None, Some(terminal), None, - &expect!["8"], + &expect!["7"], &None, ); } @@ -661,7 +661,7 @@ fn evaluate_arithmetic_let() { Some(new_env), Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -692,7 +692,7 @@ fn evaluate_fundamental_conditional() { None, Some(terminal), None, - &expect!["28"], + &expect!["22"], &None, ); } @@ -719,7 +719,7 @@ fn evaluate_fundamental_conditional() { None, Some(terminal), None, - &expect!["26"], + &expect!["22"], &None, ); } @@ -803,7 +803,7 @@ fn evaluate_recursion1() { None, Some(terminal), None, - &expect!["76"], + &expect!["64"], &None, ); } @@ -828,7 +828,7 @@ fn evaluate_recursion2() { None, Some(terminal), None, - &expect!["163"], + &expect!["122"], &None, ); } @@ -851,7 +851,7 @@ fn evaluate_recursion_multiarg() { None, Some(terminal), None, - &expect!["68"], + &expect!["56"], &None, ); } @@ -877,7 +877,7 @@ fn evaluate_recursion_optimized() { None, Some(terminal), None, - &expect!["66"], + &expect!["57"], &None, ); } @@ -902,7 +902,7 @@ fn evaluate_tail_recursion() { None, Some(terminal), None, - &expect!["105"], + &expect!["80"], &None, ); } @@ -930,7 +930,7 @@ fn evaluate_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["92"], + &expect!["73"], &None, ); } @@ -951,7 +951,7 @@ fn evaluate_multiple_letrec_bindings() { None, Some(terminal), None, - &expect!["20"], + &expect!["19"], &None, ); } @@ -972,7 +972,7 @@ fn evaluate_multiple_letrec_bindings_referencing() { None, Some(terminal), None, - &expect!["28"], + &expect!["25"], &None, ); } @@ -1004,7 +1004,7 @@ fn evaluate_multiple_letrec_bindings_recursive() { None, Some(terminal), None, - &expect!["175"], + &expect!["144"], &None, ); } @@ -1028,7 +1028,7 @@ fn nested_let_closure_regression() { None, Some(terminal), None, - &expect!["11"], + &expect!["9"], &None, ); } @@ -1045,7 +1045,7 @@ fn nested_let_closure_regression() { None, Some(terminal), None, - &expect!["11"], + &expect!["9"], &None, ); } @@ -1175,7 +1175,7 @@ fn evaluate_zero_arg_lambda() { None, Some(terminal), None, - &expect!["10"], + &expect!["9"], &None, ); } @@ -1238,7 +1238,7 @@ fn evaluate_make_tree() { None, Some(terminal), None, - &expect!["445"], + &expect!["397"], &None, ); } @@ -1284,7 +1284,7 @@ fn evaluate_map_tree_bug() { None, Some(terminal), None, - &expect!["125"], + &expect!["103"], &None, ); } @@ -1311,7 +1311,7 @@ fn evaluate_map_tree_numequal_bug() { None, Some(error), None, - &expect!["125"], + &expect!["103"], &None, ); } @@ -1346,7 +1346,7 @@ fn env_lost_bug() { None, Some(terminal), None, - &expect!["22"], + &expect!["18"], &None, ); } @@ -1371,7 +1371,7 @@ fn dont_discard_rest_env() { None, Some(terminal), None, - &expect!["20"], + &expect!["15"], &None, ); } @@ -1677,7 +1677,7 @@ fn go_translate() { None, None, None, - &expect!["840"], + &expect!["509"], &None, ); } @@ -2391,7 +2391,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["17"], + &expect!["16"], &None, ); } @@ -2410,7 +2410,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["22"], + &expect!["21"], &None, ); } @@ -2434,7 +2434,7 @@ fn test_num_syntax_implications() { None, Some(terminal), None, - &expect!["8"], + &expect!["7"], &None, ); } @@ -2567,7 +2567,7 @@ fn test_quoted_symbols() { None, Some(terminal), None, - &expect!["11"], + &expect!["10"], &None, ); } @@ -3340,7 +3340,7 @@ fn test_fold_cons_regression() { None, Some(terminal), None, - &expect!["92"], + &expect!["67"], &None, ); } diff --git a/src/proof/tests/nova_tests_lem.rs b/src/proof/tests/nova_tests_lem.rs index 74499a580a..9c16ab95ac 100644 --- a/src/proof/tests/nova_tests_lem.rs +++ b/src/proof/tests/nova_tests_lem.rs @@ -126,7 +126,7 @@ fn test_prove_arithmetic_let() { None, Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -360,7 +360,7 @@ fn test_prove_recursion1() { None, Some(terminal), None, - &expect!["55"], + &expect!["47"], &None, ); } @@ -384,7 +384,7 @@ fn test_prove_recursion2() { None, Some(terminal), None, - &expect!["76"], + &expect!["59"], &None, ); } @@ -514,7 +514,7 @@ fn test_prove_evaluate2() { None, Some(terminal), None, - &expect!["8"], + &expect!["7"], &None, ); } @@ -582,7 +582,7 @@ fn test_prove_evaluate5() { None, Some(terminal), None, - &expect!["11"], + &expect!["10"], &None, ); } @@ -814,7 +814,7 @@ fn test_prove_adder() { None, Some(terminal), None, - &expect!["10"], + &expect!["9"], &None, ); } @@ -1084,7 +1084,7 @@ fn test_prove_let() { None, Some(terminal), None, - &expect!["15"], + &expect!["12"], &None, ); } @@ -1109,7 +1109,7 @@ fn test_prove_arithmetic() { None, Some(terminal), None, - &expect!["18"], + &expect!["15"], &None, ); } @@ -1131,7 +1131,7 @@ fn test_prove_comparison() { None, Some(terminal), None, - &expect!["18"], + &expect!["15"], &None, ); } @@ -1160,7 +1160,7 @@ fn test_prove_conditional() { None, Some(terminal), None, - &expect!["28"], + &expect!["22"], &None, ); } @@ -1189,7 +1189,7 @@ fn test_prove_conditional2() { None, Some(terminal), None, - &expect!["26"], + &expect!["22"], &None, ); } @@ -1215,7 +1215,7 @@ fn test_prove_fundamental_conditional_bug() { None, Some(terminal), None, - &expect!["25"], + &expect!["20"], &None, ); } @@ -1256,7 +1256,7 @@ fn test_prove_recursion() { None, Some(terminal), None, - &expect!["55"], + &expect!["47"], &None, ); } @@ -1278,7 +1278,7 @@ fn test_prove_recursion_multiarg() { None, Some(terminal), None, - &expect!["49"], + &expect!["41"], &None, ); } @@ -1303,7 +1303,7 @@ fn test_prove_recursion_optimized() { None, Some(terminal), None, - &expect!["49"], + &expect!["43"], &None, ); } @@ -1327,7 +1327,7 @@ fn test_prove_tail_recursion() { None, Some(terminal), None, - &expect!["76"], + &expect!["59"], &None, ); } @@ -1353,7 +1353,7 @@ fn test_prove_tail_recursion_somewhat_optimized() { None, Some(terminal), None, - &expect!["68"], &None + &expect!["55"], &None ); } @@ -1378,7 +1378,7 @@ fn test_prove_no_mutual_recursion() { None, Some(terminal), None, - &expect!["21"], + &expect!["19"], &None, ); } @@ -1403,7 +1403,7 @@ fn test_prove_no_mutual_recursion_error() { None, Some(error), None, - &expect!["24"], + &expect!["20"], &None, ); } @@ -1632,7 +1632,7 @@ fn test_prove_nested_let_closure_regression() { None, Some(terminal), None, - &expect!["11"], + &expect!["9"], &None, ); } @@ -1655,7 +1655,7 @@ fn test_prove_minimal_tail_call() { None, Some(terminal), None, - &expect!["47"], + &expect!["44"], &None, ); } @@ -1677,7 +1677,7 @@ fn test_prove_cons_in_function1() { None, Some(terminal), None, - &expect!["12"], + &expect!["11"], &None, ); } @@ -1699,7 +1699,7 @@ fn test_prove_cons_in_function2() { None, Some(terminal), None, - &expect!["12"], + &expect!["11"], &None, ); } @@ -1741,7 +1741,7 @@ fn test_prove_multiple_letrec_bindings() { None, Some(terminal), None, - &expect!["73"], + &expect!["68"], &None, ); } @@ -1765,7 +1765,7 @@ fn test_prove_tail_call2() { None, Some(terminal), None, - &expect!["78"], + &expect!["71"], &None, ); } @@ -1785,7 +1785,7 @@ fn test_prove_multiple_letrecstar_bindings() { None, Some(terminal), None, - &expect!["20"], + &expect!["19"], &None, ); } @@ -1805,7 +1805,7 @@ fn test_prove_multiple_letrecstar_bindings_referencing() { None, Some(terminal), None, - &expect!["28"], + &expect!["25"], &None, ); } @@ -1836,7 +1836,7 @@ fn test_prove_multiple_letrecstar_bindings_recursive() { None, Some(terminal), None, - &expect!["175"], + &expect!["144"], &None, ); } @@ -1858,7 +1858,7 @@ fn test_prove_dont_discard_rest_env() { None, Some(terminal), None, - &expect!["20"], + &expect!["15"], &None, ); } @@ -1884,7 +1884,7 @@ fn test_prove_fibonacci() { None, Some(terminal), None, - &expect!["60"], + &expect!["40"], 5, false, None, @@ -1948,7 +1948,7 @@ fn test_prove_chained_functional_commitment() { None, Some(terminal), None, - &expect!["30"], + &expect!["24"], &None, ); } @@ -3003,7 +3003,7 @@ fn test_relational_edge_case_identity() { None, Some(terminal), None, - &expect!["17"], + &expect!["16"], &None, ); } @@ -3104,7 +3104,7 @@ fn test_prove_functional_commitment() { None, Some(terminal), None, - &expect!["21"], + &expect!["19"], &None, ); } @@ -3134,7 +3134,7 @@ fn test_prove_complicated_functional_commitment() { None, Some(terminal), None, - &expect!["83"], + &expect!["69"], &None, ); } @@ -3157,7 +3157,7 @@ fn test_prove_test_fold_cons_regression() { None, Some(terminal), None, - &expect!["92"], + &expect!["67"], &None, ); } @@ -3242,7 +3242,7 @@ fn test_prove_test_env_not_nil_and_binding_nil() { let expr = "(let ((a 1) (b 2)) c)"; let error = s.cont_error(); - test_aux::<_, _, M1<'_, _>>(s, expr, None, None, Some(error), None, &expect!["7"], &None); + test_aux::<_, _, M1<'_, _>>(s, expr, None, None, Some(error), None, &expect!["5"], &None); } #[test] diff --git a/src/tag.rs b/src/tag.rs index af2bc41673..bf6a644c1a 100644 --- a/src/tag.rs +++ b/src/tag.rs @@ -51,6 +51,7 @@ pub enum ExprTag { U64, Key, Cproc, + RecVar, } impl From for u16 { @@ -80,6 +81,7 @@ impl fmt::Display for ExprTag { ExprTag::Comm => write!(f, "comm#"), ExprTag::U64 => write!(f, "u64#"), ExprTag::Cproc => write!(f, "cproc#"), + ExprTag::RecVar => write!(f, "rec_var#"), } } }