Theory ML_Unification_Hints

✐‹creator "Kevin Kappelmann"›
section ‹Unification Hints›
theory ML_Unification_Hints
  imports
    ML_Unification_Hints_Base
    ML_Unifiers
begin

paragraph ‹Summary›
text ‹Setup of unification hints.›

text ‹We now set up two unifiers using unification hints. The first one allows for recursive
applications of unification hints when unifying a hint's conclusion ‹lhs ≡ rhs› with a goal
‹lhs' ≡ rhs'›.
The second disallows recursive applications of unification hints. Recursive applications have to be
made explicit in the hint itself (cf. @{dir "../Examples"}).

While the former can be convenient for local hint registrations and quick developments,
it is advisable to use the second for global hints to avoid unexpected looping behaviour.›

ML‹
\<^functor_instance>‹struct_name: Unification_Hints_Rec
  functor_name: Term_Index_Unification_Hints
  id: ‹"rec_uhint"›
  more_args: ‹
    structure TI = Discrimination_Tree
    structure Args = Term_Index_Unification_Hints_Args
    val init_args = {
      concl_unifier = SOME Mixed_Comb_Unification.fo_hop_comb_unify,
      prems_unifier = SOME (Mixed_Comb_Unification.fo_hop_comb_unify
        |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
      normalisers = SOME Mixed_Comb_Unification.norms_fo_hop_comb_unify,
      retrieval = SOME (Args.mk_retrieval_sym_pair (K TI.unifiables |> Args.retrieve_transfer)
        TI.norm_term),
      hint_preprocessor = SOME (K I)}››
›
local_setup ‹Unification_Hints_Rec.setup_attribute NONE›

text‹Standard recursive unification hints using @{ML Mixed_Comb_Unification.fo_hop_comb_unify} when
looking for hints are accessible via @{attribute rec_uhint}.

∗‹Note:› when we retrieve a potential unification hint with conclusion ‹lhs ≡ rhs› for a goal
‹lhs' ≡ rhs'›, we consider those hints whose lhs or rhs potentially higher-order unifies with
lhs' or rhs' ∗‹without using hints›. For otherwise, any hint ‹lhs ≡ rhs› applied to a goal
‹rhs ≡ lhs› leads to an immediate loop. The retrieval can be further restricted and modified with
the retrieval setting of @{attribute rec_uhint}.›

declare [[ucombine ‹Unification_Combine.eunif_data
  (Unification_Combine.metadata (Unification_Hints_Rec.binding, Prio.LOW),
  Unification_Hints_Rec.try_hints
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
    Mixed_Comb_Unification.norms_fo_hop_comb_unify)
  |> K)›]]

ML‹
\<^functor_instance>‹struct_name: Unification_Hints
  functor_name: Term_Index_Unification_Hints
  id: ‹"uhint"›
  more_args: ‹
    structure TI = Discrimination_Tree
    structure Args = Term_Index_Unification_Hints_Args
    val init_args = {
      concl_unifier = NONE,
      prems_unifier = SOME (Mixed_Comb_Unification.fo_hop_comb_unify
        |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
      normalisers = SOME Mixed_Comb_Unification.norms_fo_hop_comb_unify,
      retrieval = SOME (Args.mk_retrieval_sym_pair (K TI.unifiables |> Args.retrieve_transfer)
        TI.norm_term),
      hint_preprocessor = SOME (K I)}››
›
local_setup ‹Unification_Hints.setup_attribute NONE›
declare [[uhint config concl_unifier: ‹fn binders =>
  Unification_Combine.delete_id Unification_Hints.binding
  (*TODO: should we also remove the recursive hint unifier here? time will tell...*)
  (* #> Unification_Combine.delete_id Unification_Hints_Rec.binding *)
  |> Context.proof_map
  #> Mixed_Comb_Unification.fo_hop_comb_unify binders›]]

text‹Standard non-recursive unification hints using @{ML Mixed_Comb_Unification.fo_hop_comb_unify}
when looking for hints are accessible via @{attribute uhint}.

∗‹Note:› there will be no recursive usage of unification hints when searching for potential
unification hints in this case. See also @{dir "../Examples"}.›

declare [[ucombine ‹Unification_Combine.eunif_data
  (Unification_Combine.metadata (Unification_Hints.binding, Prio.LOW1),
  Unification_Hints.try_hints
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
      Mixed_Comb_Unification.norms_fo_hop_comb_unify)
  |> K)›]]


text‹Examples see @{dir "../Examples"}.›

end