Theory ML_Unifiers

✐‹creator "Kevin Kappelmann"›
theory ML_Unifiers
  imports
    ML_Costs_Priorities
    ML_Functor_Instances
    ML_Unifiers_Base
    Simps_To
begin

paragraph ‹Summary›
text ‹More unifiers.›

paragraph ‹Derived Unifiers›

ML_file‹var_higher_order_pattern_unification.ML›

subparagraph ‹Unification via Simplification›

lemma eq_if_SIMPS_TO_UNIF_if_SIMPS_TO_UNIF:
  assumes "t ≡⇧?> t'"
  and "s ≡⇧?> t'"
  shows "s ≡ t"
  using assms by (simp add: SIMPS_TO_eq SIMPS_TO_UNIF_eq)

ML_file‹simplifier_unification.ML›

paragraph ‹Combining Unifiers›

ML_file‹unification_combine.ML›
ML‹
\<^functor_instance>‹struct_name: Unification_Combine
  functor_name: Unification_Combine_Functor
  id: ‹"ucombine"››
›
local_setup ‹Unification_Combine.setup_attribute NONE›

paragraph ‹Mixture of Unifiers›

ML_file‹mixed_unification.ML›
ML‹
\<^functor_instance>‹struct_name: Mixed_Comb_Unification
  functor_name: Mixed_Comb_Unification_Functor
  id: ‹"mixed_unif"›
  more_args: ‹structure UC = Unification_Combine››
›

declare [[ucombine ‹Unification_Combine.eunif_data
  (Unification_Combine.metadata (\<^binding>‹var_hop_unify›, Prio.HIGH1),
  Var_Higher_Order_Pattern_Unification.e_unify
  #> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
    Mixed_Comb_Unification.norms_fo_hop_comb_unify))›]]

ML‹
structure Unification_Combine :
  sig
    include UNIFICATION_COMBINE
    structure HO_Unify : EXTENDED_HIGHER_ORDER_UNIFICATION_DATA
  end =
struct open Unification_Combine
\<^functor_instance>‹struct_name: HO_Unify
  functor_name: Extended_Higher_Order_Unification_Data
  path: FI.long_name
  id: ‹FI.prefix_id "ho_unify"›
  more_args: ‹
    val parent_logger = logger
    val init_args = {
      search_bound = SOME (Config.get @{context} Unify.search_bound),
      results_bound = SOME 10,
      silence_bound_exceeded = SOME false
    }››
end
›
local_setup‹Unification_Combine.HO_Unify.setup_attribute NONE›

declare [[ucombine ‹Unification_Combine.eunif_data
  (Unification_Combine.metadata (Unification_Combine.HO_Unify.binding, Prio.VERY_LOW),
  K Unification_Combine.HO_Unify.unify)›]]

declare [[ucombine ‹
  let open Term_Normalisation
    (*ignore changes of schematic variables to avoid loops due to index-raising of some tactics*)
    val eq_beta_eta_dummy_vars = apply2 (Same.commit beta_eta_short #> dummy_vars) #> op aconv
    val e_unif = Mixed_Comb_Unification.fo_hop_comb_e_unify Unification_Util.unify_types
    val norms = Mixed_Comb_Unification.norms_fo_hop_comb_unify
    fun simp_unif unify_theory = Simplifier_Unification.simp_unify_progress eq_beta_eta_dummy_vars
      (Simplifier_Unification.simp_unify norms (e_unif Unification_Combinator.fail_unify) norms)
        (Unification_Util.inst_norm_term' norms) (e_unif unify_theory)
      |> Type_Unification.e_unify Unification_Util.unify_types
    val metadata = Unification_Combine.metadata (\<^binding>‹simp_unify›, Prio.MEDIUM)
  in Unification_Combine.eunif_data (metadata, simp_unif) end›]]

end