(* 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 keep_partial_instances: 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 *)
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 keep_partial_instances =
Attrib.setup_config_bool @{binding monomorph_keep_partial_instances} (K true)
(* 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 prepare schematic_consts_of rthms =
let
val empty_sub = ((0, false, false), Vartab.empty)
fun prep (r, thm) ((i, idx), (consts, subs)) =
if not (Term.exists_type typ_has_tvars (Thm.prop_of thm)) then
(Ground thm, ((i+1, idx + Thm.maxidx_of thm + 1), (consts, subs)))
else
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 subs' = Inttab.update (i, [empty_sub]) subs
val thm_info = Schematic {
index = i,
theorem = thm',
tvars = Term.add_tvars (Thm.prop_of thm') [],
schematics = schematics,
initial_round = r }
in (thm_info, ((i+1, idx'), (consts', subs'))) end
in fold_map prep rthms ((0, 0), (Symtab.empty, Inttab.empty)) ||> snd end
(** collecting substitutions **)
fun exceeded limit = (limit <= 0)
fun exceeded_limit (limit, _, _) = exceeded limit
fun with_all_grounds cx grounds f =
if exceeded_limit cx then I else Symtab.fold f grounds
fun with_all_type_combinations cx schematics f (n, Ts) =
if exceeded_limit cx then I
else fold_product f (Symtab.lookup_list schematics n) Ts
fun derive_new_substs thy cx new_grounds schematics subst =
with_all_grounds cx new_grounds
(with_all_type_combinations cx schematics (fn T => fn U =>
(case try (Sign.typ_match thy (T, U)) subst of
NONE => I
| SOME subst' => cons subst'))) []
fun same_subst subst' (_, subst) = subst' |> Vartab.forall (fn (n, (_, T)) =>
Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false)
fun known_subst sub subs1 subs2 subst =
same_subst subst sub orelse exists (same_subst subst) subs1 orelse
exists (same_subst subst) subs2
fun within_limit f cx = if exceeded_limit cx then cx else f cx
fun fold_partial_substs derive add = within_limit (
let
fun fold_partial [] cx = cx
| fold_partial (sub :: subs) (limit, subs', next) =
if exceeded limit then (limit, sub :: subs @ subs', next)
else sub |> (fn ((generation, full, _), subst) =>
if full then fold_partial subs (limit, sub :: subs', next)
else
(case filter_out (known_subst sub subs subs') (derive subst) of
[] => fold_partial subs (limit, sub :: subs', next)
| substs =>
(limit, ((generation, full, true), subst) :: subs', next)
|> fold (within_limit o add) substs
|> fold_partial subs))
in (fn (limit, subs, next) => fold_partial subs (limit, [], next)) end)
fun refine ctxt round known_grounds new_grounds (tvars, schematics) cx =
let
val thy = Proof_Context.theory_of ctxt
val count_partial = Config.get ctxt keep_partial_instances
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 typ_has_tvars T' then I
else if member (op =) (Symtab.lookup_list known_grounds n) T' then I
else Symtab.cons_list (n, T')
end
fun add_new_subst subst (limit, subs, next_grounds) =
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 :: subs, next_grounds') end
in
fold_partial_substs (derive_new_substs thy cx new_grounds schematics)
add_new_subst cx
end
(*
'known_grounds' are all constant names known to occur schematically
associated with all ground instances considered so far
*)
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 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 (known_grounds, (limit, substitutions, initial_grounds)) end
fun is_new round initial_round = (round = initial_round)
fun is_active round initial_round = (round > initial_round)
fun fold_schematic pred f = fold (fn
Schematic {index, theorem, tvars, schematics, initial_round} =>
if pred initial_round then f theorem (index, tvars, schematics) else I
| Ground _ => I)
fun focus f _ (index, tvars, schematics) (limit, subs, next_grounds) =
let
val (limit', isubs', next_grounds') =
(limit, Inttab.lookup_list subs index, next_grounds)
|> f (tvars, schematics)
in (limit', Inttab.update (index, isubs') subs, next_grounds') end
fun collect_substitutions thm_infos ctxt round subst_ctxt =
let val (known_grounds, (limit, subs, next_grounds)) = subst_ctxt
in
if exceeded limit then subst_ctxt
else
let
fun collect thm _ = collect_instances known_grounds thm
val new = fold_schematic (is_new round) collect thm_infos next_grounds
val known' = Symtab.merge_list (op =) (known_grounds, new)
val step = focus o refine ctxt round known'
in
(limit, subs, Symtab.empty)
|> not (Symtab.is_empty new) ?
fold_schematic (is_active round) (step new) thm_infos
|> fold_schematic (is_new round) (step known') thm_infos
|> 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) subs 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 subs index
|> map_filter (with_subst tvars (instantiate theorem))
in (map inst thm_infos, ctxt) end
fun instantiate_all ctxt thm_infos (_, (_, subs, _)) =
if Config.get ctxt keep_partial_instances then
let fun is_refined ((_, _, refined), _) = refined
in
(Inttab.map (K (filter_out is_refined)) subs, thm_infos)
|-> instantiate_all' (new_super_type ctxt thm_infos)
end
else instantiate_all' (NONE, ctxt) subs thm_infos
(** overall procedure **)
fun limit_rounds ctxt f =
let
val max = Config.get ctxt max_rounds
fun round i x = if i > max then x else round (i + 1) (f ctxt i x)
in round 1 end
fun monomorph schematic_consts_of rthms ctxt =
let
val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms
in
if Symtab.is_empty known_grounds then
(map (single o pair 0 o snd) rthms, ctxt)
else
make_subst_ctxt ctxt thm_infos known_grounds subs
|> limit_rounds ctxt (collect_substitutions thm_infos)
|> instantiate_all ctxt thm_infos
end
end