task(2/7): entail repr refine

hazelgrove · May 17, 2024 · 82e6358 · 82e6358
1 parent b1ab19c
commit 82e6358
Show file tree

Hide file tree

Showing 7 changed files with 37 additions and 7 deletions.
diff --git a/src/haz3lcore/dynamics/EvalCtx.re b/src/haz3lcore/dynamics/EvalCtx.re
@@ -201,6 +201,8 @@ let rec unwrap = (ctx: t, sel: cls): option(t) => {
   | (Cons2, Cons2(_, c))
   | (ListConcat1, ListConcat1(c, _))
   | (ListConcat2, ListConcat2(_, c))
+  | (Entail1, Entail1(c, _))
+  | (Entail2, Entail2(_, c))
   | (Test, Test(_, c))
   | (Prj, Prj(c, _)) => Some(c)
   | (ListLit(n), ListLit(_, _, _, c, (ld, _)))
@@ -249,7 +251,9 @@ let rec unwrap = (ctx: t, sel: cls): option(t) => {
   | (Sequence1, Sequence2(_))
   | (Sequence2, Sequence1(_))
   | (ListConcat1, ListConcat2(_))
-  | (ListConcat2, ListConcat1(_)) => None
+  | (ListConcat2, ListConcat1(_))
+  | (Entail1, Entail2(_))
+  | (Entail2, Entail1(_)) => None
   | (FilterPattern, _) => None
   | (Filter, _) => Some(ctx)
   | (tag, Filter(_, c)) => unwrap(c, tag)

diff --git a/src/haz3lcore/dynamics/EvaluatorError.re b/src/haz3lcore/dynamics/EvaluatorError.re
@@ -14,6 +14,7 @@ type t =
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
   | InvalidBoxedPropLit(DHExp.t)
+  | InvalidBoxedJudgementLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))

diff --git a/src/haz3lcore/dynamics/EvaluatorError.rei b/src/haz3lcore/dynamics/EvaluatorError.rei
@@ -12,6 +12,7 @@ type t =
   | InvalidBoxedListLit(DHExp.t)
   | InvalidBoxedStringLit(DHExp.t)
   | InvalidBoxedPropLit(DHExp.t)
+  | InvalidBoxedJudgementLit(DHExp.t)
   | InvalidBoxedTuple(DHExp.t)
   | InvalidBuiltin(string)
   | BadBuiltinAp(string, list(DHExp.t))

diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
@@ -557,11 +557,24 @@ module Transition = (EV: EV_MODE) => {
         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,
-      });
+      switch (unbox_list(dctx'), dprop') {
+      | (ListLit(_, _, Prop, ctx), PropLit(prop)) =>
+        switch (
+          ctx
+          |> List.map(Builtins.Pervasives.Impls.prop_of)
+          |> Util.OptUtil.sequence
+        ) {
+        | Some(ctx) =>
+          Step({
+            apply: () =>
+              JudgementLit(Derivation.Judgement.Entail(ctx, prop)),
+            kind: Entail,
+            value: true,
+          })
+        | None => Indet
+        }
+      | _ => Indet
+      };
     | ListLit(u, i, ty, ds) =>
       let. _ = otherwise(env, ds => ListLit(u, i, ty, ds))
       and. _ =

diff --git a/src/haz3lcore/statics/Self.re b/src/haz3lcore/statics/Self.re
@@ -146,3 +146,9 @@ let list_concat = (ctx: Ctx.t, tys: list(Typ.t), ids: list(Id.t)): t =>
   | None => NoJoin(List, add_source(ids, tys))
   | Some(ty) => Just(ty)
   };
+
+let entail = (tctx: Typ.t, tprop: Typ.t, ids: list(Id.t)): t =>
+  switch (tctx, tprop) {
+  | (List(Prop), Prop) => Just(Judgement)
+  | _ => NoJoin(List, add_source(ids, [tctx, tprop]))
+  };
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
@@ -255,10 +255,11 @@ and uexp_to_info_map =
       m,
     );
   | Entail(e1, e2) =>
+    let ids = List.map(UExp.rep_id, [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),
+      ~self=Self.entail(e1.ty, e2.ty, ids),
       ~co_ctx=CoCtx.union([e1.co_ctx, e2.co_ctx]),
       m,
     );

diff --git a/src/haz3lweb/explainthis/data/OpExp.re b/src/haz3lweb/explainthis/data/OpExp.re
@@ -760,6 +760,8 @@ let str_concat_exp: form = {
   };
 };
 
+let _exp1 = exp("p1");
+let _exp2 = exp("p2");
 let prop_and_exp_coloring_ids =
     (~left_id: Id.t, ~right_id: Id.t): list((Id.t, Id.t)) =>
   _binop_exp_coloring_ids(
@@ -817,6 +819,8 @@ let prop_implies_exp: form = {
   };
 };
 
+let _exp1 = exp("ctx");
+let _exp2 = exp("prop");
 let entail_exp_coloring_ids =
     (~ctx_id: Id.t, ~prop_id: Id.t): list((Id.t, Id.t)) =>
   _binop_exp_coloring_ids(