update jdmt writing term

src/haz3lcore/derivation/DrvElab.re

@@ -26,6 +26,7 @@ and elab_jdmt: Drv.Exp.t => t =
   }
 and elab_ctxt: Drv.Exp.t => t =
   ctx => {
+    let hole: term = Hole(Drv.Exp.show(ctx));
     let term: term =
       switch (exp_term_of(ctx)) {
       | Hole(s) => Hole(TermBase.TypeHole.show(s))
@@ -37,8 +38,22 @@ and elab_ctxt: Drv.Exp.t => t =
           |> List.concat
           |> List.fold_left(cons_ctx, []),
         )
-      | _ => Hole(Drv.Exp.show(ctx))
+      | Cons(p, ctx) =>
+        switch (IdTagged.term_of(elab_ctxt(ctx))) {
+        | Ctx(ps) => Ctx(cons_ctx(ps, elab_prop(p)))
+        | _ => hole
+        }
+      | Concat(ctx1, ctx2) =>
+        switch (
+          IdTagged.term_of(elab_ctxt(ctx1)),
+          IdTagged.term_of(elab_ctxt(ctx2)),
+        ) {
+        | (Ctx(ps1), Ctx(ps2)) => Ctx(List.fold_left(cons_ctx, ps2, ps1))
+        | _ => hole
+        }
+      | _ => hole
       };
+    print_endline("elab_ctxt" ++ DrvSyntax.show_term(term));
     {...ctx, term};
   }
 and elab_prop: Drv.Exp.t => t =
@@ -127,7 +142,7 @@ and elab_exp: Drv.Exp.t => t =
       | PrjR(e) => PrjR(elab_exp(e))
       | InjL => hole
       | InjR => hole
-      | Case(e, x, e1, y, e2) =>
+      | Case(e, [(x, e1), (y, e2)]) =>
         let e = elab_exp(e);
         let e1 = elab_exp(e1);
         let e2 = elab_exp(e2);

src/haz3lcore/derivation/DrvInfo.re

@@ -157,7 +157,9 @@ let types_of_exp = (exp: Drv.Exp.t): list(ty_merged) =>
   | Val(_)
   | Eval(_)
   | Entail(_) => [Jdmt]
-  | Ctx(_) => [Ctx]
+  | Ctx(_)
+  | Cons(_)
+  | Concat(_) => [Ctx]
   | HasType(_)
   | Syn(_)
   | Ana(_)

src/haz3lcore/derivation/DrvSyntax.re

@@ -590,11 +590,21 @@ let rec subst_ty: (t, string, t) => t =
 
 let mem_ctx = p => List.exists(eq(p));
 
+// Note(zhiyao): This implementation of cons_ctx is not linear.
 let cons_ctx = (ctx, p) => {
-  let cmp = p' => show(p') <= show(p);
+  let cmp = p' => show(p) < show(p');
+  let eq_key = p' =>
+    switch (IdTagged.term_of(p): term, IdTagged.term_of(p'): term) {
+    | (HasType(a, _), HasType(b, _)) => eq(a, b)
+    | (Syn(a, _), Syn(b, _)) => eq(a, b)
+    | (Ana(a, _), Ana(b, _)) => eq(a, b)
+    | _ => show(p) == show(p')
+    };
   let rec insert =
     fun
     | [] => [p]
-    | [hd, ...tl] => cmp(hd) ? [p, hd, ...tl] : [hd, ...insert(tl)];
+    | [hd, ...tl] when eq_key(hd) => [p, ...tl]
+    | [hd, ...tl] when cmp(hd) => [p, hd, ...tl]
+    | [hd, ...tl] => [hd, ...insert(tl)];
   insert(ctx);
 };

src/haz3lcore/derivation/DrvTerm.re

@@ -10,6 +10,8 @@ module ALFA_Exp = {
     | Eval
     | Entail
     | Ctx
+    | Cons
+    | Concat
     | HasType
     | Syn
     | Ana
@@ -68,6 +70,8 @@ module ALFA_Exp = {
     | Eval(_) => Eval
     | Entail(_) => Entail
     | Ctx(_) => Ctx
+    | Cons(_) => Cons
+    | Concat(_) => Concat
     | HasType(_) => HasType
     | Syn(_) => Syn
     | Ana(_) => Ana
@@ -102,6 +106,34 @@ module ALFA_Exp = {
     | Unroll => Unroll;
 };
 
+module ALFA_Rul = {
+  [@deriving (show({with_path: false}), sexp, yojson)]
+  type cls =
+    | Hole
+    | Rules;
+
+  include TermBase.ALFA_Rul;
+
+  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
+    | Rules(_, _) => Rules;
+};
+
 module ALFA_Pat = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
@@ -218,6 +250,7 @@ module Drv = {
   [@deriving (show({with_path: false}), sexp, yojson)]
   type cls =
     | Exp(ALFA_Exp.cls)
+    | Rul(ALFA_Rul.cls)
     | Pat(ALFA_Pat.cls)
     | Typ(ALFA_Typ.cls)
     | TPat(ALFA_TPat.cls);
@@ -227,27 +260,31 @@ module Drv = {
   let sort_of: t => Sort.DrvSort.t =
     fun
     | Exp(_) => Exp
+    | Rul(_) => Rul
     | Pat(_) => Pat
     | Typ(_) => Typ
     | TPat(_) => TPat;
 
   let rep_id: t => Id.t =
     fun
     | Exp(exp) => ALFA_Exp.rep_id(exp)
+    | Rul(rul) => ALFA_Rul.rep_id(rul)
     | Pat(pat) => ALFA_Pat.rep_id(pat)
     | Typ(typ) => ALFA_Typ.rep_id(typ)
     | TPat(tpat) => ALFA_TPat.rep_id(tpat);
 
   let of_id: t => list(Id.t) =
     fun
     | Exp(exp) => exp.ids
+    | Rul(rul) => rul.ids
     | Pat(pat) => pat.ids
     | Typ(typ) => typ.ids
     | TPat(tpat) => tpat.ids;
 
   let cls_of: t => cls =
     fun
     | Exp(exp) => Exp(ALFA_Exp.cls_of_term(exp.term))
+    | Rul(rul) => Rul(ALFA_Rul.cls_of_term(rul.term))
     | Pat(pat) => Pat(ALFA_Pat.cls_of_term(pat.term))
     | Typ(typ) => Typ(ALFA_Typ.cls_of_term(typ.term))
     | TPat(tpat) => TPat(ALFA_TPat.cls_of_term(tpat.term));

src/haz3lcore/dynamics/Transition.re

@@ -280,6 +280,8 @@ module Transition = (EV: EV_MODE) => {
         | Eval(e1, e2) => Eval(go_exp(e1), go_exp(e2))
         | Entail(ctx, p) => Entail(go_exp(ctx), go_exp(p))
         | Ctx(es) => Ctx(List.map(go_exp, es))
+        | Cons(e1, e2) => Cons(go_exp(e1), go_exp(e2))
+        | Concat(e1, e2) => Concat(go_exp(e1), go_exp(e2))
         | HasType(e, t) => HasType(go_exp(e), t)
         | Syn(e, t) => Syn(go_exp(e), t)
         | Ana(e, t) => Ana(go_exp(e), t)
@@ -309,8 +311,8 @@ module Transition = (EV: EV_MODE) => {
         | PrjR(e) => PrjR(go_exp(e))
         | InjL => InjL
         | InjR => InjR
-        | Case(e1, x, e2, y, e3) =>
-          Case(go_exp(e1), x, go_exp(e2), y, go_exp(e3))
+        | Case(e1, rls) =>
+          Case(go_exp(e1), List.map(((p, e)) => (p, go_exp(e)), rls))
         | Roll => Roll
         | Unroll => Unroll
         };

src/haz3lcore/lang/Form.re

@@ -400,14 +400,14 @@ let forms: list((string, t)) = [
   // Drv(Jdmt)
   ("fake_val", mk(ds, ["val", "end"], mk_op(Exp, [Exp]))),
   ("val", mk(ds, ["val", "end"], mk_op(Drv(Exp), [Drv(Exp)]))),
-  ("val_simple", mk(ii, [".val"], mk_post(P.min, Drv(Exp), []))),
-  ("fake_eval", mk(ds, ["eval", "to"], mk_pre(P.min, Exp, [Exp]))),
-  ("eval", mk(ds, ["eval", "to"], mk_pre(P.min, Drv(Exp), [Drv(Exp)]))),
-  ("eval_simple", mk_infix("$>", Drv(Exp), P.min)),
+  ("eval", mk_infix("\=/", Drv(Exp), P.min)),
   ("entail", mk_infix("|-", Drv(Exp), P.min)),
+  ("unary_entail", mk(ss, ["|-"], mk_pre(P.min, Drv(Exp), []))),
   // Drv(Ctx)
   ("alfa_exp_list", mk(ii, ["[", "]"], mk_op(Drv(Exp), [Drv(Exp)]))),
   ("alfa_cons", mk_infix(",", Drv(Exp), P.comma)),
+  ("alfa_concat", mk_infix("@", Drv(Exp), P.plus)),
+  ("alfa_cons", mk_infix("::", Drv(Exp), P.cons)),
   ("alfa_paren", mk(ii, ["(", ")"], mk_op(Drv(Exp), [Drv(Exp)]))),
   ("alfa_abbr", mk(ii, ["{", "}"], mk_op(Drv(Exp), [Pat]))),
   // Drv(Exp)
@@ -462,16 +462,13 @@ let forms: list((string, t)) = [
   ("exp_pair", mk_infix(",", Drv(Exp), P.comma)),
   ("exp_prjl", mk(ii, [".fst"], mk_post(P.ap, Drv(Exp), []))),
   ("exp_prjr", mk(ii, [".snd"], mk_post(P.ap, Drv(Exp), []))),
+  ("alfa_case", mk(ds, ["case", "end"], mk_op(Drv(Exp), [Drv(Rul)]))),
   (
-    "exp_case",
+    "alfa_rule",
     mk(
       ds,
-      ["case_sum", "of", "->", "else", "->"],
-      mk_pre(
-        P.fun_,
-        Drv(Exp),
-        [Drv(Exp), Drv(Pat), Drv(Exp), Drv(Pat)],
-      ),
+      ["|", "=>"],
+      mk_bin'(P.rule_sep, Drv(Rul), Drv(Exp), [Drv(Pat)], Drv(Exp)),
     ),
   ),
   // Drv(Pat)

src/haz3lcore/lang/Sort.re

@@ -5,6 +5,7 @@ module DrvSort = {
     | Ctx
     | Prop
     | Exp
+    | Rul
     | Pat
     | Typ
     | TPat;
@@ -15,6 +16,7 @@ module DrvSort = {
     | Prop => "Prop"
     | Ctx => "Ctx"
     | Exp => "ALFA_Exp"
+    | Rul => "ALFA_Rul"
     | Pat => "ALFA_Pat"
     | Typ => "ALFA_Typ"
     | TPat => "ALFA_TPat";
@@ -25,6 +27,7 @@ module DrvSort = {
     | Ctx => "Drv"
     | Prop => "Exp"
     | Exp => "Exp"
+    | Rul => "Rul"
     | Pat => "Pat"
     | Typ => "Typ"
     | TPat => "TPat";
@@ -37,6 +40,7 @@ module DrvSort = {
     | Ctx => "Ctx"
     | Prop => "Prop"
     | Exp => "ALFA_Exp"
+    | Rul => "ALFA_Rul"
     | Pat => "ALFA_Pat"
     | Typ => "ALFA_Typ"
     | TPat => "ALFA_TPat";
@@ -47,19 +51,21 @@ module DrvSort = {
     | Ctx => "context"
     | Prop => "proposition"
     | Exp => "ALFA expression"
+    | Rul => "ALFA rule"
     | Pat => "ALFA pattern"
     | Typ => "ALFA type"
     | TPat => "ALFA type pattern";
 
   let detail_sort: list(string) => t =
     fun
-    | [".val"] => Jdmt
     | ["val", "end"] => Jdmt
-    | ["eval", "to"] => Jdmt
     | ["|-"] => Jdmt
-    | ["$>"] => Jdmt
+    | ["\\=/"] => Jdmt
     | ["[]"] => Ctx
     | ["[", _] => Ctx
+    | [",", ",", _] => Ctx //TODO(zhiyao): not sufficient
+    | ["@"] => Ctx
+    | ["::"] => Ctx
     | _ => Exp;
 };
 

src/haz3lcore/lang/term/Drv.re

@@ -1,5 +1,6 @@
 include Term.Drv;
 module Exp = Term.ALFA_Exp;
+module Rul = Term.ALFA_Rul;
 module Pat = Term.ALFA_Pat;
 module Typ = Term.ALFA_Typ;
 module TPat = Term.ALFA_TPat;