Merge branch 'dev' into editor-output

hazelgrove · Nov 21, 2024 · 4d7dcf7 · 4d7dcf7
2 parents 7eb9fa5 + 297b04b
commit 4d7dcf7
Show file tree

Hide file tree

Showing 19 changed files with 450 additions and 538 deletions.
diff --git a/src/haz3lcore/dynamics/Builtins.re b/src/haz3lcore/dynamics/Builtins.re
@@ -41,13 +41,13 @@ let fn =
 module Pervasives = {
   module Impls = {
     /* constants */
-    let infinity = DHExp.Float(Float.infinity) |> fresh;
-    let neg_infinity = DHExp.Float(Float.neg_infinity) |> fresh;
-    let nan = DHExp.Float(Float.nan) |> fresh;
-    let epsilon_float = DHExp.Float(epsilon_float) |> fresh;
-    let pi = DHExp.Float(Float.pi) |> fresh;
-    let max_int = DHExp.Int(Int.max_int) |> fresh;
-    let min_int = DHExp.Int(Int.min_int) |> fresh;
+    let infinity = Float(Float.infinity) |> fresh;
+    let neg_infinity = Float(Float.neg_infinity) |> fresh;
+    let nan = Float(Float.nan) |> fresh;
+    let epsilon_float = Float(epsilon_float) |> fresh;
+    let pi = Float(Float.pi) |> fresh;
+    let max_int = Int(Int.max_int) |> fresh;
+    let min_int = Int(Int.min_int) |> fresh;
 
     let unary = (f: DHExp.t => result, d: DHExp.t) => {
       switch (f(d)) {
@@ -180,8 +180,8 @@ module Pervasives = {
           switch (convert(s)) {
           | Some(n) => Ok(wrap(n))
           | None =>
-            let d' = DHExp.BuiltinFun(name) |> DHExp.fresh;
-            let d' = DHExp.Ap(Forward, d', d) |> DHExp.fresh;
+            let d' = BuiltinFun(name) |> DHExp.fresh;
+            let d' = Ap(Forward, d', d) |> DHExp.fresh;
             let d' = DynamicErrorHole(d', InvalidOfString) |> DHExp.fresh;
             Ok(d');
           }
@@ -204,8 +204,7 @@ module Pervasives = {
             Ok(
               fresh(
                 DynamicErrorHole(
-                  DHExp.Ap(Forward, DHExp.BuiltinFun(name) |> fresh, d1)
-                  |> fresh,
+                  Ap(Forward, BuiltinFun(name) |> fresh, d1) |> fresh,
                   DivideByZero,
                 ),
               ),

diff --git a/src/haz3lcore/dynamics/Casts.re b/src/haz3lcore/dynamics/Casts.re
@@ -39,7 +39,7 @@ let grounded_Forall =
   );
 let grounded_Prod = length =>
   NotGroundOrHole(
-    Prod(ListUtil.replicate(length, Typ.Unknown(Internal) |> Typ.temp))
+    Prod(ListUtil.replicate(length, Unknown(Internal) |> Typ.temp))
     |> Typ.temp,
   );
 let grounded_Sum: unit => Typ.sum_map =
@@ -50,7 +50,7 @@ let grounded_List =
 let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   let is_hole: Typ.t => bool =
     fun
-    | {term: Typ.Unknown(_), _} => true
+    | {term: Unknown(_), _} => true
     | _ => false;
   switch (Typ.term_of(ty)) {
   | Unknown(_) => Hole
@@ -67,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Prod(tys) =>
     if (List.for_all(
           fun
-          | ({term: Typ.Unknown(_), _}: Typ.t) => true
+          | ({term: Unknown(_), _}: Typ.t) => true
           | _ => false,
           tys,
         )) {
@@ -134,14 +134,14 @@ let rec transition = (~recursive=false, d: DHExp.t): option(DHExp.t) => {
         | None => inner_cast
         };
       Some(
-        DHExp.Cast(inner_cast, t2_grounded |> DHExp.replace_all_ids_typ, t2)
+        Cast(inner_cast, t2_grounded |> DHExp.replace_all_ids_typ, t2)
         |> DHExp.fresh,
       );
 
     | (NotGroundOrHole(t1_grounded), Hole) =>
       /* ITGround rule */
       Some(
-        DHExp.Cast(
+        Cast(
           Cast(d1, t1, t1_grounded |> DHExp.replace_all_ids_typ)
           |> DHExp.fresh,
           t1_grounded |> DHExp.replace_all_ids_typ,
@@ -196,7 +196,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
       let (p1, d1) = unwrap_casts(p1);
       (
         p1,
-        {term: DHExp.Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
+        {term: Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
         |> transition_multiple,
       );
     | _ => (p, hole)
@@ -207,13 +207,13 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
     | EmptyHole => p
     | Cast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
-      {term: DHPat.Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
+      {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {
         term:
-          DHPat.Cast(
-            DHPat.Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
+          Cast(
+            Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
             Typ.fresh(Unknown(Internal)),
             t2,
           ),

diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
@@ -51,106 +51,103 @@ let rec compose = (ctx: t, d: DHExp.t): DHExp.t => {
   | Mark => d
   | Term({term, ids}) =>
     let wrap = DHExp.mk(ids);
-    DHExp.(
-      switch (term) {
-      | Closure(env, ctx) =>
-        let d = compose(ctx, d);
-        Closure(env, d) |> wrap;
-      | Filter(flt, ctx) =>
-        let d = compose(ctx, d);
-        Filter(flt, d) |> wrap;
-      | Seq1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Seq(d1, d2) |> wrap;
-      | Seq2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Seq(d1, d2) |> wrap;
-      | Ap1(dir, ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Ap(dir, d1, d2) |> wrap;
-      | Ap2(dir, d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Ap(dir, d1, d2) |> wrap;
-      | DeferredAp1(ctx, d2s) =>
-        let d1 = compose(ctx, d);
-        DeferredAp(d1, d2s) |> wrap;
-      | DeferredAp2(d1, ctx, (ld, rd)) =>
-        let d2 = compose(ctx, d);
-        DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap;
-      | If1(ctx, d2, d3) =>
-        let d' = compose(ctx, d);
-        If(d', d2, d3) |> wrap;
-      | If2(d1, ctx, d3) =>
-        let d' = compose(ctx, d);
-        If(d1, d', d3) |> wrap;
-      | If3(d1, d2, ctx) =>
-        let d' = compose(ctx, d);
-        If(d1, d2, d') |> wrap;
-      | Test(ctx) =>
-        let d1 = compose(ctx, d);
-        Test(d1) |> wrap;
-      | UnOp(op, ctx) =>
-        let d1 = compose(ctx, d);
-        UnOp(op, d1) |> wrap;
-      | BinOp1(op, ctx, d2) =>
-        let d1 = compose(ctx, d);
-        BinOp(op, d1, d2) |> wrap;
-      | BinOp2(op, d1, ctx) =>
-        let d2 = compose(ctx, d);
-        BinOp(op, d1, d2) |> wrap;
-      | Cons1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        Cons(d1, d2) |> wrap;
-      | Cons2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        Cons(d1, d2) |> wrap;
-      | ListConcat1(ctx, d2) =>
-        let d1 = compose(ctx, d);
-        ListConcat(d1, d2) |> wrap;
-      | ListConcat2(d1, ctx) =>
-        let d2 = compose(ctx, d);
-        ListConcat(d1, d2) |> wrap;
-      | Tuple(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
-      | ListLit(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
-      | MultiHole(ctx, (ld, rd)) =>
-        let d = compose(ctx, d);
-        MultiHole(ListUtil.rev_concat(ld, [TermBase.Any.Exp(d), ...rd]))
-        |> wrap;
-      | Let1(dp, ctx, d2) =>
-        let d = compose(ctx, d);
-        Let(dp, d, d2) |> wrap;
-      | Let2(dp, d1, ctx) =>
-        let d = compose(ctx, d);
-        Let(dp, d1, d) |> wrap;
-      | Fun(dp, ctx, env, v) =>
-        let d = compose(ctx, d);
-        Fun(dp, d, env, v) |> wrap;
-      | FixF(v, ctx, env) =>
-        let d = compose(ctx, d);
-        FixF(v, d, env) |> wrap;
-      | Cast(ctx, ty1, ty2) =>
-        let d = compose(ctx, d);
-        Cast(d, ty1, ty2) |> wrap;
-      | FailedCast(ctx, ty1, ty2) =>
-        let d = compose(ctx, d);
-        FailedCast(d, ty1, ty2) |> wrap;
-      | DynamicErrorHole(ctx, err) =>
-        let d = compose(ctx, d);
-        DynamicErrorHole(d, err) |> wrap;
-      | MatchScrut(ctx, rules) =>
-        let d = compose(ctx, d);
-        Match(d, rules) |> wrap;
-      | MatchRule(scr, p, ctx, (lr, rr)) =>
-        let d = compose(ctx, d);
-        Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap;
-      | TypAp(ctx, ty) =>
-        let d = compose(ctx, d);
-        TypAp(d, ty) |> wrap;
-      }
-    );
+    switch (term) {
+    | Closure(env, ctx) =>
+      let d = compose(ctx, d);
+      Closure(env, d) |> wrap;
+    | Filter(flt, ctx) =>
+      let d = compose(ctx, d);
+      Filter(flt, d) |> wrap;
+    | Seq1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Seq(d1, d2) |> wrap;
+    | Seq2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Seq(d1, d2) |> wrap;
+    | Ap1(dir, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Ap(dir, d1, d2) |> wrap;
+    | Ap2(dir, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Ap(dir, d1, d2) |> wrap;
+    | DeferredAp1(ctx, d2s) =>
+      let d1 = compose(ctx, d);
+      DeferredAp(d1, d2s) |> wrap;
+    | DeferredAp2(d1, ctx, (ld, rd)) =>
+      let d2 = compose(ctx, d);
+      DeferredAp(d1, ListUtil.rev_concat(ld, [d2, ...rd])) |> wrap;
+    | If1(ctx, d2, d3) =>
+      let d' = compose(ctx, d);
+      If(d', d2, d3) |> wrap;
+    | If2(d1, ctx, d3) =>
+      let d' = compose(ctx, d);
+      If(d1, d', d3) |> wrap;
+    | If3(d1, d2, ctx) =>
+      let d' = compose(ctx, d);
+      If(d1, d2, d') |> wrap;
+    | Test(ctx) =>
+      let d1 = compose(ctx, d);
+      Test(d1) |> wrap;
+    | UnOp(op, ctx) =>
+      let d1 = compose(ctx, d);
+      UnOp(op, d1) |> wrap;
+    | BinOp1(op, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      BinOp(op, d1, d2) |> wrap;
+    | BinOp2(op, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      BinOp(op, d1, d2) |> wrap;
+    | Cons1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Cons(d1, d2) |> wrap;
+    | Cons2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Cons(d1, d2) |> wrap;
+    | ListConcat1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      ListConcat(d1, d2) |> wrap;
+    | ListConcat2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      ListConcat(d1, d2) |> wrap;
+    | Tuple(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      Tuple(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
+    | ListLit(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      ListLit(ListUtil.rev_concat(ld, [d, ...rd])) |> wrap;
+    | MultiHole(ctx, (ld, rd)) =>
+      let d = compose(ctx, d);
+      MultiHole(ListUtil.rev_concat(ld, [Exp(d), ...rd])) |> wrap;
+    | Let1(dp, ctx, d2) =>
+      let d = compose(ctx, d);
+      Let(dp, d, d2) |> wrap;
+    | Let2(dp, d1, ctx) =>
+      let d = compose(ctx, d);
+      Let(dp, d1, d) |> wrap;
+    | Fun(dp, ctx, env, v) =>
+      let d = compose(ctx, d);
+      Fun(dp, d, env, v) |> wrap;
+    | FixF(v, ctx, env) =>
+      let d = compose(ctx, d);
+      FixF(v, d, env) |> wrap;
+    | Cast(ctx, ty1, ty2) =>
+      let d = compose(ctx, d);
+      Cast(d, ty1, ty2) |> wrap;
+    | FailedCast(ctx, ty1, ty2) =>
+      let d = compose(ctx, d);
+      FailedCast(d, ty1, ty2) |> wrap;
+    | DynamicErrorHole(ctx, err) =>
+      let d = compose(ctx, d);
+      DynamicErrorHole(d, err) |> wrap;
+    | MatchScrut(ctx, rules) =>
+      let d = compose(ctx, d);
+      Match(d, rules) |> wrap;
+    | MatchRule(scr, p, ctx, (lr, rr)) =>
+      let d = compose(ctx, d);
+      Match(scr, ListUtil.rev_concat(lr, [(p, d), ...rr])) |> wrap;
+    | TypAp(ctx, ty) =>
+      let d = compose(ctx, d);
+      TypAp(d, ty) |> wrap;
+    };
   };
 };
diff --git a/src/haz3lcore/dynamics/FilterEnvironment.re b/src/haz3lcore/dynamics/FilterEnvironment.re
@@ -1,2 +1,2 @@
-type t = list(TermBase.StepperFilterKind.filter);
+type t = list(TermBase.filter);
 let extends = (flt, env) => [flt, ...env];
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -24,7 +24,9 @@ let evaluate_extend_env_with_pat =
         {
           ids,
           copied,
-          IdTagged.term: TermBase.Exp.FixF(pat, exp, Some(to_extend)),
+          IdTagged.term: (
+            FixF(pat, exp, Some(to_extend)): TermBase.exp_term
+          ),
         },
       )),
       to_extend,
@@ -36,14 +38,12 @@ let evaluate_extend_env_with_pat =
         binding =>
           (
             binding,
-            TermBase.Exp.Let(
-              pat,
-              {
-                ids,
-                copied,
-                term: TermBase.Exp.FixF(pat, exp, Some(to_extend)),
-              },
-              TermBase.Exp.Var(binding) |> IdTagged.fresh,
+            (
+              Let(
+                pat,
+                {ids, copied, term: FixF(pat, exp, Some(to_extend))},
+                (Var(binding): TermBase.exp_term) |> IdTagged.fresh,
+              ): TermBase.exp_term
             )
             |> 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, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         dvars,
       );
     let fenv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         fvars,
       );
     let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv);
@@ -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, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         dvars,
       );
     let fenv_subst: list((string, 'a)) =
       List.mapi(
         (i, binding) =>
-          (binding, TermBase.Exp.Var(ids[i]) |> IdTagged.fresh),
+          (binding, (Var(ids[i]): TermBase.exp_term) |> IdTagged.fresh),
         fvars,
       );
     let denv = evaluate_extend_env(Environment.of_list(denv_subst), denv);
@@ -387,11 +387,7 @@ and matches_utpat = (d: TPat.t, f: TPat.t): bool => {
 };
 
 let matches =
-    (
-      ~env: ClosureEnvironment.t,
-      ~exp: DHExp.t,
-      ~flt: TermBase.StepperFilterKind.filter,
-    )
+    (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: TermBase.filter)
     : option(FilterAction.t) =>
   if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) {
     Some(flt.act);