Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Multiple lookups, simpler rec environment #996

Merged
merged 6 commits into from
Jan 8, 2024
Merged

Multiple lookups, simpler rec environment #996

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
f53a84e
two lookups per step
gabriel-barrett Nov 22, 2023
fa49aea
let/letrec refactor
gabriel-barrett Nov 22, 2023
e2e1e28
recursive enviroments simplified
gabriel-barrett Nov 23, 2023
271be4a
fixed eval/proof iterations
gabriel-barrett Dec 22, 2023
3a5c7e7
New tag for recursive variables
gabriel-barrett Jan 4, 2024
57b3561
fixed lurk-lib and demo tests
gabriel-barrett Jan 8, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion benches/common/fib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ pub(crate) fn fib_expr<F: LurkField>(store: &Store<F>) -> 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`.
Expand Down
174 changes: 79 additions & 95 deletions src/lem/eval.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 => {
Expand All @@ -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);
Expand Down Expand Up @@ -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");
Expand Down Expand Up @@ -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`
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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 => {
Expand Down Expand Up @@ -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 => {
Expand Down Expand Up @@ -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());
}
}
9 changes: 8 additions & 1 deletion src/lem/store.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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};
Expand Down Expand Up @@ -1004,6 +1004,13 @@ impl Ptr {
"<Opaque Sym>".into()
}
}
RecVar => {
if let Some(sym) = store.fetch_sym(&self.cast(Tag::Expr(Sym))) {
state.fmt_to_string(&sym.into())
} else {
"<Opaque RecVar>".into()
}
}
Key => {
if let Some(key) = store.fetch_key(self) {
state.fmt_to_string(&key.into())
Expand Down
Loading
Loading