Merge fixup

src/haz3lcore/lang/term/Typ.re

@@ -57,29 +57,6 @@ let (replace_temp, replace_temp_exp) = {
   );
 };
 
-let all_ids_temp = {
-  let f:
-    'a.
-    (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
-   =
-    (continue, exp) => {...exp, ids: [Id.invalid]} |> continue;
-  map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f);
-};
-
-let (replace_temp, replace_temp_exp) = {
-  let f:
-    'a.
-    (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
-   =
-    (continue, exp) =>
-      {...exp, ids: exp.ids == [Id.invalid] ? [Id.mk()] : exp.ids}
-      |> continue;
-  (
-    map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
-    TermBase.Exp.map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),
-  );
-};
-
 let hole = (tms: list(TermBase.Any.t)): TermBase.Typ.term =>
   switch (tms) {
   | [] => Unknown(Hole(EmptyHole))

src/haz3lcore/pretty/ExpToSegment.re

@@ -1078,32 +1078,32 @@ and parenthesize_typ = (typ: Typ.t): Typ.t => {
 }
 
 and parenthesize_tpat = (tpat: TPat.t): TPat.t => {
-  let (term, rewrap) = IdTagged.unwrap(tpat);
+  let (term, rewrap: TPat.term => TPat.t) = IdTagged.unwrap(tpat);
   switch (term) {
   // Indivisible forms dont' change
   | Var(_)
   | Invalid(_)
   | EmptyHole => tpat
 
   // Other forms
-  | MultiHole(xs) => TPat.MultiHole(List.map(parenthesize_any, xs)) |> rewrap
+  | MultiHole(xs) => MultiHole(List.map(parenthesize_any, xs)) |> rewrap
   };
 }
 
 and parenthesize_rul = (rul: Rul.t): Rul.t => {
-  let (term, rewrap) = IdTagged.unwrap(rul);
+  let (term, rewrap: Rul.term => Rul.t) = IdTagged.unwrap(rul);
   switch (term) {
   // Indivisible forms dont' change
   | Invalid(_) => rul
 
   // Other forms
   | Rules(e, ps) =>
-    Rul.Rules(
+    Rules(
       parenthesize(e),
       List.map(((p, e)) => (parenthesize_pat(p), parenthesize(e)), ps),
     )
     |> rewrap
-  | Hole(xs) => Rul.Hole(List.map(parenthesize_any, xs)) |> rewrap
+  | Hole(xs) => Hole(List.map(parenthesize_any, xs)) |> rewrap
   };
 }
 

src/haz3lcore/statics/Elaborator.re

@@ -18,15 +18,15 @@ module ElaborationResult = {
     | DoesNotElaborate;
 };
 
-let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): DHExp.t => {
+let fresh_cast = (d: DHExp.t, t1: Typ.t, t2: Typ.t): Exp.t => {
   Typ.eq(t1, t2)
     ? d
     : {
-      let d' =
-        Exp.Cast(d, t1, Typ.temp(Unknown(Internal)))
+      let d': Exp.t =
+        (Cast(d, t1, Typ.temp(Unknown(Internal))): Exp.term)
         |> IdTagged.fresh_deterministic(DHExp.rep_id(d))
         |> Casts.transition_multiple;
-      Cast(d', Typ.temp(Unknown(Internal)), t2)
+      (Cast(d', Typ.temp(Unknown(Internal)), t2): Exp.term)
       |> IdTagged.fresh_deterministic(DHExp.rep_id(d'))
       |> Casts.transition_multiple;
     };
@@ -312,7 +312,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         let (def, ty2) = elaborate(m, def);
         let (body, ty) = elaborate(m, body);
         let fixf =
-          Exp.FixF(p, fresh_cast(def, ty2, ty1), None)
+          (FixF(p, fresh_cast(def, ty2, ty1), None): Exp.term)
           |> IdTagged.fresh_deterministic(DHExp.rep_id(uexp));
         Let(p, fixf, body) |> rewrap |> cast_from(ty);
       };

src/haz3lcore/statics/TermBase.re

@@ -1020,7 +1020,7 @@ and ClosureEnvironment: {
   let without_keys = keys => update(Environment.without_keys(keys));
   let with_symbolic_keys = (keys, env) =>
     List.fold_right(
-      (key, env) => extend(env, (key, Exp.Var(key) |> IdTagged.fresh)),
+      (key, env) => extend(env, (key, Var(key) |> IdTagged.fresh)),
       keys,
       env,
     );

src/haz3lcore/zipper/EditorUtil.re

@@ -50,7 +50,7 @@ let rec append_exp = (e1: Exp.t, e2: Exp.t): Exp.t => {
 let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t =>
   Exp.{
     term:
-      Exp.Filter(
+      Filter(
         Filter({
           act: FilterAction.(act, One),
           pat: {

src/haz3lweb/exercises/Exercise.re

@@ -419,23 +419,22 @@ let put_stitched = (pos, s: stitched('a), x: 'a): stitched('a) =>
   | HiddenTests => {...s, hidden_tests: x}
   };
 
-let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t =>
-  Exp.{
-    term:
-      Exp.Filter(
-        Filter({
-          act: FilterAction.(act, One),
-          pat: {
-            term: Constructor("$e", Unknown(Internal) |> Typ.temp),
-            copied: false,
-            ids: [Id.mk()],
-          },
-        }),
-        term,
-      ),
-    copied: false,
-    ids: [Id.mk()],
-  };
+let wrap_filter = (act: FilterAction.action, term: UExp.t): UExp.t => {
+  term:
+    Filter(
+      Filter({
+        act: FilterAction.(act, One),
+        pat: {
+          term: Constructor("$e", Unknown(Internal) |> Typ.temp),
+          copied: false,
+          ids: [Id.mk()],
+        },
+      }),
+      term,
+    ),
+  copied: false,
+  ids: [Id.mk()],
+};
 
 let wrap = (term, editor: Editor.t): TermItem.t => {term, editor};