File ‹binders.ML›
signature BINDERS =
sig
type 'a binder = (string * typ) * 'a
type 'a binders = ('a binder) list
val add_binders : 'a binders -> 'a binders -> 'a binders
val fix_binders : (string * typ) list -> Proof.context -> term binders * Proof.context
val fix_binder : (string * typ) -> Proof.context -> term binder * Proof.context
val binder_types : 'a binders -> typ list
val nth_binder_data : 'a binders -> int -> 'a
val replace_binders : term binders -> term -> term
val replace_frees : term binders -> term -> term
val norm_binders : Term_Normalisation.term_normaliser -> term binders -> term binders
end
structure Binders : BINDERS =
struct
type 'a binder = (string * typ) * 'a
type 'a binders = ('a binder) list
fun add_binders binders1 binders2 = binders1 @ binders2
fun fix_binders nTs ctxt =
Variable.variant_fixes (map fst nTs) ctxt
|>> map2 (fn (n, T) => fn n' => ((n, T), Free (n', T))) nTs
val fix_binder = yield_singleton fix_binders
fun binder_types binders = map (snd o fst) binders
fun nth_binder_data binders = snd o nth binders
fun replace_binders binders t = let val bvars = map snd binders
in subst_bounds (bvars, t) end
val replace_frees = fold_rev (curry abstract_over o snd)
fun norm_binders norm =
map (fn ((n, _), t) => let val t' = norm t in ((n, snd (dest_Free t')), t') end)
end