merged with dev

src/haz3lcore/Measured.re

@@ -128,7 +128,13 @@ let rec add_n_rows = (origin: Point.t, row_indent, n: abs_indent, map: t): t =>
   | _ =>
     map
     |> add_n_rows(origin, row_indent, n - 1)
-    |> add_row(origin.row + n - 1, {indent: row_indent, max_col: origin.col})
+    |> add_row(
+         origin.row + n - 1,
+         {
+           indent: row_indent,
+           max_col: origin.col,
+         },
+       )
   };
 
 let add_lb = (id, indent, map) => {
@@ -180,7 +186,10 @@ let find_t = (t: Tile.t, map): measurement => {
     }) {
     | _ => failwith("find_t: inconsistent shard infor between tile and map")
     };
-  {origin: first.origin, last: last.last};
+  {
+    origin: first.origin,
+    last: last.last,
+  };
 };
 let find_p = (~msg="", p: Piece.t, map): measurement =>
   try(
@@ -212,7 +221,10 @@ let find_by_id = (id: Id.t, map: t): option(measurement) => {
             shards,
             "find_by_id",
           );
-        Some({origin: first.origin, last: last.last});
+        Some({
+          origin: first.origin,
+          last: last.last,
+        });
       | None =>
         switch (Id.Map.find_opt(id, map.projectors)) {
         | Some(m) => Some(m)
@@ -332,39 +344,90 @@ let of_segment = (seg: Segment.t, info_map: Statics.Map.t): t => {
                 contained_indent + (Id.Map.find(w.id, is_indented) ? 2 : 0);
               };
             let last =
-              Point.{row: origin.row + 1, col: container_indent + indent};
+              Point.{
+                row: origin.row + 1,
+                col: container_indent + indent,
+              };
             let map =
               map
-              |> add_w(w, {origin, last})
+              |> add_w(
+                   w,
+                   {
+                     origin,
+                     last,
+                   },
+                 )
               |> add_row(
                    origin.row,
-                   {indent: row_indent, max_col: origin.col},
+                   {
+                     indent: row_indent,
+                     max_col: origin.col,
+                   },
                  )
               |> add_lb(w.id, indent);
             (indent, last, map);
           | Secondary(w) =>
             let wspace_length =
               Unicode.length(Secondary.get_string(w.content));
-            let last = {...origin, col: origin.col + wspace_length};
-            let map = map |> add_w(w, {origin, last});
+            let last = {
+              ...origin,
+              col: origin.col + wspace_length,
+            };
+            let map =
+              map
+              |> add_w(
+                   w,
+                   {
+                     origin,
+                     last,
+                   },
+                 );
             (contained_indent, last, map);
           | Grout(g) =>
-            let last = {...origin, col: origin.col + 1};
-            let map = map |> add_g(g, {origin, last});
+            let last = {
+              ...origin,
+              col: origin.col + 1,
+            };
+            let map =
+              map
+              |> add_g(
+                   g,
+                   {
+                     origin,
+                     last,
+                   },
+                 );
             (contained_indent, last, map);
           | Projector(p) =>
             let token =
               Projector.placeholder(p, Id.Map.find_opt(p.id, info_map));
             let last = last_of_token(token, origin);
             let map = extra_rows(token, origin, map);
-            let map = add_pr(p, {origin, last}, map);
+            let map =
+              add_pr(
+                p,
+                {
+                  origin,
+                  last,
+                },
+                map,
+              );
             (contained_indent, last, map);
           | Tile(t) =>
             let add_shard = (origin, shard, map) => {
               let token = List.nth(t.label, shard);
               let map = extra_rows(token, origin, map);
               let last = last_of_token(token, origin);
-              let map = add_s(t.id, shard, {origin, last}, map);
+              let map =
+                add_s(
+                  t.id,
+                  shard,
+                  {
+                    origin,
+                    last,
+                  },
+                  map,
+                );
               (last, map);
             };
             let (last, map) =

src/haz3lcore/assistant/AssistantCtx.re

@@ -10,7 +10,10 @@ let free_variables =
       | None =>
         let joint_use_typ = CoCtx.join(ctx, entries);
         if (Typ.is_consistent(ctx, expected_ty, joint_use_typ)) {
-          Some({content: name, strategy: Pat(FromCoCtx(joint_use_typ))});
+          Some({
+            content: name,
+            strategy: Pat(FromCoCtx(joint_use_typ)),
+          });
         } else {
           None;
         };
@@ -26,7 +29,10 @@ let bound_variables = (ty_expect: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
     fun
     | Ctx.VarEntry({typ, name, _})
         when Typ.is_consistent(ctx, ty_expect, typ) =>
-      Some({content: name, strategy: Exp(Common(FromCtx(typ)))})
+      Some({
+        content: name,
+        strategy: Exp(Common(FromCtx(typ))),
+      })
     | _ => None,
     ctx,
   );
@@ -39,7 +45,10 @@ let bound_constructors =
     fun
     | Ctx.ConstructorEntry({typ, name, _})
         when Typ.is_consistent(ctx, ty, typ) =>
-      Some({content: name, strategy: wrap(FromCtx(typ))})
+      Some({
+        content: name,
+        strategy: wrap(FromCtx(typ)),
+      })
     | _ => None,
     ctx,
   );
@@ -72,7 +81,10 @@ let bound_constructor_aps = (wrap, ty: Typ.t, ctx: Ctx.t): list(Suggestion.t) =>
         when
           Typ.is_consistent(ctx, ty, ty_out)
           && !Typ.is_consistent(ctx, ty, ty_arr) =>
-      Some({content: name ++ "(", strategy: wrap(FromCtxAp(ty_out))})
+      Some({
+        content: name ++ "(",
+        strategy: wrap(FromCtxAp(ty_out)),
+      })
     | _ => None,
     ctx,
   );
@@ -82,7 +94,10 @@ let typ_context_entries = (ctx: Ctx.t): list(Suggestion.t) =>
   List.filter_map(
     fun
     | Ctx.TVarEntry({kind: Singleton(_), name, _}) =>
-      Some({content: name, strategy: Typ(FromCtx)})
+      Some({
+        content: name,
+        strategy: Typ(FromCtx),
+      })
     | _ => None,
     ctx,
   );

src/haz3lcore/assistant/AssistantForms.re

@@ -181,18 +181,29 @@ let suggest_form = (ty_map, delims_of_sort, ci: Info.t): list(Suggestion.t) => {
   | Exp =>
     List.map(
       ((content, ty)) =>
-        Suggestion.{content, strategy: Exp(Common(NewForm(ty)))},
+        Suggestion.{
+          content,
+          strategy: Exp(Common(NewForm(ty))),
+        },
       filtered,
     )
   | Pat =>
     List.map(
       ((content, ty)) =>
-        Suggestion.{content, strategy: Pat(Common(NewForm(ty)))},
+        Suggestion.{
+          content,
+          strategy: Pat(Common(NewForm(ty))),
+        },
       filtered,
     )
   | _ =>
     delims
-    |> List.map(content => Suggestion.{content, strategy: Typ(NewForm)})
+    |> List.map(content =>
+         Suggestion.{
+           content,
+           strategy: Typ(NewForm),
+         }
+       )
   };
 };
 

src/haz3lcore/assistant/TyDi.re

@@ -9,7 +9,10 @@ let suggest_backpack = (z: Zipper.t): list(Suggestion.t) => {
   | [{content, _}, ..._] =>
     switch (content) {
     | [Tile({label, shards: [idx], _})] when Zipper.can_put_down(z) => [
-        {content: List.nth(label, idx), strategy: Any(FromBackpack)},
+        {
+          content: List.nth(label, idx),
+          strategy: Any(FromBackpack),
+        },
       ]
     | _ => []
     }
@@ -52,7 +55,15 @@ let token_to_left = (z: Zipper.t): option(string) =>
 let mk_unparsed_buffer =
     (~sort: Sort.t, sibs: Siblings.t, t: Token.t): Segment.t => {
   let mold = Siblings.mold_fitting_between(sort, Precedence.max, sibs);
-  [Tile({id: Id.mk(), label: [t], shards: [0], children: [], mold})];
+  [
+    Tile({
+      id: Id.mk(),
+      label: [t],
+      shards: [0],
+      children: [],
+      mold,
+    }),
+  ];
 };
 
 /* If 'current' is a proper prefix of 'candidate', return the

src/haz3lcore/dynamics/Builtins.re

@@ -362,9 +362,18 @@ let ctx_init: Ctx.t = {
     });
   List.map(
     fun
-    | (name, Const(typ, _)) => Ctx.VarEntry({name, typ, id: Id.invalid})
+    | (name, Const(typ, _)) =>
+      Ctx.VarEntry({
+        name,
+        typ,
+        id: Id.invalid,
+      })
     | (name, Fn(t1, t2, _)) =>
-      Ctx.VarEntry({name, typ: Arrow(t1, t2) |> Typ.fresh, id: Id.invalid}),
+      Ctx.VarEntry({
+        name,
+        typ: Arrow(t1, t2) |> Typ.fresh,
+        id: Id.invalid,
+      }),
     Pervasives.builtins,
   )
   |> Ctx.extend(_, meta)

src/haz3lcore/dynamics/Casts.re

@@ -187,7 +187,11 @@ 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: DHExp.Cast(d1, t1, t2),
+          copied: p.copied,
+          ids: p.ids,
+        }
         |> transition_multiple,
       );
     | _ => (p, hole)
@@ -198,7 +202,11 @@ 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: DHPat.Cast(p1, t1, t2),
+        copied: d.copied,
+        ids: d.ids,
+      };
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {

src/haz3lcore/dynamics/DHExp.re

@@ -11,17 +11,51 @@ 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};
+  {
+    ids,
+    copied: true,
+    term,
+  };
 };
 
 // TODO: make this function emit a map of changes
 let replace_all_ids =
   map_term(
-    ~f_exp=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_pat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_typ=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_tpat=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
-    ~f_rul=(continue, exp) => {...exp, ids: [Id.mk()]} |> continue,
+    ~f_exp=
+      (continue, exp) =>
+        {
+          ...exp,
+          ids: [Id.mk()],
+        }
+        |> continue,
+    ~f_pat=
+      (continue, exp) =>
+        {
+          ...exp,
+          ids: [Id.mk()],
+        }
+        |> continue,
+    ~f_typ=
+      (continue, exp) =>
+        {
+          ...exp,
+          ids: [Id.mk()],
+        }
+        |> continue,
+    ~f_tpat=
+      (continue, exp) =>
+        {
+          ...exp,
+          ids: [Id.mk()],
+        }
+        |> continue,
+    ~f_rul=
+      (continue, exp) =>
+        {
+          ...exp,
+          ids: [Id.mk()],
+        }
+        |> continue,
   );
 
 // TODO: make this function emit a map of changes

src/haz3lcore/dynamics/Elaborator.re

@@ -393,7 +393,11 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let kind' =
         switch (kind) {
         | Residue(_) => kind
-        | Filter({act, pat}) => Filter({act, pat: elaborate(m, pat) |> fst})
+        | Filter({act, pat}) =>
+          Filter({
+            act,
+            pat: elaborate(m, pat) |> fst,
+          })
         };
       Filter(kind', e') |> rewrap |> cast_from(t);
     | Closure(env, e) =>