intro new sort ctxt

src/haz3lcore/assistant/AssistantForms.re

@@ -34,7 +34,12 @@ module Typ = {
     ("test" ++ leading_expander, Prod([]) |> Typ.fresh),
     ("type" ++ leading_expander, unk),
     ("val" ++ leading_expander, unk),
-    ("entail" ++ leading_expander, unk),
+    ("entail_hastype" ++ leading_expander, unk),
+    // ("entail_ana" ++ leading_expander, unk),
+    // ("entail_syn" ++ leading_expander, unk),
+    ("of_alfa_exp" ++ leading_expander, unk),
+    ("of_prop" ++ leading_expander, unk),
+    ("of_ctxt" ++ leading_expander, unk),
     ("eval" ++ leading_expander, unk),
   ];
 

src/haz3lcore/derivation/DrvElab.re

@@ -6,15 +6,10 @@ let to_list = d =>
   | _ => [d]
   };
 
-let to_ctx = d =>
-  switch (DrvSyntax.term_of(d)) {
-  | Ctx(_) => d
-  | _ => Ctx([d]) |> DrvSyntax.fresh
-  };
-
 let rec elaborate: Drv.t => t =
   fun
   | Jdmt(jdmt) => elab_jdmt(jdmt)
+  | Ctxt(ctxt) => elab_ctxt(ctxt)
   | Prop(prop) => elab_prop(prop)
   | Exp(exp) => elab_exp(exp)
   | Pat(pat) => elab_pat(pat)
@@ -27,16 +22,43 @@ and elab_jdmt: Drv.Jdmt.t => t =
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
       | Val(e) => Val(elab_exp(e))
       | Eval(e1, e2) => Eval(elab_exp(e1), elab_exp(e2))
-      | Entail(p1, p2) => Entail(elab_prop(p1) |> to_ctx, elab_prop(p2))
+      | Entail(ctx, p) => Entail(elab_ctxt(ctx), elab_prop(p))
       };
     {...jdmt, term};
   }
+and elab_ctxt: Drv.Ctxt.t => t =
+  ctxt => {
+    let rec prop_term_of: Drv.Prop.t => Drv.Prop.term =
+      pat =>
+        switch (pat.term) {
+        | Parens(p) => prop_term_of(p)
+        | p => p
+        };
+    let term: term =
+      switch (ctxt.term) {
+      | Hole(s) => Hole(TermBase.TypeHole.show(s))
+      | Ctxt(p) =>
+        switch (prop_term_of(p)) {
+        | Tuple(ps) =>
+          Ctx(
+            ps
+            |> List.map(elab_prop)
+            |> List.map(to_list)
+            |> List.concat
+            |> List.fold_left(cons_ctx, []),
+          )
+        | _ => Ctx([elab_prop(p)])
+        }
+      };
+    {...ctxt, term};
+  }
 and elab_prop: Drv.Prop.t => t =
   prop => {
+    let hole: term = Hole(Drv.Prop.show(prop));
     let term: term =
       switch (prop.term) {
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
-      | HasTy(e, t) => HasTy(elab_exp(e), elab_typ(t))
+      | HasType(e, t) => HasType(elab_exp(e), elab_typ(t))
       | Syn(e, t) => Syn(elab_exp(e), elab_typ(t))
       | Ana(e, t) => Ana(elab_exp(e), elab_typ(t))
       | Var(x) => Atom(x)
@@ -45,15 +67,8 @@ and elab_prop: Drv.Prop.t => t =
       | Impl(p1, p2) => Impl(elab_prop(p1), elab_prop(p2))
       | Truth => Truth
       | Falsity => Falsity
-      | Tuple(ps) =>
-        Ctx(
-          ps
-          |> List.map(elab_prop)
-          |> List.map(to_list)
-          |> List.concat
-          |> List.fold_left(cons_ctx, []),
-        )
-      | Abbr(_) => Hole(Drv.Prop.show(prop))
+      | Tuple(_) => hole
+      | Abbr(_) => hole
       | Parens(p) => IdTagged.term_of(elab_prop(p))
       };
     {...prop, term};

src/haz3lcore/derivation/DrvInfo.re

@@ -24,6 +24,14 @@ type jdmt = {
   status: status_common,
 };
 
+[@deriving (show({with_path: false}), sexp, yojson)]
+type ctxt = {
+  term: Drv.Ctxt.t,
+  cls: Cls.t,
+  ancestors,
+  status: status_common,
+};
+
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error_prop =
   | BadToken(Token.t)
@@ -111,6 +119,7 @@ type tpat = {
 [@deriving (show({with_path: false}), sexp, yojson)]
 type t =
   | Jdmt(jdmt)
+  | Ctxt(ctxt)
   | Prop(prop)
   | Exp(exp)
   | Pat(pat)
@@ -120,6 +129,7 @@ type t =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type error =
   | Jdmt(error_common)
+  | Ctxt(error_common)
   | Prop(error_prop)
   | Exp(error_exp)
   | Pat(error_pat)
@@ -129,6 +139,7 @@ type error =
 let sort_of: t => Sort.DrvSort.t =
   fun
   | Jdmt(_) => Jdmt
+  | Ctxt(_) => Ctxt
   | Prop(_) => Prop
   | Exp(_) => Exp
   | Pat(_) => Pat
@@ -138,6 +149,7 @@ let sort_of: t => Sort.DrvSort.t =
 let cls_of: t => Cls.t =
   fun
   | Jdmt(jdmt) => jdmt.cls
+  | Ctxt(ctxt) => ctxt.cls
   | Prop(prop) => prop.cls
   | Exp(exp) => exp.cls
   | Pat(pat) => pat.cls
@@ -147,6 +159,7 @@ let cls_of: t => Cls.t =
 let id_of: t => Id.t =
   fun
   | Jdmt(jdmt) => Drv.Jdmt.rep_id(jdmt.term)
+  | Ctxt(ctxt) => Drv.Ctxt.rep_id(ctxt.term)
   | Prop(prop) => Drv.Prop.rep_id(prop.term)
   | Exp(exp) => Drv.Exp.rep_id(exp.term)
   | Pat(pat) => Drv.Pat.rep_id(pat.term)
@@ -156,12 +169,14 @@ let id_of: t => Id.t =
 let error_of: t => option(error) =
   fun
   | Jdmt({status: NotInHole(_), _})
+  | Ctxt({status: NotInHole(_), _})
   | Prop({status: NotInHole(_), _})
   | Exp({status: NotInHole(_), _})
   | Pat({status: NotInHole(_), _})
   | Typ({status: NotInHole(_), _})
   | TPat({status: NotInHole(_), _}) => None
   | Jdmt({status: InHole(err), _}) => Some(Jdmt(err))
+  | Ctxt({status: InHole(err), _}) => Some(Ctxt(err))
   | Prop({status: InHole(err), _}) => Some(Prop(err))
   | Exp({status: InHole(err), _}) => Some(Exp(err))
   | Pat({status: InHole(err), _}) => Some(Pat(err))
@@ -171,6 +186,7 @@ let error_of: t => option(error) =
 [@deriving (show({with_path: false}), sexp, yojson)]
 type status_drv =
   | Jdmt(status_common)
+  | Ctxt(status_common)
   | Prop(status_prop)
   | Exp(status_exp)
   | Pat(status_pat)
@@ -184,6 +200,13 @@ let status_jdmt = (jdmt: Drv.Jdmt.t): status_common =>
   | _ => NotInHole()
   };
 
+let status_ctxt = (ctxt: Drv.Ctxt.t): status_common =>
+  switch (ctxt.term) {
+  | Hole(Invalid(token)) => InHole(BadToken(token))
+  | Hole(MultiHole(_)) => InHole(MultiHole)
+  | _ => NotInHole()
+  };
+
 let status_prop = (prop: Drv.Prop.t): status_prop =>
   switch (prop.term) {
   | Hole(Invalid(token)) => InHole(BadToken(token))
@@ -222,6 +245,7 @@ let status_tpat = (tpat: Drv.TPat.t): status_common =>
 let status_drv = (drv: Drv.t): status_drv =>
   switch (drv) {
   | Jdmt(term) => Jdmt(status_jdmt(term))
+  | Ctxt(term) => Ctxt(status_ctxt(term))
   | Prop(term) => Prop(status_prop(term))
   | Exp(term) => Exp(status_exp(term))
   | Pat(term) => Pat(status_pat(term))
@@ -232,12 +256,14 @@ let status_drv = (drv: Drv.t): status_drv =>
 let is_error = (ci: t): bool => {
   switch (ci) {
   | Jdmt({status: InHole(_), _})
+  | Ctxt({status: InHole(_), _})
   | Prop({status: InHole(_), _})
   | Exp({status: InHole(_), _})
   | Pat({status: InHole(_), _})
   | Typ({status: InHole(_), _})
   | TPat({status: InHole(_), _}) => true
   | Jdmt({status: NotInHole(_), _})
+  | Ctxt({status: NotInHole(_), _})
   | Prop({status: NotInHole(_), _})
   | Exp({status: NotInHole(_), _})
   | Pat({status: NotInHole(_), _})
@@ -249,6 +275,7 @@ let is_error = (ci: t): bool => {
 let ancestors_of: t => ancestors =
   fun
   | Jdmt({ancestors, _})
+  | Ctxt({ancestors, _})
   | Prop({ancestors, _})
   | Exp({ancestors, _})
   | Pat({ancestors, _})
@@ -261,6 +288,12 @@ let derived_jdmt = (jdmt: Drv.Jdmt.t, ~ancestors): jdmt => {
   {term: jdmt, cls, status, ancestors};
 };
 
+let derived_ctxt = (ctxt: Drv.Ctxt.t, ~ancestors): ctxt => {
+  let cls = Cls.Drv(Ctxt(Drv.Ctxt.cls_of_term(ctxt.term)));
+  let status = status_ctxt(ctxt);
+  {term: ctxt, cls, status, ancestors};
+};
+
 let derived_prop = (prop: Drv.Prop.t, ~ancestors): prop => {
   let cls = Cls.Drv(Prop(Drv.Prop.cls_of_term(prop.term)));
   let status = status_prop(prop);
@@ -294,6 +327,7 @@ let derived_tpat = (tpat: Drv.TPat.t, ~ancestors): tpat => {
 let derived_drv = (drv: Drv.t, ~ancestors): t => {
   switch (drv) {
   | Jdmt(jdmt) => Jdmt(derived_jdmt(jdmt, ~ancestors))
+  | Ctxt(ctxt) => Ctxt(derived_ctxt(ctxt, ~ancestors))
   | Prop(prop) => Prop(derived_prop(prop, ~ancestors))
   | Exp(exp) => Exp(derived_exp(exp, ~ancestors))
   | Pat(pat) => Pat(derived_pat(pat, ~ancestors))

src/haz3lcore/derivation/DrvSyntax.re

@@ -24,7 +24,7 @@ type term =
   | Eval(t, t)
   | Entail(t, t)
   // Proposition
-  | HasTy(t, t)
+  | HasType(t, t)
   | Syn(t, t)
   | Ana(t, t)
   | Atom(string)
@@ -93,7 +93,7 @@ type cls =
   | Val
   | Eval
   | Entail
-  | HasTy
+  | HasType
   | Syn
   | Ana
   | Atom
@@ -152,7 +152,7 @@ let precedence: t => int =
     | Val(_) => P.filter
     | Eval(_) => P.filter
     | Entail(_) => P.filter
-    | HasTy(_) => P.semi
+    | HasType(_) => P.semi
     | Syn(_) => P.semi
     | Ana(_) => P.semi
     | Atom(_) => P.max
@@ -293,7 +293,7 @@ let rec repr = (p: int, prop: t): list(string) => {
     | Unroll(a) => repr_aba_tight(["unroll(", ")"], [a])
     | TPat(x) => x |> mk
     | Pat(x) => x |> mk
-    | HasTy(a, b) => repr_binop(":", a, b)
+    | HasType(a, b) => repr_binop(":", a, b)
     | Syn(a, b) => repr_binop("⇒", a, b)
     | Ana(a, b) => repr_binop("⇐", a, b)
     }
@@ -395,8 +395,8 @@ let rec eq: (t, t) => bool =
     | (TPat(_), _) => false
     | (Pat(a), Pat(b)) => String.equal(a, b)
     | (Pat(_), _) => false
-    | (HasTy(a1, a2), HasTy(b1, b2)) => eq(a1, b1) && eq(a2, b2)
-    | (HasTy(_), _) => false
+    | (HasType(a1, a2), HasType(b1, b2)) => eq(a1, b1) && eq(a2, b2)
+    | (HasType(_), _) => false
     | (Syn(a1, a2), Syn(b1, b2)) => eq(a1, b1) && eq(a2, b2)
     | (Syn(_), _) => false
     | (Ana(a1, a2), Ana(b1, b2)) => eq(a1, b1) && eq(a2, b2)
@@ -486,7 +486,7 @@ let rec subst: (t, string, t) => t =
     | TPat(_)
     | Pat(_)
     // Proposition
-    | HasTy(_)
+    | HasType(_)
     | Syn(_)
     | Ana(_) => e
     // Logic
@@ -571,7 +571,7 @@ let rec subst_ty: (t, string, t) => t =
     | TPat(_)
     | Pat(_) => e
     // Proposition
-    | HasTy(_)
+    | HasType(_)
     | Syn(_)
     | Ana(_) => e
     // Logic

src/haz3lcore/derivation/DrvTerm.re

@@ -30,11 +30,39 @@ module Jdmt = {
     | Entail(_) => Entail;
 };
 
+module Ctxt = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type cls =
+    | Hole
+    | Ctxt;
+
+  include TermBase.Ctxt;
+
+  let hole = (tms: list(TermBase.Any.t)): term =>
+    Hole(List.is_empty(tms) ? EmptyHole : MultiHole(tms));
+
+  let rep_id = ({ids, _}: t) => {
+    assert(ids != []);
+    List.hd(ids);
+  };
+
+  let term_of: t => term = IdTagged.term_of;
+
+  let unwrap: t => (term, term => t) = IdTagged.unwrap;
+
+  let fresh: term => t = IdTagged.fresh;
+
+  let cls_of_term: term => cls =
+    fun
+    | Hole(_) => Hole
+    | Ctxt(_) => Ctxt;
+};
+
 module Prop = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Hole
-    | HasTy
+    | HasType
     | Syn
     | Ana
     | Var
@@ -66,7 +94,7 @@ module Prop = {
   let cls_of_term: term => cls =
     fun
     | Hole(_) => Hole
-    | HasTy(_) => HasTy
+    | HasType(_) => HasType
     | Syn(_) => Syn
     | Ana(_) => Ana
     | Var(_) => Var
@@ -276,6 +304,7 @@ module Drv = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Jdmt(Jdmt.cls)
+    | Ctxt(Ctxt.cls)
     | Prop(Prop.cls)
     | Exp(ALFA_Exp.cls)
     | Pat(ALFA_Pat.cls)
@@ -287,6 +316,7 @@ module Drv = {
   let sort_of: t => Sort.DrvSort.t =
     fun
     | Jdmt(_) => Jdmt
+    | Ctxt(_) => Ctxt
     | Prop(_) => Prop
     | Exp(_) => Exp
     | Pat(_) => Pat
@@ -296,6 +326,7 @@ module Drv = {
   let rep_id: t => Id.t =
     fun
     | Jdmt(jdmt) => Jdmt.rep_id(jdmt)
+    | Ctxt(ctxt) => Ctxt.rep_id(ctxt)
     | Prop(prop) => Prop.rep_id(prop)
     | Exp(exp) => ALFA_Exp.rep_id(exp)
     | Pat(pat) => ALFA_Pat.rep_id(pat)
@@ -305,6 +336,7 @@ module Drv = {
   let of_id: t => list(Id.t) =
     fun
     | Jdmt(jdmt) => jdmt.ids
+    | Ctxt(ctxt) => ctxt.ids
     | Prop(prop) => prop.ids
     | Exp(exp) => exp.ids
     | Pat(pat) => pat.ids
@@ -314,6 +346,7 @@ module Drv = {
   let cls_of: t => cls =
     fun
     | Jdmt(jdmt) => Jdmt(Jdmt.cls_of_term(jdmt.term))
+    | Ctxt(ctxt) => Ctxt(Ctxt.cls_of_term(ctxt.term))
     | Prop(prop) => Prop(Prop.cls_of_term(prop.term))
     | Exp(exp) => Exp(ALFA_Exp.cls_of_term(exp.term))
     | Pat(pat) => Pat(ALFA_Pat.cls_of_term(pat.term))