Implement transitivity
diff --git a/spectec/doc/semantics/il/2-env.spectec b/spectec/doc/semantics/il/2-env.spectec index 0fff887..0605802 100644 --- a/spectec/doc/semantics/il/2-env.spectec +++ b/spectec/doc/semantics/il/2-env.spectec
@@ -9,14 +9,17 @@ { TYP (id, typdef)*, FUN (id, fundef)*, REL (id, reldef)*, - GRAM (id, gramdef)* + GRAM (id, gramdef)*, } ;; Environment -syntax E = {S, EXP (id, typ)*} - +syntax E = + { S, + EXP (id, typ)*, + EQ (exp, exp)* + } def $composeenvs(E*) : E hint(show (++)%) def $composeenvs(eps) = {} @@ -39,20 +42,22 @@ ;; Lookup - def $lookup_typ(S, id) : typdef? hint(show %.TYP#(%)) def $lookup_fun(S, id) : fundef? hint(show %.FUN#(%)) def $lookup_rel(S, id) : reldef? hint(show %.REL#(%)) def $lookup_gram(S, id) : gramdef? hint(show %.GRAM#(%)) -def $lookup_exp(S, id) : typ? hint(show %.EXP#(%)) +def $lookup_exp(E, id) : typ? hint(show %.EXP#(%)) +def $lookup_eq(E, exp) : exp? hint(show %.EQ#(%)) -def $lookup_(syntax Y, (id, Y)*, id) : Y? -def $lookup_(syntax Y, eps, x') = eps -def $lookup_(syntax Y, (x, y)* (x', y'), x') = y' -def $lookup_(syntax Y, (x, y)* (x'', y'), x') = $lookup_(Y, (x, y)*, x') -- if x'' =/= x' +def $lookup__(syntax X, syntax Y, (X, Y)*, X) : Y? +def $lookup__(syntax X, syntax Y, eps, x') = eps +def $lookup__(syntax X, syntax Y, (x, y)* (x', y'), x') = y' +def $lookup__(syntax X, syntax Y, (x, y)* (x'', y'), x') = + $lookup__(X, Y, (x, y)*, x') -- if x'' =/= x' -def $lookup_typ(S, x) = $lookup_(typdef, S.TYP, x) -def $lookup_fun(S, x) = $lookup_(fundef, S.FUN, x) -def $lookup_rel(S, x) = $lookup_(reldef, S.REL, x) -def $lookup_gram(S, x) = $lookup_(gramdef, S.GRAM, x) -def $lookup_exp(E, x) = $lookup_(typ, E.EXP, x) +def $lookup_typ(S, x) = $lookup__(id, typdef, S.TYP, x) +def $lookup_fun(S, x) = $lookup__(id, fundef, S.FUN, x) +def $lookup_rel(S, x) = $lookup__(id, reldef, S.REL, x) +def $lookup_gram(S, x) = $lookup__(id, gramdef, S.GRAM, x) +def $lookup_exp(E, x) = $lookup__(id, typ, E.EXP, x) +def $lookup_eq(E, e) = $lookup__(exp, exp, E.EQ, e)
diff --git a/spectec/doc/semantics/il/5-reduction.spectec b/spectec/doc/semantics/il/5-reduction.spectec index 272c8e9..a5d625c 100644 --- a/spectec/doc/semantics/il/5-reduction.spectec +++ b/spectec/doc/semantics/il/5-reduction.spectec
@@ -1,8 +1,7 @@ ;; Types -relation Reduce_typ: S |- typ ~>* typ? relation Step_typ: S |- typ ~> typ? -relation Eq_typ: S |- typ == typ +relation Reduce_typ: S |- typ ~>* typ? relation Expand_typ: S |- typ ~~ deftyp @@ -16,14 +15,6 @@ -- Reduce_typ: S |- t ~>* MATCH x WITH (INST `{} `=> dt) inst* -rule Eq_typ: - S |- t_1 == t_2 - -- Reduce_typ: S |- t_1 ~>* t'_1 - -- Reduce_typ: S |- t_2 ~>* t'_2 - -- if t'_1 = t'_2 - ;; Note: defined types are nominal - - rule Reduce_typ/refl: S |- t ~>* t @@ -230,14 +221,6 @@ relation Reduce_exp: S |- exp ~>* exp? relation Step_exp: S |- exp ~> exp? relation Step_expfield: S |- expfield ~> expfield? -relation Eq_exp: S |- exp == exp - - -rule Eq_exp: - S |- e_1 == e_2 - -- Reduce_exp: S |- e_1 ~>* e'_1 - -- Reduce_exp: S |- e_2 ~>* e'_2 - -- if e'_1 = e'_2 rule Reduce_exp/refl: @@ -1249,14 +1232,6 @@ relation Reduce_arg: S |- arg ~>* arg? relation Step_arg: S |- arg ~> arg? -relation Eq_arg: S |- arg == arg - - -rule Eq_arg: - S |- a_1 == a_2 - -- Reduce_arg: S |- a_1 ~>* a'_1 - -- Reduce_arg: S |- a_2 ~>* a'_2 - -- if a'_1 = a'_2 rule Reduce_arg/refl: @@ -1388,14 +1363,6 @@ relation Reduce_prems: S |- prem* ~>* prem*? relation Step_prems: S |- prem* ~>_subst prem*? -relation Eq_prems: S |- prem* == prem* - - -rule Eq_prems: - S |- pr_1* == pr_2* - -- Reduce_prems: S |- pr_1* ~>* pr'_1* - -- Reduce_prems: S |- pr_2* ~>* pr'_2* - -- if pr'_1* = pr'_2* rule Reduce_prems/refl:
diff --git a/spectec/doc/semantics/il/6-typing.spectec b/spectec/doc/semantics/il/6-typing.spectec index 44b4af9..36ad13a 100644 --- a/spectec/doc/semantics/il/6-typing.spectec +++ b/spectec/doc/semantics/il/6-typing.spectec
@@ -12,6 +12,83 @@ -- (Catable_typ: E |- t' CATABLE)* +;; Equivalence + +relation Eq_typ: E |- typ == typ +relation Eq_exp: E |- exp == exp +relation Eq_arg: E |- arg == arg + +rule Eq_typ/var: + E |- VAR x a_1* == VAR x a_2* + -- (Eq_arg: E |- a_1 == a_2)* + +rule Eq_typ/tup: + E |- TUP (x_1 `: t_1) tb_1* == TUP (x_2 `: t_2) tb_2* + -- Eq_typ: E |- t_1 == t_2 + -- Eq_typ: E ++ {EXP (x_1, t_1)} |- TUP tb_1* == $subst_typ({EXP (x_2, VAR x_1)}, TUP tb2*) + +rule Eq_typ/iter: + E |- ITER t_1 it == ITER t_2 it + -- Eq_typ: E |- t_1 == t_2 + +rule Eq_typ/refl: + E |- t == t + +rule Eq_typ/trans: + E |- t_1 == t_2 + -- Eq_typ: E |- t_1 == t' + -- Eq_typ: E |- t' == t_2 + +rule Eq_typ/reduce: + E |- t_1 == t_2 + -- Reduce_typ: E |- t_1 ~>* t'_1 + -- Reduce_typ: E |- t_2 ~>* t'_2 + -- if t'_1 = t'_2 + ;; Note: defined types are nominal + + +rule Eq_exp/refl: + E |- e == e + +rule Eq_exp/trans: + E |- e_1 == e_2 + -- Eq_exp: E |- e_1 == e' + -- Eq_exp: E |- e' == e_2 + +rule Eq_exp/reduce: + E |- e_1 == e_2 + -- Reduce_exp: E |- e_1 ~>* e'_1 + -- Reduce_exp: E |- e_2 ~>* e'_2 + -- if e'_1 = e'_2 + +rule Eq_exp/recall: + E |- e_1 == e_2 + -- if (e_1, e_2) <- E.EQ + + +rule Eq_arg/EXP: + E |- EXP e_1 == EXP e_2 + -- Eq_exp: E |- e_1 == e_2 + +rule Eq_arg/TYP: + E |- TYP t_1== TYP t_2 + -- Eq_typ: E |- t_1 == t_2 + +rule Eq_arg/refl: + E |- a == a + +rule Eq_arg/trans: + E |- a_1 == a_2 + -- Eq_arg: E |- a_1 == a' + -- Eq_arg: E |- a' == a_2 + +rule Eq_arg/reduce: + E |- a_1 == a_2 + -- Reduce_arg: E |- a_1 ~>* a'_1 + -- Reduce_arg: E |- a_2 ~>* a'_2 + -- if a'_1 = a'_2 + + ;; Subtyping relation Sub_numtyp: |- numtyp <: numtyp @@ -519,6 +596,10 @@ E |- IF e : OK -| {} -- Ok_exp: E |- e : BOOL +rule Ok_prem/IF-EQ: + E |- IF (CMP EQ e_1 e_2) : OK -| {EQ (e1, e2)} + -- Ok_exp: E |- CMP EQ e_1 e_2 : BOOL + rule Ok_prem/ELSE: E |- ELSE : OK -| {} @@ -527,7 +608,7 @@ -- Ok_prem: E |- pr : OK -| {} rule Ok_prem/LET: - E |- LET `{q*} e_1 `= e_2 : OK -| $paramenv(q*) + E |- LET `{q*} e_1 `= e_2 : OK -| $paramenv(q*) ++ {EQ (e1, e2)} -- Ok_exp: E ++ $paramenv(q*) |- e_1 : t -- Ok_exp: E |- e_2 : t
diff --git a/spectec/src/il/env.ml b/spectec/src/il/env.ml index ce3d227..f2fc9c9 100644 --- a/spectec/src/il/env.ml +++ b/spectec/src/il/env.ml
@@ -95,13 +95,21 @@ let rebind_rel env id rhs = {env with rels = rebind "relation" env.rels id rhs} let rebind_gram env id rhs = {env with grams = rebind "grammar" env.grams id rhs} -let record_eq env e1 e2 = {env with eqs = (e1, e2)::env.eqs} +let record_eq env e1 e2 = + match Eq.compare_exp e1 e2 with + | +1 -> {env with eqs = (e1, e2)::env.eqs} + | -1 -> {env with eqs = (e2, e1)::env.eqs} + | _ -> env + let recall_eq env e1 e2 = List.exists (fun (x, y) -> Eq.eq_exp x e1 && Eq.eq_exp y e2 || Eq.eq_exp x e2 && Eq.eq_exp y e1 ) env.eqs +let recall_eq_simp env e = + Option.map snd (List.find_opt (fun (x, _) -> Eq.eq_exp e x) env.eqs) + (* Extraction *)
diff --git a/spectec/src/il/eq.ml b/spectec/src/il/eq.ml index 0883605..2e2797d 100644 --- a/spectec/src/il/eq.ml +++ b/spectec/src/il/eq.ml
@@ -5,6 +5,9 @@ (* Helpers *) +let eq_pair eq_x eq_y (x1, y1) (x2, y2) = + eq_x x1 x2 && eq_y y1 y2 + let eq_opt eq_x xo1 xo2 = match xo1, xo2 with | Some x1, Some x2 -> eq_x x1 x2 @@ -13,20 +16,12 @@ let eq_list eq_x xs1 xs2 = List.length xs1 = List.length xs2 && List.for_all2 eq_x xs1 xs2 -let eq_pair eq_x eq_y (x1, y1) (x2, y2) = - eq_x x1 x2 && eq_y y1 y2 - (* Ids *) -let eq_id x1 x2 = - x1.it = x2.it - -let eq_atom atom1 atom2 = - Atom.eq atom1 atom2 - -let eq_mixop op1 op2 = - Mixop.eq op1 op2 +let eq_id x1 x2 = x1.it = x2.it +let eq_atom = Atom.eq +let eq_mixop = Mixop.eq (* Iteration *) @@ -75,7 +70,8 @@ | CmpE (op1, ot1, e11, e12), CmpE (op2, ot2, e21, e22) -> op1 = op2 && ot1 = ot2 && eq_exp e11 e21 && eq_exp e12 e22 | LiftE e11, LiftE e21 - | LenE e11, LenE e21 -> eq_exp e11 e21 + | LenE e11, LenE e21 + | TheE e11, TheE e21 -> eq_exp e11 e21 | IdxE (e11, e12), IdxE (e21, e22) | CompE (e11, e12), CompE (e21, e22) | MemE (e11, e12), MemE (e21, e22) @@ -98,7 +94,6 @@ eq_exp e11 e21 && eq_iterexp iter1 iter2 | OptE eo1, OptE eo2 -> eq_opt eq_exp eo1 eo2 | ProjE (e1, i1), ProjE (e2, i2) -> eq_exp e1 e2 && i1 = i2 - | TheE e1, TheE e2 -> eq_exp e1 e2 | CaseE (op1, e1, ch1), CaseE (op2, e2, ch2) -> eq_mixop op1 op2 && eq_exp e1 e2 && ch1 = ch2 | CvtE (e1, nt11, nt12), CvtE (e2, nt21, nt22) -> @@ -128,8 +123,8 @@ and eq_sym g1 g2 = match g1.it, g2.it with - | VarG (x1, args1), VarG (x2, args2) -> - eq_id x1 x2 && eq_list eq_arg args1 args2 + | VarG (x1, as1), VarG (x2, as2) -> + eq_id x1 x2 && eq_list eq_arg as1 as2 | SeqG gs1, SeqG gs2 | AltG gs1, AltG gs2 -> eq_list eq_sym gs1 gs2 | RangeG (g11, g12), RangeG (g21, g22) -> eq_sym g11 g21 && eq_sym g12 g22 @@ -172,3 +167,158 @@ | GramP (x1, ps1, t1), GramP (x2, ps2, t2) -> eq_id x1 x2 && eq_list eq_param ps1 ps2 && eq_typ t1 t2 | _, _ -> false + + + +(* Total Ordering *) + +let (>>) o1 o2 = if o1 = 0 then o2 else o1 + +let compare_pair f g (x1, y1) (x2, y2) = + match f x1 x2 with + | 0 -> g y1 y2 + | o -> o + +let compare_opt f xo1 xo2 = + match xo1, xo2 with + | None, None -> 0 + | _, None -> +1 + | None, _ -> -1 + | Some x1, Some x2 -> f x1 x2 + +let rec compare_list f xs1 xs2 = + match xs1, xs2 with + | [], [] -> 0 + | _, [] -> +1 + | [], _ -> -1 + | x1::xs1', x2::xs2' -> + match f x1 x2 with + | 0 -> compare_list f xs1' xs2' + | o -> o + + +(* Ids *) + +let compare_id x1 x2 = compare x1.it x2.it +let compare_atom = Atom.compare +let compare_mixop = Mixop.compare + + +(* Iterators *) + +let rec compare_iter iter1 iter2 = + match iter1, iter2 with + | ListN (e1, xo1), ListN (e2, xo2) -> + compare_exp e1 e2 >> compare_opt compare_id xo1 xo2 + | _, _ -> compare iter1 iter2 + + +(* Types *) + +and compare_typ t1 t2 = + match t1.it, t2.it with + | VarT (x1, as1), VarT (x2, as2) -> + compare_id x1 x2 >> compare_list compare_arg as1 as2 + | TupT xts1, TupT xts2 -> + compare_list (compare_pair compare_id compare_typ) xts1 xts2 + | IterT (t11, iter1), IterT (t21, iter2) -> + compare_typ t11 t21 >> compare_iter iter1 iter2 + | _, _ -> compare t1.it t2.it + +(* Expressions *) + +and compare_exp e1 e2 = + match e1.it, e2.it with + | VarE x1, VarE x2 -> compare_id x1 x2 + | UnE (op1, ot1, e11), UnE (op2, ot2, e21) -> + compare op1 op2 >> compare ot1 ot2 >> compare_exp e11 e21 + | BinE (op1, ot1, e11, e12), BinE (op2, ot2, e21, e22) -> + compare op1 op2 >> compare ot1 ot2 >> + compare_list compare_exp [e11; e12] [e21; e22] + | CmpE (op1, ot1, e11, e12), CmpE (op2, ot2, e21, e22) -> + compare op1 op2 >> compare ot1 ot2 >> + compare_list compare_exp [e11; e12] [e21; e22] + | LiftE e11, LiftE e21 + | LenE e11, LenE e21 + | TheE e11, TheE e21 -> + compare_exp e11 e21 + | IdxE (e11, e12), IdxE (e21, e22) + | CompE (e11, e12), CompE (e21, e22) + | MemE (e11, e12), MemE (e21, e22) + | CatE (e11, e12), CatE (e21, e22) -> + compare_list compare_exp [e11; e12] [e21; e22] + | SliceE (e11, e12, e13), SliceE (e21, e22, e23) -> + compare_list compare_exp [e11; e12; e13] [e21; e22; e23] + | UpdE (e11, p1, e12), UpdE (e21, p2, e22) + | ExtE (e11, p1, e12), ExtE (e21, p2, e22) -> + compare_exp e11 e21 >> compare_path p1 p2 >> compare_exp e12 e22 + | TupE es1, TupE es2 + | ListE es1, ListE es2 -> + compare_list compare_exp es1 es2 + | StrE (efs1, ch1), StrE (efs2 , ch2)-> + compare_list compare_expfield efs1 efs2 >> compare ch1 ch2 + | DotE (e11, atom1), DotE (e21, atom2) -> + compare_exp e11 e21 >> compare_atom atom1 atom2 + | UncaseE (e1, op1), UncaseE (e2, op2) -> + compare_mixop op1 op2 >> compare_exp e1 e2 + | CallE (x1, as1), CallE (x2, as2) -> + compare_id x1 x2 >> compare_list compare_arg as1 as2 + | IterE (e11, iter1), IterE (e21, iter2) -> + compare_exp e11 e21 >> compare_iterexp iter1 iter2 + | OptE eo1, OptE eo2 -> + compare_opt compare_exp eo1 eo2 + | ProjE (e1, i1), ProjE (e2, i2) -> + compare_exp e1 e2 >> compare i1 i2 + | CaseE (op1, e1, ch1), CaseE (op2, e2, ch2) -> + compare_mixop op1 op2 >> compare_exp e1 e2 >> compare ch1 ch2 + | CvtE (e1, nt11, nt12), CvtE (e2, nt21, nt22) -> + compare_exp e1 e2 >> compare nt11 nt21 >> compare nt12 nt22 + | SubE (e1, t11, t12), SubE (e2, t21, t22) -> + compare_exp e1 e2 >> compare_list compare_typ [t11; t12] [t21; t22] + | _, _ -> compare e1.it e2.it + +and compare_expfield (atom1, e1) (atom2, e2) = + compare_atom atom1 atom2 >> compare_exp e1 e2 + +and compare_path p1 p2 = + match p1.it, p2.it with + | IdxP (p11, e1), IdxP (p21, e2) -> + compare_path p11 p21 >> compare_exp e1 e2 + | SliceP (p11, e11, e12), SliceP (p21, e21, e22) -> + compare_path p11 p21 >> compare_exp e11 e21 >> compare_exp e12 e22 + | DotP (p11, atom1), DotP (p21, atom2) -> + compare_path p11 p21 >> compare_atom atom1 atom2 + | _, _ -> compare p1.it p2.it + +and compare_iterexp (iter1, xes1) (iter2, xes2) = + compare_iter iter1 iter2 >> + compare_list (compare_pair compare_id compare_exp) xes1 xes2 + + +(* Grammars *) + +and compare_sym g1 g2 = + match g1.it, g2.it with + | VarG (x1, as1), VarG (x2, as2) -> + compare_id x1 x2 >> compare_list compare_arg as1 as2 + | SeqG gs1, SeqG gs2 + | AltG gs1, AltG gs2 -> + compare_list compare_sym gs1 gs2 + | RangeG (g11, g12), RangeG (g21, g22) -> + compare_list compare_sym [g11; g12] [g21; g22] + | IterG (g11, iter1), IterG (g21, iter2) -> + compare_sym g11 g21 >> compare_iterexp iter1 iter2 + | AttrG (e1, g11), AttrG (e2, g21) -> + compare_exp e1 e2 >> compare_sym g11 g21 + | _, _ -> compare g1.it g2.it + + +(* Definitions *) + +and compare_arg a1 a2 = + match a1.it, a2.it with + | ExpA e1, ExpA e2 -> compare_exp e1 e2 + | TypA t1, TypA t2 -> compare_typ t1 t2 + | DefA x1, DefA x2 -> compare_id x1 x2 + | GramA g1, GramA g2 -> compare_sym g1 g2 + | _, _ -> compare a1.it a2.it
diff --git a/spectec/src/il/eq.mli b/spectec/src/il/eq.mli index 18f0b69..2110e3a 100644 --- a/spectec/src/il/eq.mli +++ b/spectec/src/il/eq.mli
@@ -16,3 +16,14 @@ val eq_opt : ('a -> 'a -> bool) -> 'a option -> 'a option -> bool val eq_list : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool + +val compare_id : id -> id -> int +val compare_atom : atom -> atom -> int +val compare_mixop : mixop -> mixop -> int +val compare_iter : iter -> iter -> int +val compare_iterexp : iterexp -> iterexp -> int +val compare_typ : typ -> typ -> int +val compare_exp : exp -> exp -> int +val compare_path : path -> path -> int +val compare_sym : sym -> sym -> int +val compare_arg : arg -> arg -> int
diff --git a/spectec/src/il/eval.ml b/spectec/src/il/eval.ml index 1b52956..8b818ee 100644 --- a/spectec/src/il/eval.ml +++ b/spectec/src/il/eval.ml
@@ -1191,17 +1191,23 @@ (fun _ -> fmt "%s == %s" (il_exp e1) (il_exp e2)) Bool.to_string ) @@ fun _ -> (* TODO(3, rossberg): this does not reduce inner type arguments *) - match reduce_exp static env e1, reduce_exp static env e2 with - | Ok e1', Ok e2' -> - Eq.eq_exp e1' e2' || Env.recall_eq env e1' e2' - | (Ok e1' | Error e1'), (Ok e2' | Error e2') when static -> - Eq.eq_exp e1' e2' || Env.recall_eq env e1' e2' - | Error _, _ -> - Error.error e1.at "validation" - "expression failed to evaluate during pattern-matching" - | _, Error _ -> - Error.error e2.at "validation" - "expression failed to evaluate during pattern-matching" + let e1', e2' = + match reduce_exp static env e1, reduce_exp static env e2 with + | Ok e1', Ok e2' -> e1', e2' + | (Ok e1' | Error e1'), (Ok e2' | Error e2') when static -> e1', e2' + | Error _, _ -> + Error.error e1.at "validation" + "expression failed to evaluate during pattern-matching" + | _, Error _ -> + Error.error e2.at "validation" + "expression failed to evaluate during pattern-matching" + in + Eq.eq_exp e1' e2' || Eq.eq_exp (recall_exp env e1') (recall_exp env e2') + +and recall_exp env e = + match Env.recall_eq_simp env e with + | None -> e + | Some e' -> recall_exp env e' and equiv_sym _env g1 g2 = Debug.(log "il.equiv_sym"
diff --git a/spectec/src/xl/mixop.ml b/spectec/src/xl/mixop.ml index 701de9a..06d00d0 100644 --- a/spectec/src/xl/mixop.ml +++ b/spectec/src/xl/mixop.ml
@@ -71,8 +71,19 @@ | Infix (mixop1, atom, mixop2) -> flatten mixop1 ++ [[atom]] ++ flatten mixop2 | Seq mixops -> List.fold_left (++) [[]] (List.map flatten mixops) -let compare mixop1 mixop2 = - List.compare (List.compare Atom.compare) (flatten mixop1) (flatten mixop2) +let (>>) o1 o2 = if o1 = 0 then o2 else o1 + +let rec compare mixop1 mixop2 = + match mixop1, mixop2 with + | Arg x1, Arg x2 -> Stdlib.compare x1 x2 + | Atom a1, Atom a2 -> Atom.compare a1 a2 + | Brack (a11, op11, a12), Brack (a21, op21, a22) -> + Atom.compare a11 a21 >> compare op11 op21 >> Atom.compare a12 a22 + | Infix (op11, a1, op12), Infix (op21, a2, op22) -> + compare op11 op21 >> Atom.compare a1 a2 >> compare op12 op22 + | Seq (op1::ops1), Seq (op2::ops2) -> + (match compare op1 op2 with 0 -> compare (Seq ops1) (Seq ops2) | o -> o) + | _, _ -> Stdlib.compare mixop1 mixop2 let eq mixop1 mixop2 = compare mixop1 mixop2 = 0