Adds theorem and proof construct

src/haz3lcore/dynamics/Elaborator.re

@@ -199,6 +199,7 @@ let rec dhexp_of_uexp =
       | Test(test) =>
         let+ dtest = dhexp_of_uexp(m, test);
         DHExp.Test(id, dtest);
+      | Theorem(_, _, e) => dhexp_of_uexp(m, e)
       | Filter(act, cond, body) =>
         let* dcond = dhexp_of_uexp(~in_filter=true, m, cond);
         let+ dbody = dhexp_of_uexp(m, body);

src/haz3lcore/lang/Form.re

@@ -103,6 +103,7 @@ let keywords = [
   "type",
   "case",
   "test",
+  "theorem",
   "if",
   "then",
   "else",
@@ -318,6 +319,11 @@ let forms: list((string, t)) = [
     mk(ds, ["type", "=", "in"], mk_pre(P.let_, Exp, [TPat, Typ])),
   ),
   ("if_", mk(ds, ["if", "then", "else"], mk_pre(P.if_, Exp, [Exp, Exp]))),
+  (
+    "theorem_",
+    // use same precedence for Theorem and Let, using let_ directly
+    mk(ds, ["theorem", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp])),
+  ),
 ];
 
 let get: String.t => t =

src/haz3lcore/lang/Precedence.re

@@ -31,7 +31,6 @@ let rule_arr = 19;
 let rule_pre = 20;
 let rule_sep = 21;
 let case_ = 22;
-
 let min = 23;
 
 let compare = (p1: t, p2: t): int =>

src/haz3lcore/statics/MakeTerm.re

@@ -185,6 +185,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["!"], []) => UnOp(Bool(Not), r)
         | (["fun", "->"], [Pat(pat)]) => Fun(pat, r)
         | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r)
+        | (["theorem", "=", "in"], [Pat(pat), Exp(def)]) =>
+          Theorem(pat, def, r)
         | (["hide", "in"], [Exp(filter)]) =>
           Filter((Eval, One), filter, r)
         | (["eval", "in"], [Exp(filter)]) =>

src/haz3lcore/statics/Statics.re

@@ -274,6 +274,14 @@ and uexp_to_info_map =
   | Test(e) =>
     let (e, m) = go(~mode=Ana(Bool), e, m);
     add(~self=Just(Prod([])), ~co_ctx=e.co_ctx, m);
+  | Theorem(_, def, body) =>
+    let (def, m) = go(~mode=Syn, def, m);
+    let (body, m) = go(~mode, body, m);
+    add(
+      ~self=Just(body.ty),
+      ~co_ctx=CoCtx.union([def.co_ctx, body.co_ctx]),
+      m,
+    );
   | Filter(_, cond, body) =>
     let (cond, m) = go(~mode, cond, m, ~is_in_filter=true);
     let (body, m) = go(~mode, body, m);

src/haz3lcore/statics/Term.re

@@ -447,7 +447,8 @@ module UExp = {
     | UnOp(op_un)
     | BinOp(op_bin)
     | Match
-    | ListConcat;
+    | ListConcat
+    | Theorem;
 
   let hole = (tms: list(any)): term =>
     switch (tms) {
@@ -488,7 +489,8 @@ module UExp = {
     | ListConcat(_) => ListConcat
     | UnOp(op, _) => UnOp(op)
     | BinOp(op, _, _) => BinOp(op)
-    | Match(_) => Match;
+    | Match(_) => Match
+    | Theorem(_) => Theorem;
 
   let show_op_un_meta: op_un_meta => string =
     fun
@@ -582,7 +584,8 @@ module UExp = {
     | ListConcat => "List Concatenation"
     | BinOp(op) => show_binop(op)
     | UnOp(op) => show_unop(op)
-    | Match => "Case expression";
+    | Match => "Case expression"
+    | Theorem => "Theorem";
 
   let rec is_fun = (e: t) => {
     switch (e.term) {
@@ -612,6 +615,7 @@ module UExp = {
     | UnOp(_)
     | BinOp(_)
     | Match(_)
+    | Theorem(_)
     | Constructor(_) => false
     };
   };
@@ -646,6 +650,7 @@ module UExp = {
       | UnOp(_)
       | BinOp(_)
       | Match(_)
+      | Theorem(_)
       | Constructor(_) => false
       }
     );

src/haz3lcore/statics/TermBase.re

@@ -122,6 +122,7 @@ and UExp: {
     | If
     | Seq
     | Test
+    | Theorem
     | Filter
     | Parens
     | Cons
@@ -152,6 +153,7 @@ and UExp: {
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
+    | Theorem(UPat.t, t, t) // NOTE(nishant): diff types?
     | Filter(FilterAction.t, t, t)
     | Parens(t) // (
     | Cons(t, t)
@@ -253,6 +255,7 @@ and UExp: {
     | If
     | Seq
     | Test
+    | Theorem
     | Filter
     | Parens
     | Cons
@@ -283,6 +286,7 @@ and UExp: {
     | If(t, t, t)
     | Seq(t, t)
     | Test(t)
+    | Theorem(UPat.t, t, t) // NOTE(nishant): diff types?
     | Filter(FilterAction.t, t, t)
     | Parens(t) // (
     | Cons(t, t)

src/haz3lcore/zipper/EditorUtil.re

@@ -75,6 +75,9 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Let(p, edef, ebody) =>
     let ebody' = append_exp(ebody, e2);
     TermBase.UExp.{ids: e1.ids, term: Let(p, edef, ebody')};
+  | Theorem(name, edef, ebody) =>
+    let ebody' = append_exp(ebody, e2);
+    TermBase.UExp.{ids: e1.ids, term: Theorem(name, edef, ebody')};
   | TyAlias(tp, tdef, ebody) =>
     let ebody' = append_exp(ebody, e2);
     TermBase.UExp.{ids: e1.ids, term: TyAlias(tp, tdef, ebody')};

src/haz3lschool/SyntaxTest.re

@@ -50,6 +50,9 @@ let rec var_mention = (name: string, uexp: Term.UExp.t): bool => {
   | Let(p, def, body) =>
     find_var_upat(name, p)
       ? false : var_mention(name, def) || var_mention(name, body)
+  | Theorem(p, def, body) =>
+    find_var_upat(name, p)
+      ? false : var_mention(name, def) || var_mention(name, body)
   | Test(u)
   | Parens(u)
   | UnOp(_, u)
@@ -96,6 +99,9 @@ let rec var_applied = (name: string, uexp: Term.UExp.t): bool => {
   | Let(p, def, body) =>
     find_var_upat(name, p)
       ? false : var_applied(name, def) || var_applied(name, body)
+  | Theorem(p, def, body) =>
+    find_var_upat(name, p)
+      ? false : var_applied(name, def) || var_applied(name, body)
   | Test(u)
   | Parens(u)
   | UnOp(_, u)
@@ -181,6 +187,8 @@ let rec find_fn =
   switch (uexp.term) {
   | Let(up, def, body) =>
     l |> find_in_let(name, up, def) |> find_fn(name, body)
+  | Theorem(up, def, body) =>
+    l |> find_in_let(name, up, def) |> find_fn(name, body)
   | ListLit(ul)
   | Tuple(ul) =>
     List.fold_left((acc, u1) => {find_fn(name, u1, acc)}, l, ul)
@@ -248,6 +256,9 @@ let rec tail_check = (name: string, uexp: Term.UExp.t): bool => {
   | Let(p, def, body) =>
     find_var_upat(name, p) || var_mention(name, def)
       ? false : tail_check(name, body)
+  | Theorem(p, def, body) =>
+    find_var_upat(name, p) || var_mention(name, def)
+      ? false : tail_check(name, body)
   | ListLit(l)
   | Tuple(l) =>
     //If l has no recursive calls then true

src/haz3lweb/view/ExplainThis.re

@@ -1641,6 +1641,63 @@ let get_doc =
             ),
           TestExp.tests,
         );
+      // TODO(nishant): add explanation for Theorem(body) here in the style of Test above
+      // TODO(nishant): use p, def somehow (p, def, body)
+      // | Theorem(pat, def, body) =>
+      // let pat = bypass_parens_and_annot_pat(pat);
+      // let pat_id = List.nth(pat.ids, 0);
+      // let def_id = List.nth(def.ids, 0);
+      // let body_id = List.nth(body.ids, 0);
+      // let basic = group_id => {
+      //   get_message(
+      //     ~colorings=LetExp.let_base_exp_coloring_ids(~pat_id, ~def_id),
+      //     ~format=
+      //       Some(
+      //         msg =>
+      //           Printf.sprintf(
+      //             Scanf.format_from_string(msg, "%s%s"),
+      //             Id.to_string(def_id),
+      //             Id.to_string(pat_id),
+      //           ),
+      //       ),
+      //     group_id,
+      //   );
+      // };
+      // | Theorem(pat, def, body) =>
+      //   let pat = bypass_parens_and_annot_pat(pat);
+      //   let pat_id = List.nth(pat.ids, 0);
+      //   let def_id = List.nth(def.ids, 0);
+      //   let body_id = List.nth(body.ids, 0);
+      //   get_message(
+      //     ~colorings=LetExp.let_base_exp_coloring_ids(~pat_id, ~def_id),
+      //     ~format=
+      //       Some(
+      //         msg =>
+      //           Printf.sprintf(
+      //             Scanf.format_from_string(msg, "%s%s%s"),
+      //             Id.to_string(def_id),
+      //             Id.to_string(pat_id),
+      //             Id.to_string(body_id),
+      //           ),
+      //       ),
+      //     TestExp.tests,
+      //   );
+      | Theorem(_, _, body) =>
+        let body_id = List.nth(body.ids, 0);
+        get_message(
+          // TODO: add coloring for theorem
+          ~colorings=TestExp.test_exp_coloring_ids(~body_id),
+          ~format=
+            Some(
+              msg =>
+                Printf.sprintf(
+                  Scanf.format_from_string(msg, "%s"),
+                  Id.to_string(body_id),
+                ),
+            ),
+          // TODO change below to Theorem equivalent
+          TestExp.tests,
+        );
       | Parens(term) => get_message_exp(term.term) // No Special message?
       | Cons(hd, tl) =>
         let hd_id = List.nth(hd.ids, 0);