# HG changeset patch # User blanchet # Date 1378732924 -7200 # Node ID f7d8224641deaf131ace4e29b023175f43a5bd11 # Parent 8c3ccb31446950f8e97f71db43f4e01d96d6489c move metis to new monomorphizer diff -r 8c3ccb314469 -r f7d8224641de src/HOL/ATP.thy --- a/src/HOL/ATP.thy Mon Sep 09 15:22:04 2013 +0200 +++ b/src/HOL/ATP.thy Mon Sep 09 15:22:04 2013 +0200 @@ -11,7 +11,6 @@ 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 8c3ccb314469 -r f7d8224641de src/HOL/Tools/Metis/metis_generate.ML --- a/src/HOL/Tools/Metis/metis_generate.ML Mon Sep 09 15:22:04 2013 +0200 +++ b/src/HOL/Tools/Metis/metis_generate.ML Mon Sep 09 15:22:04 2013 +0200 @@ -215,9 +215,8 @@ else conj_clauses @ fact_clauses |> map (pair 0) - |> rpair (ctxt |> Config.put Legacy_Monomorph.keep_partial_instances false) - |-> Legacy_Monomorph.monomorph atp_schematic_consts_of - |> fst |> chop (length conj_clauses) + |> Monomorph.monomorph atp_schematic_consts_of ctxt + |> chop (length conj_clauses) |> pairself (maps (map (zero_var_indexes o snd))) val num_conjs = length conj_clauses (* Pretend every clause is a "simp" rule, to guide the term ordering. *) diff -r 8c3ccb314469 -r f7d8224641de src/HOL/Tools/legacy_monomorph.ML --- a/src/HOL/Tools/legacy_monomorph.ML Mon Sep 09 15:22:04 2013 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,331 +0,0 @@ -(* 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 -