Theory ML_Unification.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: Standard_Unification_Hints_Rec
  functor_name: Term_Index_Unification_Hints
  id: ‹"rec"›
  more_args: ‹
    structure TI = Discrimination_Tree
    val init_args = {
      concl_unifier = SOME Standard_Mixed_Comb_Unification.first_higherp_comb_unify,
      prems_unifier = SOME (Standard_Mixed_Comb_Unification.first_higherp_comb_unify
        |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
      normalisers = SOME Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify,
      retrieval = SOME (Term_Index_Unification_Hints_Args.mk_retrieval_sym_pair
        TI.unifiables TI.norm_term),
      hint_preprocessor = SOME (K I)}››
›
local_setup ‹Standard_Unification_Hints_Rec.setup_attribute NONE›

text‹Standard unification hints using
@{ML Standard_Mixed_Comb_Unification.first_higherp_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 by
via the retrieval setting of @{attribute rec_uhint}.›

declare [[ucombine ‹Standard_Unification_Combine.eunif_data
  (Standard_Unification_Combine.metadata Standard_Unification_Hints_Rec.binding Prio.LOW,
  Standard_Unification_Hints_Rec.try_hints
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
    Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify)
  |> K)›]]

ML‹
\<^functor_instance>‹struct_name: Standard_Unification_Hints
  functor_name: Term_Index_Unification_Hints
  id: ‹""›
  more_args: ‹
    structure TI = Discrimination_Tree
    val init_args = {
      concl_unifier = NONE,
      prems_unifier = SOME (Standard_Mixed_Comb_Unification.first_higherp_comb_unify
        |> Unification_Combinator.norm_unifier Envir_Normalisation.beta_norm_term_unif),
      normalisers = SOME Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify,
      retrieval = SOME (Term_Index_Unification_Hints_Args.mk_retrieval_sym_pair
        TI.unifiables TI.norm_term),
      hint_preprocessor = SOME (K I)}››
›
local_setup ‹Standard_Unification_Hints.setup_attribute NONE›
declare [[uhint config: concl_unifier = ‹fn binders =>
  Standard_Unification_Combine.delete_eunif_data
    (Standard_Unification_Combine.metadata Standard_Unification_Hints.binding Prio.LOW1)
  (*TODO: should we also remove the recursive hint unifier here? time will tell...*)
  (*#> Standard_Unification_Combine.delete_eunif_data
    (Standard_Unification_Combine.metadata Standard_Unification_Hints_Rec.binding Prio.LOW)*)
  |> Context.proof_map
  #> Standard_Mixed_Comb_Unification.first_higherp_comb_unify binders›]]

text‹Standard unification hints using
@{ML Standard_Mixed_Comb_Unification.first_higherp_comb_unify} when looking for hints,
without using fallback list of unifiers, 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 ‹Standard_Unification_Combine.eunif_data
  (Standard_Unification_Combine.metadata Standard_Unification_Hints.binding Prio.LOW1,
  Standard_Unification_Hints.try_hints
  |> Unification_Combinator.norm_unifier (Unification_Util.inst_norm_term'
      Standard_Mixed_Comb_Unification.norms_first_higherp_comb_unify)
  |> K)›]]


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

end