# HG changeset patch # User wenzelm # Date 1223578391 -7200 # Node ID 26743a1591f522046192c1ebf98b59fb7748bf6e # Parent 637f2808ab647bc6015402e9d0cceba465d33196 improved performance of skolem cache, due to parallel map; misc tuning, less verbosity; diff -r 637f2808ab64 -r 26743a1591f5 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Thu Oct 09 20:53:10 2008 +0200 +++ b/src/HOL/Tools/res_axioms.ML Thu Oct 09 20:53:11 2008 +0200 @@ -35,6 +35,7 @@ | type_has_empty_sort (Type (_, Ts)) = exists type_has_empty_sort Ts | type_has_empty_sort _ = false; + (**** Transformation of Elimination Rules into First-Order Formulas****) val cfalse = cterm_of HOL.thy HOLogic.false_const; @@ -54,6 +55,7 @@ (*To enforce single-threading*) exception Clausify_failure of theory; + (**** SKOLEMIZATION BY INFERENCE (lcp) ****) fun rhs_extra_types lhsT rhs = @@ -76,9 +78,6 @@ val args0 = term_frees xtp (*get the formal parameter list*) val Ts = map type_of args0 val extraTs = rhs_extra_types (Ts ---> T) xtp - val _ = if null extraTs then () else - warning ("Skolemization: extra type vars: " ^ - commas_quote (map (Syntax.string_of_typ_global thy) extraTs)) val argsx = map (fn T => Free (gensym "vsk", T)) extraTs val args = argsx @ args0 val cT = extraTs ---> Ts ---> T @@ -165,9 +164,9 @@ (*FIXME: requires more use of cterm constructors*) fun abstract ct = - let val _ = Output.debug (fn()=>" abstraction: " ^ Display.string_of_cterm ct) + let + val thy = theory_of_cterm ct val Abs(x,_,body) = term_of ct - val thy = theory_of_cterm ct val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct) val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K} @@ -209,7 +208,7 @@ end; (*Traverse a theorem, declaring abstraction function definitions. String s is the suggested - prefix for the constants. Resulting theory is returned in the first theorem. *) + prefix for the constants.*) fun combinators_aux ct = if lambda_free (term_of ct) then reflexive ct else @@ -217,13 +216,10 @@ Abs _ => let val (cv,cta) = Thm.dest_abs NONE ct val (v,Tv) = (dest_Free o term_of) cv - val _ = Output.debug (fn()=>" recursion: " ^ Display.string_of_cterm cta); val u_th = combinators_aux cta - val _ = Output.debug (fn()=>" returned " ^ Display.string_of_thm u_th); val cu = Thm.rhs_of u_th val comb_eq = abstract (Thm.cabs cv cu) - in Output.debug (fn()=>" abstraction result: " ^ Display.string_of_thm comb_eq); - (transitive (abstract_rule v cv u_th) comb_eq) end + in transitive (abstract_rule v cv u_th) comb_eq end | t1 $ t2 => let val (ct1,ct2) = Thm.dest_comb ct in combination (combinators_aux ct1) (combinators_aux ct2) end; @@ -231,10 +227,8 @@ fun combinators th = if lambda_free (prop_of th) then th else - let val _ = Output.debug (fn()=>"Conversion to combinators: " ^ Display.string_of_thm th); - val th = Drule.eta_contraction_rule th + let val th = Drule.eta_contraction_rule th val eqth = combinators_aux (cprop_of th) - val _ = Output.debug (fn()=>"Conversion result: " ^ Display.string_of_thm eqth); in equal_elim eqth th end handle THM (msg,_,_) => (warning ("Error in the combinator translation of " ^ Display.string_of_thm th); @@ -359,29 +353,12 @@ in cnfs |> map combinators |> Variable.export ctxt2 ctxt0 |> Meson.finish_cnf end handle THM _ => []; -(*Declare Skolem functions for a theorem, supplied in nnf and with its name. - It returns a modified theory, unless skolemization fails.*) -fun skolem (name, th0) thy = - let - val th = Thm.transfer thy th0 - val ctxt0 = Variable.thm_context th - in - try (to_nnf th) ctxt0 |> Option.map (fn (nnfth, ctxt1) => - let - val s = flatten_name name - val (defs, thy') = declare_skofuns s nnfth thy - val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1 - val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 - |> Meson.finish_cnf |> map Thm.close_derivation - in (cnfs', thy') end) - end; - (*The cache prevents repeated clausification of a theorem, and also repeated declaration of Skolem functions.*) structure ThmCache = TheoryDataFun ( - type T = thm list Thmtab.table * unit Symtab.table - val empty = (Thmtab.empty, Symtab.empty) + type T = thm list Thmtab.table * unit Symtab.table; + val empty = (Thmtab.empty, Symtab.empty); val copy = I; val extend = I; fun merge _ ((cache1, seen1), (cache2, seen2)) : T = @@ -411,19 +388,12 @@ let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs val intros = safeIs @ hazIs val elims = map Classical.classical_rule (safeEs @ hazEs) - in - Output.debug (fn () => "rules_of_claset intros: " ^ Int.toString(length intros) ^ - " elims: " ^ Int.toString(length elims)); - map pairname (intros @ elims) - end; + in map pairname (intros @ elims) end; fun rules_of_simpset ss = let val ({rules,...}, _) = rep_ss ss val simps = Net.entries rules - in - Output.debug (fn () => "rules_of_simpset: " ^ Int.toString(length simps)); - map (fn r => (#name r, #thm r)) simps - end; + in map (fn r => (#name r, #thm r)) simps end; fun claset_rules_of ctxt = rules_of_claset (local_claset_of ctxt); fun simpset_rules_of ctxt = rules_of_simpset (local_simpset_of ctxt); @@ -448,28 +418,51 @@ (**** Convert all facts of the theory into clauses (ResClause.clause, or ResHolClause.clause) ****) -(*Populate the clause cache using the supplied theorem. Return the clausal form - and modified theory.*) -fun skolem_cache_thm name (i, th) thy = - if bad_for_atp th then thy - else - (case lookup_cache thy th of - SOME _ => thy - | NONE => - (case skolem (name ^ "_" ^ string_of_int (i + 1), th) thy of - NONE => thy - | SOME (cls, thy') => update_cache (th, cls) thy')); +local + +fun skolem_def (name, th) thy = + let val ctxt0 = Variable.thm_context th in + (case try (to_nnf th) ctxt0 of + NONE => (NONE, thy) + | SOME (nnfth, ctxt1) => + let val (defs, thy') = declare_skofuns (flatten_name name) nnfth thy + in (SOME (th, ctxt0, ctxt1, nnfth, defs), thy') end) + end; -fun skolem_cache_fact (name, ths) (changed, thy) = - if (Sign.base_name name) mem_string multi_base_blacklist orelse already_seen thy name - then (changed, thy) - else (true, thy |> mark_seen name |> fold_index (skolem_cache_thm name) ths); +fun skolem_cnfs (th, ctxt0, ctxt1, nnfth, defs) = + let + val (cnfs, ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1; + val cnfs' = cnfs + |> map combinators + |> Variable.export ctxt2 ctxt0 + |> Meson.finish_cnf + |> map Thm.close_derivation; + in (th, cnfs') end; + +in fun saturate_skolem_cache thy = - (case Facts.fold_static skolem_cache_fact (PureThy.facts_of thy) (false, thy) of - (false, _) => NONE - | (true, thy') => SOME thy'); + let + val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) => + if already_seen thy name then I else cons (name, ths)); + val new_thms = (new_facts, []) |-> fold (fn (name, ths) => + if member (op =) multi_base_blacklist (Sign.base_name name) then I + else fold_index (fn (i, th) => + if bad_for_atp th orelse is_some (lookup_cache thy th) then I + else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); + in + if null new_facts then NONE + else + let + val (defs, thy') = thy + |> fold (mark_seen o #1) new_facts + |> fold_map skolem_def (sort_distinct (Thm.thm_ord o pairself snd) new_thms) + |>> map_filter I; + val cache_entries = ParList.map skolem_cnfs defs; + in SOME (fold update_cache cache_entries thy') end + end; +end; val suppress_endtheory = ref false; @@ -484,7 +477,7 @@ (*** meson proof methods ***) -(*Expand all new*definitions of abstraction or Skolem functions in a proof state.*) +(*Expand all new definitions of abstraction or Skolem functions in a proof state.*) fun is_absko (Const ("==", _) $ Free (a,_) $ u) = String.isPrefix "sko_" a | is_absko _ = false; @@ -504,17 +497,12 @@ (map Thm.term_of hyps) val fixed = term_frees (concl_of st) @ foldl (gen_union (op aconv)) [] (map term_frees remaining_hyps) - in Output.debug (fn _ => "expand_defs_tac: " ^ Display.string_of_thm st); - Output.debug (fn _ => " st0: " ^ Display.string_of_thm st0); - Output.debug (fn _ => " defs: " ^ commas (map Display.string_of_cterm defs)); - Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] - end; + in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end; fun meson_general_tac ths i st0 = let val thy = Thm.theory_of_thm st0 - val _ = Output.debug (fn () => "Meson called: " ^ cat_lines (map Display.string_of_thm ths)) in (Meson.meson_claset_tac (maps (cnf_axiom thy) ths) HOL_cs i THEN expand_defs_tac st0) st0 end; val meson_method_setup = Method.add_methods @@ -577,4 +565,3 @@ Theory.at_end clause_cache_endtheory; end; -