From 7273c8eb499c74b825ffa71b248d9cf0af0d7de5 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Mon, 16 Sep 2024 11:51:27 -0400 Subject: [PATCH 1/3] Track unbound variables in expressions --- src/haz3lcore/dynamics/Elaborator.re | 7 ++++--- src/haz3lcore/dynamics/FilterMatcher.re | 16 ++++++++-------- src/haz3lcore/dynamics/Stepper.re | 1 + src/haz3lcore/dynamics/Substitution.re | 3 ++- src/haz3lcore/dynamics/Transition.re | 19 +++++++++++++++---- src/haz3lcore/dynamics/TypeAssignment.re | 2 +- src/haz3lcore/dynamics/ValueChecker.re | 2 +- src/haz3lcore/prog/Interface.re | 2 +- src/haz3lcore/statics/Info.re | 2 +- src/haz3lcore/statics/MakeTerm.re | 2 +- src/haz3lcore/statics/Statics.re | 10 +++++++--- src/haz3lcore/statics/TermBase.re | 6 +++--- src/haz3lschool/SyntaxTest.re | 9 +++++---- src/haz3lweb/view/ExplainThis.re | 2 +- src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re | 7 ++++--- 15 files changed, 55 insertions(+), 35 deletions(-) diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re index c1f3aa12d7..13065b3967 100644 --- a/src/haz3lcore/dynamics/Elaborator.re +++ b/src/haz3lcore/dynamics/Elaborator.re @@ -277,7 +277,8 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | Tuple(es) => let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip; Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp); - | Var(v) => + | Var(_, true) => uexp |> cast_from(Typ.temp(Typ.Unknown(Internal))) + | Var(v, false) => uexp |> cast_from( Ctx.lookup_var(ctx, v) @@ -423,9 +424,9 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => { | UnOp(Meta(Unquote), e) => switch (e.term) { // TODO: confirm whether these types are correct - | Var("e") => + | Var("e", _) => Constructor("$e", Unknown(Internal) |> Typ.temp) |> rewrap - | Var("v") => + | Var("v", _) => Constructor("$v", Unknown(Internal) |> Typ.temp) |> rewrap | _ => DHExp.EmptyHole diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re index d6d0bcc543..4506fc7840 100644 --- a/src/haz3lcore/dynamics/FilterMatcher.re +++ b/src/haz3lcore/dynamics/FilterMatcher.re @@ -43,7 +43,7 @@ let evaluate_extend_env_with_pat = copied, term: TermBase.Exp.FixF(pat, exp, Some(to_extend)), }, - TermBase.Exp.Var(binding) |> IdTagged.fresh, + TermBase.Exp.Var(binding, false) |> IdTagged.fresh, ) |> IdTagged.fresh, ), @@ -75,13 +75,13 @@ let tangle = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, TermBase.Exp.Var(ids[i], false) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, TermBase.Exp.Var(ids[i], false) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); @@ -167,7 +167,7 @@ let rec matches_exp = | (FailedCast(d, _, _), _) => matches_exp(d, f) | (Filter(Residue(_), d), _) => matches_exp(d, f) - | (Var(dx), Var(fx)) => + | (Var(dx, _), Var(fx, _)) => if (String.starts_with(~prefix=alpha_magic, dx) && String.starts_with(~prefix=alpha_magic, fx)) { String.equal(dx, fx); @@ -182,12 +182,12 @@ let rec matches_exp = | (None, None) => true }; } - | (Var(dx), _) => + | (Var(dx, _), _) => switch (ClosureEnvironment.lookup(denv, dx)) { | Some(d) => matches_exp(d, f) | None => false } - | (_, Var(fx)) => + | (_, Var(fx, _)) => switch (ClosureEnvironment.lookup(fenv, fx)) { | Some(f) => matches_exp(d, f) | None => false @@ -356,13 +356,13 @@ and matches_fun = let denv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, TermBase.Exp.Var(ids[i], false) |> IdTagged.fresh), dvars, ); let fenv_subst: list((string, 'a)) = List.mapi( (i, binding) => - (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh), + (binding, TermBase.Exp.Var(ids[i], false) |> IdTagged.fresh), fvars, ); let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv); diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re index 8b977cdf5f..199cabac94 100644 --- a/src/haz3lcore/dynamics/Stepper.re +++ b/src/haz3lcore/dynamics/Stepper.re @@ -347,6 +347,7 @@ let get_justification: step_kind => string = | FunClosure => "function closure" | RemoveTypeAlias => "define type" | RemoveParens => "remove parentheses" + | VarLookupFail => "lookup failure" | UnOp(Meta(Unquote)) => failwith("INVALID STEP"); type step_info = { diff --git a/src/haz3lcore/dynamics/Substitution.re b/src/haz3lcore/dynamics/Substitution.re index 5d918e520b..ef79125986 100644 --- a/src/haz3lcore/dynamics/Substitution.re +++ b/src/haz3lcore/dynamics/Substitution.re @@ -2,12 +2,13 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => { let (term, rewrap) = DHExp.unwrap(d2); switch (term) { - | Var(y) => + | Var(y, false) => if (Var.eq(x, y)) { d1; } else { d2; } + | Var(_, true) => d2 | Invalid(_) => d2 | Undefined => d2 | Seq(d3, d4) => diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re index a54c9d18d8..da1d0611bb 100644 --- a/src/haz3lcore/dynamics/Transition.re +++ b/src/haz3lcore/dynamics/Transition.re @@ -46,6 +46,7 @@ open PatternMatch; type step_kind = | InvalidStep | VarLookup + | VarLookupFail | Seq | LetBind | FunClosure @@ -164,8 +165,8 @@ module Transition = (EV: EV_MODE) => { // Transition rules switch (term) { - | Var(x) => - let. _ = otherwise(env, Var(x) |> rewrap); + | Var(x, false) => + let. _ = otherwise(env, Var(x, false) |> rewrap); switch (ClosureEnvironment.lookup(env, x)) { | Some(d) => Step({ @@ -174,8 +175,17 @@ module Transition = (EV: EV_MODE) => { kind: VarLookup, is_value: false, }) - | None => Indet + | None => + Step({ + expr: Var(x, true) |> rewrap, + state_update, + kind: VarLookupFail, + is_value: false, + }) }; + | Var(_, true) => + let. _ = otherwise(env, d); + Indet; | Seq(d1, d2) => let. _ = otherwise(env, d1 => Seq(d1, d2) |> rewrap) and. _ = @@ -240,7 +250,7 @@ module Transition = (EV: EV_MODE) => { Let( dp, FixF(dp, d1, Some(env)) |> rewrap, - Var(binding) |> fresh, + Var(binding, false) |> fresh, ) |> fresh, ), @@ -808,4 +818,5 @@ let should_hide_step_kind = (~settings: CoreSettings.Evaluation.t) => | BuiltinWrap | FunClosure | FixClosure + | VarLookupFail | RemoveParens => true; diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index f4979d94bf..5d14e27360 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -133,7 +133,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => let* ctx' = env_extend_ctx(env, m, ctx); typ_of_dhexp(ctx', m, d); | Filter(_, d) => typ_of_dhexp(ctx, m, d) - | Var(name) => + | Var(name, _) => let* var = Ctx.lookup_var(ctx, name); Some(var.typ); | Seq(d1, d2) => diff --git a/src/haz3lcore/dynamics/ValueChecker.re b/src/haz3lcore/dynamics/ValueChecker.re index 39f43daeed..a3b3ffb472 100644 --- a/src/haz3lcore/dynamics/ValueChecker.re +++ b/src/haz3lcore/dynamics/ValueChecker.re @@ -87,7 +87,7 @@ let rec check_value = (state, env, d) => let rec check_value_mod_ctx = ((), env, d) => switch (DHExp.term_of(d)) { - | Var(x) => + | Var(x, false) => switch (ClosureEnvironment.lookup(env, x)) { | Some(v) => check_value_mod_ctx((), env, v) | None => CV.transition(check_value_mod_ctx, (), env, d) diff --git a/src/haz3lcore/prog/Interface.re b/src/haz3lcore/prog/Interface.re index 3249b1aef2..5e6cb7babf 100644 --- a/src/haz3lcore/prog/Interface.re +++ b/src/haz3lcore/prog/Interface.re @@ -1,4 +1,4 @@ -let dh_err = (error: string): DHExp.t => Var(error) |> DHExp.fresh; +let dh_err = (error: string): DHExp.t => Var(error, true) |> DHExp.fresh; let elaborate = Core.Memo.general(~cache_size_bound=1000, Elaborator.uexp_elab); diff --git a/src/haz3lcore/statics/Info.re b/src/haz3lcore/statics/Info.re index 8aaaeaae3d..ebf33cfc7b 100644 --- a/src/haz3lcore/statics/Info.re +++ b/src/haz3lcore/statics/Info.re @@ -673,7 +673,7 @@ let derived_tpat = (~utpat: TPat.t, ~ctx, ~ancestors): tpat => { exists in the context, return the id where the binding occurs */ let get_binding_site = (info: t): option(Id.t) => { switch (info) { - | InfoExp({term: {term: Var(name), _}, ctx, _}) => + | InfoExp({term: {term: Var(name, _), _}, ctx, _}) => let+ entry = Ctx.lookup_var(ctx, name); entry.id; | InfoExp({term: {term: Constructor(name, _), _}, ctx, _}) diff --git a/src/haz3lcore/statics/MakeTerm.re b/src/haz3lcore/statics/MakeTerm.re index 673af0bb89..2252443e22 100644 --- a/src/haz3lcore/statics/MakeTerm.re +++ b/src/haz3lcore/statics/MakeTerm.re @@ -188,7 +188,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = { | ([t], []) when Form.is_string(t) => ret(String(Form.strip_quotes(t))) | ([t], []) when Form.is_float(t) => ret(Float(float_of_string(t))) - | ([t], []) when Form.is_var(t) => ret(Var(t)) + | ([t], []) when Form.is_var(t) => ret(Var(t, false)) | ([t], []) when Form.is_ctr(t) => ret(Constructor(t, Unknown(Internal) |> Typ.temp)) | (["(", ")"], [Exp(body)]) => ret(Parens(body)) diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re index aca1ce0389..9694701698 100644 --- a/src/haz3lcore/statics/Statics.re +++ b/src/haz3lcore/statics/Statics.re @@ -260,7 +260,9 @@ and uexp_to_info_map = ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]), m, ); - | Var(name) => + | Var(name, true) => + add'(~self=Self.of_exp_var([], name), ~co_ctx=CoCtx.empty, m) + | Var(name, false) => add'( ~self=Self.of_exp_var(ctx, name), ~co_ctx=CoCtx.singleton(name, UExp.rep_id(uexp), Mode.ty_of(mode)), @@ -276,8 +278,10 @@ and uexp_to_info_map = copied: false, term: switch (e.term) { - | Var("e") => UExp.Constructor("$e", Unknown(Internal) |> Typ.temp) - | Var("v") => UExp.Constructor("$v", Unknown(Internal) |> Typ.temp) + | Var("e", _) => + UExp.Constructor("$e", Unknown(Internal) |> Typ.temp) + | Var("v", _) => + UExp.Constructor("$v", Unknown(Internal) |> Typ.temp) | _ => e.term }, }; diff --git a/src/haz3lcore/statics/TermBase.re b/src/haz3lcore/statics/TermBase.re index f0585955c6..5629ffc523 100644 --- a/src/haz3lcore/statics/TermBase.re +++ b/src/haz3lcore/statics/TermBase.re @@ -154,7 +154,7 @@ and Exp: { ) | TypFun(TPat.t, t, option(Var.t)) | Tuple(list(t)) - | Var(Var.t) + | Var(Var.t, bool) // bool is true if the variable is unbound | Let(Pat.t, t, t) | FixF(Pat.t, t, option(ClosureEnvironment.t)) | TyAlias(TPat.t, Typ.t, t) @@ -221,7 +221,7 @@ and Exp: { ) | TypFun(TPat.t, t, option(string)) | Tuple(list(t)) - | Var(Var.t) + | Var(Var.t, bool) // bool is true if the variable is unbound | Let(Pat.t, t, t) | FixF(Pat.t, t, [@show.opaque] option(ClosureEnvironment.t)) | TyAlias(TPat.t, Typ.t, t) @@ -363,7 +363,7 @@ and Exp: { TPat.fast_equal(tp1, tp2) && fast_equal(e1, e2) | (Tuple(xs), Tuple(ys)) => List.length(xs) == List.length(ys) && List.equal(fast_equal, xs, ys) - | (Var(v1), Var(v2)) => v1 == v2 + | (Var(v1, b1), Var(v2, b2)) => v1 == v2 && b1 == b2 | (Let(p1, e1, e2), Let(p2, e3, e4)) => Pat.fast_equal(p1, p2) && fast_equal(e1, e3) && fast_equal(e2, e4) | (FixF(p1, e1, c1), FixF(p2, e2, c2)) => diff --git a/src/haz3lschool/SyntaxTest.re b/src/haz3lschool/SyntaxTest.re index 23dff72251..797f84ca5a 100644 --- a/src/haz3lschool/SyntaxTest.re +++ b/src/haz3lschool/SyntaxTest.re @@ -169,7 +169,8 @@ let rec var_mention_upat = (name: string, upat: Pat.t): bool => { */ let rec var_mention = (name: string, uexp: Exp.t): bool => { switch (uexp.term) { - | Var(x) => x == name + | Var(x, false) => x == name + | Var(_, true) | EmptyHole | Invalid(_) | MultiHole(_) @@ -258,7 +259,7 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => { | Filter(_, u) => var_applied(name, u) | TypAp(u, _) => switch (u.term) { - | Var(x) => x == name ? true : false + | Var(x, _) => x == name ? true : false | _ => var_applied(name, u) } | DynamicErrorHole(_) => false @@ -269,12 +270,12 @@ let rec var_applied = (name: string, uexp: Exp.t): bool => { | Cast(d, _, _) => var_applied(name, d) | Ap(_, u1, u2) => switch (u1.term) { - | Var(x) => x == name ? true : var_applied(name, u2) + | Var(x, _) => x == name ? true : var_applied(name, u2) | _ => var_applied(name, u1) || var_applied(name, u2) } | DeferredAp(u1, us) => switch (u1.term) { - | Var(x) => x == name ? true : List.exists(var_applied(name), us) + | Var(x, _) => x == name ? true : List.exists(var_applied(name), us) | _ => List.exists(var_applied(name), us) } | Cons(u1, u2) diff --git a/src/haz3lweb/view/ExplainThis.re b/src/haz3lweb/view/ExplainThis.re index cbfdf4df9f..9c8c4cc6a8 100644 --- a/src/haz3lweb/view/ExplainThis.re +++ b/src/haz3lweb/view/ExplainThis.re @@ -1125,7 +1125,7 @@ let get_doc = } | _ => basic(TupleExp.tuples) }; - | Var(n) => get_message(TerminalExp.var_exps(n)) + | Var(n, _) => get_message(TerminalExp.var_exps(n)) | Let(pat, def, body) => let pat = bypass_parens_and_annot_pat(pat); let pat_id = List.nth(pat.ids, 0); diff --git a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re index ffb0eed0c5..c19a85173a 100644 --- a/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re +++ b/src/haz3lweb/view/dhcode/layout/DHDoc_Exp.re @@ -150,6 +150,7 @@ let mk = | (TypFunAp, _) // TODO: Could also do something here for type variable substitution like in FunAp? | (InvalidStep, _) | (VarLookup, _) + | (VarLookupFail, _) | (Seq, _) | (FunClosure, _) | (FixClosure, _) @@ -294,8 +295,8 @@ let mk = env, ) | Invalid(t) => DHDoc_common.mk_InvalidText(t) - | Var(x) when settings.show_lookup_steps => text(x) - | Var(x) => + | Var(x, _) when settings.show_lookup_steps => text(x) + | Var(x, _) => switch (ClosureEnvironment.lookup(env, x)) { | None => text(x) | Some(d') => @@ -649,7 +650,7 @@ let mk = switch (substitution) { | Some((step, _)) => switch (DHExp.term_of(step.d_loc)) { - | Var(v) when List.mem(v, recent_subst) => + | Var(v, _) when List.mem(v, recent_subst) => hcats([text(v) |> annot(DHAnnot.Substituted), doc]) | _ => doc } From ac01fc3bfeb73307e55cb9021000e19e1095ab47 Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Mon, 16 Sep 2024 14:03:04 -0400 Subject: [PATCH 2/3] Update tests --- test/Test_Elaboration.re | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re index 1c5a7c7271..6d150155c7 100644 --- a/test/Test_Elaboration.re +++ b/test/Test_Elaboration.re @@ -20,7 +20,7 @@ let empty_hole = () => alco_check("Empty hole", u2, dhexp_of_uexp(u2)); let u3: Exp.t = { ids: [id_at(0)], - term: Parens({ids: [id_at(1)], term: Var("y"), copied: false}), + term: Parens({ids: [id_at(1)], term: Var("y", false), copied: false}), copied: false, }; @@ -30,7 +30,11 @@ let u4: Exp.t = Let( Tuple([Var("a") |> Pat.fresh, Var("b") |> Pat.fresh]) |> Pat.fresh, Tuple([Int(4) |> Exp.fresh, Int(6) |> Exp.fresh]) |> Exp.fresh, - BinOp(Int(Minus), Var("a") |> Exp.fresh, Var("b") |> Exp.fresh) + BinOp( + Int(Minus), + Var("a", false) |> Exp.fresh, + Var("b", false) |> Exp.fresh, + ) |> Exp.fresh, ) |> Exp.fresh; @@ -39,7 +43,7 @@ let let_exp = () => alco_check("Let expression for tuple (a, b)", u4, dhexp_of_uexp(u4)); let u5 = - BinOp(Int(Plus), Bool(false) |> Exp.fresh, Var("y") |> Exp.fresh) + BinOp(Int(Plus), Bool(false) |> Exp.fresh, Var("y", false) |> Exp.fresh) |> Exp.fresh; let d5 = @@ -48,7 +52,7 @@ let d5 = FailedCast(Bool(false) |> Exp.fresh, Bool |> Typ.fresh, Int |> Typ.fresh) |> Exp.fresh, Cast( - Var("y") |> Exp.fresh, + Var("y", false) |> Exp.fresh, Unknown(Internal) |> Typ.fresh, Int |> Typ.fresh, ) @@ -85,7 +89,7 @@ let u7: Exp.t = None, ) |> Exp.fresh, - Var("y") |> Exp.fresh, + Var("y", false) |> Exp.fresh, ) |> Exp.fresh; @@ -147,7 +151,7 @@ let u9: Exp.t = |> Pat.fresh, Fun( Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x") |> Exp.fresh) + BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x", false) |> Exp.fresh) |> Exp.fresh, None, None, @@ -162,7 +166,7 @@ let d9: Exp.t = Var("f") |> Pat.fresh, Fun( Var("x") |> Pat.fresh, - BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x") |> Exp.fresh) + BinOp(Int(Plus), Int(1) |> Exp.fresh, Var("x", false) |> Exp.fresh) |> Exp.fresh, None, Some("f"), From ee7f1129dad9ed9ff2a9d16979f225416fdcc1fe Mon Sep 17 00:00:00 2001 From: Matt Keenan Date: Wed, 2 Oct 2024 15:59:53 -0400 Subject: [PATCH 3/3] Assign Unknown Type to Unbound Variables. --- src/haz3lcore/dynamics/TypeAssignment.re | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/haz3lcore/dynamics/TypeAssignment.re b/src/haz3lcore/dynamics/TypeAssignment.re index 5d14e27360..f6dca2fb15 100644 --- a/src/haz3lcore/dynamics/TypeAssignment.re +++ b/src/haz3lcore/dynamics/TypeAssignment.re @@ -133,9 +133,12 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) => let* ctx' = env_extend_ctx(env, m, ctx); typ_of_dhexp(ctx', m, d); | Filter(_, d) => typ_of_dhexp(ctx, m, d) + | Var(_, true) => Some(Unknown(Internal) |> Typ.temp) | Var(name, _) => - let* var = Ctx.lookup_var(ctx, name); - Some(var.typ); + Ctx.lookup_var(ctx, name) + |> Option.map((x: Ctx.var_entry) => x.typ) + |> Option.value(~default=Unknown(Internal) |> Typ.temp) + |> Option.some | Seq(d1, d2) => let* _ = typ_of_dhexp(ctx, m, d1); typ_of_dhexp(ctx, m, d2);