--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 12:15:17 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 30 12:20:04 2011 +0100
@@ -399,19 +399,22 @@
fun filter_used_facts used = filter (member (op =) used o fst)
-fun preplay_one_line_proof debug timeout ths state i reconstructor =
+fun preplay_one_line_proof debug timeout ths state i reconstructors =
let
- fun preplay reconstructor =
- let val timer = Timer.startRealTimer () in
- case timed_reconstructor reconstructor debug timeout ths state i of
- SOME (SOME _) => Preplayed (reconstructor, Timer.checkRealTimer timer)
- | _ =>
- if reconstructor = Metis then preplay MetisFT else Failed_to_Preplay
- end
- handle TimeLimit.TimeOut => Trust_Playable (reconstructor, SOME timeout)
+ fun preplay [] [] = Failed_to_Preplay
+ | preplay (timed_out :: _) [] = Trust_Playable (timed_out, SOME timeout)
+ | preplay timed_out (reconstructor :: reconstructors) =
+ let val timer = Timer.startRealTimer () in
+ case timed_reconstructor reconstructor debug timeout ths state i of
+ SOME (SOME _) =>
+ Preplayed (reconstructor, Timer.checkRealTimer timer)
+ | _ => preplay timed_out reconstructors
+ end
+ handle TimeLimit.TimeOut =>
+ preplay (reconstructor :: timed_out) reconstructors
in
- if timeout = Time.zeroTime then Trust_Playable (reconstructor, NONE)
- else preplay reconstructor
+ if timeout = Time.zeroTime then Trust_Playable (hd reconstructors, NONE)
+ else preplay [] reconstructors
end
@@ -590,7 +593,8 @@
length facts |> is_none max_relevant
? Integer.min best_max_relevant
val (format, type_sys) =
- determine_format_and_type_sys best_type_systems formats type_sys
+ determine_format_and_type_sys best_type_systems formats
+ type_sys
val fairly_sound = is_type_sys_fairly_sound type_sys
val facts =
facts |> not fairly_sound
@@ -751,16 +755,16 @@
val used_facts =
used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
atp_proof
- val reconstructor =
- if uses_typed_helpers typed_helpers atp_proof then MetisFT
- else Metis
+ val reconstructors =
+ if uses_typed_helpers typed_helpers atp_proof then [MetisFT, Metis]
+ else [Metis, MetisFT]
val used_ths =
facts |> map untranslated_fact
|> filter_used_facts used_facts
|> map snd
val preplay =
preplay_one_line_proof debug preplay_timeout used_ths state subgoal
- reconstructor
+ reconstructors
val full_types = uses_typed_helpers typed_helpers atp_proof
val isar_params =
(debug, full_types, isar_shrink_factor, type_sys, pool,
@@ -950,7 +954,7 @@
else "smt_solver = " ^ maybe_quote name
val preplay =
case preplay_one_line_proof debug preplay_timeout used_ths state
- subgoal Metis of
+ subgoal [Metis, MetisFT] of
p as Preplayed _ => p
| _ => Trust_Playable (SMT (smt_settings ()), NONE)
val one_line_params =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/monomorph.ML Mon May 30 12:20:04 2011 +0100
@@ -0,0 +1,334 @@
+(* Title: HOL/Tools/SMT/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
+