From 67b3853bb647348da78b2bcb37ecc484c13b92a3 Mon Sep 17 00:00:00 2001 From: ZhiyaoZhong Date: Tue, 15 Oct 2024 14:48:15 -0400 Subject: [PATCH] fix rebase minor --- src/haz3lcore/derivation/DrvElab.re | 32 +- src/haz3lcore/derivation/DrvSyntax.re | 140 +--- src/haz3lcore/derivation/RuleSpec.re | 100 ++- src/haz3lcore/derivation/RuleTest.re | 608 +++++++++--------- src/haz3lcore/derivation/RuleVerify.re | 5 +- src/haz3lweb/explainthis/ExplainThisForm.re | 35 +- src/haz3lweb/explainthis/data/DeductionExp.re | 4 +- src/haz3lweb/view/exercise/ExerciseMode.re | 1 + 8 files changed, 384 insertions(+), 541 deletions(-) diff --git a/src/haz3lcore/derivation/DrvElab.re b/src/haz3lcore/derivation/DrvElab.re index 09151c2e3..5d731e140 100644 --- a/src/haz3lcore/derivation/DrvElab.re +++ b/src/haz3lcore/derivation/DrvElab.re @@ -104,29 +104,9 @@ and elab_exp: Drv.Exp.t => t = | False => False | If(e1, e2, e3) => If(elab_exp(e1), elab_exp(e2), elab_exp(e3)) | Var(x) => Var(x) - | Let(x, e1, e2) => - let e1 = elab_exp(e1); - let e2 = elab_exp(e2); - switch (pat_term_of(x)) { - | Var(_) => Let(elab_pat(x), e1, e2) - | Cast(x, t) => LetAnn(elab_pat(x), elab_typ(t), e1, e2) - | Pair(x, y) => LetPair(elab_pat(x), elab_pat(y), e1, e2) - | _ => hole - }; - | Fix(x, e) => - let e = elab_exp(e); - switch (pat_term_of(x)) { - | Var(_) => Fix(elab_pat(x), e) - | Cast(x, t) => FixAnn(elab_pat(x), elab_typ(t), e) - | _ => hole - }; - | Fun(x, e) => - let e = elab_exp(e); - switch (pat_term_of(x)) { - | Var(_) => Fun(elab_pat(x), e) - | Cast(x, t) => FunAnn(elab_pat(x), elab_typ(t), e) - | _ => hole - }; + | Let(p, e1, e2) => Let(elab_pat(p), elab_exp(e1), elab_exp(e2)) + | Fix(p, e) => Fix(elab_pat(p), elab_exp(e)) + | Fun(x, e) => Fun(elab_pat(x), elab_exp(e)) | Ap(e1, e2) => let e2 = elab_exp(e2); switch (exp_term_of(e1)) { @@ -166,11 +146,11 @@ and elab_pat: Drv.Pat.t => t = switch (pat.term) { | Hole(s) => Hole(TermBase.TypeHole.show(s)) | Var(x) => Pat(x) - | Cast(_) + | Cast(x, t) => Cast(elab_pat(x), elab_typ(t)) + | Pair(x, y) => PatPair(elab_pat(x), elab_pat(y)) | InjL | InjR - | Ap(_) - | Pair(_) => Hole(Drv.Pat.show(pat)) + | Ap(_) => Hole(Drv.Pat.show(pat)) | Parens(p) => IdTagged.term_of(elab_pat(p)) }; {...pat, term}; diff --git a/src/haz3lcore/derivation/DrvSyntax.re b/src/haz3lcore/derivation/DrvSyntax.re index 1155fe6e1..2eaf66fb5 100644 --- a/src/haz3lcore/derivation/DrvSyntax.re +++ b/src/haz3lcore/derivation/DrvSyntax.re @@ -50,17 +50,13 @@ type term = | If(t, t, t) | Var(string) | Let(t, t, t) - | LetAnn(t, t, t, t) | Fix(t, t) - | FixAnn(t, t, t) | Fun(t, t) - | FunAnn(t, t, t) | Ap(t, t) | Pair(t, t) | Triv | PrjL(t) | PrjR(t) - | LetPair(t, t, t, t) | InjL(t) | InjR(t) | Case(t, t, t, t, t) @@ -68,6 +64,8 @@ type term = | Unroll(t) // ALFA Pat | Pat(string) + | Cast(t, t) // We allow at most one annotation for Let/Fun/Fix + | PatPair(t, t) // ALFA Typ | Num | Bool @@ -90,63 +88,6 @@ let unwrap: t => (term, term => t) = IdTagged.unwrap; let temp = (term: term) => IdTagged.{term, ids: [Id.invalid], copied: false}; -[@deriving (show({with_path: false}), sexp, yojson)] -type cls = - | Hole - | Val - | Eval - | Entail - | Type - | HasType - | Syn - | Ana - | Atom - | And - | Or - | Impl - | Truth - | Falsity - | Ctx - | NumLit - | Neg - | Plus - | Minus - | Times - | Lt - | Gt - | Eq - | True - | False - | If - | Var - | Let - | LetAnn - | Fix - | FixAnn - | Fun - | FunAnn - | Ap - | Pair - | Triv - | PrjL - | PrjR - | LetPair - | InjL - | InjR - | Case - | Roll - | Unroll - | Pat - | Num - | Bool - | Arrow - | Prod - | Unit - | Sum - | TVar - | Rec - | TPat; - module P = Precedence; // Note(zhiyao): We have a little bit different precedence for printing @@ -185,23 +126,21 @@ let precedence: t => int = | If(_) => P.if_ | Var(_) => P.max | Let(_) => P.let_ - | LetAnn(_) => P.let_ | Fix(_) => P.fun_ - | FixAnn(_) => P.fun_ | Fun(_) => P.fun_ - | FunAnn(_) => P.fun_ | Ap(_) => P.ap | Pair(_) => P.max | Triv => P.max | PrjL(_) => P.ap | PrjR(_) => P.ap - | LetPair(_) => P.let_ | InjL(_) => P.ap | InjR(_) => P.ap | Case(_) => P.fun_ | Roll(_) => P.ap | Unroll(_) => P.ap | Pat(_) => P.max + | Cast(_, _) => P.ann + | PatPair(_) => P.comma | Num => P.max | Bool => P.max | Arrow(_) => P.type_arrow @@ -245,17 +184,13 @@ let children = (syntax: t): list(t) => | If(a, b, c) => [a, b, c] | Var(_) => [] | Let(a, b, c) => [a, b, c] - | LetAnn(a, b, c, d) => [a, b, c, d] | Fix(a, b) => [a, b] - | FixAnn(a, b, c) => [a, b, c] | Fun(a, b) => [a, b] - | FunAnn(a, b, c) => [a, b, c] | Ap(a, b) => [a, b] | Pair(a, b) => [a, b] | Triv => [] | PrjL(a) => [a] | PrjR(a) => [a] - | LetPair(a, b, c, d) => [a, b, c, d] | InjL(a) => [a] | InjR(a) => [a] | Case(a, b, c, d, e) => [a, b, c, d, e] @@ -263,6 +198,8 @@ let children = (syntax: t): list(t) => | Unroll(a) => [a] // ALFA Pat | Pat(_) => [] + | Cast(a, b) => [a, b] + | PatPair(a, b) => [a, b] // ALFA Typ | Num => [] | Bool => [] @@ -338,23 +275,21 @@ let repr = (~sp: string=" ", p: int, syntax: t): Aba.t(string, t) => { | If(_) => ["if", "then", "else"] |> pre | Var(x) => x |> op_sg | Let(_) => ["let", "be", "in"] |> pre - | LetAnn(_) => ["let", ":", "be", "in"] |> pre | Fix(_) => ["fix", "→"] |> pre - | FixAnn(_) => ["fix", ":", "→"] |> pre | Fun(_) => ["fun", "→"] |> pre - | FunAnn(_) => ["fun", ":", "→"] |> pre | Ap(_) => ["", " ", ""] | Pair(_) => ["(", ",", ")"] |> op | Triv => "()" |> op_sg | PrjL(_) => ".fst" |> post_sg | PrjR(_) => ".snd" |> post_sg - | LetPair(_) => ["let (", ",", ") be", "in"] |> pre | InjL(_) => "L" |> pre_sg | InjR(_) => "R" |> pre_sg | Case(_) => ["case", "of L(", ") →", "else R(", ") →"] |> pre | Roll(_) => ["roll(", ")"] |> op | Unroll(_) => ["unroll(", ")"] |> op | Pat(s) => s |> op_sg + | Cast(_) => ":" |> bin_sg + | PatPair(_) => "," |> bin_sg | TPat(s) => s |> op_sg | Type(_) => "type" |> post_sg | HasType(_) => ":" |> bin_sg @@ -376,9 +311,11 @@ let rec subst: (t, string, t) => t = (v, x, e) => { let (term, rewrap: term => t) = IdTagged.unwrap(e); let subst = subst(v, x); - let is_shadow = (p: t) => + let rec is_shadow = (p: t) => switch (IdTagged.term_of(p)) { | Pat(x') => String.equal(x', x) + | Cast(p, _) => is_shadow(p) + | PatPair(p1, p2) => is_shadow(p1) || is_shadow(p2) | _ => false }; let subst' = p => is_shadow(p) ? Fun.id : subst; @@ -408,25 +345,13 @@ let rec subst: (t, string, t) => t = | If(e1, e2, e3) => If(subst(e1), subst(e2), subst(e3)) |> rewrap | Var(x') => String.equal(x', x) ? v : e | Let(x, e1, e2) => Let(x, subst(e1), subst'(x, e2)) |> rewrap - | LetAnn(x, t, e1, e2) => - LetAnn(x, t, subst(e1), subst'(x, e2)) |> rewrap | Fix(x, e) => Fix(x, subst'(x, e)) |> rewrap - | FixAnn(x, t, e) => FixAnn(x, t, subst'(x, e)) |> rewrap | Fun(x, e) => Fun(x, subst'(x, e)) |> rewrap - | FunAnn(x, t, e) => FunAnn(x, t, subst'(x, e)) |> rewrap | Ap(e1, e2) => Ap(subst(e1), subst(e2)) |> rewrap | Pair(e1, e2) => Pair(subst(e1), subst(e2)) |> rewrap | Triv => e | PrjL(e) => PrjL(subst(e)) |> rewrap | PrjR(e) => PrjR(subst(e)) |> rewrap - | LetPair(x, y, e1, e2) => - LetPair( - x, - y, - subst(e1), - is_shadow(x) || is_shadow(y) ? e2 : subst(e2), - ) - |> rewrap | InjL(e) => InjL(subst(e)) |> rewrap | InjR(e) => InjR(subst(e)) |> rewrap | Case(e1, x, e2, y, e3) => @@ -436,6 +361,8 @@ let rec subst: (t, string, t) => t = // Meta | TPat(_) | Pat(_) + | Cast(_) + | PatPair(_) => e // Proposition | Type(_) | HasType(_) @@ -491,37 +418,26 @@ let rec subst_ty: (t, string, t) => t = | If(e1, e2, e3) => If(subst_ty(e1), subst_ty(e2), subst_ty(e3)) |> rewrap | Var(_) => e - | Let(x, e1, e2) => Let(x, subst_ty(e1), subst_ty(e2)) |> rewrap - | LetAnn(x, t, e1, e2) => - LetAnn(x, subst_ty(t), subst_ty(e1), subst_ty(e2)) |> rewrap - | Fix(x, e) => Fix(x, subst_ty(e)) |> rewrap - | FixAnn(x, t, e) => FixAnn(x, subst_ty(t), subst_ty(e)) |> rewrap - | Fun(x, e) => Fun(x, subst_ty(e)) |> rewrap - | FunAnn(x, t, e) => FunAnn(x, subst_ty(t), subst_ty(e)) |> rewrap + | Let(x, e1, e2) => + Let(subst_ty(x), subst_ty(e1), subst_ty(e2)) |> rewrap + | Fix(x, e) => Fix(subst_ty(x), subst_ty(e)) |> rewrap + | Fun(x, e) => Fun(subst_ty(x), subst_ty(e)) |> rewrap | Ap(e1, e2) => Ap(subst_ty(e1), subst_ty(e2)) |> rewrap | Pair(e1, e2) => Pair(subst_ty(e1), subst_ty(e2)) |> rewrap | Triv => e | PrjL(e) => PrjL(subst_ty(e)) |> rewrap | PrjR(e) => PrjR(subst_ty(e)) |> rewrap - | LetPair(x, y, e1, e2) => - LetPair(subst_ty(x), subst_ty(y), subst_ty(e1), subst_ty(e2)) - |> rewrap | InjL(e) => InjL(subst_ty(e)) |> rewrap | InjR(e) => InjR(subst_ty(e)) |> rewrap | Case(e1, x, e2, y, e3) => - Case( - subst_ty(e1), - subst_ty(x), - subst_ty(e2), - subst_ty(y), - subst_ty(e3), - ) - |> rewrap + Case(subst_ty(e1), x, subst_ty(e2), y, subst_ty(e3)) |> rewrap | Roll(e) => Roll(subst_ty(e)) |> rewrap | Unroll(e) => Unroll(subst_ty(e)) |> rewrap // Meta | TPat(_) | Pat(_) => e + | Cast(x, t) => Cast(subst_ty(x), subst_ty(t)) |> rewrap + | PatPair(x, y) => PatPair(subst_ty(x), subst_ty(y)) |> rewrap // Proposition | Type(_) | HasType(_) @@ -594,19 +510,10 @@ let rec eq: (t, t) => bool = | (Let(a1, a2, a3), Let(b1, b2, b3)) => eq(a1, b1) && eq(a2, b2) && eq(a3, b3) | (Let(_), _) => false - | (LetAnn(a1, a2, a3, a4), LetAnn(b1, b2, b3, b4)) => - eq(a1, b1) && eq(a2, b2) && eq(a3, b3) && eq(a4, b4) - | (LetAnn(_), _) => false | (Fix(a1, a2), Fix(b1, b2)) => eq(a1, b1) && eq(a2, b2) | (Fix(_), _) => false - | (FixAnn(a1, a2, a3), FixAnn(b1, b2, b3)) => - eq(a1, b1) && eq(a2, b2) && eq(a3, b3) - | (FixAnn(_), _) => false | (Fun(a1, a2), Fun(b1, b2)) => eq(a1, b1) && eq(a2, b2) | (Fun(_), _) => false - | (FunAnn(a1, a2, a3), FunAnn(b1, b2, b3)) => - eq(a1, b1) && eq(a2, b2) && eq(a3, b3) - | (FunAnn(_), _) => false | (Ap(a1, a2), Ap(b1, b2)) => eq(a1, b1) && eq(a2, b2) | (Ap(_), _) => false | (Pair(a1, a2), Pair(b1, b2)) => eq(a1, b1) && eq(a2, b2) @@ -617,9 +524,6 @@ let rec eq: (t, t) => bool = | (PrjL(_), _) => false | (PrjR(a), PrjR(b)) => eq(a, b) | (PrjR(_), _) => false - | (LetPair(a1, a2, a3, a4), LetPair(b1, b2, b3, b4)) => - eq(a1, b1) && eq(a2, b2) && eq(a3, b3) && eq(a4, b4) - | (LetPair(_), _) => false | (InjL(a), InjL(b)) => eq(a, b) | (InjL(_), _) => false | (InjR(a), InjR(b)) => eq(a, b) @@ -635,6 +539,10 @@ let rec eq: (t, t) => bool = | (TPat(_), _) => false | (Pat(a), Pat(b)) => String.equal(a, b) | (Pat(_), _) => false + | (Cast(a1, a2), Cast(b1, b2)) => eq(a1, b1) && eq(a2, b2) + | (Cast(_), _) => false + | (PatPair(a1, a2), PatPair(b1, b2)) => eq(a1, b1) && eq(a2, b2) + | (PatPair(_), _) => false | (Type(a), Type(b)) => eq(a, b) | (Type(_), _) => false | (HasType(a1, a2), HasType(b1, b2)) => eq(a1, b1) && eq(a2, b2) diff --git a/src/haz3lcore/derivation/RuleSpec.re b/src/haz3lcore/derivation/RuleSpec.re index adebd9d89..00667ea86 100644 --- a/src/haz3lcore/derivation/RuleSpec.re +++ b/src/haz3lcore/derivation/RuleSpec.re @@ -35,17 +35,13 @@ module M = (W: Wrapper) => { | If(t, t, t) | Var(t) // Copy self | Let(t, t, t) - | LetAnn(t, t, t, t) | Fix(t, t) - | FixAnn(t, t, t) | Fun(t, t) - | FunAnn(t, t, t) | Ap(t, t) | Pair(t, t) | Triv | PrjL(t) | PrjR(t) - | LetPair(t, t, t, t) | InjL(t) | InjR(t) | Case(t, t, t, t, t) @@ -62,6 +58,9 @@ module M = (W: Wrapper) => { | Rec(t, t) // ALFA Pat | Pat(t) // Copy self + | Cast(t, t) // We allow at most one annotation for Let/Fun/Fix + | PatStrip(t) // Match either Pat or Cast + | PatPair(t, t) | TPat(t) // Copy self // Logical Proposition | Atom(t) // Copy self @@ -108,19 +107,13 @@ let rec map_reg = (f: string => string, spec: t): t => { | If(a, b, c) => If(map_reg(a), map_reg(b), map_reg(c)) | Var(a) => Var(map_reg(a)) | Let(a, b, c) => Let(map_reg(a), map_reg(b), map_reg(c)) - | LetAnn(a, b, c, d) => - LetAnn(map_reg(a), map_reg(b), map_reg(c), map_reg(d)) | Fix(a, b) => Fix(map_reg(a), map_reg(b)) - | FixAnn(a, b, c) => FixAnn(map_reg(a), map_reg(b), map_reg(c)) | Fun(a, b) => Fun(map_reg(a), map_reg(b)) - | FunAnn(a, b, c) => FunAnn(map_reg(a), map_reg(b), map_reg(c)) | Ap(a, b) => Ap(map_reg(a), map_reg(b)) | Pair(a, b) => Pair(map_reg(a), map_reg(b)) | Triv => Triv | PrjL(a) => PrjL(map_reg(a)) | PrjR(a) => PrjR(map_reg(a)) - | LetPair(a, b, c, d) => - LetPair(map_reg(a), map_reg(b), map_reg(c), map_reg(d)) | InjL(a) => InjL(map_reg(a)) | InjR(a) => InjR(map_reg(a)) | Case(a, b, c, d, e) => @@ -136,6 +129,9 @@ let rec map_reg = (f: string => string, spec: t): t => { | TVar(a) => TVar(map_reg(a)) | Rec(a, b) => Rec(map_reg(a), map_reg(b)) | Pat(a) => Pat(map_reg(a)) + | Cast(a, b) => Cast(map_reg(a), map_reg(b)) + | PatStrip(a) => PatStrip(map_reg(a)) + | PatPair(a, b) => PatPair(map_reg(a), map_reg(b)) | TPat(a) => TPat(map_reg(a)) | Atom(a) => Atom(map_reg(a)) | And(a, b) => And(map_reg(a), map_reg(b)) @@ -172,23 +168,13 @@ let rec of_syntax = (spec: t): DrvSyntax.t => { | Var(r) => of_syntax(r) | Let(a, b, c) => Let(of_syntax(a), of_syntax(b), of_syntax(c)) |> rewrap - | LetAnn(a, b, c, d) => - LetAnn(of_syntax(a), of_syntax(b), of_syntax(c), of_syntax(d)) - |> rewrap | Fix(a, b) => Fix(of_syntax(a), of_syntax(b)) |> rewrap - | FixAnn(a, b, c) => - FixAnn(of_syntax(a), of_syntax(b), of_syntax(c)) |> rewrap | Fun(a, b) => Fun(of_syntax(a), of_syntax(b)) |> rewrap - | FunAnn(a, b, c) => - FunAnn(of_syntax(a), of_syntax(b), of_syntax(c)) |> rewrap | Ap(a, b) => Ap(of_syntax(a), of_syntax(b)) |> rewrap | Pair(a, b) => Pair(of_syntax(a), of_syntax(b)) |> rewrap | Triv => Triv |> rewrap | PrjL(a) => PrjL(of_syntax(a)) |> rewrap | PrjR(a) => PrjR(of_syntax(a)) |> rewrap - | LetPair(a, b, c, d) => - LetPair(of_syntax(a), of_syntax(b), of_syntax(c), of_syntax(d)) - |> rewrap | InjL(a) => InjL(of_syntax(a)) |> rewrap | InjR(a) => InjR(of_syntax(a)) |> rewrap | Case(a, b, c, d, e) => @@ -211,6 +197,9 @@ let rec of_syntax = (spec: t): DrvSyntax.t => { | TVar(r) => of_syntax(r) | Rec(a, b) => Rec(of_syntax(a), of_syntax(b)) |> rewrap | Pat(r) => of_syntax(r) + | Cast(a, b) => Cast(of_syntax(a), of_syntax(b)) |> rewrap + | PatStrip(r) => of_syntax(r) + | PatPair(a, b) => PatPair(of_syntax(a), of_syntax(b)) |> rewrap | TPat(r) => of_syntax(r) | Atom(r) => of_syntax(r) | And(a, b) => And(of_syntax(a), of_syntax(b)) |> rewrap @@ -298,25 +287,13 @@ let rec go: ((map, list(failure)), specced) => (map, list(failure)) = | (Var(r), Var(_)) => info |> go(r, syntax) | (Let(ra, rb, rc), Let(a, b, c)) => info |> go(ra, a) |> go(rb, b) |> go(rc, c) - | (Let(ra, rb, rc), LetAnn(a, _, b, c)) => - info |> go(ra, a) |> go(rb, b) |> go(rc, c) // Note(zhiyao): we allow Let to be annotated - | (LetAnn(ra, rb, rc, rd), LetAnn(a, b, c, d)) => - info |> go(ra, a) |> go(rb, b) |> go(rc, c) |> go(rd, d) | (Fix(ra, rb), Fix(a, b)) => info |> go(ra, a) |> go(rb, b) - | (Fix(ra, rb), FixAnn(a, _, b)) => info |> go(ra, a) |> go(rb, b) // Note(zhiyao): we allow Fix to be annotated - | (FixAnn(ra, rb, rc), FixAnn(a, b, c)) => - info |> go(ra, a) |> go(rb, b) |> go(rc, c) | (Fun(ra, rb), Fun(a, b)) => info |> go(ra, a) |> go(rb, b) - | (Fun(ra, rb), FunAnn(a, _, b)) => info |> go(ra, a) |> go(rb, b) // Note(zhiyao): we allow Fun to be annotated - | (FunAnn(ra, rb, rc), FunAnn(a, b, c)) => - info |> go(ra, a) |> go(rb, b) |> go(rc, c) | (Ap(ra, rb), Ap(a, b)) => info |> go(ra, a) |> go(rb, b) | (Pair(ra, rb), Pair(a, b)) => info |> go(ra, a) |> go(rb, b) | (Triv, Triv) => info | (PrjL(ra), PrjL(a)) => info |> go(ra, a) | (PrjR(ra), PrjR(a)) => info |> go(ra, a) - | (LetPair(ra, rb, rc, rd), LetPair(a, b, c, d)) => - info |> go(ra, a) |> go(rb, b) |> go(rc, c) |> go(rd, d) | (InjL(ra), InjL(a)) => info |> go(ra, a) | (InjR(ra), InjR(a)) => info |> go(ra, a) | (Case(ra, rb, rc, rd, re), Case(a, b, c, d, e)) => @@ -339,6 +316,11 @@ let rec go: ((map, list(failure)), specced) => (map, list(failure)) = | (Rec(ra, rb), Rec(a, b)) => info |> go(ra, a) |> go(rb, b) // ALFA Pat | (Pat(r), Pat(_)) => info |> go(r, syntax) + | (Cast(ra, rb), Cast(a, b)) => info |> go(ra, a) |> go(rb, b) + | (PatStrip(r), Pat(_)) => info |> go(r, syntax) + | (PatStrip(r), Cast({term: Pat(_), _}, _)) => info |> go(r, syntax) + | (PatPair(ra, rb), PatPair(a, b)) => info |> go(ra, a) |> go(rb, b) + // ALFA TPat | (TPat(r), TPat(_)) => info |> go(r, syntax) // Logical Proposition | (Atom(r), Atom(_)) => info |> go(r, syntax) @@ -368,17 +350,13 @@ let rec go: ((map, list(failure)), specced) => (map, list(failure)) = | (If(_), _) | (Var(_), _) | (Let(_), _) - | (LetAnn(_), _) | (Fix(_), _) - | (FixAnn(_), _) | (Fun(_), _) - | (FunAnn(_), _) | (Ap(_), _) | (Pair(_), _) | (Triv, _) | (PrjL(_), _) | (PrjR(_), _) - | (LetPair(_), _) | (InjL(_), _) | (InjR(_), _) | (Case(_), _) @@ -393,6 +371,9 @@ let rec go: ((map, list(failure)), specced) => (map, list(failure)) = | (TVar(_), _) | (Rec(_), _) | (Pat(_), _) + | (Cast(_), _) + | (PatStrip(_), _) + | (PatPair(_), _) | (TPat(_), _) | (Atom(_), _) | (And(_), _) @@ -555,11 +536,11 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { | T_Var => (has(gamma, Var(x), t), []) | S_Var => (syn(gamma, Var(x), t), []) | T_LetAnn => ( - has(gamma, LetAnn(Pat(x), t_def, e_def, e_body), t), + has(gamma, Let(Cast(Pat(x), t_def), e_def, e_body), t), [has(gamma, e_def, t_def), has(gamma', e_body, t)], ) | T_LetAnn_TV => ( - has(gamma, LetAnn(Pat(x), t_def, e_def, e_body), t), + has(gamma, Let(Cast(Pat(x), t_def), e_def, e_body), t), [ type_(delta, t_def), has(gamma, e_def, t_def), @@ -567,11 +548,11 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { ], ) | S_LetAnn => ( - syn(gamma, LetAnn(Pat(x), t_def, e_def, e_body), t), + syn(gamma, Let(Cast(Pat(x), t_def), e_def, e_body), t), [ana(gamma, e_def, t_def), syn(gamma', e_body, t)], ) | A_LetAnn => ( - ana(gamma, LetAnn(Pat(x), t_def, e_def, e_body), t), + ana(gamma, Let(Cast(Pat(x), t_def), e_def, e_body), t), [ana(gamma, e_def, t_def), ana(gamma', e_body, t)], ) | T_Let => ( @@ -587,23 +568,23 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { [syn(gamma, e_def, t_def), ana(gamma', e_body, t)], ) | E_Let => ( - eval(Let(Pat(x), e_def, e_body), v), + eval(Let(PatStrip(x), e_def, e_body), v), [eval(e_def, v_def), eval(e_body', v)], ) | T_FunAnn => ( - has(gamma, FunAnn(Pat(x), t_in, e_body), Arrow(t_in, t_out)), + has(gamma, Fun(Cast(Pat(x), t_in), e_body), Arrow(t_in, t_out)), [has(gamma', e_body, t_out)], ) | T_FunAnn_TV => ( - has(gamma, FunAnn(Pat(x), t_in, e_body), Arrow(t_in, t_out)), + has(gamma, Fun(Cast(Pat(x), t_in), e_body), Arrow(t_in, t_out)), [type_(delta, t_in), has(gamma', e_body, t_out)], ) | S_FunAnn => ( - syn(gamma, FunAnn(Pat(x), t_in, e_body), Arrow(t_in, t_out)), + syn(gamma, Fun(Cast(Pat(x), t_in), e_body), Arrow(t_in, t_out)), [syn(gamma', e_body, t_out)], ) | A_FunAnn => ( - ana(gamma, FunAnn(Pat(x), t_in, e_body), Arrow(t_in, t_out)), + ana(gamma, Fun(Cast(Pat(x), t_in), e_body), Arrow(t_in, t_out)), [ana(gamma', e_body, t_out)], ) | T_Fun => ( @@ -625,7 +606,11 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { ) | E_Ap => ( eval(Ap(e1, e2), v), - [eval(e1, Fun(Pat(x), e_body)), eval(e2, v2), eval(e_body', v)], + [ + eval(e1, Fun(PatStrip(x), e_body)), + eval(e2, v2), + eval(e_body', v), + ], ) | T_Triv => (has(gamma, Triv, Unit), []) | S_Triv => (syn(gamma, Triv, Unit), []) @@ -648,19 +633,19 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { [eval(e1, v1), eval(e2, v2)], ) | T_LetPair => ( - has(gamma, LetPair(Pat(x), Pat(y), e_def, e_body), t), + has(gamma, Let(PatPair(Pat(x), Pat(y)), e_def, e_body), t), [has(gamma, e_def, Prod(t1, t2)), has(gamma', e_body, t)], ) | S_LetPair => ( - syn(gamma, LetPair(Pat(x), Pat(y), e_def, e_body), t), + syn(gamma, Let(PatPair(Pat(x), Pat(y)), e_def, e_body), t), [syn(gamma, e_def, Prod(t1, t2)), syn(gamma', e_body, t)], ) | A_LetPair => ( - ana(gamma, LetPair(Pat(x), Pat(y), e_def, e_body), t), + ana(gamma, Let(PatPair(Pat(x), Pat(y)), e_def, e_body), t), [syn(gamma, e_def, Prod(t1, t2)), ana(gamma', e_body, t)], ) | E_LetPair => ( - eval(LetPair(Pat(x), Pat(y), e_def, e_body), v), + eval(Let(PatPair(PatStrip(x), PatStrip(y)), e_def, e_body), v), [eval(e_def, Pair(v1, v2)), eval(e_body', v)], ) | T_PrjL => (has(gamma, PrjL(e), t1), [has(gamma, e, Prod(t1, t2))]) @@ -710,15 +695,15 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { [eval(e, InjR(v)), eval(e2', v2)], ) | T_FixAnn => ( - has(gamma, FixAnn(Pat(x), t, e), t), + has(gamma, Fix(Cast(Pat(x), t), e), t), [has(gamma', e, t)], ) | T_FixAnn_TV => ( - has(gamma, FixAnn(Pat(x), t, e), t), + has(gamma, Fix(Cast(Pat(x), t), e), t), [type_(delta, t), has(gamma', e, t)], ) | T_Fix => (has(gamma, Fix(Pat(x), e), t), [has(gamma', e, t)]) - | E_Fix => (eval(Fix(Pat(x), e_body), v), [eval(e', v)]) + | E_Fix => (eval(Fix(PatStrip(x), e_body), v), [eval(e', v)]) | T_Roll => ( has(gamma, Roll(e), Rec(tpat, t_body)), [has(gamma, e, t_body')], @@ -777,19 +762,13 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { | If(a, b, c) => If(fresh(a), fresh(b), fresh(c)) | Var(a) => Var(fresh(a)) | Let(a, b, c) => Let(fresh(a), fresh(b), fresh(c)) - | LetAnn(a, b, c, d) => - LetAnn(fresh(a), fresh(b), fresh(c), fresh(d)) | Fix(a, b) => Fix(fresh(a), fresh(b)) - | FixAnn(a, b, c) => FixAnn(fresh(a), fresh(b), fresh(c)) | Fun(a, b) => Fun(fresh(a), fresh(b)) - | FunAnn(a, b, c) => FunAnn(fresh(a), fresh(b), fresh(c)) | Ap(a, b) => Ap(fresh(a), fresh(b)) | Pair(a, b) => Pair(fresh(a), fresh(b)) | Triv => Triv | PrjL(a) => PrjL(fresh(a)) | PrjR(a) => PrjR(fresh(a)) - | LetPair(a, b, c, d) => - LetPair(fresh(a), fresh(b), fresh(c), fresh(d)) | InjL(a) => InjL(fresh(a)) | InjR(a) => InjR(fresh(a)) | Case(a, b, c, d, e) => @@ -805,6 +784,9 @@ let of_spec = (rule: Rule.t): (t, list(t)) => { | TVar(a) => TVar(fresh(a)) | Rec(a, b) => Rec(fresh(a), fresh(b)) | Pat(a) => Pat(fresh(a)) + | Cast(a, b) => Cast(fresh(a), fresh(b)) + | PatStrip(a) => PatStrip(fresh(a)) + | PatPair(a, b) => PatPair(fresh(a), fresh(b)) | TPat(a) => TPat(fresh(a)) | Atom(a) => Atom(fresh(a)) | And(a, b) => And(fresh(a), fresh(b)) diff --git a/src/haz3lcore/derivation/RuleTest.re b/src/haz3lcore/derivation/RuleTest.re index 5e3fe0b19..09e49bf5e 100644 --- a/src/haz3lcore/derivation/RuleTest.re +++ b/src/haz3lcore/derivation/RuleTest.re @@ -1,245 +1,218 @@ open Util; -[@deriving (show({with_path: false}), sexp, yojson)] -type op = - // Get what has been registered - | Get(string) - // These op do not take effect on frontend, but is essential - | VarOfPat(op) // Pat => Var - | TVarOfTPat(op) // TPat => TVar - // These op perform syntax reconstruction - | HasType(op, op) // HasType(Var, Typ) - | Type(op) // Type(TVar) - | Fix(op, op) // Fix(Pat, Exp) - | Rec(op, op) // Rec(TPat, Typ) - // These op perform pure calculation - | Subst((op, op), op) // Subst((v, Pat), e) - | SubstTy((op, op), op) // SubstTy((v, TPat), Typ) - | Cons(op, op) - | Neg(op) - | Plus(op, op) - | Minus(op, op) - | Times(op, op); - -// module Unbox = { -// // Note (Zhiyao): This module is responsible for unboxing syntax elements with -// // primitive types, such as NumLit(int) and Var(string). We handle unboxing in -// // this separate module to avoid using GADTs in the main module. -// // -// // However, in RuleSpec, we have already checked the syntax cls, so (suppose -// // our implementation is correct) we should not raise any exception here. We -// // are simply unboxing the syntax to its primitive type. - -// type t(_) = -// | Ctx: t(list(DrvSyntax.t)) -// | NumLit: t(int) -// | Var: t(string) -// | TVar: t(string) -// | Pat: t(string) -// | TPat: t(string) -// | Atom: t(string); +let rec string_of_pat = syntax => + switch (DrvSyntax.term_of(syntax)) { + | Pat(s) => s + | Cast(p, _) => string_of_pat(p) + | _ => failwith("string_of_pat: expected Pat") + }; +let string_of_tpat = syntax => + switch (DrvSyntax.term_of(syntax)) { + | TPat(s) => s + | _ => failwith("string_of_pat: expected Pat") + }; +let rec int_of_numlit = syntax => + switch (DrvSyntax.term_of(syntax)) { + | NumLit(i) => i + | Neg(syntax') => - int_of_numlit(syntax') + | _ => failwith("int_of_numlit: expected NumLit") + }; +let list_of_ctx = syntax => + switch (DrvSyntax.term_of(syntax)) { + | Ctx(xs) => xs + | _ => failwith("list_of_ctx: expected Ctx") + }; -// let rec go: type a. (DrvSyntax.t, t(a)) => result(a, RuleSpec.failure) = -// (syntax, op) => { -// switch ((op, DrvSyntax.term_of(syntax))) { -// | (Ctx, Ctx(ctx)) => Ok(ctx) -// | (NumLit, NumLit(n)) => Ok(n) -// | (Var, Var(s)) => Ok(s) -// | (TVar, TVar(s)) => Ok(s) -// | (Pat, Pat(s)) => Ok(s) -// | (TPat, TPat(s)) => Ok(s) -// | (Atom, Atom(s)) => Ok(s) -// | (Ctx, _) -// | (NumLit, _) -// | (Var, _) -// | (TVar, _) -// | (Pat, _) -// | (TPat, _) -// | (Atom, _) => failwith("RuleTest.Unbox.go: cannot unbox") -// }; -// }; -// }; +module Operation = { + [@deriving (show({with_path: false}), sexp, yojson)] + type t = + // Get what has been registered + | Get(string) + // These t do not take effect on frontend, but is essential + | VarOfPat(t) // VarOfPat(Pat(_)) + | TVarOfTPat(t) // TVarOfTPat(TPat(_)) + // These t perform syntax reconstruction + | HasType(t, t) // HasType(Var(_), _) + | Type(t) // Type(TVar(_)) + | Fix(t, t) // Fix(Pat(_), _) + | Rec(t, t) // Rec(TPat(_), _) + // These t perform pure calculation + | Subst((t, t), t) // Subst((_, Pat(_)), _) + | SubstTy((t, t), t) // SubstTy((_, TPat(_)), _) + | Cons(t, t) // Cons(_, Ctx(_)) + | Neg(t) // Neg(NumLit(_)) + | Plus(t, t) // Plus(NumLit(_), NumLit(_)) + | Minus(t, t) // Minus(NumLit(_), NumLit(_)) + | Times(t, t); // Times(NumLit(_), NumLit(_)) -// module Operation = { -// // [@deriving (show({with_path: false}), sexp, yojson)] + let precedence: t => int = { + module P = Precedence; + fun + | Get(_) => P.max + | VarOfPat(_) => P.max + | TVarOfTPat(_) => P.max + | HasType(_, _) => P.ann + | Type(_) => P.ann + | Fix(_) => P.fun_ + | Rec(_) => P.type_arrow + 2 + | Subst(_) => P.ap + | SubstTy(_) => P.ap + | Cons(_) => P.comma + | Neg(_) => P.neg + | Plus(_) => P.plus + | Minus(_) => P.plus + | Times(_) => P.mult; + }; -// type specced = RuleSpec.specced; + let repr = (~sp: string=" ", p: int, operation: t): Aba.t(string, t) => { + let p' = precedence(operation); + let tight_start = s => + s == "" + || List.exists(String.ends_with(s, ~suffix=_), ["/", "「", "」"]); + let tight_end = s => + s == "" + || List.exists(String.starts_with(s, ~prefix=_), ["/", "」", ","]); + let mk_parens = labels => + labels + |> ListUtil.map_first(s => p < p' ? "(" ++ s : s) + |> ListUtil.map_last(s => p < p' ? s ++ ")" : s); + let op = labels => + labels + |> List.map(s => + (tight_end(s) ? "" : sp) ++ s ++ (tight_start(s) ? "" : sp) + ) + |> ListUtil.map_first(s => + String.trim(s) ++ (tight_start(s) ? "" : sp) + ) + |> ListUtil.map_last(s => (tight_end(s) ? "" : sp) ++ String.trim(s)) + |> mk_parens; + let bin = (labels: list(string)) => op([""] @ labels @ [""]); + let pre = (labels: list(string)) => op(labels @ [""]); + let post = (labels: list(string)) => op([""] @ labels); + let op_sg = (label: string) => [label]; + let bin_sg = (label: string) => bin([label]); + let pre_sg = (label: string) => pre([label]); + let post_sg = (label: string) => post([label]); + switch (operation) { + | Get(s) => (s |> op_sg, []) + | VarOfPat(p) => ([] |> bin, [p]) + | TVarOfTPat(t) => ([] |> bin, [t]) + | HasType(x, t) => (":" |> bin_sg, [x, t]) + | Type(a) => ("type" |> post_sg, [a]) + | Fix(p, e) => (["fix", "→"] |> pre, [p, e]) + | Rec(t, a) => (["rec", "is"] |> pre, [t, a]) + | Subst((v, x), e) => (["「", "/", "」"] |> pre, [v, x, e]) + | SubstTy((t, a), e) => (["「", "/", "」"] |> pre, [t, a, e]) + | Cons(e, l) => ("," |> bin_sg, [l, e]) + | Neg(n) => ("-" |> pre_sg, [n]) + | Plus(n1, n2) => ("+" |> bin_sg, [n1, n2]) + | Minus(n1, n2) => ("-" |> bin_sg, [n1, n2]) + | Times(n1, n2) => ("×" |> bin_sg, [n1, n2]) + }; + }; -// type t(_) = -// // Get what has been registered -// | Unbox(Unbox.t('a), SymbolMap.key): t('a) -// | Get(string): t(syntax) -// // Reconstructing -// | Type(t(syntax)): t(syntax) -// | HasType(t(syntax), t(syntax)): t(syntax) -// | Fix(t(syntax), t(syntax)): t(syntax) -// | Rec(t(syntax), t(syntax)): t(syntax) -// | Var(t(string)): t(syntax) -// | TVar(t(string)): t(syntax) -// | NumLit(t(int)): t(syntax) -// // Operations -// | Subst((t(syntax), t(string)), t(syntax)): t(syntax) -// | SubstTy((t(syntax), t(string)), t(syntax)): t(syntax) -// | Cons(t(syntax), t(list(syntax))): t(syntax) -// | Neg(t(int)): t(int) -// | Plus(t(int), t(int)): t(int) -// | Minus(t(int), t(int)): t(int) -// | Times(t(int), t(int)): t(int); + let rec show = (p, syntax) => + syntax + |> repr(p) + |> Aba.join(Fun.id, show(precedence(syntax))) + |> String.concat(""); -// type failure = -// | FailUnbox(RuleSpec.specced) -// | NotReg; // No chance to show in frontend + let show = show(Precedence.min); -// let rec go: type a. (RuleSpec.map, t(a)) => result(a, failure) = -// (map, op) => { -// let (let$) = (x, f) => -// switch (x) { -// | Ok(x) => f(x) -// | Error(e) => Error(e) -// }; -// let go = go(map); -// switch (op) { -// | Get(s) => -// switch (RuleSpec.Map.find_opt(s, map)) { -// | Some((_, syntax)) => Ok(syntax) -// | None => Error(NotReg) -// } -// | D_Ctx(a) => -// let$ syntax = go(a); -// switch (DrvSyntax.term_of(syntax)) { -// | Ctx(ctx) => Ok(ctx) -// | _ => Error("RuleTest.go: not a context") -// }; -// | D_NumLit(a) => -// let$ syntax = go(a); -// switch (DrvSyntax.term_of(syntax)) { -// | NumLit(n) => Ok(n) -// | _ => Error("RuleTest.go: not a number") -// }; -// | _ => failwith("RuleTest.go: not implemented") -// }; -// }; -// }; + let rec show_linked = (p, map: RuleSpec.map, op) => + switch (op) { + | Get(s) => + switch (RuleSpec.Map.find_opt(s, map)) { + | Some(specced) => RuleSpec.show_linked(specced) + | None => s + } + | _ => + op + |> repr(p) + |> Aba.join(Fun.id, show_linked(precedence(op), map)) + |> String.concat("") + }; -module P = Precedence; + let show_linked = show_linked(Precedence.min); -let precedence_op: op => int = - fun - | Get(_) => P.max - | VarOfPat(_) => P.max - | TVarOfTPat(_) => P.max - | HasType(_, _) => P.ann - | Type(_) => P.ann - | Fix(_) => P.fun_ - | Rec(_) => P.type_arrow + 2 - | Subst(_) => P.ap - | SubstTy(_) => P.ap - | Cons(_) => P.comma - | Neg(_) => P.neg - | Plus(_) => P.plus - | Minus(_) => P.plus - | Times(_) => P.mult; + let rec get_symbols: t => list(string) = + fun + | Get(s) => [s] + | VarOfPat(p) => get_symbols(p) + | TVarOfTPat(t) => get_symbols(t) + | HasType(x, t) => get_symbols(x) @ get_symbols(t) + | Type(a) => get_symbols(a) + | Fix(p, e) => get_symbols(p) @ get_symbols(e) + | Rec(t, a) => get_symbols(t) @ get_symbols(a) + | Subst((v, x), e) => get_symbols(v) @ get_symbols(x) @ get_symbols(e) + | SubstTy((t, a), e) => + get_symbols(t) @ get_symbols(a) @ get_symbols(e) + | Cons(e, l) => get_symbols(e) @ get_symbols(l) + | Neg(n) => get_symbols(n) + | Plus(n1, n2) => get_symbols(n1) @ get_symbols(n2) + | Minus(n1, n2) => get_symbols(n1) @ get_symbols(n2) + | Times(n1, n2) => get_symbols(n1) @ get_symbols(n2); -let repr_op = (~sp: string=" ", p: int, operation: op): Aba.t(string, op) => { - let p' = precedence_op(operation); - let tight_start = s => - s == "" - || List.exists(String.ends_with(s, ~suffix=_), ["/", "「", "」"]); - let tight_end = s => - s == "" - || List.exists(String.starts_with(s, ~prefix=_), ["/", "」", ","]); - let mk_parens = labels => - labels - |> ListUtil.map_first(s => p < p' ? "(" ++ s : s) - |> ListUtil.map_last(s => p < p' ? s ++ ")" : s); - let op = labels => - labels - |> List.map(s => - (tight_end(s) ? "" : sp) ++ s ++ (tight_start(s) ? "" : sp) - ) - |> ListUtil.map_first(s => String.trim(s) ++ (tight_start(s) ? "" : sp)) - |> ListUtil.map_last(s => (tight_end(s) ? "" : sp) ++ String.trim(s)) - |> mk_parens; - let bin = (labels: list(string)) => op([""] @ labels @ [""]); - let pre = (labels: list(string)) => op(labels @ [""]); - let post = (labels: list(string)) => op([""] @ labels); - let op_sg = (label: string) => [label]; - let bin_sg = (label: string) => bin([label]); - let pre_sg = (label: string) => pre([label]); - let post_sg = (label: string) => post([label]); - switch (operation) { - | Get(s) => (s |> op_sg, []) - | VarOfPat(p) => ([] |> bin, [p]) - | TVarOfTPat(t) => ([] |> bin, [t]) - | HasType(x, t) => (":" |> bin_sg, [x, t]) - | Type(a) => ("type" |> post_sg, [a]) - | Fix(p, e) => (["fix", "→"] |> pre, [p, e]) - | Rec(t, a) => (["rec", "is"] |> pre, [t, a]) - | Subst((v, x), e) => (["「", "/", "」"] |> pre, [v, x, e]) - | SubstTy((t, a), e) => (["「", "/", "」"] |> pre, [t, a, e]) - | Cons(e, l) => ("," |> bin_sg, [l, e]) - | Neg(n) => ("-" |> pre_sg, [n]) - | Plus(n1, n2) => ("+" |> bin_sg, [n1, n2]) - | Minus(n1, n2) => ("-" |> bin_sg, [n1, n2]) - | Times(n1, n2) => ("×" |> bin_sg, [n1, n2]) - }; + let rec go: (RuleSpec.map, t) => DrvSyntax.t = + (map, op) => { + let go = go(map); + switch (op) { + | Get(s) => + switch (RuleSpec.Map.find_opt(s, map)) { + | Some((_, syntax)) => syntax + | None => Hole("Not found: " ++ s) |> DrvSyntax.fresh + } + | VarOfPat(p) => + let p = go(p); + let (_, rewrap: DrvSyntax.term => 'b) = IdTagged.unwrap(p); + Var(p |> string_of_pat) |> rewrap; + | TVarOfTPat(t) => + let t = go(t); + let (_, rewrap: DrvSyntax.term => 'b) = IdTagged.unwrap(t); + TVar(t |> string_of_tpat) |> rewrap; + | HasType(x, t) => HasType(go(x), go(t)) |> DrvSyntax.fresh + | Type(a) => Type(go(a)) |> DrvSyntax.fresh + | Fix(p, e) => Fix(go(p), go(e)) |> DrvSyntax.fresh + | Rec(t, a) => Rec(go(t), go(a)) |> DrvSyntax.fresh + | Subst((v, x), e) => + DrvSyntax.subst(go(v), go(x) |> string_of_pat, go(e)) + | SubstTy((t, a), e) => + DrvSyntax.subst_ty(go(t), go(a) |> string_of_tpat, go(e)) + | Cons(p, ctx) => + let p = go(p); + let ctx = go(ctx) |> list_of_ctx; + Ctx(DrvSyntax.cons_ctx(ctx, p)) |> DrvSyntax.fresh; + | Neg(n) => + let n = go(n) |> int_of_numlit; + NumLit(- n) |> DrvSyntax.fresh; + | Plus(n1, n2) => + let n1 = go(n1) |> int_of_numlit; + let n2 = go(n2) |> int_of_numlit; + NumLit(n1 + n2) |> DrvSyntax.fresh; + | Minus(n1, n2) => + let n1 = go(n1) |> int_of_numlit; + let n2 = go(n2) |> int_of_numlit; + NumLit(n1 - n2) |> DrvSyntax.fresh; + | Times(n1, n2) => + let n1 = go(n1) |> int_of_numlit; + let n2 = go(n2) |> int_of_numlit; + NumLit(n1 * n2) |> DrvSyntax.fresh; + }; + }; }; -let rec show_op = (p, syntax) => - syntax - |> repr_op(p) - |> Aba.join(Fun.id, show_op(precedence_op(syntax))) - |> String.concat(""); - -let show_op = show_op(P.min); - -let rec show_linked_op = (p, map: RuleSpec.map, op) => - switch (op) { - | Get(s) => - switch (RuleSpec.Map.find_opt(s, map)) { - | Some(specced) => RuleSpec.show_linked(specced) - | None => s - } - | _ => - op - |> repr_op(p) - |> Aba.join(Fun.id, show_linked_op(precedence_op(op), map)) - |> String.concat("") - }; - -let show_linked_op = show_linked_op(P.min); - -let rec get_symbols_op: op => list(string) = - fun - | Get(s) => [s] - | VarOfPat(p) => get_symbols_op(p) - | TVarOfTPat(t) => get_symbols_op(t) - | HasType(x, t) => get_symbols_op(x) @ get_symbols_op(t) - | Type(a) => get_symbols_op(a) - | Fix(p, e) => get_symbols_op(p) @ get_symbols_op(e) - | Rec(t, a) => get_symbols_op(t) @ get_symbols_op(a) - | Subst((v, x), e) => - get_symbols_op(v) @ get_symbols_op(x) @ get_symbols_op(e) - | SubstTy((t, a), e) => - get_symbols_op(t) @ get_symbols_op(a) @ get_symbols_op(e) - | Cons(e, l) => get_symbols_op(e) @ get_symbols_op(l) - | Neg(n) => get_symbols_op(n) - | Plus(n1, n2) => get_symbols_op(n1) @ get_symbols_op(n2) - | Minus(n1, n2) => get_symbols_op(n1) @ get_symbols_op(n2) - | Times(n1, n2) => get_symbols_op(n1) @ get_symbols_op(n2); - [@deriving (show({with_path: false}), sexp, yojson)] type t = - | Eq(op, op) - | NotEq(op, op) - | Lt(op, op) - | NotLt(op, op) - | Gt(op, op) - | NotGt(op, op) - | Mem(op, op) - | Subset(op, op); + | Eq(Operation.t, Operation.t) + | NotEq(Operation.t, Operation.t) + | Lt(Operation.t, Operation.t) + | NotLt(Operation.t, Operation.t) + | Gt(Operation.t, Operation.t) + | NotGt(Operation.t, Operation.t) + | Mem(Operation.t, Operation.t) + | Subset(Operation.t, Operation.t); -let repr = (~sp: string=" ", test: t): Aba.t(string, op) => { +let repr = (~sp: string=" ", test: t): Aba.t(string, Operation.t) => { let op = labels => labels |> List.map(s => sp ++ s ++ sp) @@ -260,7 +233,7 @@ let repr = (~sp: string=" ", test: t): Aba.t(string, op) => { }; let show = syntax => - syntax |> repr |> Aba.join(Fun.id, show_op) |> String.concat(""); + syntax |> repr |> Aba.join(Fun.id, Operation.show) |> String.concat(""); let show_linked = (map: RuleSpec.map, test: t) => test @@ -272,7 +245,7 @@ let show_linked = (map: RuleSpec.map, test: t) => | _ => aba } ) - |> Aba.join(Fun.id, show_linked_op(map)) + |> Aba.join(Fun.id, Operation.show_linked(map)) |> String.concat(""); let get_symbols: t => list(string) = @@ -284,80 +257,11 @@ let get_symbols: t => list(string) = | Gt(a, b) | NotGt(a, b) | Mem(a, b) - | Subset(a, b) => get_symbols_op(a) @ get_symbols_op(b); - -let string_of_pat = syntax => - switch (DrvSyntax.term_of(syntax)) { - | Pat(s) => s - | _ => failwith("string_of_pat: expected Pat") - }; -let string_of_tpat = syntax => - switch (DrvSyntax.term_of(syntax)) { - | TPat(s) => s - | _ => failwith("string_of_pat: expected Pat") - }; -let rec int_of_numlit = syntax => - switch (DrvSyntax.term_of(syntax)) { - | NumLit(i) => i - | Neg(syntax') => - int_of_numlit(syntax') - | _ => failwith("int_of_numlit: expected NumLit") - }; -let list_of_ctx = syntax => - switch (DrvSyntax.term_of(syntax)) { - | Ctx(xs) => xs - | _ => failwith("list_of_ctx: expected Ctx") - }; - -let rec go_op: (RuleSpec.map, op) => DrvSyntax.t = - (map, op) => { - let go_op = go_op(map); - switch (op) { - | Get(s) => - switch (RuleSpec.Map.find_opt(s, map)) { - | Some((_, syntax)) => syntax - | None => Hole("Not found: " ++ s) |> DrvSyntax.fresh - } - | VarOfPat(p) => - let p = go_op(p); - let (_, rewrap: DrvSyntax.term => 'b) = IdTagged.unwrap(p); - Var(p |> string_of_pat) |> rewrap; - | TVarOfTPat(t) => - let t = go_op(t); - let (_, rewrap: DrvSyntax.term => 'b) = IdTagged.unwrap(t); - TVar(t |> string_of_tpat) |> rewrap; - | HasType(x, t) => HasType(go_op(x), go_op(t)) |> DrvSyntax.fresh - | Type(a) => Type(go_op(a)) |> DrvSyntax.fresh - | Fix(p, e) => Fix(go_op(p), go_op(e)) |> DrvSyntax.fresh - | Rec(t, a) => Rec(go_op(t), go_op(a)) |> DrvSyntax.fresh - | Subst((v, x), e) => - DrvSyntax.subst(go_op(v), go_op(x) |> string_of_pat, go_op(e)) - | SubstTy((t, a), e) => - DrvSyntax.subst_ty(go_op(t), go_op(a) |> string_of_tpat, go_op(e)) - | Cons(p, ctx) => - let p = go_op(p); - let ctx = go_op(ctx) |> list_of_ctx; - Ctx(DrvSyntax.cons_ctx(ctx, p)) |> DrvSyntax.fresh; - | Neg(n) => - let n = go_op(n) |> int_of_numlit; - NumLit(- n) |> DrvSyntax.fresh; - | Plus(n1, n2) => - let n1 = go_op(n1) |> int_of_numlit; - let n2 = go_op(n2) |> int_of_numlit; - NumLit(n1 + n2) |> DrvSyntax.fresh; - | Minus(n1, n2) => - let n1 = go_op(n1) |> int_of_numlit; - let n2 = go_op(n2) |> int_of_numlit; - NumLit(n1 - n2) |> DrvSyntax.fresh; - | Times(n1, n2) => - let n1 = go_op(n1) |> int_of_numlit; - let n2 = go_op(n2) |> int_of_numlit; - NumLit(n1 * n2) |> DrvSyntax.fresh; - }; - }; + | Subset(a, b) => Operation.get_symbols(a) @ Operation.get_symbols(b); let go: (RuleSpec.map, t) => bool = (map, test) => { - let go_op = go_op(map); + let go_op = Operation.go(map); switch (test) { | Eq(a, b) => DrvSyntax.eq(go_op(a), go_op(b)) | NotEq(a, b) => DrvSyntax.eq(go_op(a), go_op(b)) @@ -388,14 +292,14 @@ let go: (RuleSpec.map, t) => bool = }; }; -let of_tests = (rule: Rule.t): list(t) => { +let of_tests: Rule.t => list(t) = { module SymbolMap = SymbolMap.M({ - type target = op; + type target = Operation.t; let f: string => target = s => Get(s); }); SymbolMap.( - switch (rule) { + fun // Type Validity | TV_Num | TV_Bool @@ -542,6 +446,104 @@ let of_tests = (rule: Rule.t): list(t) => { | Implies_E => [] | Truth_I => [] | Falsity_E => [] - } ); }; + +// module Unbox = { +// // Note (Zhiyao): This module is responsible for unboxing syntax elements with +// // primitive types, such as NumLit(int) and Var(string). We handle unboxing in +// // this separate module to avoid using GADTs in the main module. +// // +// // However, in RuleSpec, we have already checked the syntax cls, so (suppose +// // our implementation is correct) we should not raise any exception here. We +// // are simply unboxing the syntax to its primitive type. + +// type t(_) = +// | Ctx: t(list(DrvSyntax.t)) +// | NumLit: t(int) +// | Var: t(string) +// | TVar: t(string) +// | Pat: t(string) +// | TPat: t(string) +// | Atom: t(string); + +// let rec go: type a. (DrvSyntax.t, t(a)) => result(a, RuleSpec.failure) = +// (syntax, op) => { +// switch ((op, DrvSyntax.term_of(syntax))) { +// | (Ctx, Ctx(ctx)) => Ok(ctx) +// | (NumLit, NumLit(n)) => Ok(n) +// | (Var, Var(s)) => Ok(s) +// | (TVar, TVar(s)) => Ok(s) +// | (Pat, Pat(s)) => Ok(s) +// | (TPat, TPat(s)) => Ok(s) +// | (Atom, Atom(s)) => Ok(s) +// | (Ctx, _) +// | (NumLit, _) +// | (Var, _) +// | (TVar, _) +// | (Pat, _) +// | (TPat, _) +// | (Atom, _) => failwith("RuleTest.Unbox.go: cannot unbox") +// }; +// }; +// }; + +// module Operation = { +// // [@deriving (show({with_path: false}), sexp, yojson)] + +// type specced = RuleSpec.specced; + +// type t(_) = +// // Get what has been registered +// | Unbox(Unbox.t('a), SymbolMap.key): t('a) +// | Get(string): t(syntax) +// // Reconstructing +// | Type(t(syntax)): t(syntax) +// | HasType(t(syntax), t(syntax)): t(syntax) +// | Fix(t(syntax), t(syntax)): t(syntax) +// | Rec(t(syntax), t(syntax)): t(syntax) +// | Var(t(string)): t(syntax) +// | TVar(t(string)): t(syntax) +// | NumLit(t(int)): t(syntax) +// // Operations +// | Subst((t(syntax), t(string)), t(syntax)): t(syntax) +// | SubstTy((t(syntax), t(string)), t(syntax)): t(syntax) +// | Cons(t(syntax), t(list(syntax))): t(syntax) +// | Neg(t(int)): t(int) +// | Plus(t(int), t(int)): t(int) +// | Minus(t(int), t(int)): t(int) +// | Times(t(int), t(int)): t(int); + +// type failure = +// | FailUnbox(RuleSpec.specced) +// | NotReg; // No chance to show in frontend + +// let rec go: type a. (RuleSpec.map, t(a)) => result(a, failure) = +// (map, op) => { +// let (let$) = (x, f) => +// switch (x) { +// | Ok(x) => f(x) +// | Error(e) => Error(e) +// }; +// let go = go(map); +// switch (op) { +// | Get(s) => +// switch (RuleSpec.Map.find_opt(s, map)) { +// | Some((_, syntax)) => Ok(syntax) +// | None => Error(NotReg) +// } +// | D_Ctx(a) => +// let$ syntax = go(a); +// switch (DrvSyntax.term_of(syntax)) { +// | Ctx(ctx) => Ok(ctx) +// | _ => Error("RuleTest.go: not a context") +// }; +// | D_NumLit(a) => +// let$ syntax = go(a); +// switch (DrvSyntax.term_of(syntax)) { +// | NumLit(n) => Ok(n) +// | _ => Error("RuleTest.go: not a number") +// }; +// | _ => failwith("RuleTest.go: not implemented") +// }; +// }; diff --git a/src/haz3lcore/derivation/RuleVerify.re b/src/haz3lcore/derivation/RuleVerify.re index 9701c4270..85e214f0a 100644 --- a/src/haz3lcore/derivation/RuleVerify.re +++ b/src/haz3lcore/derivation/RuleVerify.re @@ -12,7 +12,7 @@ type tests = list(RuleTest.t); let spec_fill_eq_test: (RuleTest.t, RuleSpec.t) => RuleSpec.t = fun | Eq(Get(s'), op) => - RuleSpec.map_reg(s => s == s' ? RuleTest.show_op(op) : s) + RuleSpec.map_reg(s => s == s' ? RuleTest.Operation.show(op) : s) | _ => Fun.id; let spec_fill_eq_tests: (spec, tests) => spec = @@ -26,7 +26,8 @@ let spec_fill_eq_tests: (spec, tests) => spec = let tests_fill_eq_tests: tests => tests = List.map( fun - | RuleTest.Eq(Get(s), op) => RuleTest.Eq(Get(RuleTest.show_op(op)), op) + | RuleTest.Eq(Get(_), op) => + RuleTest.Eq(Get(RuleTest.Operation.show(op)), op) | _ as test => test, ); diff --git a/src/haz3lweb/explainthis/ExplainThisForm.re b/src/haz3lweb/explainthis/ExplainThisForm.re index ef18d93da..ad2404061 100644 --- a/src/haz3lweb/explainthis/ExplainThisForm.re +++ b/src/haz3lweb/explainthis/ExplainThisForm.re @@ -150,36 +150,9 @@ type pat_sub_form_id = | Ctr | Ap; -[@deriving (show({with_path: false}), sexp, yojson)] -type test_id = - | Neg - | Plus - | Minus - | Times - | Lt - | NotLt - | Gt - | NotGt - | Eq - | NotEq - | Subst - | Subst2 - | SubstTy - | Cons - | ConsHasTy - | ConsHasTy2 - | ConsValid - | Mem - | MemHasTy - | Subset; - [@deriving (show({with_path: false}), sexp, yojson)] type form_id = - | DrvPremiseMismatch - | DrvFailUnbox - | DrvNotAList - | DrvNotEqual - | DrvFailTest(test_id) + | Derivation | EmptyHoleExp | MultiHoleExp | TrivExp @@ -275,11 +248,7 @@ type form = { // MAYBE don't even need an id at all for the group - just use the most specific (1st) form id in forms [@deriving (show({with_path: false}), sexp, yojson)] type group_id = - | DrvPremiseMismatch - | DrvFailUnbox - | DrvNotAList - | DrvNotEqual - | DrvFailTest(test_id) + | Derivation | EmptyHoleExp | MultiHoleExp | TrivExp diff --git a/src/haz3lweb/explainthis/data/DeductionExp.re b/src/haz3lweb/explainthis/data/DeductionExp.re index 391007685..5af640f29 100644 --- a/src/haz3lweb/explainthis/data/DeductionExp.re +++ b/src/haz3lweb/explainthis/data/DeductionExp.re @@ -181,10 +181,10 @@ let show_ghost = (t: option(t)) => }; let premise_mismatch: group = { - id: DrvPremiseMismatch, + id: Derivation, forms: [ { - id: DrvPremiseMismatch, + id: Derivation, syntactic_form: [], expandable_id: None, explanation: "", diff --git a/src/haz3lweb/view/exercise/ExerciseMode.re b/src/haz3lweb/view/exercise/ExerciseMode.re index 477cca813..78f8ab40b 100644 --- a/src/haz3lweb/view/exercise/ExerciseMode.re +++ b/src/haz3lweb/view/exercise/ExerciseMode.re @@ -76,6 +76,7 @@ let view = Some( { open Haz3lcore; + print_endline("Uncaught Rule: " ++ Rule.show(rule)); let spec = RuleSpec.of_spec(rule); let tests = RuleTest.of_tests(rule); let (spec, tests) =