skolem_cache: ignore internal theorems -- major speedup;
authorwenzelm
Wed Oct 03 00:03:00 2007 +0200 (2007-10-03)
changeset 24821cc55041ca8ba
parent 24820 c0c7e6ebf35f
child 24822 b854842e0b8d
skolem_cache: ignore internal theorems -- major speedup;
skolem_cache_theorems_of: efficient folding of table;
replaced get_axiom by Thm.get_axiom_i (avoids name space fishing);
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Oct 03 00:02:58 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Oct 03 00:03:00 2007 +0200
     1.3 @@ -76,8 +76,8 @@
     1.4  fun rhs_extra_types lhsT rhs =
     1.5    let val lhs_vars = Term.add_tfreesT lhsT []
     1.6        fun add_new_TFrees (TFree v) =
     1.7 -	    if member (op =) lhs_vars v then I else insert (op =) (TFree v)
     1.8 -	| add_new_TFrees _ = I
     1.9 +            if member (op =) lhs_vars v then I else insert (op =) (TFree v)
    1.10 +        | add_new_TFrees _ = I
    1.11        val rhs_consts = fold_aterms (fn Const c => insert (op =) c | _ => I) rhs []
    1.12    in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
    1.13  
    1.14 @@ -105,10 +105,10 @@
    1.15                    Sign.add_consts_authentic [Markup.property_internal] [(cname, cT, NoSyn)] thy
    1.16                             (*Theory is augmented with the constant, then its def*)
    1.17                  val cdef = cname ^ "_def"
    1.18 -                val thy'' = Theory.add_defs_i false false [(cdef, equals cT $ c $ rhs)] thy'
    1.19 +                val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
    1.20                              handle ERROR _ => raise Clausify_failure thy'
    1.21              in dec_sko (subst_bound (list_comb(c,args), p))
    1.22 -			       (thy'', get_axiom thy'' cdef :: axs)
    1.23 +                               (thy'', Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef) :: axs)
    1.24              end
    1.25          | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
    1.26              (*Universal quant: insert a free variable into body and continue*)
    1.27 @@ -279,11 +279,11 @@
    1.28                                       (*Theory is augmented with the constant,
    1.29                                         then its definition*)
    1.30                            val cdef = cname ^ "_def"
    1.31 -                          val thy = Theory.add_defs_i false false
    1.32 +                          val thy = Theory.add_defs_i true false
    1.33                                         [(cdef, equals cT $ c $ rhs)] thy
    1.34                                      handle ERROR _ => raise Clausify_failure thy
    1.35 -                          val _ = Output.debug (fn()=> "Definition is " ^ string_of_thm (get_axiom thy cdef));
    1.36 -                          val ax = get_axiom thy cdef |> freeze_thm
    1.37 +                          val ax = Thm.get_axiom_i thy (Sign.full_name thy cdef)
    1.38 +                                     |> Drule.unvarify
    1.39                                       |> mk_object_eq |> strip_lambdas (length args)
    1.40                                       |> mk_meta_eq |> Meson.generalize
    1.41                            val (_,ax') = Option.valOf (match_rhs thy abs_v_u ax)
    1.42 @@ -507,7 +507,7 @@
    1.43             | SOME (cls,thy') =>
    1.44                   (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^
    1.45                                           " clauses inserted into cache: " ^ name_or_string th);
    1.46 -                  (cls, ThmCache.put (Thmtab.update (th,cls) (ThmCache.get thy')) thy')))
    1.47 +                  (cls, ThmCache.map (Thmtab.update (th,cls)) thy')))
    1.48      | SOME cls => (cls,thy);
    1.49  
    1.50  (*Exported function to convert Isabelle theorems into axiom clauses*)
    1.51 @@ -515,9 +515,9 @@
    1.52    let val thy = Theory.merge (Theory.deref atp_linkup_thy_ref, Thm.theory_of_thm th)
    1.53    in
    1.54        case Thmtab.lookup (ThmCache.get thy) th of
    1.55 -	  NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
    1.56 -		   map Goal.close_result (skolem_thm th))
    1.57 -	| SOME cls => cls
    1.58 +          NONE => (Output.debug (fn () => "cnf_axiom: " ^ name_or_string th);
    1.59 +                   map Goal.close_result (skolem_thm th))
    1.60 +        | SOME cls => cls
    1.61    end;
    1.62  
    1.63  fun pairname th = (PureThy.get_name_hint th, th);
    1.64 @@ -575,11 +575,13 @@
    1.65  
    1.66  val mark_skolemized = Sign.add_consts_i [("ResAxioms_endtheory", HOLogic.boolT, NoSyn)];
    1.67  
    1.68 -fun skolem_cache th thy = #2 (skolem_cache_thm th thy);
    1.69 +fun skolem_cache th thy =
    1.70 +  if PureThy.is_internal th then thy
    1.71 +  else #2 (skolem_cache_thm th thy);
    1.72  
    1.73 -fun skolem_cache_all thy = fold skolem_cache (map #2 (PureThy.all_thms_of thy)) thy;
    1.74 -
    1.75 -fun skolem_cache_new thy = fold skolem_cache (map #2 (PureThy.thms_of thy)) thy;
    1.76 +val skolem_cache_theorems_of = Symtab.fold (fold skolem_cache o snd) o #2 o PureThy.theorems_of;
    1.77 +fun skolem_cache_node thy = skolem_cache_theorems_of thy thy;
    1.78 +fun skolem_cache_all thy = fold skolem_cache_theorems_of (thy :: Theory.ancestors_of thy) thy;
    1.79  
    1.80  (*The cache can be kept smaller by inspecting the prop of each thm. Can ignore all that are
    1.81    lambda_free, but then the individual theory caches become much bigger.*)
    1.82 @@ -588,7 +590,7 @@
    1.83  fun clause_cache_endtheory thy =
    1.84    let val _ = Output.debug (fn () => "RexAxioms end theory action: " ^ Context.str_of_thy thy)
    1.85    in
    1.86 -    Option.map skolem_cache_new (try mark_skolemized thy)
    1.87 +    Option.map skolem_cache_node (try mark_skolemized thy)
    1.88    end;
    1.89  
    1.90  (*** meson proof methods ***)