Theory ML_Unification_Tests_Base

✐‹creator "Kevin Kappelmann"›
subsection ‹Test Setup›
theory ML_Unification_Tests_Base
  imports
    ML_Unification_Hints
    SpecCheck.SpecCheck
    Main
begin

paragraph ‹Summary›
text ‹Shared setup for unification tests. We use \<^cite>‹speccheck› to generate
tests and create unit tests.›

ML‹
  @{functor_instance struct_name = Test_Unification_Hints
    and functor_name = Term_Index_Unification_Hints
    and id = ‹"test"›
    and more_args = ‹
      structure TI = Discrimination_Tree
      val init_args = {
        concl_unifier = SOME (Higher_Order_Pattern_Unification.match
          |> Type_Unification.e_match Unification_Util.match_types),
        normalisers = SOME Unification_Util.beta_eta_short_norms_unif,
        prems_unifier = SOME (Higher_Order_Pattern_Unification.unify
          |> Type_Unification.e_unify Unification_Util.unify_types),
        retrieval = SOME (Term_Index_Unification_Hints_Args.mk_retrieval_sym_pair
          TI.generalisations TI.norm_term),
        hint_preprocessor = SOME (K I)
      }›}
›

ML_file ‹tests_base.ML›
ML_file ‹first_order_unification_tests.ML›

end