task(6/9): new pattern der introduced

src/haz3lcore/dynamics/DH.re

@@ -22,6 +22,7 @@ module rec DHExp: {
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
+    | Derive(t, t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)
@@ -84,6 +85,7 @@ module rec DHExp: {
     | FixF(Var.t, Typ.t, t)
     | Fun(DHPat.t, Typ.t, t, option(Var.t))
     | Ap(t, t)
+    | Derive(t, t, t)
     | ApBuiltin(string, t)
     | BuiltinFun(string)
     | Test(KeywordID.t, t)
@@ -131,6 +133,7 @@ module rec DHExp: {
     | Fun(_, _, _, _) => "Fun"
     | Closure(_, _) => "Closure"
     | Ap(_, _) => "Ap"
+    | Derive(_, _, _) => "Derive"
     | ApBuiltin(_, _) => "ApBuiltin"
     | BuiltinFun(_) => "BuiltinFun"
     | Test(_) => "Test"
@@ -195,6 +198,8 @@ module rec DHExp: {
     | FixF(a, b, c) => FixF(a, b, strip_casts(c))
     | Fun(a, b, c, d) => Fun(a, b, strip_casts(c), d)
     | Ap(a, b) => Ap(strip_casts(a), strip_casts(b))
+    | Derive(a, b, c) =>
+      Derive(strip_casts(a), strip_casts(b), strip_casts(c))
     | Test(id, a) => Test(id, strip_casts(a))
     | ApBuiltin(fn, args) => ApBuiltin(fn, strip_casts(args))
     | BuiltinFun(fn) => BuiltinFun(fn)
@@ -265,7 +270,10 @@ module rec DHExp: {
       f1 == f2 && ty1 == ty2 && fast_equal(d1, d2)
     | (Fun(dp1, ty1, d1, s1), Fun(dp2, ty2, d2, s2)) =>
       dp1 == dp2 && ty1 == ty2 && fast_equal(d1, d2) && s1 == s2
-    | (Ap(d11, d21), Ap(d12, d22))
+    | (Ap(d11, d21), Ap(d12, d22)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22)
+    | (Derive(d11, d21, d31), Derive(d12, d22, d32)) =>
+      fast_equal(d11, d12) && fast_equal(d21, d22) && fast_equal(d31, d32)
     | (Cons(d11, d21), Cons(d12, d22)) =>
       fast_equal(d11, d12) && fast_equal(d21, d22)
     | (ListConcat(d11, d21), ListConcat(d12, d22)) =>
@@ -314,6 +322,7 @@ module rec DHExp: {
     | (Fun(_), _)
     | (Test(_), _)
     | (Ap(_), _)
+    | (Derive(_), _)
     | (ApBuiltin(_), _)
     | (BuiltinFun(_), _)
     | (Cons(_), _)

src/haz3lcore/dynamics/Elaborator.re

@@ -92,6 +92,7 @@ let cast = (ctx: Ctx.t, mode: Mode.t, self_ty: Typ.t, d: DHExp.t) =>
     /* Normal cases: wrap */
     | BoundVar(_)
     | Ap(_)
+    | Derive(_)
     | ApBuiltin(_)
     | BuiltinFun(_)
     | Prj(_)
@@ -285,6 +286,11 @@ let rec dhexp_of_uexp =
         let* c_fn = dhexp_of_uexp(m, fn);
         let+ c_arg = dhexp_of_uexp(m, arg);
         DHExp.Ap(c_fn, c_arg);
+      | Derive(conclusion, premises, rule) =>
+        let* dconcl = dhexp_of_uexp(m, conclusion);
+        let* dprems = dhexp_of_uexp(m, premises);
+        let+ drule = dhexp_of_uexp(m, rule);
+        DHExp.Derive(dconcl, dprems, drule);
       | DeferredAp(fn, args) =>
         switch (err_status) {
         | InHole(BadPartialAp(NoDeferredArgs)) => dhexp_of_uexp(m, fn)

src/haz3lcore/dynamics/EvalCtx.re

@@ -13,6 +13,9 @@ type cls =
   | Let2
   | Ap1
   | Ap2
+  | Derive1
+  | Derive2
+  | Derive3
   | Fun
   | FixF
   | BinBoolOp1
@@ -65,6 +68,9 @@ type t =
   | FixF(Var.t, Typ.t, t)
   | Ap1(t, DHExp.t)
   | Ap2(DHExp.t, t)
+  | Derive1(t, DHExp.t, DHExp.t)
+  | Derive2(DHExp.t, t, DHExp.t)
+  | Derive3(DHExp.t, DHExp.t, t)
   | IfThenElse1(if_consistency, t, DHExp.t, DHExp.t)
   | IfThenElse2(if_consistency, DHExp.t, t, DHExp.t)
   | IfThenElse3(if_consistency, DHExp.t, DHExp.t, t)
@@ -138,6 +144,9 @@ let rec fuzzy_mark =
   | FixF(_)
   | Ap1(_)
   | Ap2(_)
+  | Derive1(_)
+  | Derive2(_)
+  | Derive3(_)
   | IfThenElse1(_)
   | IfThenElse2(_)
   | IfThenElse3(_)

src/haz3lcore/dynamics/EvaluatorPost.re

@@ -64,6 +64,12 @@ let rec pp_eval = (d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_eval(d2);
     Ap(d1', d2') |> return;
 
+  | Derive(d1, d2, d3) =>
+    let* d1' = pp_eval(d1);
+    let* d2' = pp_eval(d2);
+    let+ d3' = pp_eval(d3);
+    Derive(d1', d2', d3');
+
   | ApBuiltin(f, d1) =>
     let* d1' = pp_eval(d1);
     ApBuiltin(f, d1') |> return;
@@ -321,6 +327,12 @@ and pp_uneval = (env: ClosureEnvironment.t, d: DHExp.t): m(DHExp.t) =>
     let* d2' = pp_uneval(env, d2);
     Ap(d1', d2') |> return;
 
+  | Derive(d1, d2, d3) =>
+    let* d1' = pp_uneval(env, d1);
+    let* d2' = pp_uneval(env, d2);
+    let+ d3' = pp_uneval(env, d3);
+    Derive(d1', d2', d3');
+
   | ApBuiltin(f, d1) =>
     let* d1' = pp_uneval(env, d1);
     ApBuiltin(f, d1') |> return;
@@ -545,6 +557,11 @@ let rec track_children_of_hole =
       track_children_of_hole_rules(hii, parent, rules)
     );
 
+  | Derive(d1, d2, d3) =>
+    let hii = track_children_of_hole(hii, parent, d1);
+    let hii = track_children_of_hole(hii, parent, d2);
+    track_children_of_hole(hii, parent, d3);
+
   | ApBuiltin(_, d) => track_children_of_hole(hii, parent, d)
 
   /* Hole types */

src/haz3lcore/dynamics/EvaluatorStep.re

@@ -234,6 +234,15 @@ let rec compose = (ctx: EvalCtx.t, d: DHExp.t): DHExp.t => {
     | Ap2(d1, ctx) =>
       let d2 = compose(ctx, d);
       Ap(d1, d2);
+    | Derive1(ctx, d2, d3) =>
+      let d1 = compose(ctx, d);
+      Derive(d1, d2, d3);
+    | Derive2(d1, ctx, d3) =>
+      let d2 = compose(ctx, d);
+      Derive(d1, d2, d3);
+    | Derive3(d1, d2, ctx) =>
+      let d3 = compose(ctx, d);
+      Derive(d1, d2, d3);
     | ApBuiltin(s, ctx) =>
       let d' = compose(ctx, d);
       ApBuiltin(s, d');

src/haz3lcore/dynamics/FilterMatcher.re

@@ -109,6 +109,12 @@ let rec matches_exp =
     matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
   | (Ap(_), _) => false
 
+  | (Derive(d1, d2, d3), Derive(f1, f2, f3)) =>
+    matches_exp(env, d1, f1)
+    && matches_exp(env, d2, f2)
+    && matches_exp(env, d3, f3)
+  | (Derive(_), _) => false
+
   | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) =>
     dc == fc
     && matches_exp(env, d1, f1)

src/haz3lcore/dynamics/PatternMatch.re

@@ -241,6 +241,7 @@ and matches_cast_Sum =
   | InvalidText(_)
   | Let(_)
   | Ap(_)
+  | Derive(_)
   | ApBuiltin(_)
   | BinBoolOp(_)
   | BinIntOp(_)
@@ -344,6 +345,7 @@ and matches_cast_Tuple =
   | Closure(_, _) => IndetMatch
   | Filter(_, _) => IndetMatch
   | Ap(_, _) => IndetMatch
+  | Derive(_) => IndetMatch
   | ApBuiltin(_, _) => IndetMatch
   | BinBoolOp(_, _, _)
   | BinIntOp(_, _, _)
@@ -488,6 +490,7 @@ and matches_cast_Cons =
   | Closure(_, d') => matches_cast_Cons(dp, d', elt_casts)
   | Filter(_, d') => matches_cast_Cons(dp, d', elt_casts)
   | Ap(_, _) => IndetMatch
+  | Derive(_) => IndetMatch
   | ApBuiltin(_, _) => IndetMatch
   | BinBoolOp(_, _, _)
   | BinIntOp(_, _, _)

src/haz3lcore/dynamics/Stepper.re

@@ -89,6 +89,15 @@ let rec matches =
     | Ap2(d1, ctx) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Ap2(d1, ctx);
+    | Derive1(ctx, d2, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive1(ctx, d2, d3);
+    | Derive2(d1, ctx, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive2(d1, ctx, d3);
+    | Derive3(d1, d2, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Derive3(d1, d2, ctx);
     | IfThenElse1(c, ctx, d2, d3) =>
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       IfThenElse1(c, ctx, d2, d3);

src/haz3lcore/dynamics/Substitution.re

@@ -52,6 +52,11 @@ 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);
     Ap(d3, d4);
+  | Derive(d3, d4, d5) =>
+    let d3 = subst_var(d1, x, d3);
+    let d4 = subst_var(d1, x, d4);
+    let d5 = subst_var(d1, x, d5);
+    Derive(d3, d4, d5);
   | ApBuiltin(ident, d1) =>
     let d2 = subst_var(d1, x, d1);
     ApBuiltin(ident, d2);

src/haz3lcore/dynamics/Transition.re

@@ -305,6 +305,47 @@ module Transition = (EV: EV_MODE) => {
           value: true,
         })
       };
+    | Derive(conclusion, premises, rule) =>
+      let. _ =
+        otherwise(env, (conclusion, premises, rule) =>
+          Derive(conclusion, premises, rule)
+        )
+      and. rule' =
+        req_final(
+          req(state, env),
+          rule => Derive3(conclusion, premises, rule),
+          rule,
+        )
+      and. premises' =
+        req_final(
+          req(state, env),
+          premises => Derive2(conclusion, premises, rule),
+          premises,
+        )
+      and. conclusion' =
+        req_final(
+          req(state, env),
+          conclusion => Derive1(conclusion, premises, rule),
+          conclusion,
+        );
+      switch (rule') {
+      | BuiltinFun(ident) =>
+        Step({
+          apply: () => {
+            ApBuiltin(ident, Tuple([conclusion', premises']));
+          },
+          kind: BuiltinAp(ident),
+          value: false,
+        })
+      | _ =>
+        Step({
+          apply: () => {
+            raise(EvaluatorError.Exception(InvalidBoxedFun(rule')));
+          },
+          kind: InvalidStep,
+          value: true,
+        })
+      };
     | ApBuiltin(ident, arg) =>
       let. _ = otherwise(env, arg => ApBuiltin(ident, arg))
       and. arg' =

src/haz3lcore/statics/MakeTerm.re

@@ -186,6 +186,8 @@ and exp_term: unsorted => (UExp.term, list(Id.t)) = {
         | (["!"], []) => UnOp(Bool(Not), r)
         | (["fun", "->"], [Pat(pat)]) => Fun(pat, r)
         | (["let", "=", "in"], [Pat(pat), Exp(def)]) => Let(pat, def, r)
+        | (["der", "\\", "of"], [Exp(conclusion), Exp(premises)]) =>
+          Derive(conclusion, premises, r)
         | (["hide", "in"], [Exp(filter)]) =>
           Filter((Eval, One), filter, r)
         | (["eval", "in"], [Exp(filter)]) =>

src/haz3lcore/statics/Statics.re

@@ -330,6 +330,20 @@ and uexp_to_info_map =
       && !Typ.is_consistent(ctx, ty_in, Prod([]))
         ? BadTrivAp(ty_in) : Just(ty_out);
     add(~self, ~co_ctx=CoCtx.union([fn.co_ctx, arg.co_ctx]), m);
+  | Derive(conclusion, premises, rule) =>
+    let (rule, m) =
+      go(
+        ~mode=Ana(Arrow(Prod([Judgement, List(Judgement)]), Judgement)),
+        rule,
+        m,
+      );
+    let (conclusion, m) = go(~mode=Ana(Judgement), conclusion, m);
+    let (premises, m) = go(~mode=Ana(List(Judgement)), premises, m);
+    add(
+      ~self=Just(Judgement),
+      ~co_ctx=CoCtx.union([rule.co_ctx, conclusion.co_ctx, premises.co_ctx]),
+      m,
+    );
   | DeferredAp(fn, args) =>
     let fn_mode = Mode.of_ap(ctx, mode, UExp.ctr_name(fn));
     let (fn, m) = go(~mode=fn_mode, fn, m);

src/haz3lcore/statics/Term.re

@@ -404,6 +404,7 @@ module UExp = {
     | Let
     | TyAlias
     | Ap
+    | Derive
     | DeferredAp
     | Pipeline
     | If
@@ -451,6 +452,7 @@ module UExp = {
     | Let(_) => Let
     | TyAlias(_) => TyAlias
     | Ap(_) => Ap
+    | Derive(_) => Derive
     | DeferredAp(_) => DeferredAp
     | Pipeline(_) => Pipeline
     | If(_) => If
@@ -557,6 +559,7 @@ module UExp = {
     | Let => "Let expression"
     | TyAlias => "Type Alias definition"
     | Ap => "Application"
+    | Derive => "Derivation"
     | DeferredAp => "Partial Application"
     | Pipeline => "Pipeline expression"
     | If => "If expression"
@@ -592,6 +595,7 @@ module UExp = {
     | Let(_)
     | TyAlias(_)
     | Ap(_)
+    | Derive(_)
     | DeferredAp(_)
     | Pipeline(_)
     | If(_)
@@ -631,6 +635,7 @@ module UExp = {
       | Let(_)
       | TyAlias(_)
       | Ap(_)
+      | Derive(_)
       | DeferredAp(_)
       | Pipeline(_)
       | If(_)
@@ -685,6 +690,7 @@ module UExp = {
       | Filter(_)
       | TyAlias(_)
       | Ap(_)
+      | Derive(_)
       | DeferredAp(_)
       | Pipeline(_)
       | If(_)

src/haz3lcore/statics/TermBase.re

@@ -128,6 +128,7 @@ and UExp: {
     | Var
     | Let
     | Ap
+    | Derive
     | If
     | Seq
     | Test
@@ -166,6 +167,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Derive(t, t, t)
     | DeferredAp(t, list(t))
     | Pipeline(t, t)
     | If(t, t, t)
@@ -280,6 +282,7 @@ and UExp: {
     | Var
     | Let
     | Ap
+    | Derive
     | If
     | Seq
     | Test
@@ -318,6 +321,7 @@ and UExp: {
     | Let(UPat.t, t, t)
     | TyAlias(UTPat.t, UTyp.t, t)
     | Ap(t, t)
+    | Derive(t, t, t)
     | DeferredAp(t, list(t))
     | Pipeline(t, t)
     | If(t, t, t)

src/haz3lcore/zipper/EditorUtil.re

@@ -60,6 +60,7 @@ let rec append_exp = (e1: TermBase.UExp.t, e2: TermBase.UExp.t) => {
   | Tuple(_)
   | Var(_)
   | Ap(_)
+  | Derive(_)
   | DeferredAp(_)
   | Pipeline(_)
   | If(_)