# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID 6df6e56fd7cd5f50bc3a1d2a8ff357f46bb5a015
# Parent  97f8c6c88134ec3a99dc2f0182b7b4f6c5642641
tuning (in particular, Symtab instead of AList)

diff -r 97f8c6c88134 -r 6df6e56fd7cd src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -125,7 +125,7 @@
     (string * string) problem -> (string * string) problem
   val filter_cnf_ueq_problem :
     (string * string) problem -> (string * string) problem
-  val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
+  val declared_syms_in_problem : 'a problem -> 'a list
   val nice_atp_problem :
     bool -> atp_format -> ('a * (string * string) problem_line list) list
     -> ('a * string problem_line list) list
@@ -689,7 +689,7 @@
 
 (** Symbol declarations **)
 
-fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
+fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = cons sym
   | add_declared_syms_in_problem_line _ = I
 fun declared_syms_in_problem problem =
   fold (fold add_declared_syms_in_problem_line o snd) problem []
@@ -785,9 +785,9 @@
     if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
        String.isSubstring "_" s then
       s
-    else if s = "Dl" orelse s = "DL" then
+    else if is_tptp_variable s then
       (* "DL" appears to be a SPASS 3.7 keyword *)
-      s ^ "_"
+      if s = "DL" then s ^ "_" else s
     else
       String.substring (s, 0, n - 1) ^
       String.str (Char.toUpper (String.sub (s, n - 1)))
diff -r 97f8c6c88134 -r 6df6e56fd7cd src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -131,8 +131,8 @@
 val avoid_first_order_ghost_type_vars = false
 
 val bound_var_prefix = "B_"
-val all_bound_var_prefix = "BA_"
-val exist_bound_var_prefix = "BE_"
+val all_bound_var_prefix = "A_"
+val exist_bound_var_prefix = "E_"
 val schematic_var_prefix = "V_"
 val fixed_var_prefix = "v_"
 val tvar_prefix = "T_"
@@ -824,10 +824,10 @@
 
 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
 
-fun insert_type ctxt get_T x xs =
+fun insert_type thy get_T x xs =
   let val T = get_T x in
-    if exists (type_instance ctxt T o get_T) xs then xs
-    else x :: filter_out (type_generalization ctxt T o get_T) xs
+    if exists (type_instance thy T o get_T) xs then xs
+    else x :: filter_out (type_generalization thy T o get_T) xs
   end
 
 (* The Booleans indicate whether all type arguments should be kept. *)
@@ -1342,20 +1342,24 @@
   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        (Noninf_Nonmono_Types (strictness, grain)) T =
-    grain = Ghost_Type_Arg_Vars orelse
-    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
-     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
-          (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
-           is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
-                                           T)))
+    let val thy = Proof_Context.theory_of ctxt in
+      grain = Ghost_Type_Arg_Vars orelse
+      (exists (type_intersect thy T) maybe_nonmono_Ts andalso
+       not (exists (type_instance thy T) surely_infinite_Ts orelse
+            (not (member (type_equiv thy) maybe_finite_Ts T) andalso
+             is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
+                                             T)))
+    end
   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
                              maybe_nonmono_Ts, ...}
                        (Fin_Nonmono_Types grain) T =
-    grain = Ghost_Type_Arg_Vars orelse
-    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
-     (exists (type_generalization ctxt T) surely_finite_Ts orelse
-      (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
-       is_type_surely_finite ctxt T)))
+    let val thy = Proof_Context.theory_of ctxt in
+      grain = Ghost_Type_Arg_Vars orelse
+      (exists (type_intersect thy T) maybe_nonmono_Ts andalso
+       (exists (type_generalization thy T) surely_finite_Ts orelse
+        (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
+         is_type_surely_finite ctxt T)))
+    end
   | should_encode_type _ _ _ _ = false
 
 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
@@ -1425,8 +1429,8 @@
     fun consider_var_ary const_T var_T max_ary =
       let
         fun iter ary T =
-          if ary = max_ary orelse type_instance ctxt var_T T orelse
-             type_instance ctxt T var_T then
+          if ary = max_ary orelse type_instance thy var_T T orelse
+             type_instance thy T var_T then
             ary
           else
             iter (ary + 1) (range_type T)
@@ -1445,7 +1449,7 @@
              min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
              max_ary = max_ary, types = types, in_conj = in_conj}
           val fun_var_Ts' =
-            fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
+            fun_var_Ts |> can dest_funT T ? insert_type thy I T
         in
           if bool_vars' = bool_vars andalso
              pointer_eq (fun_var_Ts', fun_var_Ts) then
@@ -1473,7 +1477,7 @@
                     let
                       val pred_sym =
                         pred_sym andalso top_level andalso not bool_vars
-                      val types' = types |> insert_type ctxt I T
+                      val types' = types |> insert_type thy I T
                       val in_conj = in_conj orelse conj_fact
                       val min_ary =
                         if (app_op_level = Sufficient_App_Op orelse
@@ -2070,7 +2074,7 @@
     map (decl_line_for_class order) classes
   | _ => []
 
-fun sym_decl_table_for_facts ctxt format type_enc sym_tab
+fun sym_decl_table_for_facts thy format type_enc sym_tab
                              (conjs, facts, extra_tms) =
   let
     fun add_iterm_syms tm =
@@ -2091,8 +2095,8 @@
            in
              if decl_sym then
                Symtab.map_default (s, [])
-                   (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
-                                         in_conj))
+                   (insert_type thy #3 (s', T_args, T, pred_sym, length args,
+                                        in_conj))
              else
                I
            end
@@ -2102,7 +2106,7 @@
       end
     val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
     fun add_formula_var_types (AQuant (_, xs, phi)) =
-        fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
+        fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
         #> add_formula_var_types phi
       | add_formula_var_types (AConn (_, phis)) =
         fold add_formula_var_types phis
@@ -2119,12 +2123,12 @@
               | _ => I)
       in
         Symtab.map_default (s, [])
-                           (insert_type ctxt #3 (s', [T], T, false, 0, false))
+                           (insert_type thy #3 (s', [T], T, false, 0, false))
       end
     fun add_TYPE_const () =
       let val (s, s') = TYPE_name in
         Symtab.map_default (s, [])
-            (insert_type ctxt #3
+            (insert_type thy #3
                          (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
       end
   in
@@ -2158,44 +2162,46 @@
         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
         (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
                   surely_infinite_Ts, maybe_nonmono_Ts}) =
-    if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
-      case level of
-        Noninf_Nonmono_Types (strictness, _) =>
-        if exists (type_instance ctxt T) surely_infinite_Ts orelse
-           member (type_equiv ctxt) maybe_finite_Ts T then
-          mono
-        else if is_type_kind_of_surely_infinite ctxt strictness
-                                                surely_infinite_Ts T then
-          {maybe_finite_Ts = maybe_finite_Ts,
-           surely_finite_Ts = surely_finite_Ts,
-           maybe_infinite_Ts = maybe_infinite_Ts,
-           surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
-           maybe_nonmono_Ts = maybe_nonmono_Ts}
-        else
-          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
-           surely_finite_Ts = surely_finite_Ts,
-           maybe_infinite_Ts = maybe_infinite_Ts,
-           surely_infinite_Ts = surely_infinite_Ts,
-           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
-      | Fin_Nonmono_Types _ =>
-        if exists (type_instance ctxt T) surely_finite_Ts orelse
-           member (type_equiv ctxt) maybe_infinite_Ts T then
-          mono
-        else if is_type_surely_finite ctxt T then
-          {maybe_finite_Ts = maybe_finite_Ts,
-           surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
-           maybe_infinite_Ts = maybe_infinite_Ts,
-           surely_infinite_Ts = surely_infinite_Ts,
-           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
-        else
-          {maybe_finite_Ts = maybe_finite_Ts,
-           surely_finite_Ts = surely_finite_Ts,
-           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
-           surely_infinite_Ts = surely_infinite_Ts,
-           maybe_nonmono_Ts = maybe_nonmono_Ts}
-      | _ => mono
-    else
-      mono
+    let val thy = Proof_Context.theory_of ctxt in
+      if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
+        case level of
+          Noninf_Nonmono_Types (strictness, _) =>
+          if exists (type_instance thy T) surely_infinite_Ts orelse
+             member (type_equiv thy) maybe_finite_Ts T then
+            mono
+          else if is_type_kind_of_surely_infinite ctxt strictness
+                                                  surely_infinite_Ts T then
+            {maybe_finite_Ts = maybe_finite_Ts,
+             surely_finite_Ts = surely_finite_Ts,
+             maybe_infinite_Ts = maybe_infinite_Ts,
+             surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
+             maybe_nonmono_Ts = maybe_nonmono_Ts}
+          else
+            {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
+             surely_finite_Ts = surely_finite_Ts,
+             maybe_infinite_Ts = maybe_infinite_Ts,
+             surely_infinite_Ts = surely_infinite_Ts,
+             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
+        | Fin_Nonmono_Types _ =>
+          if exists (type_instance thy T) surely_finite_Ts orelse
+             member (type_equiv thy) maybe_infinite_Ts T then
+            mono
+          else if is_type_surely_finite ctxt T then
+            {maybe_finite_Ts = maybe_finite_Ts,
+             surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
+             maybe_infinite_Ts = maybe_infinite_Ts,
+             surely_infinite_Ts = surely_infinite_Ts,
+             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
+          else
+            {maybe_finite_Ts = maybe_finite_Ts,
+             surely_finite_Ts = surely_finite_Ts,
+             maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
+             surely_infinite_Ts = surely_infinite_Ts,
+             maybe_nonmono_Ts = maybe_nonmono_Ts}
+        | _ => mono
+      else
+        mono
+    end
   | add_iterm_mononotonicity_info _ _ _ _ mono = mono
 fun add_fact_mononotonicity_info ctxt level
         ({kind, iformula, ...} : translated_formula) =
@@ -2210,9 +2216,10 @@
 
 fun add_iformula_monotonic_types ctxt mono type_enc =
   let
+    val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
     val should_encode = should_encode_type ctxt mono level
-    fun add_type T = not (should_encode T) ? insert_type ctxt I T
+    fun add_type T = not (should_encode T) ? insert_type thy I T
     fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
       | add_args _ = I
     and add_term tm = add_type (ityp_of tm) #> add_args tm
@@ -2360,12 +2367,12 @@
 
 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
 
-fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
+fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
     let
       val T = result_type_of_decl decl
               |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
     in
-      if forall (type_generalization ctxt T o result_type_of_decl) decls' then
+      if forall (type_generalization thy T o result_type_of_decl) decls' then
         [decl]
       else
         decls
@@ -2378,7 +2385,8 @@
     Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
   | Guards (_, level) =>
     let
-      val decls = decls |> rationalize_decls ctxt
+      val thy = Proof_Context.theory_of ctxt
+      val decls = decls |> rationalize_decls thy
       val n = length decls
       val decls =
         decls |> filter (should_encode_type ctxt mono level
@@ -2517,10 +2525,9 @@
 
 fun undeclared_syms_in_problem type_enc problem =
   let
-    val declared = declared_syms_in_problem problem
     fun do_sym (name as (s, _)) ty =
-      if is_tptp_user_symbol s andalso not (member (op =) declared name) then
-        AList.default (op =) (name, ty)
+      if is_tptp_user_symbol s then
+        Symtab.default (s, (name, ty))
       else
         I
     fun do_type (AType (name, tys)) =
@@ -2539,17 +2546,19 @@
     fun do_problem_line (Decl (_, _, ty)) = do_type ty
       | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
   in
-    fold (fold do_problem_line o snd) problem []
-    |> filter_out (is_built_in_tptp_symbol o fst o fst)
+    Symtab.empty
+    |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
+            (declared_syms_in_problem problem)
+    |> fold (fold do_problem_line o snd) problem
   end
 
 fun declare_undeclared_syms_in_atp_problem type_enc problem =
   let
     val decls =
-      problem
-      |> undeclared_syms_in_problem type_enc
-      |> sort_wrt (fst o fst)
-      |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
+      Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
+                    | (s, (sym, ty)) =>
+                      cons (Decl (type_decl_prefix ^ s, sym, ty ())))
+                  (undeclared_syms_in_problem type_enc problem) []
   in (implicit_declsN, decls) :: problem end
 
 fun exists_subdtype P =
@@ -2622,7 +2631,7 @@
           conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
     val sym_decl_lines =
       (conjs, helpers @ facts, uncurried_alias_eq_tms)
-      |> sym_decl_table_for_facts ctxt format type_enc sym_tab
+      |> sym_decl_table_for_facts thy format type_enc sym_tab
       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
                                                type_enc mono_Ts
     val num_facts = length facts
diff -r 97f8c6c88134 -r 6df6e56fd7cd src/HOL/Tools/ATP/atp_util.ML
--- a/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -16,10 +16,10 @@
   val maybe_quote : string -> string
   val string_from_ext_time : bool * Time.time -> string
   val string_from_time : Time.time -> string
-  val type_instance : Proof.context -> typ -> typ -> bool
-  val type_generalization : Proof.context -> typ -> typ -> bool
-  val type_intersect : Proof.context -> typ -> typ -> bool
-  val type_equiv : Proof.context -> typ * typ -> bool
+  val type_instance : theory -> typ -> typ -> bool
+  val type_generalization : theory -> typ -> typ -> bool
+  val type_intersect : theory -> typ -> typ -> bool
+  val type_equiv : theory -> typ * typ -> bool
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
@@ -123,14 +123,12 @@
 
 val string_from_time = string_from_ext_time o pair false
 
-fun type_instance ctxt T T' =
-  Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
-fun type_generalization ctxt T T' = type_instance ctxt T' T
-fun type_intersect ctxt T T' =
-  can (Sign.typ_unify (Proof_Context.theory_of ctxt)
-                      (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
+fun type_instance thy T T' = Sign.typ_instance thy (T, T')
+fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
+fun type_intersect thy T T' =
+  can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
       (Vartab.empty, 0)
-val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
+val type_equiv = Sign.typ_equiv
 
 fun varify_type ctxt T =
   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
@@ -177,7 +175,7 @@
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case AList.lookup (type_equiv ctxt) assigns T of
+      else case AList.lookup (type_equiv thy) assigns T of
         SOME k => k
       | NONE =>
         case T of