Theorem keyword

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,9 @@ let rec ground_cases_of = (ty: Typ.t): ground_cases => {
   | String
   | Var(_)
   | Rec(_)
+  | Type(_, {term: Unknown(_), _})
   | Forall(_, {term: Unknown(_), _})
+  | Equals({term: EmptyHole, _}, {term: EmptyHole, _})
   | Arrow({term: Unknown(_), _}, {term: Unknown(_), _})
   | List({term: Unknown(_), _}) => Ground
   | Parens(ty) => ground_cases_of(ty)
@@ -79,7 +88,9 @@ 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
+  | Type(_) => grounded_Type
   | Forall(_) => grounded_Forall
+  | Equals(_) => grounded_Equals
   | List(_) => grounded_List
   | 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(_)
@@ -120,6 +121,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
@@ -273,7 +273,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);
@@ -317,6 +317,39 @@ let rec elaborate = (m: Statics.Map.t, uexp: UExp.t): (DHExp.t, Typ.t) => {
         let fixf = FixF(p, fresh_cast(def, ty2, ty1), None) |> DHExp.fresh;
         Exp.Let(p, fixf, body) |> rewrap |> cast_from(ty);
       };
+    | 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
+          | TypFun(tpat, e, _) => TypFun(tpat, e, 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.Theorem(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.Theorem(p, fixf, body) |> rewrap |> cast_from(ty);
+      };
     | FixF(p, e, env) =>
       let (p', typ) = elaborate_pattern(m, p);
       let (e', tye) = elaborate(m, e);
@@ -356,7 +389,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(

src/haz3lcore/dynamics/FilterMatcher.re

@@ -247,6 +247,10 @@ let rec matches_exp =
       }
     | (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)
     | (TypAp(_), _) => false
@@ -371,6 +375,56 @@ and matches_fun =
   };
 }
 
+and matches_pat = (d: Pat.t, f: Pat.t): bool => {
+  switch (d |> DHPat.term_of, f |> DHPat.term_of) {
+  // Matt: I'm not sure what the exact semantics of matching should be here.
+  | (Parens(x), _) => matches_pat(x, f)
+  | (_, Parens(x)) => matches_pat(d, x)
+  | (Cast(x, _, _), _) => matches_pat(x, f)
+  | (_, Cast(x, _, _)) => matches_pat(d, x)
+  | (_, EmptyHole) => true
+  | (MultiHole(_), MultiHole(_)) => true
+  | (MultiHole(_), _) => false
+  | (Wild, Wild) => true
+  | (Wild, _) => false
+  | (Int(dv), Int(fv)) => dv == fv
+  | (Int(_), _) => false
+  | (Float(dv), Float(fv)) => dv == fv
+  | (Float(_), _) => false
+  | (Bool(dv), Bool(fv)) => dv == fv
+  | (Bool(_), _) => false
+  | (String(dv), String(fv)) => dv == fv
+  | (String(_), _) => false
+  | (ListLit(dl), ListLit(fl)) =>
+    switch (
+      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
+    ) {
+    | exception (Invalid_argument(_)) => false
+    | res => res
+    }
+  | (ListLit(_), _) => false
+  | (Constructor(dt, _), Constructor(ft, _)) => dt == ft
+  | (Constructor(_), _) => false
+  | (Var(_), Var(_)) => true
+  | (Var(_), _) => false
+  | (Tuple(dl), Tuple(fl)) =>
+    switch (
+      List.fold_left2((res, d, f) => res && matches_pat(d, f), true, dl, fl)
+    ) {
+    | exception (Invalid_argument(_)) => false
+    | res => res
+    }
+  | (Tuple(_), _) => false
+  | (Ap(d1, d2), Ap(f1, f2)) => matches_pat(d1, f1) && matches_pat(d2, f2)
+  | (Ap(_), _) => false
+  | (Cons(d1, d2), Cons(f1, f2)) =>
+    matches_pat(d1, f1) && matches_pat(d2, f2)
+  | (Cons(_), _) => false
+  | (EmptyHole, _) => false
+  | (Invalid(_), _) => false
+  };
+}
+
 and matches_typ = (d: Typ.t, f: Typ.t) => {
   Typ.eq(d, f);
 }

src/haz3lcore/dynamics/Substitution.re

@@ -18,6 +18,15 @@ let rec subst_var = (m, d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t => {
     let dbody = subst_var(m, d1, x, dbody);
     let filter = subst_var_filter(m, d1, x, filter);
     Filter(filter, dbody) |> 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;
   | Let(dp, d3, d4) =>
     let d3 = subst_var(m, d1, x, d3);
     let d4 =

src/haz3lcore/dynamics/Transition.re

@@ -192,6 +192,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);
@@ -299,8 +310,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/TypeAssignment.re

@@ -143,6 +143,10 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     let* ty1 = typ_of_dhexp(ctx, m, de);
     let* ctx = dhpat_extend_ctx(dhp, ty1, ctx);
     typ_of_dhexp(ctx, m, db);
+  | Theorem(dhp, de, db) =>
+    let* ty1 = typ_of_dhexp(ctx, m, de);
+    let* ctx = dhpat_extend_ctx(dhp, ty1, ctx);
+    typ_of_dhexp(ctx, m, db);
   | FixF(dhp, d, env) =>
     let* ty_p = dhpat_synthesize(dhp, ctx);
     let* ctx =
@@ -167,13 +171,13 @@ and typ_of_dhexp = (ctx: Ctx.t, m: Statics.Map.t, dh: DHExp.t): option(Typ.t) =>
     let ctx =
       Ctx.extend_tvar(ctx, {name, id: TPat.rep_id(utpat), kind: Abstract});
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(utpat, ty) |> Typ.temp);
+    Some(Typ.Type(utpat, ty) |> Typ.temp);
   | TypFun(_, d, _) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    Some(Typ.Forall(Var("?") |> TPat.fresh, ty) |> Typ.temp);
+    Some(Typ.Type(Var("?") |> TPat.fresh, ty) |> Typ.temp);
   | TypAp(d, ty1) =>
     let* ty = typ_of_dhexp(ctx, m, d);
-    let* (name, ty2) = Typ.matched_forall_strict(ctx, ty);
+    let* (name, ty2) = Typ.matched_type_strict(ctx, ty);
     switch (name) {
     | Some(name) => Some(Typ.subst(ty1, name, ty2))
     | None => Some(ty2)

src/haz3lcore/dynamics/Unboxing.re

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

src/haz3lcore/lang/Form.re

@@ -103,6 +103,9 @@ let keywords = [
   "if",
   "then",
   "else",
+  "theorem",
+  "proof",
+  "forall",
 ];
 let reserved_keywords = ["of", "when", "with", "switch", "match"];
 let keyword_regexp = regexp("^(" ++ String.concat("|", keywords) ++ ")$");
@@ -297,6 +300,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]))),
+  ("prop-equals", 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]))),
@@ -311,7 +315,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]))),
+  ("forall-type", mk(ds, ["type", "->"], mk_pre(P.fun_, Typ, [TPat]))),
+  ("forall-term", mk(ds, ["forall", "->"], mk_pre(P.fun_, Typ, [Pat]))),
   ("rec", mk(ds, ["rec", "->"], mk_pre(P.fun_, Typ, [TPat]))),
   (
     "rule",
@@ -325,6 +330,10 @@ let forms: list((string, t)) = [
   ("filter_debug", mk(ds, ["debug", "in"], mk_pre(P.let_, Exp, [Exp]))),
   // TRIPLE DELIMITERS
   ("let_", mk(ds, ["let", "=", "in"], mk_pre(P.let_, Exp, [Pat, Exp]))),
+  (
+    "theorem_",
+    mk(ds, ["theorem", "proof", "in"], mk_pre(P.let_, Exp, [Pat, Exp])),
+  ),
   (
     "type_alias",
     mk(ds, ["type", "=", "in"], mk_pre(P.let_, Exp, [TPat, Typ])),
@@ -333,7 +342,7 @@ let forms: list((string, t)) = [
 ];
 
 let get: String.t => t =
-  name => Util.ListUtil.assoc_err(name, forms, "Forms.get");
+  name => Util.ListUtil.assoc_err(name, forms, "Form.get: " ++ name);
 
 let delims: list(Token.t) =
   forms