Theory Higher_Order_Pattern_ML_Unification_Tests
subsection ‹Higher-Order Pattern ML Unification Tests›
theory Higher_Order_Pattern_ML_Unification_Tests
imports
ML_Unification_Tests_Base
begin
paragraph ‹Summary›
text ‹Tests for @{ML_structure "Higher_Order_Pattern_Unification"}.›
ML‹
structure Prop = SpecCheck_Property
structure UC = Unification_Combinator
structure UU = Unification_Util
open Unification_Tests_Base
structure Unif = Higher_Order_Pattern_Unification
val norm_match_types = Type_Unification.e_match UU.match_types
val match = Unif.match |> norm_match_types
val closed_match = match []
val match_hints =
let fun match binders =
UC.add_fallback_matcher
(fn match_theory => Unif.e_match UU.match_types match_theory match_theory
|> norm_match_types)
((fn binders =>
(Hints.map_retrieval (Term_Index_Unification_Hints_Args.mk_retrieval_pair
Hints.TI.generalisations Hints.TI.norm_term |> K)
#> Hints.UH.map_concl_unifier (match |> K)
#> Hints.UH.map_normalisers (Unif.norms_match |> K)
#> Hints.UH.map_prems_unifier (match |> K))
|> Context.proof_map
#> Test_Unification_Hints.try_hints binders)
|> UC.norm_matcher (UU.inst_norm_term' Unif.norms_match))
binders
in match [] end
val norm_unif_types = Type_Unification.e_unify UU.unify_types
val unify = Unif.unify |> norm_unif_types
val closed_unify = unify []
val unify_hints =
let fun unif binders =
UC.add_fallback_unifier
(fn unif_theory => Unif.e_unify UU.unify_types unif_theory unif_theory
|> norm_unif_types)
((fn binders =>
(Hints.UH.map_concl_unifier (match |> K)
#> Hints.UH.map_normalisers (Unif.norms_unify |> K)
#> Hints.UH.map_prems_unifier (unif |> K))
|> Context.proof_map
#> Test_Unification_Hints.try_hints binders)
|> UC.norm_unifier (UU.inst_norm_term' Unif.norms_unify))
binders
in unif [] end
›
subsubsection ‹Matching›
paragraph ‹Unit Tests›
ML_command‹
let
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
|> Variable.declare_term @{term "f :: nat ⇒ bool ⇒ nat"}
val tests = map (apply2 (Syntax.read_term ctxt))[
("?x :: nat", "(?x + 1 :: nat)"),
("(g :: nat ⇒ nat ⇒ nat) ?x ?x", "(g :: nat ⇒ nat ⇒ nat) (?x + 1) (?x + 1)"),
("λy. (?x :: nat ⇒ ?'Z) y", "λy. f y"),
("(g :: ?'X ⇒ ?'Y ⇒ ?'Z) (x :: ?'X) (y :: ?'Y)", "(g :: ?'Y ⇒ ?'Z ⇒ ?'Z) (x :: ?'Y) (y :: ?'Z)"),
("(g :: ?'Z ⇒ ?'X)", "λ(x :: ?'X). (g :: ?'X ⇒ ?'Y) x"),
("λ (x :: nat). (0 :: nat)", "λ (x :: nat). (0 :: nat)"),
("λ (x :: nat). x", "λ (x :: nat). x"),
("λ (x :: nat) (y :: bool). (x, y)", "λ (x :: nat) (y :: bool). (x, y)"),
("λ (x :: ?'A) (y :: bool). (?x :: ?'A ⇒ bool ⇒ ?'Z) x y", "λ (x :: nat) (y :: bool). f x y"),
("λ(x :: ?'X). (g :: ?'X ⇒ ?'X) x", "(g :: ?'X ⇒ ?'X)"),
("λy. (?x :: nat ⇒ bool ⇒ nat) y", "λy. f y"),
("λy z. (?x :: nat ⇒ bool ⇒ nat) y z", "f")
]
val check = check_unit_tests_hints_match tests true []
in
Lecker.test_group ctxt () [
check "match" closed_match,
check "match_hints" match_hints
]
end
›
subparagraph ‹Asymmetry›
ML_command‹
let
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
|> Variable.declare_term @{term "f :: nat ⇒ bool ⇒ nat"}
val tests = map (apply2 (Syntax.read_term ctxt))[
("λy. f y", "λy. (?x :: nat ⇒ bool ⇒ nat) y")
]
val check = check_unit_tests_hints_match tests false []
in
Lecker.test_group ctxt () [
check "match" closed_match,
check "match_hints" match_hints
]
end
›
subparagraph ‹Ground Hints›
ML_command‹
let
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
"?x ≡ 2 ⟹ ?x + (-?x :: int) ≡ 0",
"?x ≡ 0 ⟹ ?y ≡ 0 ⟹ (?x :: int) + ?y ≡ 0"
]
val tests = map (apply2 (Syntax.read_term ctxt))[
("(2 + -2) + (0 + 0) :: int", "0 :: int")
]
val check_hints = check_unit_tests_hints_match tests
in
Lecker.test_group ctxt () [
check_hints false [] "match" closed_match,
check_hints false [] "match_hints without hints" match_hints,
check_hints true hints "match_hints with hints" match_hints
]
end
›
subsubsection ‹Unification›
paragraph ‹Generated Tests›
subparagraph ‹First-Order›
ML_command‹
structure Test_Params =
struct
val unify = closed_unify
val unify_hints = unify_hints
val params = {
nv = 10,
ni = 10,
max_h = 5,
max_args = 4
}
end
structure First_Order_Tests = First_Order_Unification_Tests(Test_Params)
val _ = First_Order_Tests.tests @{context} (SpecCheck_Random.new ())
›
subparagraph ‹Higher-Order Pattern›
ML_file‹higher_order_pattern_unification_tests.ML›
ML_command‹
val ctxt = @{context}
val tests = Higher_Order_Pattern_Unification_Tests.unit_tests_unifiable ctxt
val check_hints = check_unit_tests_hints_unif tests
val _ = Lecker.test_group ctxt () [
check_hints true [] "unify" closed_unify,
check_hints true [] "unify_hints" unify_hints
]
›
paragraph ‹Unit Tests›
subparagraph ‹With Unification Hints›
ML_command‹
let
val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic @{context}
|> Variable.declare_term @{term "f :: (nat ⇒ nat) × nat ⇒ nat"}
|> Variable.declare_term @{term "g :: nat × nat ⇒ nat"}
|> Variable.declare_term @{term "h :: nat"}
val hints = map (Skip_Proof.make_thm (Proof_Context.theory_of ctxt) o Syntax.read_term ctxt) [
"?x ≡ (0 :: nat) ⟹ ?y ≡ ?z ⟹ ?x + ?y ≡ ?z",
"(?x :: ?'X) ≡ (?y :: ?'X) ⟹ id ?x ≡ ?y",
"(?x1 :: nat) ≡ ?x2 ⟹ (?y1 :: nat) ≡ ?y2 ⟹ ?x1 + ?y1 ≡ ?y2 + ?x2"
]
val tests = map (apply2 (Syntax.read_term ctxt)) [
("λ x y. 0 + 1 :: nat", "λ x y. 1 :: nat"),
("λ x. 0 + 0 + x :: nat", "λ x. x :: nat"),
("λ x y. 0 + Suc ?x", "λ x y. Suc 2"),
("λ (x :: nat) (y :: nat). y + (0 + x)", "λ (x :: nat) (y :: nat). x + (0 + y)"),
("f (λ u. g (?x, h), h)", "id (f (λ u. ?y, 0 + h))")
]
val check_hints = check_unit_tests_hints_unif tests
in
Lecker.test_group ctxt () [
check_hints false [] "unify" closed_unify,
check_hints false [] "unify_hints without hints" unify_hints,
check_hints true hints "unify_hints with hints" unify_hints
]
end
›
end