Introduce custom annotation on grammar

src/haz3lcore/dynamics/Casts.re

@@ -196,7 +196,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
       let (p1, d1) = unwrap_casts(p1);
       (
         p1,
-        {term: Cast(d1, t1, t2), copied: p.copied, ids: p.ids}
+        {term: Cast(d1, t1, t2), annotation: p.annotation}
         |> transition_multiple,
       );
     | _ => (p, hole)
@@ -207,7 +207,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
     | EmptyHole => p
     | Cast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
-      {term: Cast(p1, t1, t2), copied: d.copied, ids: d.ids};
+      {term: Cast(p1, t1, t2), annotation: d.annotation};
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {
@@ -217,8 +217,7 @@ let pattern_fixup = (p: DHPat.t): DHPat.t => {
             Typ.fresh(Unknown(Internal)),
             t2,
           ),
-        copied: d.copied,
-        ids: d.ids,
+        annotation: d.annotation,
       };
     | _ => failwith("unexpected term in rewrap_casts")
     };

src/haz3lcore/dynamics/DHExp.re

@@ -11,15 +11,21 @@ let term_of: t => term = IdTagged.term_of;
 let fast_copy: (Id.t, t) => t = IdTagged.fast_copy;
 
 let mk = (ids, term): t => {
-  {ids, copied: true, term};
+  {
+    term,
+    annotation: {
+      ids,
+      copied: true,
+    },
+  };
 };
 
 // TODO: make this function emit a map of changes
 let repair_ids =
   map_term(
     ~f_exp=
       (continue, exp) =>
-        if (exp.copied) {
+        if (IdTagged.copied(exp)) {
           replace_all_ids(exp);
         } else {
           continue(exp);
@@ -45,7 +51,7 @@ let repair_ids_typ =
         },
     ~f_typ=
       (continue, typ) =>
-        if (typ.copied) {
+        if (IdTagged.copied(typ)) {
           replace_all_ids_typ(typ);
         } else {
           continue(typ);

src/haz3lcore/dynamics/FilterMatcher.re

@@ -22,12 +22,12 @@ let evaluate_extend_env_with_pat =
       Environment.singleton((
         fname,
         {
-          ids,
-          copied,
-          IdTagged.term: (
-            FixF(pat, exp, Some(to_extend)): TermBase.exp_term
-          ),
-        },
+          annotation: {
+            ids,
+            copied,
+          },
+          term: FixF(pat, exp, Some(to_extend)),
+        }: TermBase.exp_t,
       )),
       to_extend,
     )
@@ -41,7 +41,13 @@ let evaluate_extend_env_with_pat =
             (
               Let(
                 pat,
-                {ids, copied, term: FixF(pat, exp, Some(to_extend))},
+                {
+                  term: FixF(pat, exp, Some(to_extend)),
+                  annotation: {
+                    ids,
+                    copied,
+                  },
+                },
                 (Var(binding): TermBase.exp_term) |> IdTagged.fresh,
               ): TermBase.exp_term
             )
@@ -132,16 +138,44 @@ let rec matches_exp =
       | Some((denv, fenv)) => matches_exp(~denv, dc, ~fenv, fc)
       }
     | (FixF(dp, dc, None), _) =>
-      let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv);
+      let denv =
+        evaluate_extend_env_with_pat(
+          IdTagged.ids(d),
+          IdTagged.copied(d),
+          dp,
+          dc,
+          denv,
+        );
       matches_exp(~denv, dc, ~fenv, f);
     | (FixF(dp, dc, Some(denv)), _) =>
-      let denv = evaluate_extend_env_with_pat(d.ids, d.copied, dp, dc, denv);
+      let denv =
+        evaluate_extend_env_with_pat(
+          IdTagged.ids(d),
+          IdTagged.copied(d),
+          dp,
+          dc,
+          denv,
+        );
       matches_exp(~denv, dc, ~fenv, f);
     | (_, FixF(fp, fc, None)) =>
-      let fenv = evaluate_extend_env_with_pat(f.ids, f.copied, fp, fc, fenv);
+      let fenv =
+        evaluate_extend_env_with_pat(
+          IdTagged.ids(f),
+          IdTagged.copied(f),
+          fp,
+          fc,
+          fenv,
+        );
       matches_exp(~denv, d, ~fenv, fc);
     | (_, FixF(fp, fc, Some(fenv))) =>
-      let fenv = evaluate_extend_env_with_pat(f.ids, f.copied, fp, fc, fenv);
+      let fenv =
+        evaluate_extend_env_with_pat(
+          IdTagged.ids(f),
+          IdTagged.copied(f),
+          fp,
+          fc,
+          fenv,
+        );
       matches_exp(~denv, d, ~fenv, fc);
 
     | (_, Constructor("$v", _)) =>

src/haz3lcore/lang/term/IdTagged.re

@@ -1,35 +1,52 @@
 open Util;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
-type t('a) = {
-  [@show.opaque]
-  ids: list(Id.t),
-  [@show.opaque]
-  /* Exp invariant: copied should always be false, and the id should be unique
-     DHExp invariant: if copied is true, then this term and its children may not
-     have unique ids. The flag is used to avoid deep-copying expressions during
-     evaluation, while keeping track of where we will need to replace the ids
-     at the end of evaluation to keep them unique.*/
-  copied: bool,
-  term: 'a,
-};
+type t('a) = Grammar.Annotated.t('a, Grammar.IdTag.t);
 
 // To be used if you want to remove the id from the debug output
 // let pp: ((Format.formatter, 'a) => unit, Format.formatter, t('a)) => unit =
 //   (fmt_a, formatter, ta) => {
 //     fmt_a(formatter, ta.term);
 //   };
-let fresh = term => {
-  {ids: [Id.mk()], copied: false, term};
+let fresh = (term: 'a): Grammar.Annotated.t('a, Grammar.IdTag.t) => {
+  {
+    term,
+    annotation: {
+      ids: [Id.mk()],
+      copied: false,
+    },
+  };
+};
+let fresh_deterministic = (prev_id, term): t('a) => {
+  {
+    term,
+    annotation: {
+      ids: [Id.next(prev_id)],
+      copied: false,
+    },
+  };
+};
+
+let term_of = (x: Grammar.Annotated.t('a, 'b)) => x.term;
+let unwrap = (x: t('a)) => (x.term, term' => {...x, term: term'});
+let rep_id =
+    ({annotation: {ids, _}, _}: Grammar.Annotated.t('a, Grammar.IdTag.t)) =>
+  List.hd(ids);
+
+let fast_copy = (id, {term, _}: t('a)): t('a) => {
+  term,
+  annotation: {
+    copied: true,
+    ids: [id],
+  },
 };
-let fresh_deterministic = (prev_id, term) => {
-  {ids: [Id.next(prev_id)], copied: false, term};
+let new_ids = ({term, annotation: {ids: _, copied}}: t('a)): t('a) => {
+  term,
+  annotation: {
+    ids: [Id.mk()],
+    copied,
+  },
 };
 
-let term_of = x => x.term;
-let unwrap = x => (x.term, term' => {...x, term: term'});
-let rep_id = ({ids, _}) => List.hd(ids);
-let fast_copy = (id, {term, _}) => {ids: [id], term, copied: true};
-let new_ids =
-  fun
-  | {ids: _, term, copied} => {ids: [Id.mk()], term, copied};
+let ids = ({annotation: {ids, _}, _}: t('a)) => ids;
+let copied = ({annotation: {copied, _}, _}: t('a)) => copied;

src/haz3lcore/lang/term/Typ.re

@@ -31,15 +31,30 @@ let fresh: term => t = IdTagged.fresh;
 /* fresh assigns a random id, whereas temp assigns Id.invalid, which
    is a lot faster, and since we so often make types and throw them away
    shortly after, it makes sense to use it. */
-let temp: term => t = term => {term, ids: [Id.invalid], copied: false};
+let temp: term => t =
+  term => {
+    term,
+    annotation: {
+      ids: [Id.invalid],
+      copied: false,
+    },
+  };
 let rep_id: t => Id.t = IdTagged.rep_id;
 
 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;
+    (continue, exp) =>
+      {
+        term: exp.term,
+        annotation: {
+          ...exp.annotation,
+          ids: [Id.invalid],
+        },
+      }
+      |> continue;
   map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f);
 };
 
@@ -49,7 +64,15 @@ let (replace_temp, replace_temp_exp) = {
     (IdTagged.t('a) => IdTagged.t('a), IdTagged.t('a)) => IdTagged.t('a)
    =
     (continue, exp) =>
-      {...exp, ids: exp.ids == [Id.invalid] ? [Id.mk()] : exp.ids}
+      {
+        ...exp,
+        annotation: {
+          ...exp.annotation,
+          ids:
+            exp.annotation.ids == [Id.invalid]
+              ? [Id.mk()] : exp.annotation.ids,
+        },
+      }
       |> continue;
   (
     map_term(~f_exp=f, ~f_pat=f, ~f_typ=f, ~f_tpat=f, ~f_rul=f),

src/haz3lcore/pretty/ExpToSegment.re

@@ -696,8 +696,8 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let* x = go(x)
     and* xs = xs |> List.map(go) |> all;
     let (id, ids) = (
-      exp.ids |> List.hd,
-      exp.ids |> List.tl |> pad_ids(List.length(xs)),
+      IdTagged.ids(exp) |> List.hd,
+      IdTagged.ids(exp) |> List.tl |> pad_ids(List.length(xs)),
     );
     let form = (x, xs) =>
       mk_form(
@@ -795,7 +795,7 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     // TODO: Add optional newlines
     let+ x = go(x)
     and+ xs = xs |> List.map(go) |> all;
-    let ids = exp.ids |> pad_ids(List.length(xs));
+    let ids = IdTagged.ids(exp) |> pad_ids(List.length(xs));
     x
     @ List.flatten(
         List.map2((id, x) => [mk_form("comma_exp", id, [])] @ x, ids, xs),
@@ -854,8 +854,8 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
     let+ e = go(e)
     and+ es = es |> List.map(go) |> all;
     let (id, ids) = (
-      exp.ids |> List.hd,
-      exp.ids |> List.tl |> pad_ids(List.length(es)),
+      IdTagged.ids(exp) |> List.hd,
+      IdTagged.ids(exp) |> List.tl |> pad_ids(List.length(es)),
     );
     e
     @ [
@@ -953,8 +953,8 @@ let rec exp_to_pretty = (~settings: Settings.t, exp: Exp.t): pretty => {
       |> all;
     };
     let (id, ids) = (
-      exp.ids |> List.hd,
-      exp.ids |> List.tl |> pad_ids(List.length(rs)),
+      IdTagged.ids(exp) |> List.hd,
+      IdTagged.ids(exp) |> List.tl |> pad_ids(List.length(rs)),
     );
     [
       mk_form(
@@ -1006,8 +1006,8 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
     let* x = go(x)
     and* xs = xs |> List.map(go) |> all;
     let (id, ids) = (
-      pat.ids |> List.hd,
-      pat.ids |> List.tl |> pad_ids(List.length(xs)),
+      IdTagged.ids(pat) |> List.hd,
+      IdTagged.ids(pat) |> List.tl |> pad_ids(List.length(xs)),
     );
     p_just([
       mk_form(
@@ -1035,7 +1035,7 @@ and pat_to_pretty = (~settings: Settings.t, pat: Pat.t): pretty => {
   | Tuple([x, ...xs]) =>
     let+ x = go(x)
     and+ xs = xs |> List.map(go) |> all;
-    let ids = pat.ids |> pad_ids(List.length(xs));
+    let ids = IdTagged.ids(pat) |> pad_ids(List.length(xs));
     x
     @ List.flatten(
         List.map2((id, x) => [mk_form("comma_pat", id, [])] @ x, ids, xs),
@@ -1118,7 +1118,7 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
     @ List.flatten(
         List.map2(
           (id, t) => [mk_form("comma_typ", id, [])] @ t,
-          typ.ids |> pad_ids(ts |> List.length),
+          IdTagged.ids(typ) |> pad_ids(ts |> List.length),
           ts,
         ),
       );
@@ -1152,7 +1152,7 @@ and typ_to_pretty = (~settings: Settings.t, typ: Typ.t): pretty => {
     let+ t = go_constructor(t);
     [mk_form("typ_sum_single", id, [])] @ t;
   | Sum([t, ...ts]) =>
-    let ids = typ.ids |> pad_ids(List.length(ts) + 1);
+    let ids = IdTagged.ids(typ) |> pad_ids(List.length(ts) + 1);
     let id = List.hd(ids);
     let ids = List.tl(ids);
     let+ t = go_constructor(t)

src/haz3lcore/prog/CachedStatics.re

@@ -10,13 +10,17 @@ type t = {
 
 let empty: t = {
   term: {
-    ids: [Id.invalid],
-    copied: false,
+    annotation: {
+      ids: [Id.invalid],
+      copied: false,
+    },
     term: Tuple([]),
   },
   elaborated: {
-    ids: [Id.invalid],
-    copied: false,
+    annotation: {
+      ids: [Id.invalid],
+      copied: false,
+    },
     term: Tuple([]),
   },
   info_map: Id.Map.empty,