(* Title: HOL/Tools/monomorph.ML
Author: Sascha Boehme, TU Muenchen
Monomorphization of theorems, i.e., computation of all (necessary)
instances. This procedure is incomplete in general, but works well for
most practical problems.
For a list of universally closed theorems (without schematic term
variables), monomorphization computes a list of theorems with schematic
term variables: all polymorphic constants (i.e., constants occurring both
with ground types and schematic type variables) are instantiated with all
(necessary) ground types; thereby theorems containing these constants are
copied. To prevent nontermination, there is an upper limit for the number
of iterations involved in the fixpoint construction.
The search for instances is performed on the constants with schematic
types, which are extracted from the initial set of theorems. The search
constructs, for each theorem with those constants, a set of substitutions,
which, in the end, is applied to all corresponding theorems. Remaining
schematic type variables are substituted with fresh types.
Searching for necessary substitutions is an iterative fixpoint
construction: each iteration computes all required instances required by
the ground instances computed in the previous step and which haven't been
found before. Computed substitutions are always nontrivial: schematic type
variables are never mapped to schematic type variables.
*)
signature MONOMORPH =
sig
(* utility function *)
val typ_has_tvars: typ -> bool
val all_schematic_consts_of: term -> typ list Symtab.table
val add_schematic_consts_of: term -> typ list Symtab.table ->
typ list Symtab.table
(* configuration options *)
val max_rounds: int Config.T
val max_new_instances: int Config.T
val complete_instances: bool Config.T
val verbose: bool Config.T
(* monomorphization *)
val monomorph: (term -> typ list Symtab.table) -> (int * thm) list ->
Proof.context -> (int * thm) list list * Proof.context
end
structure Monomorph: MONOMORPH =
struct
(* utility functions *)
fun fold_env _ [] y = y
| fold_env f (x :: xs) y = fold_env f xs (f xs x y)
val typ_has_tvars = Term.exists_subtype (fn TVar _ => true | _ => false)
fun add_schematic_const (c as (_, T)) =
if typ_has_tvars T then Symtab.insert_list (op =) c else I
fun add_schematic_consts_of t =
Term.fold_aterms (fn Const c => add_schematic_const c | _ => I) t
fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
(* configuration options *)
val max_rounds = Attrib.setup_config_int @{binding monomorph_max_rounds} (K 5)
val max_new_instances =
Attrib.setup_config_int @{binding monomorph_max_new_instances} (K 300)
val complete_instances =
Attrib.setup_config_bool @{binding monomorph_complete_instances} (K true)
val verbose = Attrib.setup_config_bool @{binding monomorph_verbose} (K true)
fun show_info ctxt msg = if Config.get ctxt verbose then tracing msg else ()
(* monomorphization *)
(** preparing the problem **)
datatype thm_info =
Ground of thm |
Schematic of {
index: int,
theorem: thm,
tvars: (indexname * sort) list,
schematics: typ list Symtab.table,
initial_round: int }
fun make_thm_info index initial_round schematics thm =
if Symtab.is_empty schematics then Ground thm
else Schematic {
index = index,
theorem = thm,
tvars = Term.add_tvars (Thm.prop_of thm) [],
schematics = schematics,
initial_round = initial_round }
fun prepare schematic_consts_of rthms =
let
val empty_subst = ((0, false, false), Vartab.empty)
fun prep (r, thm) ((i, idx), (consts, substs)) =
let
(* increase indices to avoid clashes of type variables *)
val thm' = Thm.incr_indexes idx thm
val idx' = Thm.maxidx_of thm' + 1
val schematics = schematic_consts_of (Thm.prop_of thm')
val consts' =
Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics consts
val substs' = Inttab.update (i, [empty_subst]) substs
in
(make_thm_info i r schematics thm', ((i+1, idx'), (consts', substs')))
end
in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
(** collecting substitutions **)
fun add_relevant_instances known_grounds (Const (c as (n, T))) =
if typ_has_tvars T orelse not (Symtab.defined known_grounds n) then I
else if member (op =) (Symtab.lookup_list known_grounds n) T then I
else Symtab.insert_list (op =) c
| add_relevant_instances _ _ = I
fun collect_instances known_grounds thm =
Term.fold_aterms (add_relevant_instances known_grounds) (Thm.prop_of thm)
fun exceeded_limit (limit, _, _) = (limit <= 0)
fun with_substs index f (limit, substitutions, next_grounds) =
let
val substs = Inttab.lookup_list substitutions index
val (limit', substs', next_grounds') = f (limit, substs, next_grounds)
in (limit', Inttab.update (index, substs') substitutions, next_grounds') end
fun with_grounds grounds f cx =
if exceeded_limit cx then cx else Symtab.fold f grounds cx
fun with_all_combinations schematics f (n, Ts) cx =
if exceeded_limit cx then cx
else fold_product f (Symtab.lookup_list schematics n) Ts cx
fun with_partial_substs f T U (cx as (limit, substs, next_grounds)) =
if exceeded_limit cx then cx
else fold_env (f (T, U)) substs (limit, [], next_grounds)
fun same_subst subst =
Vartab.forall (fn (n, (_, T)) =>
Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
(* FIXME: necessary? would it have an impact?
comparing substitutions can be tricky ... *)
fun known substs1 substs2 subst = false
fun refine ctxt known_grounds new_grounds info =
let
val thy = Proof_Context.theory_of ctxt
val count_partial = Config.get ctxt complete_instances
val (round, index, _, tvars, schematics) = info
fun refine_subst TU = try (Sign.typ_match thy TU)
fun add_new_ground subst n T =
let val T' = Envir.subst_type subst T
in
(* FIXME: maybe keep types in a table or net for known_grounds,
that might improve efficiency here
*)
if member (op =) (Symtab.lookup_list known_grounds n) T' then I
else Symtab.cons_list (n, T')
end
fun refine_step subst limit next_grounds substs =
let
val full = forall (Vartab.defined subst o fst) tvars
val limit' =
if full orelse count_partial then limit - 1 else limit
val sub = ((round, full, false), subst)
val next_grounds' =
(schematics, next_grounds)
|-> Symtab.fold (uncurry (fold o add_new_ground subst))
in (limit', sub :: substs, next_grounds') end
fun refine_substs TU substs sub (cx as (limit, substs', next_grounds)) =
let val ((generation, full, _), subst) = sub
in
if exceeded_limit cx orelse full then
(limit, sub :: substs', next_grounds)
else
(case refine_subst TU subst of
NONE => (limit, sub :: substs', next_grounds)
| SOME subst' =>
if (same_subst subst orf known substs substs') subst' then
(limit, sub :: substs', next_grounds)
else
substs'
|> cons ((generation, full, true), subst)
|> refine_step subst' limit next_grounds)
end
in
with_substs index (
with_grounds new_grounds (with_all_combinations schematics (
with_partial_substs refine_substs)))
end
fun make_subst_ctxt ctxt thm_infos (known_grounds, substitutions) =
let
val limit = Config.get ctxt max_new_instances
fun add_ground_consts (Ground thm) = collect_instances known_grounds thm
| add_ground_consts (Schematic _) = I
val initial_grounds = fold add_ground_consts thm_infos Symtab.empty
in (thm_infos, (known_grounds, (limit, substitutions, initial_grounds))) end
fun with_new round f thm_info =
(case thm_info of
Schematic {index, theorem, tvars, schematics, initial_round} =>
if initial_round <> round then I
else f (round, index, theorem, tvars, schematics)
| Ground _ => I)
fun with_active round f thm_info =
(case thm_info of
Schematic {index, theorem, tvars, schematics, initial_round} =>
if initial_round < round then I
else f (round, index, theorem, tvars, schematics)
| Ground _ => I)
fun collect_substitutions ctxt round thm_infos (known_grounds, subst_ctxt) =
let val (limit, substitutions, next_grounds) = subst_ctxt
in
(*
'known_grounds' are all constant names known to occur schematically
associated with all ground instances considered so far
*)
if exceeded_limit subst_ctxt then (true, (known_grounds, subst_ctxt))
else
let
fun collect (_, _, thm, _, _) = collect_instances known_grounds thm
val new = fold (with_new round collect) thm_infos next_grounds
val known' = Symtab.merge_list (op =) (known_grounds, new)
in
if Symtab.is_empty new then (true, (known_grounds, subst_ctxt))
else
(limit, substitutions, Symtab.empty)
|> fold (with_active round (refine ctxt known_grounds new)) thm_infos
|> fold (with_new round (refine ctxt Symtab.empty known')) thm_infos
|> pair false o pair known'
end
end
(** instantiating schematic theorems **)
fun super_sort (Ground _) S = S
| super_sort (Schematic {tvars, ...}) S = merge (op =) (S, maps snd tvars)
fun new_super_type ctxt thm_infos =
let val S = fold super_sort thm_infos @{sort type}
in yield_singleton Variable.invent_types S ctxt |>> SOME o TFree end
fun add_missing_tvar T (ix, S) subst =
if Vartab.defined subst ix then subst
else Vartab.update (ix, (S, T)) subst
fun complete tvars subst T =
subst
|> Vartab.map (K (apsnd (Term.map_atyps (fn TVar _ => T | U => U))))
|> fold (add_missing_tvar T) tvars
fun instantiate_all' (mT, ctxt) substitutions thm_infos =
let
val thy = Proof_Context.theory_of ctxt
fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T)
fun cert' subst = Vartab.fold (cons o cert) subst []
fun instantiate thm subst = Thm.instantiate (cert' subst, []) thm
fun with_subst tvars f ((generation, full, _), subst) =
if full then SOME (generation, f subst)
else Option.map (pair generation o f o complete tvars subst) mT
fun inst (Ground thm) = [(0, thm)]
| inst (Schematic {theorem, tvars, index, ...}) =
Inttab.lookup_list substitutions index
|> map_filter (with_subst tvars (instantiate theorem))
in (map inst thm_infos, ctxt) end
fun instantiate_all ctxt thm_infos (_, (_, substitutions, _)) =
if Config.get ctxt complete_instances then
let
fun refined ((_, _, true), _) = true
| refined _ = false
in
(Inttab.map (K (filter_out refined)) substitutions, thm_infos)
|-> instantiate_all' (new_super_type ctxt thm_infos)
end
else instantiate_all' (NONE, ctxt) substitutions thm_infos
(** overall procedure **)
fun limit_rounds ctxt f thm_infos =
let
val max = Config.get ctxt max_rounds
fun round _ (true, x) = (thm_infos, x)
| round i (_, x) =
if i <= max then round (i + 1) (f ctxt i thm_infos x)
else (
show_info ctxt "Warning: Monomorphization limit reached";
(thm_infos, x))
in round 1 o pair false end
fun monomorph schematic_consts_of rthms ctxt =
rthms
|> prepare schematic_consts_of
|-> make_subst_ctxt ctxt
|-> limit_rounds ctxt collect_substitutions
|-> instantiate_all ctxt
end