Adds theorem and proof construct [new base]

src/haz3lcore/assistant/AssistantForms.re

@@ -27,7 +27,7 @@ module Typ = {
     ("fun" ++ leading_expander, Arrow(unk, unk) |> Typ.fresh),
     (
       "typfun" ++ leading_expander,
-      Forall(Var("") |> TPat.fresh, unk) |> Typ.fresh,
+      Type(Var("") |> TPat.fresh, unk) |> Typ.fresh,
     ),
     ("if" ++ leading_expander, unk),
     ("let" ++ leading_expander, unk),

src/haz3lcore/dynamics/Casts.re

@@ -32,10 +32,17 @@ let grounded_Arrow =
     Arrow(Unknown(Internal) |> Typ.temp, Unknown(Internal) |> Typ.temp)
     |> Typ.temp,
   );
+let grounded_Type =
+  NotGroundOrHole(
+    Type(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp,
+  );
 let grounded_Forall =
   NotGroundOrHole(
-    Forall(EmptyHole |> TPat.fresh, Unknown(Internal) |> Typ.temp)
-    |> Typ.temp,
+    Forall(EmptyHole |> Pat.fresh, Unknown(Internal) |> Typ.temp) |> Typ.temp,
+  );
+let grounded_Equals =
+  NotGroundOrHole(
+    Equals(EmptyHole |> Exp.fresh, EmptyHole |> Exp.fresh) |> Typ.temp,
   );
 let grounded_Prod = length =>
   NotGroundOrHole(
@@ -60,7 +67,7 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | String
   | Var(_)
   | Rec(_)
-  | Forall(_, {term: Unknown(_), _})
+  | Type(_, {term: Unknown(_), _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
   | Parens(ty) => ground_cases_of(ty)
@@ -79,8 +86,10 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
     sm |> ConstructorMap.is_ground(is_hole)
       ? Ground : NotGroundOrHole(Sum(grounded_Sum()) |> Typ.temp)
   | Arrow(_, _) => grounded_Arrow
-  | Forall(_) => grounded_Forall
+  | Type(_) => grounded_Type
   | List(_) => grounded_List
+  | Forall(_) => grounded_Forall
+  | Equals(_) => grounded_Equals
   | Ap(_) => failwith("type application in dynamics")
   };
 };

src/haz3lcore/dynamics/DHExp.re

@@ -52,6 +52,7 @@ let rec strip_casts =
         | Seq(_)
         | Filter(_)
         | Let(_)
+        | Theorem(_)
         | FixF(_)
         | TyAlias(_)
         | Fun(_)
@@ -119,6 +120,7 @@ let ty_subst = (s: Typ.t, tpat: TPat.t, exp: t): t => {
           | Closure(_)
           | Seq(_)
           | Let(_)
+          | Theorem(_)
           | Ap(_)
           | BuiltinFun(_)
           | BinOp(_)

src/haz3lcore/dynamics/Elaborator.re

@@ -65,9 +65,9 @@ let elaborated_type = (m: Statics.Map.t, uexp: UExp.t): (Typ.t, Ctx.t, 'a) => {
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
       Typ.Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
-      let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
+      let (tpat, ty) = Typ.matched_type(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Typ.Type(tpat, ty) |> Typ.temp;
     // We need to remove the synswitches from this type.
     | Ana(ana_ty) => Typ.match_synswitch(ana_ty, self_ty)
     };
@@ -92,9 +92,9 @@ let elaborated_pat_type = (m: Statics.Map.t, upat: UPat.t): (Typ.t, Ctx.t) => {
       let (ty1, ty2) = Typ.matched_arrow(ctx, self_ty);
       Typ.Arrow(ty1, ty2) |> Typ.temp;
     | SynTypFun =>
-      let (tpat, ty) = Typ.matched_forall(ctx, self_ty);
+      let (tpat, ty) = Typ.matched_type(ctx, self_ty);
       let tpat = Option.value(tpat, ~default=TPat.fresh(EmptyHole));
-      Typ.Forall(tpat, ty) |> Typ.temp;
+      Typ.Type(tpat, ty) |> Typ.temp;
     | Ana(ana_ty) =>
       switch (prev_synswitch) {
       | None => ana_ty
@@ -270,7 +270,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       let (e', tye) = elaborate(m, e);
       Exp.TypFun(tpat, e', name)
       |> rewrap
-      |> cast_from(Typ.Forall(tpat, tye) |> Typ.temp);
+      |> cast_from(Typ.Type(tpat, tye) |> Typ.temp);
     | Tuple(es) =>
       let (ds, tys) = List.map(elaborate(m), es) |> ListUtil.unzip;
       Exp.Tuple(ds) |> rewrap |> cast_from(Prod(tys) |> Typ.temp);
@@ -281,6 +281,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
            |> Option.map((x: Ctx.var_entry) => x.typ |> Typ.normalize(ctx))
            |> Option.value(~default=Typ.temp(Typ.Unknown(Internal))),
          )
+    | Theorem(p, def, body)
     | Let(p, def, body) =>
       let add_name: (option(string), DHExp.t) => DHExp.t = (
         (name, exp) => {
@@ -352,7 +353,7 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       |> cast_from(Arrow(remaining_arg_ty, tyf2) |> Typ.temp);
     | TypAp(e, ut) =>
       let (e', tye) = elaborate(m, e);
-      let (tpat, tye') = Typ.matched_forall(ctx, tye);
+      let (tpat, tye') = Typ.matched_type(ctx, tye);
       let ut' = Typ.normalize(ctx, ut);
       let tye'' =
         Typ.subst(
@@ -381,6 +382,38 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
       Test(fresh_cast(e', t, Bool |> Typ.temp))
       |> rewrap
       |> cast_from(Prod([]) |> Typ.temp);
+    // | Theorem(p, def, body) =>
+    //   let add_name: (option(string), DHExp.t) => DHExp.t = (
+    //     (name, exp) => {
+    //       let (term, rewrap) = DHExp.unwrap(exp);
+    //       switch (term) {
+    //       | Fun(p, e, ctx, _) => Fun(p, e, ctx, name) |> rewrap
+    //       | _ => exp
+    //       };
+    //     }
+    //   );
+    //   let (p, ty1) = elaborate_pattern(m, p);
+    //   let is_recursive =
+    //     Statics.is_recursive(ctx, p, def, ty1)
+    //     && Pat.get_bindings(p)
+    //     |> Option.get
+    //     |> List.exists(f => VarMap.lookup(co_ctx, f) != None);
+    //   if (!is_recursive) {
+    //     let def = add_name(Pat.get_var(p), def);
+    //     let (def, ty2) = elaborate(m, def);
+    //     let (body, ty) = elaborate(m, body);
+    //     Exp.Let(p, fresh_cast(def, ty2, ty1), body)
+    //     |> rewrap
+    //     |> cast_from(ty);
+    //   } else {
+    //     // TODO: Add names to mutually recursive functions
+    //     // TODO: Don't add fixpoint if there already is one
+    //     let def = add_name(Option.map(s => s ++ "+", Pat.get_var(p)), def);
+    //     let (def, ty2) = elaborate(m, def);
+    //     let (body, ty) = elaborate(m, body);
+    //     let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh;
+    //     Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty);
+    //   };
     | Filter(kind, e) =>
       let (e', t) = elaborate(m, e);
       let kind' =

src/haz3lcore/dynamics/FilterMatcher.re

@@ -192,6 +192,9 @@ let rec matches_exp =
     | (Let(dp, d1, d2), Let(fp, f1, f2)) =>
       matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
     | (Let(_), _) => false
+    | (Theorem(dp, d1, d2), Theorem(fp, f1, f2)) =>
+      matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Theorem(_), _) => false
 
     | (TypAp(d1, t1), TypAp(d2, t2)) =>
       matches_exp(d1, d2) && matches_typ(t1, t2)

src/haz3lcore/dynamics/Substitution.re

@@ -26,6 +26,15 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
         subst_var(m, d1, x, d4);
       };
     Let(dp, d3, d4) |> rewrap;
+  | Theorem(dp, d3, d4) =>
+    let d3 = subst_var(m, d1, x, d3);
+    let d4 =
+      if (DHPat.binds_var(m, x, dp)) {
+        d4;
+      } else {
+        subst_var(m, d1, x, d4);
+      };
+    Theorem(dp, d3, d4) |> rewrap;
   | FixF(y, d3, env) =>
     let env' = Option.map(subst_var_env(m, d1, x), env);
     let d3 =

src/haz3lcore/dynamics/Transition.re

@@ -193,6 +193,17 @@ module Transition = (EV: EV_MODE) => {
         kind: LetBind,
         is_value: false,
       });
+    | Theorem(dp, d1, d2) =>
+      let. _ = otherwise(env, d1 => Theorem(dp, d1, d2) |> rewrap)
+      and. d1' =
+        req_final(req(state, env), d1 => Let1(dp, d1, d2) |> wrap_ctx, d1);
+      let.match env' = (env, matches(dp, d1'));
+      Step({
+        expr: Closure(env', d2) |> fresh,
+        state_update,
+        kind: LetBind,
+        is_value: false,
+      });
     | TypFun(_)
     | Fun(_, _, Some(_), _) =>
       let. _ = otherwise(env, d);
@@ -300,8 +311,8 @@ module Transition = (EV: EV_MODE) => {
         })
       | Cast(
           d'',
-          {term: Forall(tp1, _), _} as t1,
-          {term: Forall(tp2, _), _} as t2,
+          {term: Type(tp1, _), _} as t1,
+          {term: Type(tp2, _), _} as t2,
         ) =>
         /* Rule ITTApCast */
         Step({

src/haz3lcore/dynamics/Unboxing.re

@@ -175,6 +175,7 @@ let rec unbox: type a. (unbox_request(a), DHExp.t) => unboxed(a) =
         _,
         Invalid(_) | EmptyHole | MultiHole(_) | DynamicErrorHole(_) | Var(_) |
         Let(_) |
+        Theorem(_) |
         Fun(_, _, _, None) |
         FixF(_) |
         TyAlias(_) |

src/haz3lcore/lang/Form.re

@@ -104,8 +104,11 @@ let keywords = [
   "let",
   "in",
   "type",
+  "forall",
   "case",
   "test",
+  "theorem",
+  "proof",
   "if",
   "then",
   "else",
@@ -298,6 +301,7 @@ let forms: list((string, t)) = [
   ("parens_exp", mk(ii, ["(", ")"], mk_op(Exp, [Exp]))),
   ("parens_pat", mk(ii, ["(", ")"], mk_op(Pat, [Pat]))),
   ("parens_typ", mk(ii, ["(", ")"], mk_op(Typ, [Typ]))),
+  ("pequals", mk(ii, ["{", "=", "}"], mk_op(Typ, [Exp, Exp]))),
   ("ap_exp_empty", mk(ii, ["()"], mk_post(P.ap, Exp, []))),
   ("ap_exp", mk(ii, ["(", ")"], mk_post(P.ap, Exp, [Exp]))),
   ("ap_pat", mk(ii, ["(", ")"], mk_post(P.ap, Pat, [Pat]))),
@@ -312,7 +316,8 @@ let forms: list((string, t)) = [
   ("fun_", mk(ds, ["fun", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   ("fix", mk(ds, ["fix", "->"], mk_pre(P.fun_, Exp, [Pat]))),
   ("typfun", mk(ds, ["typfun", "->"], mk_pre(P.fun_, Exp, [TPat]))),
-  ("forall", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [TPat]))),
+  ("type", mk(ds, ["type", "->"], mk_pre(P.fun_, Typ, [TPat]))),
+  ("forall", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [Pat]))),
   ("rec", mk(ds, ["rec", "->"], mk_pre(P.fun_, Typ, [TPat]))),
   (
     "rule",
@@ -331,6 +336,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", "proof", "in"], mk_pre(P.let_, Exp, [Pat, Exp])),
+  ),
 ];
 
 let get: String.t => t =