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
  functor_name: Term_Index_Unification_Hints
  id: ‹"test"›
  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