fix tylr parsing

src/haz3lcore/derivation/DrvTerm.re

@@ -284,7 +284,7 @@ module Drv = {
 
   include TermBase.Drv;
 
-  let of_typ: t => DrvTyp.t =
+  let sort_of: t => Sort.DrvSort.t =
     fun
     | Jdmt(_) => Jdmt
     | Prop(_) => Prop

src/haz3lcore/dynamics/Casts.re

@@ -58,7 +58,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | Int
   | Float
   | String
-  | Derivation(_)
+  | Term(_)
   | Var(_)
   | Rec(_)
   | Forall(_, {term: Unknown(_), _})

src/haz3lcore/dynamics/DHExp.re

@@ -78,7 +78,7 @@ let rec strip_casts =
         | TypAp(_)
         | Undefined
         | If(_)
-        | Derivation(_) => continue(exp)
+        | Term(_) => continue(exp)
         /* Remove casts*/
         | FailedCast(d, _, _)
         | Cast(d, _, _) => strip_casts(d)
@@ -113,7 +113,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
             /* Note that we do not have to worry about capture avoidance, since s will always be closed. */
             }
           | Cast(_)
-          | Derivation(_)
+          | Term(_)
           | FixF(_)
           | Fun(_)
           | TypAp(_)

src/haz3lcore/dynamics/Elaborator.re

@@ -242,8 +242,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
     | Bool(_) => uexp |> cast_from(Bool |> Typ.temp)
     | Float(_) => uexp |> cast_from(Float |> Typ.temp)
     | String(_) => uexp |> cast_from(String |> Typ.temp)
-    | Derivation(d) =>
-      uexp |> cast_from(Derivation(Drv.of_typ(d)) |> Typ.temp)
+    | Term(term) => uexp |> cast_from(Term(Any.sort_of(term)) |> Typ.temp)
     | ListLit(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       let inner_type =

src/haz3lcore/dynamics/FilterMatcher.re

@@ -214,8 +214,8 @@ let rec matches_exp =
     | (String(dv), String(fv)) => dv == fv
     | (String(_), _) => false
 
-    | (Derivation(d), Derivation(f)) => d == f
-    | (Derivation(_), _) => false
+    | (Term(d), Term(f)) => d == f
+    | (Term(_), _) => false
 
     | (
         Constructor(_),

src/haz3lcore/dynamics/Substitution.re

@@ -64,7 +64,7 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
   | Int(_)
   | Float(_)
   | String(_)
-  | Derivation(_)
+  | Term(_)
   | Constructor(_) => d2
   | ListLit(ds) => ListLit(List.map(subst_var(m, d1, x), ds)) |> rewrap
   | Cons(d3, d4) =>

src/haz3lcore/dynamics/Transition.re

@@ -290,7 +290,7 @@ module Transition = (EV: EV_MODE) => {
             };
           let+ e =
             switch (DHExp.term_of(d)) {
-            | Derivation(Prop(e)) => Ok(e)
+            | Term(Drv(Prop(e))) => Ok(e)
             | _ => Error("Pat Not Prop type")
             };
           e |> IdTagged.unwrap |> fst;
@@ -347,7 +347,7 @@ module Transition = (EV: EV_MODE) => {
             };
           let+ e =
             switch (DHExp.term_of(d)) {
-            | Derivation(Exp(e)) => Ok(e)
+            | Term(Drv(Exp(e))) => Ok(e)
             | _ => Error("Pat Not ALFA_Exp type")
             };
           e |> IdTagged.unwrap |> fst;
@@ -358,9 +358,9 @@ module Transition = (EV: EV_MODE) => {
     let (term, rewrap) = IdTagged.unwrap(d);
     let term: term =
       switch (term) {
-      | Derivation(Jdmt(jdmt)) => Derivation(Jdmt(go_jdmt(jdmt)))
-      | Derivation(Prop(prop)) => Derivation(Prop(go_prop(prop)))
-      | Derivation(Exp(exp)) => Derivation(Exp(go_exp(exp)))
+      | Term(Drv(Jdmt(jdmt))) => Term(Drv(Jdmt(go_jdmt(jdmt))))
+      | Term(Drv(Prop(prop))) => Term(Drv(Prop(go_prop(prop))))
+      | Term(Drv(Exp(exp))) => Term(Drv(Exp(go_exp(exp))))
       | _ => term
       };
     term |> rewrap;
@@ -659,7 +659,7 @@ module Transition = (EV: EV_MODE) => {
     | BuiltinFun(_) =>
       let. _ = otherwise(env, d);
       Constructor;
-    | Derivation(_) =>
+    | Term(_) =>
       let. _ = otherwise(env, d);
       let d' = replace_drv_abbrs(env, d);
       if (DHExp.fast_equal(d, d')) {

src/haz3lcore/dynamics/TypeAssignment.re

@@ -226,7 +226,7 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
   | Int(_) => Some(Int |> Typ.temp)
   | Float(_) => Some(Float |> Typ.temp)
   | String(_) => Some(String |> Typ.temp)
-  | Derivation(d) => Some(Derivation(Drv.of_typ(d)) |> Typ.temp)
+  | Term(d) => Some(Term(Any.sort_of(d)) |> Typ.temp)
   | BinOp(Bool(_), d1, d2) =>
     let* ty1 = typ_of_dhexp(ctx, m, d1);
     let* ty2 = typ_of_dhexp(ctx, m, d2);

src/haz3lcore/dynamics/Unboxing.re

@@ -145,8 +145,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
        in elaboration or in the cast calculus. */
     | (
         _,
-        Bool(_) | Int(_) | Float(_) | String(_) | Derivation(_) |
-        Constructor(_) |
+        Bool(_) | Int(_) | Float(_) | String(_) | Term(_) | Constructor(_) |
         BuiltinFun(_) |
         Deferral(_) |
         DeferredAp(_) |

src/haz3lcore/lang/term/Typ.re

@@ -12,7 +12,7 @@ type cls =
   | Float
   | Bool
   | String
-  | Derivation
+  | Term
   | Arrow
   | Prod
   | Sum
@@ -52,7 +52,7 @@ let cls_of_term: term => cls =
   | Float => Float
   | Bool => Bool
   | String => String
-  | Derivation(_) => Derivation
+  | Term(_) => Term
   | List(_) => List
   | Arrow(_) => Arrow
   | Var(_) => Var
@@ -73,8 +73,8 @@ let show_cls: cls => string =
   | Int
   | Float
   | String
-  | Derivation
   | Bool => "Base type"
+  | Term => "Term type"
   | Var => "Type variable"
   | Constructor => "Sum constructor"
   | List => "List type"
@@ -95,7 +95,7 @@ let rec is_arrow = (typ: t) => {
   | Float
   | Bool
   | String
-  | Derivation(_)
+  | Term(_)
   | List(_)
   | Prod(_)
   | Var(_)
@@ -115,7 +115,7 @@ let rec is_forall = (typ: t) => {
   | Float
   | Bool
   | String
-  | Derivation(_)
+  | Term(_)
   | Arrow(_)
   | List(_)
   | Prod(_)
@@ -160,7 +160,7 @@ let rec free_vars = (~bound=[], ty: t): list(Var.t) =>
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => []
   | Ap(t1, t2) => free_vars(~bound, t1) @ free_vars(~bound, t2)
   | Var(v) => List.mem(v, bound) ? [] : [v]
@@ -262,8 +262,8 @@ let rec join = (~resolve=false, ~fix, ctx: Ctx.t, ty1: t, ty2: t): option(t) =>
   | (Bool, _) => None
   | (String, String) => Some(ty1)
   | (String, _) => None
-  | (Derivation(d1), Derivation(d2)) when d1 == d2 => Some(ty1)
-  | (Derivation(_), _) => None
+  | (Term(d1), Term(d2)) when d1 == d2 => Some(ty1)
+  | (Term(_), _) => None
   | (Arrow(ty1, ty2), Arrow(ty1', ty2')) =>
     let* ty1 = join'(ty1, ty1');
     let+ ty2 = join'(ty2, ty2');
@@ -299,7 +299,7 @@ let rec match_synswitch = (t1: t, t2: t) => {
   | (Float, _)
   | (Bool, _)
   | (String, _)
-  | (Derivation(_), _)
+  | (Term(_), _)
   | (Var(_), _)
   | (Ap(_), _)
   | (Rec(_), _)
@@ -356,7 +356,7 @@ let rec normalize = (ctx: Ctx.t, ty: t): t => {
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => ty
   | Parens(t) => Parens(normalize(ctx, t)) |> rewrap
   | List(t) => List(normalize(ctx, t)) |> rewrap
@@ -487,7 +487,7 @@ let rec needs_parens = (ty: t): bool =>
   | Int
   | Float
   | String
-  | Derivation(_)
+  | Term(_)
   | Bool
   | Var(_) => false
   | Rec(_, _)
@@ -516,7 +516,7 @@ let rec pretty_print = (ty: t): string =>
   | Float => "Float"
   | Bool => "Bool"
   | String => "String"
-  | Derivation(d) => DrvTyp.repr(d)
+  | Term(d) => Sort.to_string(d)
   | Var(tvar) => tvar
   | List(t) => "[" ++ pretty_print(t) ++ "]"
   | Arrow(t1, t2) => paren_pretty_print(t1) ++ " -> " ++ pretty_print(t2)

src/haz3lcore/statics/MakeTerm.re

@@ -389,7 +389,7 @@ and exp = unsorted => {
     let (term, inner_ids) = jdmt_term(unsorted);
     let ids = ids(unsorted) @ inner_ids;
     let jdmt = return(e => Drv(Jdmt(e)), ids, {ids, copied: false, term});
-    TermBase.Exp.Derivation(Jdmt(jdmt)) |> IdTagged.fresh;
+    TermBase.Exp.Term(Drv(Jdmt(jdmt))) |> IdTagged.fresh;
   | _ =>
     let ids = ids(unsorted) @ inner_ids;
     return(e => Exp(e), ids, {ids, copied: false, term});
@@ -427,13 +427,13 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           Match(scrut, rules),
           ids,
         )
-      | (["of_Typ", "end"], [Drv(Typ(ty))]) => ret(Derivation(Typ(ty)))
-      | (["of_Exp", "end"], [Drv(Exp(e))]) => ret(Derivation(Exp(e)))
-      | (["of_Pat", "end"], [Drv(Pat(p))]) => ret(Derivation(Pat(p)))
+      | (["of_Typ", "end"], [Drv(Typ(ty))]) => ret(Term(Drv(Typ(ty))))
+      | (["of_Exp", "end"], [Drv(Exp(e))]) => ret(Term(Drv(Exp(e))))
+      | (["of_Pat", "end"], [Drv(Pat(p))]) => ret(Term(Drv(Pat(p))))
       | (["of_TPat", "end"], [Drv(TPat(tp))]) =>
-        ret(Derivation(TPat(tp)))
-      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Derivation(Prop(p)))
-      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Derivation(Jdmt(j)))
+        ret(Term(Drv(TPat(tp))))
+      | (["of_Prop", "end"], [Drv(Prop(p))]) => ret(Term(Drv(Prop(p))))
+      | (["of_Jdmt", "end"], [Drv(Jdmt(j))]) => ret(Term(Drv(Jdmt(j))))
       | ([t], []) when t != " " && !Form.is_explicit_hole(t) =>
         ret(Invalid(t))
       | _ => ret(hole(tm))
@@ -463,9 +463,9 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["type", "=", "in"], [TPat(tpat), Typ(def)]) =>
           TyAlias(tpat, def, r)
         | (["prop", "=", "in"], [Pat(pat), Drv(Prop(def))]) =>
-          Let(pat, UExp.Derivation(Prop(def)) |> UExp.fresh, r)
+          Let(pat, UExp.Term(Drv(Prop(def))) |> UExp.fresh, r)
         | (["alfa", "=", "in"], [Pat(pat), Drv(Exp(def))]) =>
-          Let(pat, UExp.Derivation(Exp(def)) |> UExp.fresh, r)
+          Let(pat, UExp.Term(Drv(Exp(def))) |> UExp.fresh, r)
         | (["if", "then", "else"], [Exp(cond), Exp(conseq)]) =>
           If(cond, conseq, r)
         | _ => hole(tm)

src/haz3lcore/statics/Statics.re

@@ -226,7 +226,7 @@ and drv_to_info_map =
            ~co_ctx=CoCtx.empty,
            ~ctx,
            ~ancestors,
-           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           ~mode=Mode.Ana(Term(Drv(Prop)) |> Typ.fresh),
            p,
          )
       |> snd
@@ -295,7 +295,7 @@ and drv_to_info_map =
            ~co_ctx=CoCtx.empty,
            ~ctx,
            ~ancestors,
-           ~mode=Mode.Ana(Derivation(DrvTyp.Prop) |> Typ.fresh),
+           ~mode=Mode.Ana(Term(Drv(Exp)) |> Typ.fresh),
            p,
          )
       |> snd
@@ -428,10 +428,10 @@ and uexp_to_info_map =
   | Int(_) => atomic(Just(Int |> Typ.temp))
   | Float(_) => atomic(Just(Float |> Typ.temp))
   | String(_) => atomic(Just(String |> Typ.temp))
-  | Derivation(d) =>
-    let m = drv_to_info_map(d, m, ~ancestors, ~ctx) |> snd;
+  | Term(term) =>
+    let m = any_to_info_map(term, m, ~ancestors, ~ctx) |> snd;
     add(
-      ~self=Just(Derivation(Drv.of_typ(d)) |> Typ.temp),
+      ~self=Just(Term(Any.sort_of(term)) |> Typ.temp),
       ~co_ctx=CoCtx.empty,
       m,
     );
@@ -1045,7 +1045,7 @@ and utyp_to_info_map =
   | Int
   | Float
   | Bool
-  | Derivation(_)
+  | Term(_)
   | String => add(m)
   | Var(_) =>
     /* Names are resolved in Info.status_typ */