Summer UI Refresh (#1343)

src/haz3lcore/TermRanges.re

@@ -8,9 +8,7 @@ let union = union((_, range, _) => Some(range));
 
 /* PERF: Up to 50% reduction in some cases by memoizing
  * this function. Might be better though to just do an
- * unmemoized traversal building a hashtbl avoiding unioning.
-
-   TODO(andrew): Consider setting a limit for the hashtbl size */
+ * unmemoized traversal building a hashtbl avoiding unioning */
 let range_hash: Hashtbl.t(Tile.segment, Id.Map.t(range)) =
   Hashtbl.create(1000);
 

src/haz3lcore/assistant/AssistantForms.re

@@ -47,9 +47,9 @@ module Typ = {
     ("$==", Bool),
     ("==.", Bool),
     ("==", Bool),
-    //("!", Bool), /* annoying as != is more common */
-    ("!=", Bool),
-    ("!=.", Bool),
+    ("!", Bool),
+    //("!=", Bool), /* annoying as != is more common */
+    //("!=.", Bool), /* annoying as != is more common */
     ("<", Bool),
     (">", Bool),
     ("<=", Bool),

src/haz3lcore/lang/Form.re

@@ -65,11 +65,8 @@ let mk_nul_infix = (t: Token.t, prec) =>
 
 /* A. Secondary Notation (Comments, Whitespace, etc.)  */
 let space = " ";
-/* HACK(andrew): Using ⏎ char to represent linebreak to avoid regexp
-   issues with using \n. Someone who understands regexps better
-   should fix this. */
-let linebreak = "⏎";
-let comment_regexp = regexp("^#[^#⏎]*#$"); /* Multiline comments not supported */
+let linebreak = "\n";
+let comment_regexp = regexp("^#[^#\n]*#$"); /* Multiline comments not supported */
 let is_comment = t => match(comment_regexp, t) || t == "#";
 let is_comment_delim = t => t == "#";
 let is_secondary = t =>
@@ -79,7 +76,7 @@ let is_secondary = t =>
 
 /* is_string: last clause is a somewhat hacky way of making sure
    there are at most two quotes, in order to prevent merges */
-let string_regexp = regexp("^\"[^⏎]*\"$");
+let string_regexp = regexp("^\"[^\n]*\"$"); /* Multiline strings not supported */
 let is_string = t =>
   match(string_regexp, t) && List.length(String.split_on_char('"', t)) < 4;
 let string_delim = "\"";
@@ -119,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_'?\"#⏎\\s\\[\\]\\(\\)]+$");
+  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)
@@ -201,7 +198,6 @@ let duomerges = (lbl: Label.t): option(Label.t) =>
   | _ => None
   };
 
-//TODO(andrew): refactor atomic_forms to seperate these out
 let const_mono_delims =
   base_typs @ bools @ [undefined, wild, empty_list, empty_tuple, empty_string];
 

src/haz3lcore/lang/Molds.re

@@ -20,7 +20,6 @@ let forms_assoc: list((Label.t, list(Mold.t))) =
 let get = (label: Label.t): list(Mold.t) =>
   switch (label, List.assoc_opt(label, forms_assoc)) {
   | ([t], Some(molds)) when Form.atomic_molds(t) != [] =>
-    // TODO(andrew): does this make sense?
     Form.atomic_molds(t) @ molds
   | ([t], None) when Form.atomic_molds(t) != [] => Form.atomic_molds(t)
   | (_, Some(molds)) => molds

src/haz3lcore/lang/term/Typ.re

@@ -506,14 +506,14 @@ let rec pretty_print = (ty: t): string =>
   | String => "String"
   | Var(tvar) => tvar
   | List(t) => "[" ++ pretty_print(t) ++ "]"
-  | Arrow(t1, t2) => paren_pretty_print(t1) ++ "->" ++ pretty_print(t2)
+  | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2)
   | Sum(sm) =>
     switch (sm) {
     | [] => "+?"
     | [t0] => "+" ++ ctr_pretty_print(t0)
     | [t0, ...ts] =>
       List.fold_left(
-        (acc, t) => acc ++ "+" ++ ctr_pretty_print(t),
+        (acc, t) => acc ++ " + " ++ ctr_pretty_print(t),
         ctr_pretty_print(t0),
         ts,
       )
@@ -527,9 +527,10 @@ let rec pretty_print = (ty: t): string =>
          ts,
        )
     ++ ")"
-  | Rec(tv, t) => "rec " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+  | Rec(tv, t) =>
+    "rec " ++ pretty_print_tvar(tv) ++ " -> " ++ pretty_print(t)
   | Forall(tv, t) =>
-    "forall " ++ pretty_print_tvar(tv) ++ "->" ++ pretty_print(t)
+    "forall " ++ pretty_print_tvar(tv) ++ " -> " ++ pretty_print(t)
   }
 and ctr_pretty_print =
   fun

src/haz3lcore/statics/Statics.re

@@ -833,7 +833,6 @@ and utyp_to_info_map =
   let ancestors = [UTyp.rep_id(utyp)] @ ancestors;
   let go' = utyp_to_info_map(~ctx, ~ancestors);
   let go = go'(~expects=TypeExpected);
-  //TODO(andrew): make this return free, replacing Typ.free_vars
   switch (term) {
   | Unknown(Hole(MultiHole(tms))) =>
     let (_, m) = multi(~ctx, ~ancestors, m, tms);

src/haz3lcore/tiles/Label.re

@@ -4,13 +4,3 @@ open Util;
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t = list(Token.t);
 exception Empty_label;
-
-let length: t => int = List.length;
-
-let rev: t => t = List.rev;
-
-let hd_tl = (lbl: t): (Token.t, list(Token.t)) =>
-  switch (lbl) {
-  | [] => raise(Empty_label)
-  | [hd, ...tl] => (hd, tl)
-  };

src/haz3lcore/tiles/Mold.re

@@ -66,12 +66,6 @@ let nib_shapes = (~index=?, mold: t): Nibs.shapes => {
   (nib_l.shape, nib_r.shape);
 };
 
-module Map = {
-  type mold = t;
-  include Id.Map;
-  type nonrec t = Id.Map.t(list(mold));
-};
-
 let of_grout: (Grout.t, Sort.t) => t =
   (g, sort) => {
     nibs:
@@ -94,17 +88,6 @@ let of_secondary = (l: Nib.t) => {
   in_: [],
 };
 
-let fits_shape = (d: Direction.t, s: Nib.Shape.t, m: t): bool => {
-  let s' = Direction.choose(d, nib_shapes(m));
-  Nib.Shape.fits(s, s');
-};
-
-let consistent_shapes = (ms: list(t)) =>
-  ms
-  |> List.map(nib_shapes)
-  |> List.split
-  |> TupleUtil.map2(ListUtil.single_elem);
-
 let is_infix_op = (mold: t): bool =>
   switch (mold.nibs, mold.in_) {
   | (({shape: Concave(_), _}, {shape: Concave(_), _}), []) => true

src/haz3lcore/tiles/Nib.re

@@ -1,3 +1,5 @@
+open Util;
+
 module Shape = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type t =
@@ -21,25 +23,26 @@ module Shape = {
     | (Concave(_), Concave(_)) => false
     };
 
-  let fitting =
-    fun
-    | Convex => concave()
-    | Concave(_) => Convex;
-
   let flip =
     fun
     | Convex => concave()
     | Concave(_) => Convex;
 
-  let absolute = (d: Util.Direction.t, s: t): Util.Direction.t =>
+  let absolute = (d: Direction.t, s: t): Direction.t =>
     /* The direction an s-shaped nib on the d-hand side is facing */
     switch (s) {
     | Convex => d
-    | Concave(_) => Util.Direction.toggle(d)
+    | Concave(_) => Direction.toggle(d)
     };
 
-  let relative = (nib: Util.Direction.t, side: Util.Direction.t): t =>
+  let relative = (nib: Direction.t, side: Direction.t): t =>
     nib == side ? Convex : concave();
+
+  let direction_of = (d: Direction.t, shape: t): Direction.t =>
+    switch (shape) {
+    | Convex => d
+    | Concave(_) => Direction.toggle(d)
+    };
 };
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -50,21 +53,4 @@ type t = {
 
 let shape = n => n.shape;
 
-let fits = (l: t, r: t): bool =>
-  l.sort == r.sort && Shape.fits(l.shape, r.shape);
-
-let fitting = (nib: t): t => {...nib, shape: Shape.fitting(nib.shape)};
-
 let flip = (nib: t) => {...nib, shape: Shape.flip(nib.shape)};
-
-// let toggle = (nib: t) => {
-//   ...nib,
-//   orientation: Direction.toggle(nib.orientation),
-// };
-
-// let sort_consistent = (nib: t, nib': t) => nib.sort == nib'.sort;
-
-// let of_sort = sort => [
-//   {sort, orientation: Left},
-//   {sort, orientation: Right},
-// ];

src/haz3lcore/tiles/Nibs.re

@@ -5,7 +5,3 @@ type t = (Nib.t, Nib.t);
 type shapes = (Nib.Shape.t, Nib.Shape.t);
 
 let flip = ((l, r): t) => (r, l);
-
-let of_hole = sort => Nib.({sort, shape: Convex}, {sort, shape: Convex});
-
-let fitting = ((l, r): t) => (Nib.fitting(l), Nib.fitting(r));

src/haz3lcore/tiles/Piece.re

@@ -1,4 +1,3 @@
-// open Util;
 include Base;
 
 [@deriving (show({with_path: false}), sexp, yojson)]
@@ -53,14 +52,6 @@ let nib_sorts =
   );
 
 let sorted_children = get(_ => [], _ => [], Tile.sorted_children, _ => []);
-let children = p => sorted_children(p) |> List.split |> snd;
-
-// let is_balanced =
-//   fun
-//   | Shard(_) => false
-//   | Secondary(_)
-//   | Grout(_)
-//   | Tile(_) => true;
 
 let pop_l = (p: t): (t, segment) =>
   switch (p) {
@@ -85,13 +76,6 @@ let disassemble = (p: t): segment =>
   | Tile(t) => Tile.disassemble(t)
   };
 
-// let remold = (p: t) =>
-//   switch (p) {
-//   | Grout(_)
-//   | Secondary(_) => [p]
-//   | Tile(t) => List.map(tile, Tile.remold(t))
-//   };
-
 let shapes =
   get(
     _ => None,
@@ -138,22 +122,11 @@ let monotile: t => option(Token.t) =
     Some(Secondary.get_string(w.content))
   | _ => None;
 
-let has_ends = get(_ => true, _ => true, Tile.has_ends);
-
 let is_complete: t => bool =
   fun
   | Tile(t) => Tile.is_complete(t)
   | _ => true;
 
-let mold_of = (~shape=Nib.Shape.Convex, p: t) =>
-  // TODO(d) fix sorts
-  switch (p) {
-  | Tile(t) => t.mold
-  | Grout(g) => Mold.of_grout(g, Any)
-  | Secondary(_) => Mold.of_secondary({sort: Any, shape})
-  | Projector(p) => ProjectorBase.mold_of(p, Any)
-  };
-
 let replace_id = (id: Id.t, p: t): t =>
   switch (p) {
   | Tile(t) => Tile({...t, id})
@@ -180,3 +153,36 @@ let of_mono = (syntax: t): option(string) =>
   | Tile({label: [l], _}) => Some(l)
   | _ => None
   };
+
+let is_case_or_rule = (p: t) =>
+  switch (p) {
+  | Tile({label: ["case", "end"], _}) => true
+  | Tile({label: ["|", "=>"], _}) => true
+  | _ => false
+  };
+let is_not_case_or_rule_or_space = (p: t) =>
+  switch (p) {
+  | Tile({label: ["case", "end"], _}) => false
+  | Tile({label: ["|", "=>"], _}) => false
+  | Secondary(_) => false
+  | _ => true
+  };
+let not_comment_or_space = (p: t) =>
+  switch (p) {
+  | Secondary(s) => Secondary.is_linebreak(s)
+  | _ => true
+  };
+
+let is_term = (p: t) =>
+  switch (p) {
+  | Grout(_)
+  | Projector(_)
+  | Tile({
+      label: [_],
+      mold: {nibs: ({shape: Convex, _}, {shape: Convex, _}), _},
+      _,
+    }) =>
+    true
+  | Secondary(_) => false // debatable
+  | _ => false
+  };