Make the data constructors in termbase distinct

src/haz3lcore/assistant/AssistantForms.re

@@ -27,7 +27,7 @@ module Typ = {
     ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Forall(VarTPat("") |> TPat.fresh, unk) |> Typ.fresh,
     ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),

src/haz3lcore/dynamics/Builtins.re

@@ -41,13 +41,13 @@ let fn =
 module Pervasives = {
   module Impls = {
     /* constants */
-    let infinity = Float(Float.infinity) |> fresh;
-    let neg_infinity = Float(Float.neg_infinity) |> fresh;
-    let nan = Float(Float.nan) |> fresh;
-    let epsilon_float = Float(epsilon_float) |> fresh;
-    let pi = Float(Float.pi) |> fresh;
-    let max_int = Int(Int.max_int) |> fresh;
-    let min_int = Int(Int.min_int) |> fresh;
+    let infinity = FloatLit(Float.infinity) |> fresh;
+    let neg_infinity = FloatLit(Float.neg_infinity) |> fresh;
+    let nan = FloatLit(Float.nan) |> fresh;
+    let epsilon_float = FloatLit(epsilon_float) |> fresh;
+    let pi = FloatLit(Float.pi) |> fresh;
+    let max_int = IntLit(Int.max_int) |> fresh;
+    let min_int = IntLit(Int.min_int) |> fresh;
 
     let unary = (f: DHExp.t => result, d: DHExp.t) => {
       switch (f(d)) {
@@ -81,79 +81,79 @@ module Pervasives = {
     let is_finite =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_finite(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_finite(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
 
     let is_infinite =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_infinite(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_infinite(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
 
     let is_nan =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Bool(Float.is_nan(f))))
+        | FloatLit(f) => Ok(fresh(BoolLit(Float.is_nan(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
 
     let string_of_int =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(String(string_of_int(n))))
+        | IntLit(n) => Ok(fresh(StringLit(string_of_int(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
 
     let string_of_float =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(String(string_of_float(f))))
+        | FloatLit(f) => Ok(fresh(StringLit(string_of_float(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
 
     let string_of_bool =
       unary(d =>
         switch (term_of(d)) {
-        | Bool(b) => Ok(fresh(String(string_of_bool(b))))
+        | BoolLit(b) => Ok(fresh(StringLit(string_of_bool(b))))
         | _ => Error(InvalidBoxedBoolLit(d))
         }
       );
 
     let int_of_float =
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Int(int_of_float(f))))
+        | FloatLit(f) => Ok(fresh(IntLit(int_of_float(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
 
     let float_of_int =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(Float(float_of_int(n))))
+        | IntLit(n) => Ok(fresh(FloatLit(float_of_int(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
 
     let abs =
       unary(d =>
         switch (term_of(d)) {
-        | Int(n) => Ok(fresh(Int(abs(n))))
+        | IntLit(n) => Ok(fresh(IntLit(abs(n))))
         | _ => Error(InvalidBoxedIntLit(d))
         }
       );
 
     let float_op = fn =>
       unary(d =>
         switch (term_of(d)) {
-        | Float(f) => Ok(fresh(Float(fn(f))))
+        | FloatLit(f) => Ok(fresh(FloatLit(fn(f))))
         | _ => Error(InvalidBoxedFloatLit(d))
         }
       );
@@ -176,7 +176,7 @@ module Pervasives = {
         (convert: string => option('a), wrap: 'a => DHExp.t, name: string) =>
       unary(d =>
         switch (term_of(d)) {
-        | String(s) =>
+        | StringLit(s) =>
           switch (convert(s)) {
           | Some(n) => Ok(wrap(n))
           | None =>
@@ -190,17 +190,17 @@ module Pervasives = {
       );
 
     let int_of_string =
-      of_string(int_of_string_opt, n => Int(n) |> DHExp.fresh);
+      of_string(int_of_string_opt, n => IntLit(n) |> DHExp.fresh);
     let float_of_string =
-      of_string(float_of_string_opt, f => Float(f) |> DHExp.fresh);
+      of_string(float_of_string_opt, f => FloatLit(f) |> DHExp.fresh);
     let bool_of_string =
-      of_string(bool_of_string_opt, b => Bool(b) |> DHExp.fresh);
+      of_string(bool_of_string_opt, b => BoolLit(b) |> DHExp.fresh);
 
     let int_mod = (name, d1) =>
       binary(
         (d1, d2) =>
           switch (term_of(d1), term_of(d2)) {
-          | (Int(_), Int(0)) =>
+          | (IntLit(_), IntLit(0)) =>
             Ok(
               fresh(
                 DynamicErrorHole(
@@ -209,8 +209,8 @@ module Pervasives = {
                 ),
               ),
             )
-          | (Int(n), Int(m)) => Ok(Int(n mod m) |> fresh)
-          | (Int(_), _) =>
+          | (IntLit(n), IntLit(m)) => Ok(IntLit(n mod m) |> fresh)
+          | (IntLit(_), _) =>
             raise(EvaluatorError.Exception(InvalidBoxedIntLit(d2)))
           | (_, _) =>
             raise(EvaluatorError.Exception(InvalidBoxedIntLit(d1)))
@@ -221,60 +221,60 @@ module Pervasives = {
     let string_length =
       unary(d =>
         switch (term_of(d)) {
-        | String(s) => Ok(Int(String.length(s)) |> fresh)
+        | StringLit(s) => Ok(IntLit(String.length(s)) |> fresh)
         | _ => Error(InvalidBoxedStringLit(d))
         }
       );
 
     let string_compare =
       binary((d1, d2) =>
         switch (term_of(d1), term_of(d2)) {
-        | (String(s1), String(s2)) =>
-          Ok(Int(String.compare(s1, s2)) |> fresh)
-        | (String(_), _) => Error(InvalidBoxedStringLit(d2))
+        | (StringLit(s1), StringLit(s2)) =>
+          Ok(IntLit(String.compare(s1, s2)) |> fresh)
+        | (StringLit(_), _) => Error(InvalidBoxedStringLit(d2))
         | (_, _) => Error(InvalidBoxedStringLit(d1))
         }
       );
 
     let string_trim =
       unary(d =>
         switch (term_of(d)) {
-        | String(s) => Ok(String(String.trim(s)) |> fresh)
+        | StringLit(s) => Ok(StringLit(String.trim(s)) |> fresh)
         | _ => Error(InvalidBoxedStringLit(d))
         }
       );
 
     let string_of: DHExp.t => option(string) =
       d =>
         switch (term_of(d)) {
-        | String(s) => Some(s)
+        | StringLit(s) => Some(s)
         | _ => None
         };
 
     let string_concat =
       binary((d1, d2) =>
         switch (term_of(d1), term_of(d2)) {
-        | (String(s1), ListLit(xs)) =>
+        | (StringLit(s1), ListLit(xs)) =>
           switch (xs |> List.map(string_of) |> Util.OptUtil.sequence) {
           | None => Error(InvalidBoxedStringLit(List.hd(xs)))
-          | Some(xs) => Ok(String(String.concat(s1, xs)) |> fresh)
+          | Some(xs) => Ok(StringLit(String.concat(s1, xs)) |> fresh)
           }
-        | (String(_), _) => Error(InvalidBoxedListLit(d2))
+        | (StringLit(_), _) => Error(InvalidBoxedListLit(d2))
         | (_, _) => Error(InvalidBoxedStringLit(d1))
         }
       );
 
     let string_sub = _ =>
       ternary((d1, d2, d3) =>
         switch (term_of(d1), term_of(d2), term_of(d3)) {
-        | (String(s), Int(idx), Int(len)) =>
-          try(Ok(String(String.sub(s, idx, len)) |> fresh)) {
+        | (StringLit(s), IntLit(idx), IntLit(len)) =>
+          try(Ok(StringLit(String.sub(s, idx, len)) |> fresh)) {
           | _ =>
             // TODO: make it clear that the problem could be with d3 too
             Ok(DynamicErrorHole(d2, IndexOutOfBounds) |> fresh)
           }
-        | (String(_), Int(_), _) => Error(InvalidBoxedIntLit(d3))
-        | (String(_), _, _) => Error(InvalidBoxedIntLit(d2))
+        | (StringLit(_), IntLit(_), _) => Error(InvalidBoxedIntLit(d3))
+        | (StringLit(_), _, _) => Error(InvalidBoxedIntLit(d2))
         | (_, _, _) => Error(InvalidBoxedIntLit(d1))
         }
       );

src/haz3lcore/dynamics/Casts.re

@@ -34,7 +34,7 @@ let grounded_Arrow =
   );
 let grounded_Forall =
   NotGroundOrHole(
-    Forall(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp)
+    Forall(EmptyHoleTPat |> TPat.fresh, Unknown(Internal) |> Typ.temp)
     |> Typ.temp,
   );
 let grounded_Prod = length =>
@@ -58,12 +58,12 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
-  | Var(_)
+  | TypVar(_)
   | Rec(_)
   | Forall(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
-  | Parens(ty) => ground_cases_of(ty)
+  | TypParens(ty) => ground_cases_of(ty)
   | Prod(tys) =>
     if (List.for_all(
           fun
@@ -81,7 +81,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Arrow(_, _) => grounded_Arrow
   | Forall(_) => grounded_Forall
   | List(_) => grounded_List
-  | Ap(_) => failwith("type application in dynamics")
+  | ApTyp(_) => failwith("type application in dynamics")
   };
 };
 
@@ -183,7 +183,7 @@ let hole = EmptyHole |> DHExp.fresh;
 let pattern_fixup = (p: DHPat.t): DHPat.t => {
   let rec unwrap_casts = (p: DHPat.t): (DHPat.t, DHExp.t) => {
     switch (DHPat.term_of(p)) {
-    | Cast(p1, t1, t2) =>
+    | CastPat(p1, t1, t2) =>
       let (p1, d1) = unwrap_casts(p1);
       (
         p1,
@@ -198,13 +198,13 @@ 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: CastPat(p1, t1, t2), copied: d.copied, ids: d.ids};
     | FailedCast(d1, t1, t2) =>
       let p1 = rewrap_casts((p, d1));
       {
         term:
-          Cast(
-            Cast(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
+          CastPat(
+            CastPat(p1, t1, Typ.fresh(Unknown(Internal))) |> DHPat.fresh,
             Typ.fresh(Unknown(Internal)),
             t2,
           ),

src/haz3lcore/dynamics/DHExp.re

@@ -67,10 +67,10 @@ let rec strip_casts =
         | EmptyHole
         | Invalid(_)
         | Var(_)
-        | Bool(_)
-        | Int(_)
-        | Float(_)
-        | String(_)
+        | BoolLit(_)
+        | IntLit(_)
+        | FloatLit(_)
+        | StringLit(_)
         | Constructor(_)
         | DynamicErrorHole(_)
         | Closure(_)
@@ -135,10 +135,10 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Undefined
           | Constructor(_)
           | Var(_)
-          | Bool(_)
-          | Int(_)
-          | Float(_)
-          | String(_)
+          | BoolLit(_)
+          | IntLit(_)
+          | FloatLit(_)
+          | StringLit(_)
           | FailedCast(_, _, _)
           | MultiHole(_)
           | Deferral(_)

src/haz3lcore/dynamics/DHPat.re

@@ -12,43 +12,43 @@ let rec binds_var = (m: Statics.Map.t, x: Var.t, dp: t): bool =>
   | Some(_) => false
   | None =>
     switch (dp |> term_of) {
-    | EmptyHole
-    | MultiHole(_)
+    | EmptyHolePat
+    | MultiHolePat(_)
     | Wild
-    | Invalid(_)
-    | Int(_)
-    | Float(_)
-    | Bool(_)
-    | String(_)
-    | Constructor(_) => false
-    | Cast(y, _, _)
-    | Parens(y) => binds_var(m, x, y)
-    | Var(y) => Var.eq(x, y)
-    | Tuple(dps) => dps |> List.exists(binds_var(m, x))
-    | Cons(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
-    | ListLit(d_list) =>
+    | InvalidPat(_)
+    | IntPat(_)
+    | FloatPat(_)
+    | BoolPat(_)
+    | StringPat(_)
+    | ConstructorPat(_) => false
+    | CastPat(y, _, _)
+    | ParensPat(y) => binds_var(m, x, y)
+    | VarPat(y) => Var.eq(x, y)
+    | TuplePat(dps) => dps |> List.exists(binds_var(m, x))
+    | ConsPat(dp1, dp2) => binds_var(m, x, dp1) || binds_var(m, x, dp2)
+    | ListLitPat(d_list) =>
       let new_list = List.map(binds_var(m, x), d_list);
       List.fold_left((||), false, new_list);
-    | Ap(_, _) => false
+    | ApPat(_, _) => false
     }
   };
 
 let rec bound_vars = (dp: t): list(Var.t) =>
   switch (dp |> term_of) {
-  | EmptyHole
-  | MultiHole(_)
+  | EmptyHolePat
+  | MultiHolePat(_)
   | Wild
-  | Invalid(_)
-  | Int(_)
-  | Float(_)
-  | Bool(_)
-  | String(_)
-  | Constructor(_) => []
-  | Cast(y, _, _)
-  | Parens(y) => bound_vars(y)
-  | Var(y) => [y]
-  | Tuple(dps) => List.flatten(List.map(bound_vars, dps))
-  | Cons(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
-  | ListLit(dps) => List.flatten(List.map(bound_vars, dps))
-  | Ap(_, dp1) => bound_vars(dp1)
+  | InvalidPat(_)
+  | IntPat(_)
+  | FloatPat(_)
+  | BoolPat(_)
+  | StringPat(_)
+  | ConstructorPat(_) => []
+  | CastPat(y, _, _)
+  | ParensPat(y) => bound_vars(y)
+  | VarPat(y) => [y]
+  | TuplePat(dps) => List.flatten(List.map(bound_vars, dps))
+  | ConsPat(dp1, dp2) => bound_vars(dp1) @ bound_vars(dp2)
+  | ListLitPat(dps) => List.flatten(List.map(bound_vars, dps))
+  | ApPat(_, dp1) => bound_vars(dp1)
   };