File ‹higher_order_pattern_unification_tests.ML›

(*  Title:      ML_Unification/higher_order_pattern_unification_tests.ML
    Author:     Kevin Kappelmann

Higher-order pattern unification tests.
*)
signature HIGHER_ORDER_PATTERN_UNIFICATION_TESTS =
sig
  val unit_tests_unifiable : Proof.context -> (term * term) list
end

structure Higher_Order_Pattern_Unification_Tests : HIGHER_ORDER_PATTERN_UNIFICATION_TESTS =
struct

fun unit_tests_unifiable ctxt =
  let val ctxt = Proof_Context.set_mode Proof_Context.mode_schematic ctxt
  in map (apply2 (Syntax.read_term ctxt)) [
      ("λ x. f x", "λ x. f x"),
      ("λ (x :: ?'X). (f :: ?'X ⇒ ?'Y) x", "λ (x :: ?'X1). (?y :: ?'X1 ⇒ ?'Y1) x"),
      ("λ x. r x ?X", "λ x. r x ?Y"),
      ("λ x. (x, (λ y. (y, λ z. ?x)))", "λ x. (x, (λ y. (y, λ z. g)))"),
      ("?f :: ?'Z ⇒ ?'X ⇒ ?'Y ⇒ ?'R", "λ (x :: ?'Z). (?f :: ?'Z ⇒ ?'X1 ⇒ ?'Y1 ⇒ ?'R1) x"),
      (
        "(?x :: ?'X, ?y :: ?'Y, ?z :: ?'Z)",
        "((f :: ?'Y ⇒ ?'X) (?y :: ?'Y), (g :: ?'Z ⇒ ?'Y) (?z :: ?'Z), c :: ?'C)"
      )
    ]
  end

end