# HG changeset patch # User boehmes # Date 1364510681 -3600 # Node ID 907efc894051db7c747d4e4d5fba1b58180224cc # Parent 2b58d7b139d60de4309202de0ea3c428da023b0f new, simpler implementation of monomorphization; old monomorphization code is still available as Legacy_Monomorphization; modified SMT integration to use the new monomorphization code diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/ATP.thy --- a/src/HOL/ATP.thy Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/ATP.thy Thu Mar 28 23:44:41 2013 +0100 @@ -11,6 +11,7 @@ ML_file "Tools/lambda_lifting.ML" ML_file "Tools/monomorph.ML" +ML_file "Tools/legacy_monomorph.ML" ML_file "Tools/ATP/atp_util.ML" ML_file "Tools/ATP/atp_problem.ML" ML_file "Tools/ATP/atp_proof.ML" diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/Tools/Metis/metis_generate.ML Thu Mar 28 23:44:41 2013 +0100 @@ -216,8 +216,8 @@ else conj_clauses @ fact_clauses |> map (pair 0) - |> rpair (ctxt |> Config.put Monomorph.keep_partial_instances false) - |-> Monomorph.monomorph atp_schematic_consts_of + |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false) + |-> Legacy_Monomorph.monomorph atp_schematic_consts_of |> fst |> chop (length conj_clauses) |> pairself (maps (map (zero_var_indexes o snd))) val num_conjs = length conj_clauses diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/SMT/smt_config.ML --- a/src/HOL/Tools/SMT/smt_config.ML Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/Tools/SMT/smt_config.ML Thu Mar 28 23:44:41 2013 +0100 @@ -32,7 +32,6 @@ val trace_used_facts: bool Config.T val monomorph_limit: int Config.T val monomorph_instances: int Config.T - val monomorph_full: bool Config.T val infer_triggers: bool Config.T val drop_bad_facts: bool Config.T val filter_only_facts: bool Config.T @@ -160,7 +159,6 @@ val trace_used_facts = Attrib.setup_config_bool @{binding smt_trace_used_facts} (K false) val monomorph_limit = Attrib.setup_config_int @{binding smt_monomorph_limit} (K 10) val monomorph_instances = Attrib.setup_config_int @{binding smt_monomorph_instances} (K 500) -val monomorph_full = Attrib.setup_config_bool @{binding smt_monomorph_full} (K true) val infer_triggers = Attrib.setup_config_bool @{binding smt_infer_triggers} (K false) val drop_bad_facts = Attrib.setup_config_bool @{binding smt_drop_bad_facts} (K false) val filter_only_facts = Attrib.setup_config_bool @{binding smt_filter_only_facts} (K false) diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/SMT/smt_normalize.ML --- a/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/Tools/SMT/smt_normalize.ML Thu Mar 28 23:44:41 2013 +0100 @@ -571,11 +571,10 @@ val (thms', extra_thms) = f thms in (is ~~ thms') @ map (pair ~1) extra_thms end -fun unfold2 ithms ctxt = +fun unfold2 ctxt ithms = ithms |> map (apsnd (Conv.fconv_rule (normalize_numerals_conv ctxt))) |> burrow_ids add_nat_embedding - |> rpair ctxt @@ -594,11 +593,11 @@ fun add_extra_norm (cs, norm) = Extra_Norms.map (SMT_Utils.dict_update (cs, norm)) -fun apply_extra_norms ithms ctxt = +fun apply_extra_norms ctxt ithms = let val cs = SMT_Config.solver_class_of ctxt val es = SMT_Utils.dict_lookup (Extra_Norms.get (Context.Proof ctxt)) cs - in (burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms, ctxt) end + in burrow_ids (fold (fn e => e ctxt) es o rpair []) ithms end local val ignored = member (op =) [@{const_name All}, @{const_name Ex}, @@ -622,12 +621,12 @@ in (fn t => collect t Symtab.empty) end in -fun monomorph xthms ctxt = +fun monomorph ctxt xthms = let val (xs, thms) = split_list xthms in - (map (pair 1) thms, ctxt) - |-> Monomorph.monomorph schematic_consts_of - |>> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) + map (pair 1) thms + |> Monomorph.monomorph schematic_consts_of ctxt + |> maps (uncurry (map o pair)) o map2 pair xs o map (map snd) end end @@ -636,10 +635,10 @@ iwthms |> gen_normalize ctxt |> unfold1 ctxt + |> monomorph ctxt + |> unfold2 ctxt + |> apply_extra_norms ctxt |> rpair ctxt - |-> monomorph - |-> unfold2 - |-> apply_extra_norms val setup = Context.theory_map ( setup_atomize #> diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Mar 28 23:44:41 2013 +0100 @@ -640,10 +640,10 @@ fun repair_monomorph_context max_iters best_max_iters max_new_instances best_max_new_instances = - Config.put Monomorph.max_rounds (max_iters |> the_default best_max_iters) - #> Config.put Monomorph.max_new_instances + Config.put Legacy_Monomorph.max_rounds (max_iters |> the_default best_max_iters) + #> Config.put Legacy_Monomorph.max_new_instances (max_new_instances |> the_default best_max_new_instances) - #> Config.put Monomorph.keep_partial_instances false + #> Config.put Legacy_Monomorph.keep_partial_instances false fun suffix_for_mode Auto_Try = "_try" | suffix_for_mode Try = "_try" @@ -747,7 +747,7 @@ |> op @ |> cons (0, subgoal_th) in - Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl + Legacy_Monomorph.monomorph atp_schematic_consts_of rths ctxt |> fst |> tl |> curry ListPair.zip (map fst facts) |> maps (fn (name, rths) => map (pair name o zero_var_indexes o snd) rths) diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/legacy_monomorph.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Tools/legacy_monomorph.ML Thu Mar 28 23:44:41 2013 +0100 @@ -0,0 +1,331 @@ +(* Title: HOL/Tools/legacy_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 LEGACY_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 Legacy_Monomorph: LEGACY_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 legacy_monomorph_max_rounds} (K 5) +val max_new_instances = + Attrib.setup_config_int @{binding legacy_monomorph_max_new_instances} (K 300) +val keep_partial_instances = + Attrib.setup_config_bool @{binding legacy_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 derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => + Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) + +fun eq_subst (subst1, subst2) = + derived_subst subst1 subst2 andalso derived_subst subst2 subst1 + + +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' => insert eq_subst subst'))) [] + + +fun known_subst sub subs1 subs2 subst' = + let fun derived (_, subst) = derived_subst subst' subst + in derived sub orelse exists derived subs1 orelse exists derived subs2 end + +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 + (* The total limit of returned (ground) facts is the number of facts + given to the monomorphizer increased by max_new_instances. Since + initially ground facts are returned anyway, the limit here is not + counting them. *) + val limit = Config.get ctxt max_new_instances + + fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0 + + 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 (fn Ground thm => [(0, thm)] | _ => []) thm_infos, 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 + diff -r 2b58d7b139d6 -r 907efc894051 src/HOL/Tools/monomorph.ML --- a/src/HOL/Tools/monomorph.ML Thu Mar 28 22:42:18 2013 +0100 +++ b/src/HOL/Tools/monomorph.ML Thu Mar 28 23:44:41 2013 +0100 @@ -1,34 +1,32 @@ (* 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. +Monomorphization of theorems, i.e., computation of ground instances for +theorems with type variables. This procedure is incomplete in general, +but works well for most practical problems. -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. +Monomorphization is essentially an enumeration of substitutions that map +schematic types to ground types. Applying these substitutions to theorems +with type variables results in monomorphized ground instances. The +enumeration is driven by schematic constants (constants occurring with +type variables) and all ground instances of such constants (occurrences +without type variables). The enumeration is organized in rounds in which +all substitutions for the schematic constants are computed that are induced +by the ground instances. Any new ground instance may induce further +substitutions in a subsequent round. To prevent nontermination, there is +an upper limit of rounds involved and of the number of monomorphized ground +instances computed. -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. +Theorems to be monomorphized must be tagged with a number indicating the +initial round in which they participate first. The initial round is +ignored for theorems without type variables. For any other theorem, the +initial round must be greater than zero. Returned monomorphized theorems +carry a number showing from which monomorphization round they emerged. *) signature MONOMORPH = sig - (* utility function *) + (* utility functions *) 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 -> @@ -37,11 +35,10 @@ (* 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 + val monomorph: (term -> typ list Symtab.table) -> Proof.context -> + (int * thm) list -> (int * thm) list list end structure Monomorph: MONOMORPH = @@ -59,254 +56,16 @@ fun all_schematic_consts_of t = add_schematic_consts_of t Symtab.empty +fun clear_grounds grounds = Symtab.map (K (K [])) grounds + (* 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 derived_subst subst' subst = subst' |> Vartab.forall (fn (n, (_, T)) => - Vartab.lookup subst n |> Option.map (equal T o snd) |> the_default false) - -fun eq_subst (subst1, subst2) = - derived_subst subst1 subst2 andalso derived_subst subst2 subst1 - - -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' => insert eq_subst subst'))) [] - - -fun known_subst sub subs1 subs2 subst' = - let fun derived (_, subst) = derived_subst subst' subst - in derived sub orelse exists derived subs1 orelse exists derived subs2 end - -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 - (* The total limit of returned (ground) facts is the number of facts - given to the monomorphizer increased by max_new_instances. Since - initially ground facts are returned anyway, the limit here is not - counting them. *) - val limit = Config.get ctxt max_new_instances + - fold (fn Schematic _ => Integer.add 1 | _ => I) thm_infos 0 - - 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 @@ -314,18 +73,220 @@ 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 = +fun reached_limit ctxt n = (n >= Config.get ctxt max_new_instances) + + + +(* theorem information and related functions *) + +datatype thm_info = + Ground of thm | + Ignored | + Schematic of { + id: int, + theorem: thm, + tvars: (indexname * sort) list, + schematics: (string * typ) list, + initial_round: int} + + +fun fold_grounds f = fold (fn Ground thm => f thm | _ => I) + + +fun fold_schematic f thm_info = + (case thm_info of + Schematic {id, theorem, tvars, schematics, initial_round} => + f id theorem tvars schematics initial_round + | _ => I) + + +fun fold_schematics pred f = + let + fun apply id thm tvars schematics initial_round x = + if pred initial_round then f id thm tvars schematics x else x + in fold (fold_schematic apply) end + + + +(* collecting data *) + +(* + Theorems with type variables that cannot be instantiated should be ignored. + A type variable has only a chance to be instantiated if it occurs in the + type of one of the schematic constants. +*) +fun groundable all_tvars schematics = + let val tvars' = Symtab.fold (fold Term.add_tvarsT o snd) schematics [] + in forall (member (op =) tvars') all_tvars end + + +fun prepare schematic_consts_of rthms = let - val (thm_infos, (known_grounds, subs)) = prepare schematic_consts_of rthms + fun prep (initial_round, thm) ((id, idx), consts) = + if Term.exists_type typ_has_tvars (Thm.prop_of thm) then + let + (* increase indices to avoid clashes of type variables *) + val thm' = Thm.incr_indexes idx thm + val idx' = Thm.maxidx_of thm' + 1 + + val tvars = Term.add_tvars (Thm.prop_of thm') [] + val schematics = schematic_consts_of (Thm.prop_of thm') + val schematics' = + Symtab.fold (fn (n, Ts) => fold (cons o pair n) Ts) schematics [] + + (* collect the names of all constants that need to be instantiated *) + val consts' = + consts + |> Symtab.fold (fn (n, _) => Symtab.update (n, [])) schematics + + val thm_info = + if not (groundable tvars schematics) then Ignored + else + Schematic { + id = id, + theorem = thm', + tvars = tvars, + schematics = schematics', + initial_round = initial_round} + in (thm_info, ((id + 1, idx'), consts')) end + else (Ground thm, ((id + 1, idx + Thm.maxidx_of thm + 1), consts)) + + in fold_map prep rthms ((0, 0), Symtab.empty) ||> snd end + + + +(* collecting instances *) + +fun instantiate thy subst = + let + fun cert (ix, (S, T)) = pairself (Thm.ctyp_of thy) (TVar (ix, S), T) + fun cert' subst = Vartab.fold (cons o cert) subst [] + in Thm.instantiate (cert' subst, []) end + + +fun add_new_grounds used_grounds new_grounds thm = + let + fun mem tab (n, T) = member (op =) (Symtab.lookup_list tab n) T + fun add (Const (c as (n, _))) = + if mem used_grounds c orelse mem new_grounds c then I + else if not (Symtab.defined used_grounds n) then I + else Symtab.insert_list (op =) c + | add _ = I + in Term.fold_aterms add (Thm.prop_of thm) end + + +fun add_insts ctxt round used_grounds new_grounds id thm tvars schematics cx = + let + exception ENOUGH of + typ list Symtab.table * (int * (int * thm) list Inttab.table) + + val thy = Proof_Context.theory_of ctxt + + fun add subst (next_grounds, (n, insts)) = + let + val thm' = instantiate thy subst thm + val rthm = (round, thm') + val n_insts' = + if member (eq_snd Thm.eq_thm) (Inttab.lookup_list insts id) rthm then + (n, insts) + else (n + 1, Inttab.cons_list (id, rthm) insts) + val next_grounds' = + add_new_grounds used_grounds new_grounds thm' next_grounds + val cx' = (next_grounds', n_insts') + in if reached_limit ctxt n then raise ENOUGH cx' else cx' end + + fun with_grounds (n, T) f subst (n', Us) = + let + fun matching U = (* one-step refinement of the given substitution *) + (case try (Sign.typ_match thy (T, U)) subst of + NONE => I + | SOME subst' => f subst') + in if n = n' then fold matching Us else I end + + fun with_matching_ground c subst f = + (* Try new grounds before already used grounds. Otherwise only + substitutions already seen in previous rounds get enumerated. *) + Symtab.fold (with_grounds c (f true) subst) new_grounds #> + Symtab.fold (with_grounds c (f false) subst) used_grounds + + fun is_complete subst = + (* Check if a substitution is defined for all TVars of the theorem, + which guarantees that the instantiation with this substitution results + in a ground theorem since all matchings that led to this substitution + are with ground types only. *) + subset (op =) (tvars, Vartab.fold (cons o apsnd fst) subst []) + + fun for_schematics _ [] _ = I + | for_schematics used_new (c :: cs) subst = + with_matching_ground c subst (fn new => fn subst' => + if is_complete subst' then + if used_new orelse new then add subst' + else I + else for_schematics (used_new orelse new) cs subst') #> + for_schematics used_new cs subst in - if Symtab.is_empty known_grounds then - (map (fn Ground thm => [(0, thm)] | _ => []) thm_infos, ctxt) - else - make_subst_ctxt ctxt thm_infos known_grounds subs - |> limit_rounds ctxt (collect_substitutions thm_infos) - |> instantiate_all ctxt thm_infos + (* Enumerate all substitutions that lead to a ground instance of the + theorem not seen before. A necessary condition for such a new ground + instance is the usage of at least one ground from the new_grounds + table. The approach used here is to match all schematics of the theorem + with all relevant grounds. *) + for_schematics false schematics Vartab.empty cx + handle ENOUGH cx' => cx' end +fun is_new round initial_round = (round = initial_round) +fun is_active round initial_round = (round > initial_round) + + +fun find_instances thm_infos ctxt round (known_grounds, new_grounds, insts) = + let + val add_new = add_insts ctxt round + fun consider_all pred f (cx as (_, (n, _))) = + if reached_limit ctxt n then cx + else fold_schematics pred f thm_infos cx + + val known_grounds' = Symtab.merge_list (op =) (known_grounds, new_grounds) + val empty_grounds = clear_grounds known_grounds' + + val (new_grounds', insts') = + (Symtab.empty, insts) + |> consider_all (is_active round) (add_new known_grounds new_grounds) + |> consider_all (is_new round) (add_new empty_grounds known_grounds') + + in (known_grounds', new_grounds', insts') end + + +fun add_ground_types thm = + let fun add (n, T) = Symtab.map_entry n (insert (op =) T) + in Term.fold_aterms (fn Const c => add c | _ => I) (Thm.prop_of thm) end + + +fun collect_instances ctxt thm_infos consts = + let + val known_grounds = fold_grounds add_ground_types thm_infos consts + val empty_grounds = clear_grounds known_grounds + in + (empty_grounds, known_grounds, (0, Inttab.empty)) + |> limit_rounds ctxt (find_instances thm_infos) + |> (fn (_, _, (_, insts)) => insts) + end + + + +(* monomorphization *) + +fun instantiated_thms _ (Ground thm) = [(0, thm)] + | instantiated_thms _ Ignored = [] + | instantiated_thms insts (Schematic {id, ...}) = Inttab.lookup_list insts id + + +fun monomorph schematic_consts_of ctxt rthms = + let + val (thm_infos, consts) = prepare schematic_consts_of rthms + val insts = + if Symtab.is_empty consts then Inttab.empty + else collect_instances ctxt thm_infos consts + in map (instantiated_thms insts) thm_infos end + end -