Theory First_Order_ML_Unification_Tests

✐‹creator "Kevin Kappelmann"›
✐‹contributor "Paul Bachmann"›
subsection ‹First-Order ML Unification Tests›
theory First_Order_ML_Unification_Tests
  imports
    ML_Unification_Tests_Base
begin

paragraph ‹Summary›
text ‹Tests for @{ML_structure "First_Order_Unification"}.›

ML‹
  structure Prop = SpecCheck_Property
  structure UC = Unification_Combinator
  structure UU = Unification_Util
  open Unification_Tests_Base
  structure Unif = First_Order_Unification
  structure Norm = Envir_Normalisation
  val match = Unif.match []
  val match_hints =
    let fun match binders =
      UC.add_fallback_matcher
      (Unif.e_match UU.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 (Higher_Order_Pattern_Unification.match
          |> Type_Unification.e_match UU.match_types |> K)
        #> Hints.UH.map_normalisers (UU.beta_eta_short_norms_match |> K)
        #> Hints.UH.map_prems_unifier (match |> UC.norm_matcher Norm.beta_norm_term_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 unify = Unif.unify []
  val unify_hints =
    let fun unif binders =
      UC.add_fallback_unifier
      (Unif.e_unify UU.unify_types)
      ((fn binders =>
        (Hints.UH.map_concl_unifier (Higher_Order_Pattern_Unification.match
          |> Type_Unification.e_match UU.match_types |> K)
        #> Hints.UH.map_normalisers (UU.beta_eta_short_norms_unif |> K)
        #> Hints.UH.map_prems_unifier (unif |> UC.norm_unifier Norm.beta_norm_term_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 ⇒ ?'Z) 1", "f 1"),
      ("?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)"),
      ("?g ?x ?y d", "g ?y ?x d"),
      ("f 0 True", "(λx y. f y x) True 0"),
      ("λ (x :: ?'a) y. f y", "λ(x :: ?'b). f"),
      ("λy z. (?x :: nat ⇒ bool ⇒ nat) y z", "f"),
      ("λx. (?f :: nat ⇒ bool ⇒ nat) 0 x", "λx. f 0 x")
    ]
    val check = check_unit_tests_hints_match tests true []
  in
    Lecker.test_group ctxt () [
      check "match" 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))[
      ("f 1", "(?x :: nat ⇒ ?'Z) 1")
    ]
    val check = check_unit_tests_hints_match tests false []
  in
    Lecker.test_group ctxt () [
      check "match" 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" 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›

ML_command‹
  structure Test_Params =
  struct
    val unify = unify
    val unify_hints = unify_hints
    val params = {
      nv = 4,
      ni = 2,
      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 ())
›

paragraph ‹Unit Tests›
subparagraph ‹Occurs-Check›

ML_command‹
  let
    val unit_tests = [
      (
        Var (("x", 0), TVar (("X", 0), [])),
        Var (("y", 0), TVar (("X", 0), []) --> TFree ("'a", [])) $
          Var (("x", 0), TVar (("X", 0), []))
      ),
      (
        Var (("y", 0), TVar (("X", 0), []) --> TFree ("'a", [])) $
          Var (("x", 0), TVar (("X", 0), [])),
        Var (("x", 0), TVar (("X", 0), []))
      ),
      (
        Free (("f", [TVar (("X", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
          Var (("x", 0), TVar (("X", 0), [])) $
          Var (("y", 0), TVar (("X", 0), [])),
        Free (("f", [TVar (("X", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
          Var (("y", 0), TVar (("X", 0), [])) $ (
            Free (("g", TVar (("X", 0), []) --> TVar (("X", 0), []))) $
              Var (("x", 0), TVar (("X", 0), []))
          )
      ),
      (
        Free (("f", [TVar (("X", 0), []), TVar (("Y", 0), [])] ---> TFree ("'a", []))) $
          Var (("x", 0), TVar (("X", 0), [])) $
          Var (("y", 0), TVar (("Y", 0), [])),
        Free (("f", [TVar (("Y", 0), []), TVar (("X", 0), [])] ---> TFree ("'a", []))) $
          Var (("y", 0), TVar (("Y", 0), [])) $ (
            Free (("g", TVar (("X", 0), []) --> TVar (("X", 0), []))) $
              Var (("x", 0), TVar (("X", 0), []))
          )
      )
    ]
    fun check name unif ctxt _ =
      check_list unit_tests ("occurs-check for " ^ name)
        (Prop.prop (not o terms_unify_thms_correct_unif ctxt unif)) ctxt
      |> K ()
  in
    Lecker.test_group @{context} () [
      check "unify" unify,
      check "unify_hints" unify_hints
    ]
  end
›

subparagraph ‹Lambda-Abstractions›

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). (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. f y", "λ(x :: ?'b). f"),
      ("λ (x :: nat) (y :: bool). f x y", "λ (x :: nat) (y :: bool). (?x :: nat ⇒ bool ⇒ ?'Z) x y"),
      ("λx. (?f :: nat ⇒ bool ⇒ nat) 0 x", "λx. f ?g x"),
      ("(?f :: nat ⇒ bool ⇒ nat) (?n :: nat)", "?g :: bool ⇒ nat")
    ]
    val check = check_unit_tests_hints_unif tests true []
  in
    Lecker.test_group ctxt () [
      check "unify" unify,
      check "unify_hints" unify_hints
    ]
  end
›

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 ≡ (0 :: nat) ⟹ ?y ≡ ?z ⟹ ?x + ?y ≡ ?z"
    ]
    val tests = map (apply2 (Syntax.read_term ctxt))[
      ("λ (x :: nat) (y :: bool). x", "λ (x :: nat) (y :: bool). 0 + x"),
      ("0 + (λ (x :: nat) (y :: bool). x) 0 ?y", "0 + (λ (x :: nat) (y :: bool). 0 + x) 0 ?z")
    ]
    val check_hints = check_unit_tests_hints_unif tests
  in
    Lecker.test_group ctxt () [
      check_hints false [] "unify" unify,
      check_hints false [] "unify_hints without hints" unify_hints,
      check_hints true hints "unify_hints with hints" unify_hints
    ]
  end
›


end