Start working on a reparse that preserves whitespace

dune-project

@@ -40,6 +40,7 @@
   unionFind
   ocamlformat
   (junit_alcotest :with-test)
-  ocaml-lsp-server)) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
+  ocaml-lsp-server
+  uuseg)) ; After upgrading to opam 2.2 use with-dev https://opam.ocaml.org/blog/opam-2-2-0/
 
 ; See the complete stanza docs at https://dune.readthedocs.io/en/stable/reference/dune-project/index.html

src/haz3lcore/Unicode.re

@@ -15,22 +15,5 @@ let ellipsis = "\xE2\x80\xA6";
 // copied from hazel
 // NOTE: 30% faster than Camomile
 let length = (s: string): int => {
-  let stop = String.length(s);
-  let rec distance_aux = (start: int, count: int) =>
-    if (start + count >= stop) {
-      stop - count;
-    } else {
-      let n = Char.code(String.unsafe_get(s, start + count));
-      if (n < 0x80) {
-        distance_aux(start + 1, count);
-      } else if (n < 0xe0) {
-        distance_aux(start + 1, count + 1);
-      } else if (n < 0xf0) {
-        distance_aux(start + 1, count + 2);
-      } else {
-        distance_aux(start + 1, count + 3);
-      };
-    };
-
-  distance_aux(0, 0);
+  Util.(StringUtil.length(s));
 };

src/haz3lcore/assistant/AssistantExpander.re

@@ -4,7 +4,7 @@
  * inserted into the syntax so will not be reflected
  * in the decoration metrics */
 
-let last = t => String.sub(t, String.length(t) - 1, 1);
+let last = t => String.sub(t, Util.StringUtil.length(t) - 1, 1);
 
 let is_expander = (label: Label.t) =>
   switch (label) {

src/haz3lcore/assistant/TyDi.re

@@ -1,6 +1,6 @@
 open Util.OptUtil.Syntax;
 open Suggestion;
-
+open Util;
 /* Suggest the token at the top of the backpack, if we can put it down */
 let suggest_backpack = (z: Zipper.t): list(Suggestion.t) => {
   /* Note: Sort check unnecessary here as wouldn't be able to put down */
@@ -61,8 +61,8 @@ let suffix_of = (candidate: Token.t, current: Token.t): option(Token.t) => {
   let candidate_suffix =
     String.sub(
       candidate,
-      String.length(current),
-      String.length(candidate) - String.length(current),
+      StringUtil.length(current),
+      StringUtil.length(candidate) - StringUtil.length(current),
     );
   candidate_suffix == "" ? None : Some(candidate_suffix);
 };

src/haz3lcore/dynamics/Builtins.re

@@ -1,4 +1,5 @@
 open DHExp;
+open Util;
 
 /*
    Built-in functions for Hazel.
@@ -221,7 +222,7 @@ module Pervasives = {
     let string_length =
       unary(d =>
         switch (term_of(d)) {
-        | String(s) => Ok(Int(String.length(s)) |> fresh)
+        | String(s) => Ok(Int(StringUtil.length(s)) |> fresh)
         | _ => Error(InvalidBoxedStringLit(d))
         }
       );

src/haz3lcore/lang/Form.re

@@ -83,13 +83,13 @@ let string_delim = "\"";
 let empty_string = string_delim ++ string_delim;
 let is_string_delim = (==)(string_delim);
 let strip_quotes = s =>
-  if (String.length(s) < 2) {
+  if (StringUtil.length(s) < 2) {
     s;
   } else if (String.sub(s, 0, 1) != "\""
-             || String.sub(s, String.length(s) - 1, 1) != "\"") {
+             || String.sub(s, StringUtil.length(s) - 1, 1) != "\"") {
     s;
   } else {
-    String.sub(s, 1, String.length(s) - 2);
+    String.sub(s, 1, StringUtil.length(s) - 2);
   };
 let string_quote = s => "\"" ++ s ++ "\"";
 
@@ -116,7 +116,7 @@ let is_potential_operand = match(regexp("^[a-zA-Z0-9_'\\.?]+$"));
  *  delimiters, string delimiters, or the instant expanding paired
  *  delimiters: ()[]| */
 let potential_operator_regexp =
-  regexp("^[^a-zA-Z0-9_'?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
+  regexp("^[^a-zA-Z0-9_'¿?\"#\n\\s\\[\\]\\(\\)]+$"); /* Multiline operators not supported */
 let is_potential_operator = match(potential_operator_regexp);
 let is_potential_token = t =>
   is_potential_operand(t)
@@ -202,7 +202,11 @@ let const_mono_delims =
   base_typs @ bools @ [undefined, wild, empty_list, empty_tuple, empty_string];
 
 let explicit_hole = "?";
+let implicit_hole = "¿";
 let is_explicit_hole = t => t == explicit_hole;
+let is_implicit_hole = t => {
+  t == implicit_hole;
+};
 let bad_token_cls: string => bad_token_cls =
   t =>
     switch () {
@@ -222,6 +226,13 @@ let atomic_forms: list((string, (string => bool, list(Mold.t)))) = [
       [mk_op(Exp, []), mk_op(Pat, []), mk_op(Typ, []), mk_op(TPat, [])],
     ),
   ),
+  (
+    "implicit_hole",
+    (
+      is_implicit_hole,
+      [mk_op(Exp, []), mk_op(Pat, []), mk_op(Typ, []), mk_op(TPat, [])],
+    ),
+  ),
   ("wild", (is_wild, [mk_op(Pat, [])])),
   ("string", (is_string, [mk_op(Exp, []), mk_op(Pat, [])])),
   ("int_lit", (is_int, [mk_op(Exp, []), mk_op(Pat, [])])),

src/haz3lcore/statics/MakeTerm.re

@@ -202,7 +202,10 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           Match(scrut, rules),
           ids,
         )
-      | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
+      | ([t], [])
+          when
+            t != " "
+            && !(Form.is_explicit_hole(t) || Form.is_implicit_hole(t)) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
       }
@@ -345,7 +348,10 @@ and pat_term: unsorted => (UPat.term, list(Id.t)) = {
         | ([t], []) when Form.is_wild(t) => Wild
         | ([t], []) when Form.is_ctr(t) =>
           Constructor(t, Unknown(Internal) |> Typ.fresh)
-        | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
+        | ([t], [])
+            when
+              t != " "
+              && !(Form.is_explicit_hole(t) || Form.is_implicit_hole(t)) =>
           Invalid(t)
         | (["(", ")"], [Pat(body)]) => Parens(body)
         | (["[", "]"], [Pat(body)]) =>
@@ -409,7 +415,10 @@ and typ_term: unsorted => (UTyp.term, list(Id.t)) = {
         | ([t], []) when Form.is_typ_var(t) => Var(t)
         | (["(", ")"], [Typ(body)]) => Parens(body)
         | (["[", "]"], [Typ(body)]) => List(body)
-        | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
+        | ([t], [])
+            when
+              t != " "
+              && !(Form.is_explicit_hole(t) || Form.is_implicit_hole(t)) =>
           Unknown(Hole(Invalid(t)))
         | _ => hole(tm)
         },
@@ -477,7 +486,10 @@ and tpat_term: unsorted => TPat.term = {
       ret(
         switch (tile) {
         | ([t], []) when Form.is_typ_var(t) => Var(t)
-        | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
+        | ([t], [])
+            when
+              t != " "
+              && !(Form.is_explicit_hole(t) || Form.is_implicit_hole(t)) =>
           Invalid(t)
         | _ => hole(tm)
         },

src/haz3lcore/statics/Var.re

@@ -5,7 +5,7 @@ type t = string;
 
 let eq = String.equal;
 
-let length = String.length;
+let length = StringUtil.length;
 
 let is_true = eq("true");
 
@@ -21,7 +21,7 @@ let is_wild = eq("_");
 
 let split = (pos, name) => {
   let left_var = String.sub(name, 0, pos);
-  let right_var = String.sub(name, pos, String.length(name) - pos);
+  let right_var = String.sub(name, pos, StringUtil.length(name) - pos);
   (left_var, right_var);
 };
 

src/haz3lcore/tiles/Token.re

@@ -8,7 +8,7 @@ module Index = {
   type t = int;
 };
 
-let length = String.length;
+let length = StringUtil.length;
 let compare = String.compare;
 let rm_nth = Util.StringUtil.remove_nth;
 let rm_last = Util.StringUtil.remove_last;

src/haz3lcore/zipper/Printer.re

@@ -45,7 +45,7 @@ let to_rows =
   switch (caret) {
   | Some({row, col}) =>
     switch (ListUtil.split_nth_opt(row, rows)) {
-    | Some((pre, caret_row, suf)) when col < String.length(caret_row) =>
+    | Some((pre, caret_row, suf)) when col < StringUtil.length(caret_row) =>
       pre @ [StringUtil.insert_nth(col, caret_str, caret_row)] @ suf
     | Some((pre, caret_row, suf)) => pre @ [caret_row ++ caret_str] @ suf
     | _ => rows
@@ -78,12 +78,12 @@ let zipper_to_string =
   )
   |> String.concat("\n");
 
-let to_string_selection = (editor: Editor.t): string =>
+let to_string_selection = (~holes=?, editor: Editor.t): string =>
   to_rows(
     ~measured=measured(editor.state.zipper),
     ~caret=None,
     ~indent=" ",
-    ~holes=None,
+    ~holes,
     ~segment=editor.state.zipper.selection.content,
   )
   |> String.concat("\n");
@@ -104,5 +104,6 @@ let zipper_of_string =
 /* This serializes the current editor to text, resets the current
    editor, and then deserializes. It is intended as a (tactical)
    nuclear option for weird backpack states */
-let reparse = z =>
-  zipper_of_string(~zipper_init=Zipper.init(), zipper_to_string(z));
+let reparse = (~holes=?, z) => {
+  zipper_of_string(~zipper_init=Zipper.init(), zipper_to_string(~holes, z));
+};

src/haz3lcore/zipper/action/Action.re

@@ -84,7 +84,9 @@ type t =
   | RotateBackpack
   | MoveToBackpackTarget(planar)
   | Pick_up
-  | Put_down;
+  | Put_down
+  | RemoveAllImplicitHoles
+  | ReparseToExplicitGrout;
 
 module Failure = {
   [@deriving (show({with_path: false}), sexp, yojson)]
@@ -114,6 +116,8 @@ let is_edit: t => bool =
   | Destruct(_)
   | Pick_up
   | Put_down
+  | RemoveAllImplicitHoles
+  | ReparseToExplicitGrout
   | Buffer(Accept | Clear | Set(_)) => true
   | Copy
   | Move(_)
@@ -151,6 +155,8 @@ let is_historic: t => bool =
   | Insert(_)
   | Destruct(_)
   | Pick_up
+  | ReparseToExplicitGrout
+  | RemoveAllImplicitHoles
   | Put_down => true
   | Project(p) =>
     switch (p) {
@@ -179,7 +185,9 @@ let prevent_in_read_only_editor = (a: t) => {
   | Pick_up
   | Put_down
   | RotateBackpack
-  | MoveToBackpackTarget(_) => true
+  | MoveToBackpackTarget(_)
+  | RemoveAllImplicitHoles
+  | ReparseToExplicitGrout => true
   | Project(p) =>
     switch (p) {
     | SetSyntax(_) => true

src/haz3lcore/zipper/action/Move.re

@@ -428,4 +428,28 @@ module Make = (M: Editor.Meta.S) => {
       go(Local(Left(ByToken))),
       Piece.not_comment_or_space,
     );
+
+  // TODO Move to a different file
+  let remove_if_implicit_hole = z => {
+    switch (Indicated.piece'(~no_ws=false, ~ign=_ => false, z)) {
+    | Some((Tile({label: l, _}), Left, _)) when l == ["¿"] =>
+      Destruct.go(Left, z) |> Option.map(remold_regrout(Left))
+    | _ => Some(z)
+    };
+  };
+
+  let rec move_right_and_perform = (f, z) =>
+    switch (f(z)) {
+    | Some(z) =>
+      switch (primary(ByToken, Right, z)) {
+      | Some(z) => move_right_and_perform(f, z)
+      | None => Some(z)
+      }
+    | None => Some(z)
+    };
+
+  let remove_all_implicit_holes = z => {
+    go(Goal(Point(Point.zero)), z)
+    |> Option.bind(_, move_right_and_perform(remove_if_implicit_hole));
+  };
 };

src/haz3lcore/zipper/action/Perform.re

@@ -201,6 +201,14 @@ let go_z =
   | RotateBackpack =>
     let z = {...z, backpack: Util.ListUtil.rotate(z.backpack)};
     Ok(z);
+  | RemoveAllImplicitHoles =>
+    Move.remove_all_implicit_holes(z)
+    |> Result.of_option(~error=Action.Failure.Cant_move)
+  | ReparseToExplicitGrout =>
+    switch (Printer.reparse(~holes="¿", z)) {
+    | None => Error(CantReparse)
+    | Some(z) => Ok(z)
+    }
   | MoveToBackpackTarget((Left(_) | Right(_)) as d) =>
     if (Backpack.restricted(z.backpack)) {
       Move.to_backpack_target(d, z)

src/haz3lcore/zipper/projectors/InfoProj.re

@@ -1,7 +1,7 @@
 open Virtual_dom.Vdom;
 open Node;
 open ProjectorBase;
-
+open Util;
 let mode = (info: option(Info.t)): option(Mode.t) =>
   switch (info) {
   | Some(InfoExp({mode, _}))
@@ -68,7 +68,7 @@ module M: Projector = {
     display_ty(model, info) |> totalize_ty |> Typ.pretty_print;
 
   let placeholder = (model, info) =>
-    Inline((display(model, info.ci) |> String.length) + 5);
+    Inline((display(model, info.ci) |> StringUtil.length) + 5);
 
   let update = (model, a: action) =>
     switch (a, model) {

src/haz3lweb/Benchmark.re

@@ -42,7 +42,7 @@ let non_empty_hole : Int = true in
 
 let str_to_inserts = (str: string): list(UpdateAction.t) =>
   List.init(
-    String.length(str),
+    StringUtil.length(str),
     i => {
       let c = String.sub(str, i, 1);
       UpdateAction.PerformAction(Insert(c));

src/haz3lweb/Keyboard.re

@@ -217,6 +217,16 @@ let shortcuts = (sys: Key.sys): list(shortcut) =>
       "Reparse Current Editor",
       PerformAction(Reparse),
     ),
+    mk_shortcut(
+      ~section="Diagnostics",
+      "Reparse with explicit empty grout",
+      PerformAction(ReparseToExplicitGrout),
+    ),
+    mk_shortcut(
+      ~section="Diagnostics",
+      "Restore implicit holes",
+      PerformAction(RemoveAllImplicitHoles),
+    ),
     mk_shortcut(
       ~mdIcon="timer",
       ~section="Diagnostics",
@@ -266,7 +276,7 @@ let handle_key_event = (k: Key.t): option(UpdateAction.t) => {
     | (Down, "Home") => now(Select(Resize(Extreme(Left(ByToken)))))
     | (Down, "End") => now(Select(Resize(Extreme(Right(ByToken)))))
     | (_, "Enter") => now(Insert(Form.linebreak))
-    | _ when String.length(key) == 1 =>
+    | _ when StringUtil.length(key) == 1 =>
       /* Note: length==1 prevent specials like
        * SHIFT from being captured here */
       now(Insert(key))

src/haz3lweb/UpdateAction.re

@@ -255,6 +255,8 @@ let should_scroll_to_caret =
     | Paste(_)
     | Copy
     | Cut
+    | RemoveAllImplicitHoles
+    | ReparseToExplicitGrout
     | Reparse => true
     | Project(_)
     | Unselect(_)