File ‹higher_order_unification.ML›
signature HIGHER_ORDER_UNIFICATION =
sig
include HAS_LOGGER
val unify : Unification_Base.unifier
val norms : Unification_Base.normalisers
end
structure Higher_Order_Unification : HIGHER_ORDER_UNIFICATION =
struct
val logger = Logger.setup_new_logger Unification_Base.logger "Higher_Order_Unification"
structure Util = Unification_Util
val norms = Unification_Util.beta_eta_short_norms_unif
val unify =
let fun unif binders ctxt tp env =
let
val _ = @{log Logger.DEBUG} ctxt (fn _ => Pretty.block [
Pretty.str "Higher-order unifying ",
Util.pretty_unif_problem ctxt (apply2 (Envir.norm_term env) tp)
] |> Pretty.string_of)
val init_goal = Logic.mk_equals #> Thm.cterm_of ctxt #> Goal.init
fun create_env_thmq env =
apply2 (Binders.replace_binders binders #> (#inst_term norms env #> #norm_term norms)) tp
|> init_goal
|> HEADGOAL (match_tac ctxt @{thms Pure.reflexive})
|> Seq.map (pair env o Goal.conclude)
in
Unify.hounifiers (map fst binders) (Context.Proof ctxt, env, [tp])
|> Seq.maps (create_env_thmq o fst)
end
in Type_Unification.e_unify Util.unify_types unif end
end