change hasty to typ, check all rules except S/A

src/haz3lcore/derivation/DrvSyntax.re

@@ -215,20 +215,16 @@ let rec repr = (p: int, prop: t): list(string) => {
     |> Aba.join(mk, repr)
     |> Aba.mk(
          _,
-         List.init(List.length(bs) + List.length(as_) - 1, _ =>
-           Unicode.nbsp
-         ),
+         List.init(List.length(bs) + List.length(as_) - 1, _ => " "),
        )
     |> Aba.join(Fun.id, mk)
     |> List.concat;
   let repr_aba_tight = (as_: list(string), bs: list(t)) =>
     Aba.mk(as_, bs) |> Aba.join(mk, repr) |> List.concat;
   let repr_binop = (op: string, a: t, b: t) =>
-    [repr(a), [Unicode.nbsp ++ op ++ Unicode.nbsp], repr(b)] |> List.concat;
-  let repr_postop = (op, a: t) =>
-    [repr(a), [Unicode.nbsp ++ op]] |> List.concat;
-  let repr_preop = (op, a: t) =>
-    [[op ++ Unicode.nbsp], repr(a)] |> List.concat;
+    [repr(a), [" " ++ op ++ " "], repr(b)] |> List.concat;
+  let repr_postop = (op, a: t) => [repr(a), [" " ++ op]] |> List.concat;
+  let repr_preop = (op, a: t) => [[op ++ " "], repr(a)] |> List.concat;
   (
     switch (IdTagged.term_of(prop)) {
     | Hole(s) => Printf.sprintf("[%s]", s) |> mk

src/haz3lcore/derivation/RuleExample.re

@@ -244,15 +244,11 @@ let of_ghost: Rule.t => deduction(t) =
       {concl, prems};
     | S_Var =>
       let concl =
-        !Entail(!Ctx([!HasTy(x(), t1()), !Var("...")]), !Syn(x(), t1()));
+        !Entail(!Ctx([ctx(), !HasTy(x(), t1())]), !Syn(x(), t1()));
       {concl, prems: []};
     | T_Var =>
       let concl =
-        !
-          Entail(
-            !Ctx([!HasTy(x(), t1()), !Var("...")]),
-            !HasTy(x(), t1()),
-          );
+        !Entail(!Ctx([ctx(), !HasTy(x(), t1())]), !HasTy(x(), t1()));
       {concl, prems: []};
     | S_LetAnn =>
       let prems = [
@@ -352,7 +348,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Entail(ctx(), !HasTy(!FixAnn(xp(), t1(), e()), t1()));
       {concl, prems};
     | E_Fix =>
-      let prems = [!Eval(ex(), v())];
+      let prems = [!Eval(!Var("[fix x → e₁/x]e₁"), v())];
       let concl = !Eval(!Fix(xp(), e1()), v());
       {concl, prems};
     | S_Ap =>
@@ -436,7 +432,7 @@ let of_ghost: Rule.t => deduction(t) =
     | E_LetPair =>
       let prems = [
         !Eval(e1(), !Pair(v1(), v2())),
-        !Eval(!Var("[v2/y][v1/x]e1"), v()),
+        !Eval(!Var("[v₂/y][v₁/x]e₁"), v()),
       ];
       let concl = !Eval(!LetPair(xp(), yp(), e1(), e2()), v());
       {concl, prems};
@@ -528,7 +524,10 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Eval(!Case(e(), xp(), e1(), yp(), e2()), v());
       {concl, prems};
     | E_Case_R =>
-      let prems = [!Eval(e(), !InjR(v2())), !Eval(!Var("[v2/y]e2"), v())];
+      let prems = [
+        !Eval(e(), !InjR(v2())),
+        !Eval(!Var("[v₂/y]e₂"), v()),
+      ];
       let concl = !Eval(!Case(e(), xp(), e1(), yp(), e2()), v());
       {concl, prems};
     | T_Roll =>
@@ -553,7 +552,7 @@ let of_ghost: Rule.t => deduction(t) =
       let concl = !Eval(!Unroll(e()), v());
       {concl, prems};
     | Assumption =>
-      let concl = !Entail(!Ctx([!Var("Γ"), !TVar("p")]), p());
+      let concl = !Entail(!Ctx([ctx(), p()]), p());
       {concl, prems: []};
     | And_I =>
       let prems = [!Entail(ctx(), a()), !Entail(ctx(), b())];

src/haz3lcore/derivation/RuleVerify.re

@@ -780,7 +780,7 @@ and check: (t, operation) => result(bool, failure) =
       let$ x2 = unbox(x2, Pat);
       Ok(eq(self, subst(v2.self, x2, subst(v1.self, x1, e.self))));
     | SubstTy((t, a), e) =>
-      let$ a = unbox(a, TVar);
+      let$ a = unbox(a, TPat);
       Ok(eq(self, subst_ty(t.self, a, e.self)));
     | Cons(e, l) =>
       let$ l = unbox_list(l);
@@ -816,9 +816,6 @@ let expect_prems_num: (Rule.t, list(t)) => result(int => t, failure) =
   };
 
 let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) => {
-  prems |> List.iter(p => print_endline(show(p)));
-  print_endline(show(concl));
-
   let$ prems = expect_prems_num(rule, prems);
   // The following symbols / operators are defined for convenience just
   // under this function.
@@ -1023,11 +1020,8 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = ctx >> !!MemHasTy(x, t);
     Ok();
   | T_Var =>
-    let$ (ctx, p) = concl >> Entail(__, __);
-    // TODO: The same as rule Assumption, we make it different by
-    // checking p is a HasTy proposition
-    let$ _ = p >> HasTy(__, __);
-    let$ _ = ctx >> !!Mem(p);
+    let$ (ctx, (x, t)) = concl >> Entail(__, HasTy(__, __));
+    let$ _ = ctx >> !!MemHasTy(x, t);
     Ok();
   | S_LetAnn =>
     let$ (ctx, ((x, t_def, e_def, e_body), t)) =
@@ -1169,7 +1163,9 @@ let verify = (rule: Rule.t, prems: list(t), concl: t): result(unit, failure) =>
     let$ _ = concl >> Eval(Pair(!el, !er), Pair(!vl, !vr));
     Ok();
   | V_Pair =>
-    let$ _ = concl >> Val(Pair(__, __));
+    let$ (vl, vr) = concl >> Val(Pair(__, __));
+    let$ _ = prems(0) >> Val(!vl);
+    let$ _ = prems(1) >> Val(!vr);
     Ok();
   | S_LetPair =>
     let$ (ctx, ((x, y, e_def, e_body), t)) =

src/haz3lcore/lang/Form.re

@@ -109,7 +109,7 @@ let keywords = [
   "val",
   "eval",
   "entail",
-  "hasty",
+  "typ",
   "syn",
   "ana",
 ];
@@ -411,24 +411,24 @@ let forms: list((string, t)) = [
     "hasty",
     mk(
       ds,
-      ["hasty", ":"],
-      mk_pre'(P.semi, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
+      ["typ", ":"],
+      mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
     ),
   ),
   (
     "syn",
     mk(
       ds,
       ["syn", "=>"],
-      mk_pre'(P.semi, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
+      mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
     ),
   ),
   (
     "ana",
     mk(
       ds,
       ["ana", "<="],
-      mk_pre'(P.semi, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
+      mk_pre'(P.fun_, Drv(Prop), Drv(Prop), [Drv(Exp)], Drv(Typ)),
     ),
   ),
   ("and", mk_infix("/\\", Drv(Prop), P.and_)),

src/haz3lcore/statics/MakeTerm.re

@@ -227,7 +227,7 @@ and prop_term: unsorted => (Drv.Prop.term, list(Id.t)) = {
   | Op(([(_id, (["{", "}"], [Pat(var)]))], [])) => ret(Abbr(var))
   | Pre(([(_id, ([t1, t2], [Drv(Exp(l))]))], []), Drv(Typ(r))) as tm =>
     switch (t1, t2) {
-    | ("hasty", ":") => ret(HasTy(l, r))
+    | ("typ", ":") => ret(HasTy(l, r))
     | ("syn", "=>") => ret(Syn(l, r))
     | ("ana", "<=") => ret(Ana(l, r))
     | _ => ret(hole(tm))

src/haz3lweb/explainthis/data/DeductionExp.re

@@ -268,7 +268,7 @@ let mk_explanation_title = () =>
 
 let show_ghost = (t: option(t)) =>
   switch (t) {
-  | Some(t) => DrvSyntax.repr(t)
+  | Some(t) => DrvSyntax.repr(t) |> String.trim
   | None => "?"
   };