task(2/7): entail pattern supported

src/haz3lcore/dynamics/DH.re

@@ -39,6 +39,7 @@ module rec DHExp: {
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
+    | Entail(t, t)
     | Tuple(list(t))
     | Prj(t, int)
     | Constructor(string)
@@ -99,6 +100,7 @@ module rec DHExp: {
     | ListLit(MetaVar.t, MetaVarInst.t, Typ.t, list(t))
     | Cons(t, t)
     | ListConcat(t, t)
+    | Entail(t, t)
     | Tuple(list(t))
     | Prj(t, int)
     | Constructor(string)
@@ -144,6 +146,7 @@ module rec DHExp: {
     | ListLit(_) => "ListLit"
     | Cons(_, _) => "Cons"
     | ListConcat(_, _) => "ListConcat"
+    | Entail(_, _) => "Entail"
     | Tuple(_) => "Tuple"
     | Prj(_) => "Prj"
     | Constructor(_) => "Constructor"
@@ -180,6 +183,7 @@ module rec DHExp: {
     | Prj(d, n) => Prj(strip_casts(d), n)
     | Cons(d1, d2) => Cons(strip_casts(d1), strip_casts(d2))
     | ListConcat(d1, d2) => ListConcat(strip_casts(d1), strip_casts(d2))
+    | Entail(a, b) => Entail(strip_casts(a), strip_casts(b))
     | ListLit(a, b, c, ds) => ListLit(a, b, c, List.map(strip_casts, ds))
     | NonEmptyHole(err, u, i, d) => NonEmptyHole(err, u, i, strip_casts(d))
     | Sequence(a, b) => Sequence(strip_casts(a), strip_casts(b))
@@ -262,6 +266,8 @@ module rec DHExp: {
       fast_equal(d11, d12) && fast_equal(d21, d22)
     | (ListConcat(d11, d21), ListConcat(d12, d22)) =>
       fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (Entail(d11, d21), Entail(d12, d22)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22)
     | (Tuple(ds1), Tuple(ds2)) =>
       List.length(ds1) == List.length(ds2)
       && List.for_all2(fast_equal, ds1, ds2)
@@ -306,6 +312,7 @@ module rec DHExp: {
     | (BuiltinFun(_), _)
     | (Cons(_), _)
     | (ListConcat(_), _)
+    | (Entail(_), _)
     | (ListLit(_), _)
     | (Tuple(_), _)
     | (Prj(_), _)

src/haz3lcore/dynamics/Elaborator.re

@@ -105,6 +105,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     | BinFloatOp(_)
     | BinStringOp(_)
     | BinPropOp(_)
+    | Entail(_)
     | Test(_) => DHExp.cast(d, self_ty, ana_ty)
     };
   };
@@ -171,6 +172,10 @@ let rec dhexp_of_uexp =
         let* dc1 = dhexp_of_uexp(m, e1);
         let+ dc2 = dhexp_of_uexp(m, e2);
         DHExp.ListConcat(dc1, dc2);
+      | Entail(e1, e2) =>
+        let* dc1 = dhexp_of_uexp(m, e1);
+        let+ dc2 = dhexp_of_uexp(m, e2);
+        DHExp.Entail(dc1, dc2);
       | UnOp(Meta(Unquote), e) =>
         switch (e.term) {
         | Var("e") when in_filter => Some(Constructor("$e"))

src/haz3lcore/dynamics/EvalCtx.re

@@ -36,6 +36,8 @@ type cls =
   | Cons2
   | ListConcat1
   | ListConcat2
+  | Entail1
+  | Entail2
   | Prj
   | NonEmptyHole
   | Cast
@@ -89,6 +91,8 @@ type t =
   | Cons2(DHExp.t, t)
   | ListConcat1(t, DHExp.t)
   | ListConcat2(DHExp.t, t)
+  | Entail1(t, DHExp.t)
+  | Entail2(DHExp.t, t)
   | Prj(t, int)
   | NonEmptyHole(ErrStatus.HoleReason.t, MetaVar.t, HoleInstanceId.t, t)
   | Cast(t, Typ.t, Typ.t)
@@ -152,6 +156,8 @@ let rec fuzzy_mark =
   | Cons2(_)
   | ListConcat1(_)
   | ListConcat2(_)
+  | Entail1(_)
+  | Entail2(_)
   | Prj(_)
   | NonEmptyHole(_)
   | InvalidOperation(_)

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -105,6 +105,11 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     ListConcat(d1', d2') |> return;
 
+  | Entail(d1, d2) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    Entail(d1', d2') |> return;
+
   | ListLit(a, b, c, ds) =>
     let+ ds =
       ds
@@ -357,6 +362,11 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     ListConcat(d1', d2') |> return;
 
+  | Entail(d1, d2) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    Entail(d1', d2') |> return;
+
   | ListLit(a, b, c, ds) =>
     let+ ds =
       ds
@@ -491,6 +501,7 @@ let rec track_children_of_hole =
   | BinFloatOp(_, d1, d2)
   | BinStringOp(_, d1, d2)
   | BinPropOp(_, d1, d2)
+  | Entail(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

@@ -291,6 +291,12 @@ let rec compose = (ctx: EvalCtx.t, d: DHExp.t): DHExp.t => {
     | ListConcat2(d1, ctx) =>
       let d2 = compose(ctx, d);
       ListConcat(d1, d2);
+    | Entail1(ctx, d2) =>
+      let d1 = compose(ctx, d);
+      Entail(d1, d2);
+    | Entail2(d1, ctx) =>
+      let d2 = compose(ctx, d);
+      Entail(d1, d2);
     | Tuple(ctx, (ld, rd)) =>
       let d = compose(ctx, d);
       Tuple(rev_concat(ld, [d, ...rd]));

src/haz3lcore/dynamics/FilterMatcher.re

@@ -180,6 +180,10 @@ let rec matches_exp =
 
   | (ListConcat(_), _) => false
 
+  | (Entail(dctx, dprop), Entail(fctx, fprop)) =>
+    matches_exp(env, dctx, fctx) && matches_exp(env, dprop, fprop)
+  | (Entail(_), _) => false
+
   | (
       ConsistentCase(Case(dscrut, drule, _)),
       ConsistentCase(Case(fscrut, frule, _)),

src/haz3lcore/dynamics/PatternMatch.re

@@ -273,6 +273,7 @@ and matches_cast_Sum =
   | Closure(_)
   | Filter(_)
   | Cons(_)
+  | Entail(_)
   | ListConcat(_) => DoesNotMatch
   }
 and matches_cast_Tuple =
@@ -360,6 +361,7 @@ and matches_cast_Tuple =
   | ListLit(_) => DoesNotMatch
   | Cons(_, _) => DoesNotMatch
   | ListConcat(_) => DoesNotMatch
+  | Entail(_) => DoesNotMatch
   | Prj(_) => IndetMatch
   | Constructor(_) => DoesNotMatch
   | ConsistentCase(_)
@@ -491,6 +493,7 @@ and matches_cast_Cons =
   | BinStringOp(_)
   | BinPropOp(_)
   | ListConcat(_)
+  | Entail(_)
   | BuiltinFun(_) => DoesNotMatch
   | BoolLit(_) => DoesNotMatch
   | IntLit(_) => DoesNotMatch

src/haz3lcore/dynamics/Stepper.re

@@ -152,6 +152,12 @@ let rec matches =
     | ListConcat2(d1, ctx) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       ListConcat2(d1, ctx);
+    | Entail1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Entail1(ctx, d2);
+    | Entail2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Entail2(d1, ctx);
     | Prj(ctx, n) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Prj(ctx, n);
@@ -413,6 +419,7 @@ let get_justification: step_kind => string =
   | Conditional(_) => "conditional"
   | ListCons => "list manipulation"
   | ListConcat => "list manipulation"
+  | Entail => "entailment"
   | CaseApply => "case selection"
   | CaseNext => "case discarding"
   | Projection => "projection" // TODO(Matt): We don't want to show projection to the user

src/haz3lcore/dynamics/Substitution.re

@@ -74,6 +74,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);
     ListConcat(d3, d4);
+  | Entail(d3, d4) =>
+    let d3 = subst_var(d1, x, d3);
+    let d4 = subst_var(d1, x, d4);
+    Entail(d3, d4);
   | Tuple(ds) => Tuple(List.map(subst_var(d1, x), ds))
   | Prj(d, n) => Prj(subst_var(d1, x, d), n)
   | BinBoolOp(op, d3, d4) =>

src/haz3lcore/dynamics/Transition.re

@@ -67,6 +67,7 @@ type step_kind =
   | Projection
   | ListCons
   | ListConcat
+  | Entail
   | CaseApply
   | CaseNext
   | CompleteClosure
@@ -550,6 +551,17 @@ module Transition = (EV: EV_MODE) => {
         })
       | _ => Indet
       };
+    | Entail(dctx, dprop) =>
+      let. _ = otherwise(env, (dctx, dprop) => Entail(dctx, dprop))
+      and. dctx' =
+        req_final(req(state, env), dctx => Entail1(dctx, dprop), dctx)
+      and. dprop' =
+        req_final(req(state, env), dprop => Entail2(dctx, dprop), dprop);
+      Step({
+        apply: () => Entail(dctx', dprop'),
+        kind: CompleteFilter,
+        value: true,
+      });
     | ListLit(u, i, ty, ds) =>
       let. _ = otherwise(env, ds => ListLit(u, i, ty, ds))
       and. _ =
@@ -691,6 +703,7 @@ let should_hide_step = (~settings: CoreSettings.Evaluation.t) =>
   | BinPropOp(_)
   | ListCons
   | ListConcat
+  | Entail
   | CaseApply
   | Projection // TODO(Matt): We don't want to show projection to the user
   | Skip

src/haz3lcore/lang/Form.re

@@ -259,7 +259,7 @@ let forms: list((string, t)) = [
   ("prop_and", mk_infix("/\\", Exp, P.prop_and)),
   ("prop_or", mk_infix("\\/", Exp, P.prop_or)),
   ("prop_implies", mk_infix("==>", Exp, P.prop_implies)),
-  ("judgement_entail", mk_infix("|-", Exp, P.judgement_entail)),
+  ("entail", mk_infix("|-", Exp, P.entail)),
   ("lt", mk_infix("<", Exp, P.eqs)),
   ("gt", mk_infix(">", Exp, P.eqs)),
   ("not_equals", mk_infix("!=", Exp, P.eqs)),

src/haz3lcore/lang/Precedence.re

@@ -26,7 +26,7 @@ let fun_ = 14;
 let prop_and = 15;
 let prop_or = 16;
 let prop_implies = 17;
-let judgement_entail = 18;
+let entail = 18;
 let prod = 19;
 let semi = 20;
 let let_ = 21;

src/haz3lcore/statics/MakeTerm.re

@@ -274,6 +274,7 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
           | (["==>"], []) => BinOp(Prop(Implies), l, r)
           | (["|>"], []) => Pipeline(l, r)
           | (["@"], []) => ListConcat(l, r)
+          | (["|-"], []) => Entail(l, r)
           | _ => hole(tm)
           },
         )

src/haz3lcore/statics/Statics.re

@@ -254,6 +254,14 @@ and uexp_to_info_map =
       ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]),
       m,
     );
+  | Entail(e1, e2) =>
+    let (e1, m) = go(~mode=Ana(List(Prop)), e1, m);
+    let (e2, m) = go(~mode=Ana(Prop), e2, m);
+    add(
+      ~self=Just(Judgement),
+      ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]),
+      m,
+    );
   | Var(name) =>
     add'(
       ~self=Self.of_exp_var(ctx, name),

src/haz3lcore/statics/Term.re

@@ -415,7 +415,8 @@ module UExp = {
     | UnOp(op_un)
     | BinOp(op_bin)
     | Match
-    | ListConcat;
+    | ListConcat
+    | Entail;
 
   let hole = (tms: list(any)): term =>
     switch (tms) {
@@ -459,6 +460,7 @@ module UExp = {
     | Parens(_) => Parens
     | Cons(_) => Cons
     | ListConcat(_) => ListConcat
+    | Entail(_) => Entail
     | UnOp(op, _) => UnOp(op)
     | BinOp(op, _, _) => BinOp(op)
     | Match(_) => Match;
@@ -564,6 +566,7 @@ module UExp = {
     | Parens => "Parenthesized expression"
     | Cons => "Cons"
     | ListConcat => "List Concatenation"
+    | Entail => "Entailment"
     | BinOp(op) => show_binop(op)
     | UnOp(op) => show_unop(op)
     | Match => "Case expression";
@@ -597,6 +600,7 @@ module UExp = {
     | Filter(_)
     | Cons(_)
     | ListConcat(_)
+    | Entail(_)
     | UnOp(_)
     | BinOp(_)
     | Match(_)
@@ -635,6 +639,7 @@ module UExp = {
       | Filter(_)
       | Cons(_)
       | ListConcat(_)
+      | Entail(_)
       | UnOp(_)
       | BinOp(_)
       | Match(_)
@@ -687,6 +692,7 @@ module UExp = {
       | Test(_)
       | Cons(_)
       | ListConcat(_)
+      | Entail(_)
       | UnOp(_)
       | BinOp(_)
       | Match(_)

src/haz3lcore/statics/TermBase.re

@@ -135,6 +135,7 @@ and UExp: {
     | Parens
     | Cons
     | ListConcat
+    | Entail
     | UnOp(op_un)
     | BinOp(op_bin)
     | Match;
@@ -174,6 +175,7 @@ and UExp: {
     | Parens(t) // (
     | Cons(t, t)
     | ListConcat(t, t)
+    | Entail(t, t)
     | UnOp(op_un, t)
     | BinOp(op_bin, t, t)
     | Match(t, list((UPat.t, t)))
@@ -285,6 +287,7 @@ and UExp: {
     | Parens
     | Cons
     | ListConcat
+    | Entail
     | UnOp(op_un)
     | BinOp(op_bin)
     | Match;
@@ -324,6 +327,7 @@ and UExp: {
     | Parens(t) // (
     | Cons(t, t)
     | ListConcat(t, t)
+    | Entail(t, t)
     | UnOp(op_un, t)
     | BinOp(op_bin, t, t)
     | Match(t, list((UPat.t, t)))

src/haz3lcore/zipper/EditorUtil.re

@@ -67,6 +67,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Parens(_)
   | Cons(_)
   | ListConcat(_)
+  | Entail(_)
   | UnOp(_)
   | BinOp(_)
   | Match(_) => TermBase.UExp.{ids: [Id.mk()], term: Seq(e1, e2)}