Track unbound variables in expressions

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

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

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 = {

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

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;

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

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)

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

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, _})

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

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
         },
     };

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

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)

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

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
         }

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"),