Delete the Nul sort (#1480)

src/haz3lcore/lang/Sort.re

@@ -1,30 +1,34 @@
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t =
   | Any
-  | Nul
   | Pat
   | Typ
   | TPat
   | Rul
   | Exp;
 
+type gadt('a) =
+  | AnySort: gadt(TermBase.Any.t)
+  | PatSort: gadt(TermBase.Pat.t)
+  | TypSort: gadt(TermBase.Typ.t)
+  | TPatSort: gadt(TermBase.TPat.t)
+  | RulSort: gadt(TermBase.Rul.t)
+  | ExpSort: gadt(TermBase.Exp.t);
+
 let root = Exp;
 
-let all = [Any, Nul, Pat, Typ, Rul, Exp, TPat];
+let all = [Any, Pat, Typ, Rul, Exp, TPat];
 
 let consistent = (s, s') =>
   switch (s, s') {
   | (Any, _)
   | (_, Any) => true
-  | (Nul, _)
-  | (_, Nul) => false
   | _ => s == s'
   };
 
 let to_string =
   fun
   | Any => "Any"
-  | Nul => "Nul"
   | Pat => "Pat"
   | TPat => "TPat"
   | Typ => "Typ"
@@ -34,7 +38,6 @@ let to_string =
 let to_string_verbose =
   fun
   | Any => "any"
-  | Nul => "null"
   | Pat => "pattern"
   | TPat => "type pattern"
   | Typ => "type"

src/haz3lcore/pretty/ExpToSegment.re

@@ -672,7 +672,6 @@ and any_to_pretty = (~settings: Settings.t, any: Any.t): pretty => {
   | Typ(t) => typ_to_pretty(~settings: Settings.t, t)
   | TPat(tp) => tpat_to_pretty(~settings: Settings.t, tp)
   | Any(_)
-  | Nul(_)
   | Rul(_) =>
     //TODO: print out invalid rules properly
     let id = any |> Any.rep_id;
@@ -1182,7 +1181,6 @@ and parenthesize_any = (~show_filters: bool, any: Any.t): Any.t =>
   | TPat(tp) => TPat(parenthesize_tpat(~show_filters, tp))
   | Rul(r) => Rul(parenthesize_rul(~show_filters, r))
   | Any(_) => any
-  | Nul(_) => any
   };
 
 let exp_to_segment = (~settings: Settings.t, exp: Exp.t): Segment.t => {

src/haz3lcore/statics/MakeTerm.re

@@ -146,7 +146,6 @@ let rec go_s = (s: Sort.t, skel: Skel.t, seg: Segment.t): Term.Any.t =>
   | Typ => Typ(typ(unsorted(skel, seg)))
   | Exp => Exp(exp(unsorted(skel, seg)))
   | Rul => Rul(rul(unsorted(skel, seg)))
-  | Nul => Nul() //TODO
   | Any =>
     let tm = unsorted(skel, seg);
     let ids = ids(tm);

src/haz3lcore/statics/Statics.re

@@ -154,7 +154,6 @@ let rec any_to_info_map =
       utyp_to_info_map(~ctx, ~ancestors, ty, m) |> snd,
     )
   | Rul(_)
-  | Nul ()
   | Any () => (CoCtx.empty, m)
   }
 and multi = (~ctx, ~ancestors, m, tms) =>

src/haz3lcore/statics/Term.re

@@ -819,7 +819,6 @@ module Any = {
     | Typ(tm) => tm.ids
     | TPat(tm) => tm.ids
     | Rul(tm) => Rul.ids(~any_ids=ids, tm)
-    | Nul ()
     | Any () => [];
 
   // Terms may consist of multiple tiles, eg the commas in an n-tuple,
@@ -840,6 +839,5 @@ module Any = {
     | Typ(tm) => Typ.rep_id(tm)
     | TPat(tm) => TPat.rep_id(tm)
     | Rul(tm) => Rul.rep_id(~any_ids=ids, tm)
-    | Nul ()
     | Any () => raise(Invalid_argument("Term.rep_id"));
 };

src/haz3lcore/statics/TermBase.re

@@ -53,7 +53,6 @@ type any_t =
   | Typ(typ_t)
   | TPat(tpat_t)
   | Rul(rul_t)
-  | Nul(unit)
   | Any(unit)
 and exp_term =
   | Invalid(string)
@@ -209,7 +208,6 @@ module rec Any: {
         )
       | Rul(x) =>
         Rul(Rul.map_term(~f_exp, ~f_pat, ~f_typ, ~f_tpat, ~f_rul, ~f_any, x))
-      | Nul () => Nul()
       | Any () => Any()
       };
     x |> f_any(rec_call);
@@ -222,14 +220,12 @@ module rec Any: {
     | (Typ(x), Typ(y)) => Typ.fast_equal(x, y)
     | (TPat(x), TPat(y)) => TPat.fast_equal(x, y)
     | (Rul(x), Rul(y)) => Rul.fast_equal(x, y)
-    | (Nul (), Nul ()) => true
     | (Any (), Any ()) => true
     | (Exp(_), _)
     | (Pat(_), _)
     | (Typ(_), _)
     | (TPat(_), _)
     | (Rul(_), _)
-    | (Nul (), _)
     | (Any (), _) => false
     };
 }

src/haz3lcore/tiles/Segment.re

@@ -84,7 +84,6 @@ let rec remold = (~shape=Nib.Shape.concave(), seg: t, s: Sort.t) =>
   | Exp => remold_exp(shape, seg)
   | Rul => remold_rul(shape, seg)
   | TPat => remold_tpat(shape, seg)
-  | _ => failwith("remold unexpected")
   }
 and remold_tile = (s: Sort.t, shape, t: Tile.t): option(Tile.t) => {
   open OptUtil.Syntax;

src/haz3lcore/zipper/Editor.re

@@ -8,8 +8,7 @@ module CachedSyntax = {
     tiles: TileMap.t,
     holes: list(Grout.t),
     selection_ids: list(Id.t),
-    term: Exp.t,
-    /* This term, and the term-derived data structured below, may differ
+    /* The term-derived data structured below, may differ
      * from the term used for semantics. These terms are identical when
      * the backpack is empty. If the backpack is non-empty, then when we
      * make the term for semantics, we attempt to empty the backpack
@@ -35,7 +34,7 @@ module CachedSyntax = {
 
   let init = (z, info_map): t => {
     let segment = Zipper.unselect_and_zip(z);
-    let MakeTerm.{term, terms, projectors} = MakeTerm.go(segment);
+    let MakeTerm.{term: _, terms, projectors} = MakeTerm.go(segment);
     {
       old: false,
       segment,
@@ -44,7 +43,6 @@ module CachedSyntax = {
       holes: Segment.holes(segment),
       measured: Measured.of_segment(segment, info_map),
       selection_ids: Selection.selection_ids(z.selection),
-      term,
       terms,
       projectors,
     };