task(2/7): prop pattern supported

src/haz3lcore/assistant/AssistantForms.re

@@ -38,7 +38,6 @@ module Typ = {
     ("@", List(unk)),
     (";", unk),
     ("&&", Bool),
-    ("\\/", Bool),
     ("||", Bool),
     ("$==", Bool),
     ("==.", Bool),
@@ -65,6 +64,10 @@ module Typ = {
     ("/.", Float),
     ("**.", Float),
     ("++", String),
+    ("/\\", Prop),
+    ("\\/", Prop),
+    ("==>", Prop),
+    ("|-", Prop),
   ];
 
   let expected: Info.t => Typ.t =

src/haz3lcore/dynamics/Builtins.re

@@ -239,6 +239,22 @@ module Pervasives = {
         | Tuple([PropLit(p1), PropLit(p2)]) => Ok(PropLit(Implies(p1, p2)))
         | d => Error(InvalidBoxedTuple(d)),
       );
+
+    let prop_of: DHExp.t => option(Derivation.Prop.t) =
+      fun
+      | PropLit(p) => Some(p)
+      | _ => None;
+
+    let entail =
+      unary(
+        fun
+        | Tuple([ListLit(_, _, Prop, ctx), PropLit(p)]) =>
+          switch (ctx |> List.map(prop_of) |> Util.OptUtil.sequence) {
+          | Some(ctx) => Ok(JudgementLit(Entail(ctx, p)))
+          | None => Error(InvalidBoxedListLit(List.hd(ctx)))
+          }
+        | d => Error(InvalidBoxedTuple(d)),
+      );
   };
 
   open Impls;
@@ -300,7 +316,10 @@ module Pervasives = {
     |> fn("atom", String, Prop, atom)
     |> fn("and", Prod([Prop, Prop]), Prop, and_)
     |> fn("or", Prod([Prop, Prop]), Prop, or_)
-    |> fn("implies", Prod([Prop, Prop]), Prop, implies);
+    |> fn("implies", Prod([Prop, Prop]), Prop, implies)
+    |> const("truth", Prop, PropLit(Truth))
+    |> const("falsity", Prop, PropLit(Falsity))
+    |> fn("entail", Prod([List(Prop), Prop]), Judgement, entail);
 };
 
 let ctx_init: Ctx.t = {

src/haz3lcore/dynamics/DH.re

@@ -30,10 +30,12 @@ module rec DHExp: {
     | FloatLit(float)
     | StringLit(string)
     | PropLit(Derivation.Prop.t)
+    | JudgementLit(Derivation.Judgement.t)
     | BinBoolOp(TermBase.UExp.op_bin_bool, t, t)
     | BinIntOp(TermBase.UExp.op_bin_int, t, t)
     | BinFloatOp(TermBase.UExp.op_bin_float, t, t)
     | BinStringOp(TermBase.UExp.op_bin_string, t, t)
+    | BinPropOp(TermBase.UExp.op_bin_prop, t, t)
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
@@ -88,10 +90,12 @@ module rec DHExp: {
     | FloatLit(float)
     | StringLit(string)
     | PropLit(Derivation.Prop.t)
+    | JudgementLit(Derivation.Judgement.t)
     | BinBoolOp(TermBase.UExp.op_bin_bool, t, t)
     | BinIntOp(TermBase.UExp.op_bin_int, t, t)
     | BinFloatOp(TermBase.UExp.op_bin_float, t, t)
     | BinStringOp(TermBase.UExp.op_bin_string, t, t)
+    | BinPropOp(TermBase.UExp.op_bin_prop, t, t)
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
@@ -131,10 +135,12 @@ module rec DHExp: {
     | FloatLit(_) => "FloatLit"
     | StringLit(_) => "StringLit"
     | PropLit(_) => "PropLit"
+    | JudgementLit(_) => "JudgementLit"
     | BinBoolOp(_, _, _) => "BinBoolOp"
     | BinIntOp(_, _, _) => "BinIntOp"
     | BinFloatOp(_, _, _) => "BinFloatOp"
     | BinStringOp(_, _, _) => "BinStringOp"
+    | BinPropOp(_, _, _) => "BinPropOp"
     | ListLit(_) => "ListLit"
     | Cons(_, _) => "Cons"
     | ListConcat(_, _) => "ListConcat"
@@ -190,6 +196,7 @@ module rec DHExp: {
     | BinFloatOp(a, b, c) => BinFloatOp(a, strip_casts(b), strip_casts(c))
     | BinStringOp(a, b, c) =>
       BinStringOp(a, strip_casts(b), strip_casts(c))
+    | BinPropOp(a, b, c) => BinPropOp(a, strip_casts(b), strip_casts(c))
     | ConsistentCase(Case(a, rs, b)) =>
       ConsistentCase(
         Case(strip_casts(a), List.map(strip_casts_rule, rs), b),
@@ -210,6 +217,7 @@ module rec DHExp: {
     | FloatLit(_) as d
     | StringLit(_) as d
     | PropLit(_) as d
+    | JudgementLit(_) as d
     | Constructor(_) as d
     | InvalidOperation(_) as d => d
     | IfThenElse(consistent, c, d1, d2) =>
@@ -234,6 +242,8 @@ module rec DHExp: {
     | (StringLit(_), _) => false
     | (PropLit(p1), PropLit(p2)) => Derivation.Prop.eq(p1, p2)
     | (PropLit(_), _) => false
+    | (JudgementLit(j1), JudgementLit(j2)) => Derivation.Judgement.eq(j1, j2)
+    | (JudgementLit(_), _) => false
 
     /* Non-hole forms: recurse */
     | (Test(id1, d1), Test(id2, d2)) => id1 == id2 && fast_equal(d1, d2)
@@ -269,6 +279,8 @@ module rec DHExp: {
       op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
     | (BinStringOp(op1, d11, d21), BinStringOp(op2, d12, d22)) =>
       op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (BinPropOp(op1, d11, d21), BinPropOp(op2, d12, d22)) =>
+      op1 == op2 && fast_equal(d11, d12) && fast_equal(d21, d22)
     | (Cast(d1, ty11, ty21), Cast(d2, ty12, ty22))
     | (FailedCast(d1, ty11, ty21), FailedCast(d2, ty12, ty22)) =>
       fast_equal(d1, d2) && ty11 == ty12 && ty21 == ty22
@@ -301,6 +313,7 @@ module rec DHExp: {
     | (BinIntOp(_), _)
     | (BinFloatOp(_), _)
     | (BinStringOp(_), _)
+    | (BinPropOp(_), _)
     | (Cast(_), _)
     | (FailedCast(_), _)
     | (InvalidOperation(_), _)

src/haz3lcore/dynamics/Elaborator.re

@@ -13,7 +13,8 @@ let exp_binop_of: Term.UExp.op_bin => (Typ.t, (_, _) => DHExp.t) =
   | Int(op) => (Int, ((e1, e2) => BinIntOp(op, e1, e2)))
   | Float(op) => (Float, ((e1, e2) => BinFloatOp(op, e1, e2)))
   | Bool(op) => (Bool, ((e1, e2) => BinBoolOp(op, e1, e2)))
-  | String(op) => (String, ((e1, e2) => BinStringOp(op, e1, e2)));
+  | String(op) => (String, ((e1, e2) => BinStringOp(op, e1, e2)))
+  | Prop(op) => (Prop, ((e1, e2) => BinPropOp(op, e1, e2)));
 
 let fixed_exp_typ = (m: Statics.Map.t, e: Term.UExp.t): option(Typ.t) =>
   switch (Id.Map.find_opt(Term.UExp.rep_id(e), m)) {
@@ -98,10 +99,12 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | FloatLit(_)
     | StringLit(_)
     | PropLit(_)
+    | JudgementLit(_)
     | BinBoolOp(_)
     | BinIntOp(_)
     | BinFloatOp(_)
     | BinStringOp(_)
+    | BinPropOp(_)
     | Test(_) => DHExp.cast(d, self_ty, ana_ty)
     };
   };
@@ -146,6 +149,7 @@ let rec dhexp_of_uexp =
       | Float(n) => Some(FloatLit(n))
       | String(s) => Some(StringLit(s))
       | Prop(p) => Some(PropLit(p))
+      | Judgement(j) => Some(JudgementLit(j))
       | ListLit(es) =>
         let* ds = es |> List.map(dhexp_of_uexp(m)) |> OptUtil.sequence;
         let+ ty = fixed_exp_typ(m, uexp);

src/haz3lcore/dynamics/EvalCtx.re

@@ -23,6 +23,8 @@ type cls =
   | BinFloatOp2
   | BinStringOp1
   | BinStringOp2
+  | BinPropOp1
+  | BinPropOp2
   | IfThenElse1
   | IfThenElse2
   | IfThenElse3
@@ -71,6 +73,8 @@ type t =
   | BinFloatOp2(TermBase.UExp.op_bin_float, DHExp.t, t)
   | BinStringOp1(TermBase.UExp.op_bin_string, t, DHExp.t)
   | BinStringOp2(TermBase.UExp.op_bin_string, DHExp.t, t)
+  | BinPropOp1(TermBase.UExp.op_bin_prop, t, DHExp.t)
+  | BinPropOp2(TermBase.UExp.op_bin_prop, DHExp.t, t)
   | Tuple(t, (list(DHExp.t), list(DHExp.t)))
   | ApBuiltin(string, t)
   | Test(KeywordID.t, t)
@@ -139,6 +143,8 @@ let rec fuzzy_mark =
   | BinFloatOp2(_)
   | BinStringOp1(_)
   | BinStringOp2(_)
+  | BinPropOp1(_)
+  | BinPropOp2(_)
   | Tuple(_)
   | ApBuiltin(_)
   | ListLit(_)

src/haz3lcore/dynamics/EvaluatorError.re

@@ -13,6 +13,7 @@ type t =
   | InvalidBoxedFloatLit(DHExp.t)
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
+  | InvalidBoxedPropLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))

src/haz3lcore/dynamics/EvaluatorError.rei

@@ -11,6 +11,7 @@ type t =
   | InvalidBoxedFloatLit(DHExp.t)
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
+  | InvalidBoxedPropLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -47,6 +47,7 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d |> return
 
   | Sequence(d1, d2) =>
@@ -89,6 +90,11 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     BinStringOp(op, d1', d2') |> return;
 
+  | BinPropOp(op, d1, d2) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    BinPropOp(op, d1', d2') |> return;
+
   | Cons(d1, d2) =>
     let* d1' = pp_eval(d1);
     let* d2' = pp_eval(d2);
@@ -273,6 +279,7 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d |> return
 
   | Test(id, d1) =>
@@ -329,6 +336,11 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     BinStringOp(op, d1', d2') |> return;
 
+  | BinPropOp(op, d1, d2) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    BinPropOp(op, d1', d2') |> return;
+
   | IfThenElse(consistent, c, d1, d2) =>
     let* c' = pp_uneval(env, c);
     let* d1' = pp_uneval(env, d1);
@@ -461,6 +473,7 @@ let rec track_children_of_hole =
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | BuiltinFun(_)
   | BoundVar(_) => hii
   | Test(_, d)
@@ -477,6 +490,7 @@ let rec track_children_of_hole =
   | BinIntOp(_, d1, d2)
   | BinFloatOp(_, d1, d2)
   | BinStringOp(_, d1, d2)
+  | BinPropOp(_, d1, d2)
   | Cons(d1, d2) =>
     let hii = track_children_of_hole(hii, parent, d1);
     track_children_of_hole(hii, parent, d2);

src/haz3lcore/dynamics/EvaluatorStep.re

@@ -273,6 +273,12 @@ let rec compose = (ctx: EvalCtx.t, d: DHExp.t): DHExp.t => {
     | BinStringOp2(op, d1, ctx) =>
       let d2 = compose(ctx, d);
       BinStringOp(op, d1, d2);
+    | BinPropOp1(op, ctx, d2) =>
+      let d1 = compose(ctx, d);
+      BinPropOp(op, d1, d2);
+    | BinPropOp2(op, d1, ctx) =>
+      let d2 = compose(ctx, d);
+      BinPropOp(op, d1, d2);
     | Cons1(ctx, d2) =>
       let d1 = compose(ctx, d);
       Cons(d1, d2);

src/haz3lcore/dynamics/FilterMatcher.re

@@ -78,6 +78,9 @@ let rec matches_exp =
   | (PropLit(dv), PropLit(fv)) => Derivation.Prop.eq(dv, fv)
   | (PropLit(_), _) => false
 
+  | (JudgementLit(dv), JudgementLit(fv)) => Derivation.Judgement.eq(dv, fv)
+  | (JudgementLit(_), _) => false
+
   | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true
   | (Constructor(dt), Constructor(ft)) => dt == ft
   | (Constructor(_), _) => false
@@ -169,6 +172,12 @@ let rec matches_exp =
     && matches_exp(env, d2, f2)
   | (BinStringOp(_), _) => false
 
+  | (BinPropOp(d_op_bin, d1, d2), BinPropOp(f_op_bin, f1, f2)) =>
+    d_op_bin == f_op_bin
+    && matches_exp(env, d1, f1)
+    && matches_exp(env, d2, f2)
+  | (BinPropOp(_), _) => false
+
   | (ListConcat(_), _) => false
 
   | (

src/haz3lcore/dynamics/PatternMatch.re

@@ -246,6 +246,7 @@ and matches_cast_Sum =
   | BinIntOp(_)
   | BinFloatOp(_)
   | BinStringOp(_)
+  | BinPropOp(_)
   | InconsistentBranches(_)
   | EmptyHole(_)
   | NonEmptyHole(_)
@@ -265,6 +266,7 @@ and matches_cast_Sum =
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | ListLit(_)
   | Tuple(_)
   | Sequence(_, _)
@@ -345,6 +347,7 @@ and matches_cast_Tuple =
   | BinIntOp(_, _, _)
   | BinFloatOp(_, _, _)
   | BinStringOp(_)
+  | BinPropOp(_)
   | BoolLit(_) => DoesNotMatch
   | IntLit(_) => DoesNotMatch
   | Sequence(_)
@@ -353,6 +356,7 @@ and matches_cast_Tuple =
   | FloatLit(_) => DoesNotMatch
   | StringLit(_) => DoesNotMatch
   | PropLit(_) => DoesNotMatch
+  | JudgementLit(_) => DoesNotMatch
   | ListLit(_) => DoesNotMatch
   | Cons(_, _) => DoesNotMatch
   | ListConcat(_) => DoesNotMatch
@@ -485,6 +489,7 @@ and matches_cast_Cons =
   | BinIntOp(_, _, _)
   | BinFloatOp(_, _, _)
   | BinStringOp(_)
+  | BinPropOp(_)
   | ListConcat(_)
   | BuiltinFun(_) => DoesNotMatch
   | BoolLit(_) => DoesNotMatch
@@ -494,6 +499,7 @@ and matches_cast_Cons =
   | FloatLit(_) => DoesNotMatch
   | StringLit(_) => DoesNotMatch
   | PropLit(_) => DoesNotMatch
+  | JudgementLit(_) => DoesNotMatch
   | Tuple(_) => DoesNotMatch
   | Prj(_) => IndetMatch
   | Constructor(_) => DoesNotMatch

src/haz3lcore/dynamics/Stepper.re

@@ -122,6 +122,12 @@ let rec matches =
     | BinStringOp2(op, d1, ctx) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       BinStringOp2(op, d1, ctx);
+    | BinPropOp1(op, ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinPropOp1(op, ctx, d2);
+    | BinPropOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinPropOp2(op, d1, ctx);
     | Tuple(ctx, ds) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Tuple(ctx, ds);
@@ -402,6 +408,7 @@ let get_justification: step_kind => string =
   | BinFloatOp(Equals | NotEquals)
   | BinStringOp(Equals) => "check equality"
   | BinStringOp(Concat) => "string manipulation"
+  | BinPropOp(_) => "propositional logic"
   | BinBoolOp(_) => "boolean logic"
   | Conditional(_) => "conditional"
   | ListCons => "list manipulation"

src/haz3lcore/dynamics/Substitution.re

@@ -62,6 +62,7 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
   | FloatLit(_)
   | StringLit(_)
   | PropLit(_)
+  | JudgementLit(_)
   | Constructor(_) => d2
   | ListLit(a, b, c, ds) =>
     ListLit(a, b, c, List.map(subst_var(d1, x), ds))
@@ -91,6 +92,10 @@ let rec subst_var = (d1: DHExp.t, x: Var.t, d2: DHExp.t): DHExp.t =>
     let d3 = subst_var(d1, x, d3);
     let d4 = subst_var(d1, x, d4);
     BinStringOp(op, d3, d4);
+  | BinPropOp(op, d3, d4) =>
+    let d3 = subst_var(d1, x, d3);
+    let d4 = subst_var(d1, x, d4);
+    BinPropOp(op, d3, d4);
   | ConsistentCase(Case(d3, rules, n)) =>
     let d3 = subst_var(d1, x, d3);
     let rules = subst_var_rules(d1, x, rules);