tuning (in particular, Symtab instead of AList)
authorblanchet
Tue Mar 27 16:59:13 2012 +0300 (2012-03-27)
changeset 471506df6e56fd7cd
parent 47149 97f8c6c88134
child 47151 eaf0ffea11aa
tuning (in particular, Symtab instead of AList)
src/HOL/Tools/ATP/atp_problem.ML
src/HOL/Tools/ATP/atp_problem_generate.ML
src/HOL/Tools/ATP/atp_util.ML
     1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -125,7 +125,7 @@
     1.4      (string * string) problem -> (string * string) problem
     1.5    val filter_cnf_ueq_problem :
     1.6      (string * string) problem -> (string * string) problem
     1.7 -  val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list
     1.8 +  val declared_syms_in_problem : 'a problem -> 'a list
     1.9    val nice_atp_problem :
    1.10      bool -> atp_format -> ('a * (string * string) problem_line list) list
    1.11      -> ('a * string problem_line list) list
    1.12 @@ -689,7 +689,7 @@
    1.13  
    1.14  (** Symbol declarations **)
    1.15  
    1.16 -fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = insert (op =) sym
    1.17 +fun add_declared_syms_in_problem_line (Decl (_, sym, _)) = cons sym
    1.18    | add_declared_syms_in_problem_line _ = I
    1.19  fun declared_syms_in_problem problem =
    1.20    fold (fold add_declared_syms_in_problem_line o snd) problem []
    1.21 @@ -785,9 +785,9 @@
    1.22      if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse
    1.23         String.isSubstring "_" s then
    1.24        s
    1.25 -    else if s = "Dl" orelse s = "DL" then
    1.26 +    else if is_tptp_variable s then
    1.27        (* "DL" appears to be a SPASS 3.7 keyword *)
    1.28 -      s ^ "_"
    1.29 +      if s = "DL" then s ^ "_" else s
    1.30      else
    1.31        String.substring (s, 0, n - 1) ^
    1.32        String.str (Char.toUpper (String.sub (s, n - 1)))
     2.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     2.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Mar 27 16:59:13 2012 +0300
     2.3 @@ -131,8 +131,8 @@
     2.4  val avoid_first_order_ghost_type_vars = false
     2.5  
     2.6  val bound_var_prefix = "B_"
     2.7 -val all_bound_var_prefix = "BA_"
     2.8 -val exist_bound_var_prefix = "BE_"
     2.9 +val all_bound_var_prefix = "A_"
    2.10 +val exist_bound_var_prefix = "E_"
    2.11  val schematic_var_prefix = "V_"
    2.12  val fixed_var_prefix = "v_"
    2.13  val tvar_prefix = "T_"
    2.14 @@ -824,10 +824,10 @@
    2.15  
    2.16  fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
    2.17  
    2.18 -fun insert_type ctxt get_T x xs =
    2.19 +fun insert_type thy get_T x xs =
    2.20    let val T = get_T x in
    2.21 -    if exists (type_instance ctxt T o get_T) xs then xs
    2.22 -    else x :: filter_out (type_generalization ctxt T o get_T) xs
    2.23 +    if exists (type_instance thy T o get_T) xs then xs
    2.24 +    else x :: filter_out (type_generalization thy T o get_T) xs
    2.25    end
    2.26  
    2.27  (* The Booleans indicate whether all type arguments should be kept. *)
    2.28 @@ -1342,20 +1342,24 @@
    2.29    | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
    2.30                               maybe_nonmono_Ts, ...}
    2.31                         (Noninf_Nonmono_Types (strictness, grain)) T =
    2.32 -    grain = Ghost_Type_Arg_Vars orelse
    2.33 -    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
    2.34 -     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
    2.35 -          (not (member (type_equiv ctxt) maybe_finite_Ts T) andalso
    2.36 -           is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
    2.37 -                                           T)))
    2.38 +    let val thy = Proof_Context.theory_of ctxt in
    2.39 +      grain = Ghost_Type_Arg_Vars orelse
    2.40 +      (exists (type_intersect thy T) maybe_nonmono_Ts andalso
    2.41 +       not (exists (type_instance thy T) surely_infinite_Ts orelse
    2.42 +            (not (member (type_equiv thy) maybe_finite_Ts T) andalso
    2.43 +             is_type_kind_of_surely_infinite ctxt strictness surely_infinite_Ts
    2.44 +                                             T)))
    2.45 +    end
    2.46    | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
    2.47                               maybe_nonmono_Ts, ...}
    2.48                         (Fin_Nonmono_Types grain) T =
    2.49 -    grain = Ghost_Type_Arg_Vars orelse
    2.50 -    (exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
    2.51 -     (exists (type_generalization ctxt T) surely_finite_Ts orelse
    2.52 -      (not (member (type_equiv ctxt) maybe_infinite_Ts T) andalso
    2.53 -       is_type_surely_finite ctxt T)))
    2.54 +    let val thy = Proof_Context.theory_of ctxt in
    2.55 +      grain = Ghost_Type_Arg_Vars orelse
    2.56 +      (exists (type_intersect thy T) maybe_nonmono_Ts andalso
    2.57 +       (exists (type_generalization thy T) surely_finite_Ts orelse
    2.58 +        (not (member (type_equiv thy) maybe_infinite_Ts T) andalso
    2.59 +         is_type_surely_finite ctxt T)))
    2.60 +    end
    2.61    | should_encode_type _ _ _ _ = false
    2.62  
    2.63  fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
    2.64 @@ -1425,8 +1429,8 @@
    2.65      fun consider_var_ary const_T var_T max_ary =
    2.66        let
    2.67          fun iter ary T =
    2.68 -          if ary = max_ary orelse type_instance ctxt var_T T orelse
    2.69 -             type_instance ctxt T var_T then
    2.70 +          if ary = max_ary orelse type_instance thy var_T T orelse
    2.71 +             type_instance thy T var_T then
    2.72              ary
    2.73            else
    2.74              iter (ary + 1) (range_type T)
    2.75 @@ -1445,7 +1449,7 @@
    2.76               min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
    2.77               max_ary = max_ary, types = types, in_conj = in_conj}
    2.78            val fun_var_Ts' =
    2.79 -            fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
    2.80 +            fun_var_Ts |> can dest_funT T ? insert_type thy I T
    2.81          in
    2.82            if bool_vars' = bool_vars andalso
    2.83               pointer_eq (fun_var_Ts', fun_var_Ts) then
    2.84 @@ -1473,7 +1477,7 @@
    2.85                      let
    2.86                        val pred_sym =
    2.87                          pred_sym andalso top_level andalso not bool_vars
    2.88 -                      val types' = types |> insert_type ctxt I T
    2.89 +                      val types' = types |> insert_type thy I T
    2.90                        val in_conj = in_conj orelse conj_fact
    2.91                        val min_ary =
    2.92                          if (app_op_level = Sufficient_App_Op orelse
    2.93 @@ -2070,7 +2074,7 @@
    2.94      map (decl_line_for_class order) classes
    2.95    | _ => []
    2.96  
    2.97 -fun sym_decl_table_for_facts ctxt format type_enc sym_tab
    2.98 +fun sym_decl_table_for_facts thy format type_enc sym_tab
    2.99                               (conjs, facts, extra_tms) =
   2.100    let
   2.101      fun add_iterm_syms tm =
   2.102 @@ -2091,8 +2095,8 @@
   2.103             in
   2.104               if decl_sym then
   2.105                 Symtab.map_default (s, [])
   2.106 -                   (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
   2.107 -                                         in_conj))
   2.108 +                   (insert_type thy #3 (s', T_args, T, pred_sym, length args,
   2.109 +                                        in_conj))
   2.110               else
   2.111                 I
   2.112             end
   2.113 @@ -2102,7 +2106,7 @@
   2.114        end
   2.115      val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> fact_lift
   2.116      fun add_formula_var_types (AQuant (_, xs, phi)) =
   2.117 -        fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
   2.118 +        fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
   2.119          #> add_formula_var_types phi
   2.120        | add_formula_var_types (AConn (_, phis)) =
   2.121          fold add_formula_var_types phis
   2.122 @@ -2119,12 +2123,12 @@
   2.123                | _ => I)
   2.124        in
   2.125          Symtab.map_default (s, [])
   2.126 -                           (insert_type ctxt #3 (s', [T], T, false, 0, false))
   2.127 +                           (insert_type thy #3 (s', [T], T, false, 0, false))
   2.128        end
   2.129      fun add_TYPE_const () =
   2.130        let val (s, s') = TYPE_name in
   2.131          Symtab.map_default (s, [])
   2.132 -            (insert_type ctxt #3
   2.133 +            (insert_type thy #3
   2.134                           (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
   2.135        end
   2.136    in
   2.137 @@ -2158,44 +2162,46 @@
   2.138          (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
   2.139          (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
   2.140                    surely_infinite_Ts, maybe_nonmono_Ts}) =
   2.141 -    if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
   2.142 -      case level of
   2.143 -        Noninf_Nonmono_Types (strictness, _) =>
   2.144 -        if exists (type_instance ctxt T) surely_infinite_Ts orelse
   2.145 -           member (type_equiv ctxt) maybe_finite_Ts T then
   2.146 -          mono
   2.147 -        else if is_type_kind_of_surely_infinite ctxt strictness
   2.148 -                                                surely_infinite_Ts T then
   2.149 -          {maybe_finite_Ts = maybe_finite_Ts,
   2.150 -           surely_finite_Ts = surely_finite_Ts,
   2.151 -           maybe_infinite_Ts = maybe_infinite_Ts,
   2.152 -           surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
   2.153 -           maybe_nonmono_Ts = maybe_nonmono_Ts}
   2.154 -        else
   2.155 -          {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv ctxt) T,
   2.156 -           surely_finite_Ts = surely_finite_Ts,
   2.157 -           maybe_infinite_Ts = maybe_infinite_Ts,
   2.158 -           surely_infinite_Ts = surely_infinite_Ts,
   2.159 -           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
   2.160 -      | Fin_Nonmono_Types _ =>
   2.161 -        if exists (type_instance ctxt T) surely_finite_Ts orelse
   2.162 -           member (type_equiv ctxt) maybe_infinite_Ts T then
   2.163 -          mono
   2.164 -        else if is_type_surely_finite ctxt T then
   2.165 -          {maybe_finite_Ts = maybe_finite_Ts,
   2.166 -           surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
   2.167 -           maybe_infinite_Ts = maybe_infinite_Ts,
   2.168 -           surely_infinite_Ts = surely_infinite_Ts,
   2.169 -           maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
   2.170 -        else
   2.171 -          {maybe_finite_Ts = maybe_finite_Ts,
   2.172 -           surely_finite_Ts = surely_finite_Ts,
   2.173 -           maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv ctxt) T,
   2.174 -           surely_infinite_Ts = surely_infinite_Ts,
   2.175 -           maybe_nonmono_Ts = maybe_nonmono_Ts}
   2.176 -      | _ => mono
   2.177 -    else
   2.178 -      mono
   2.179 +    let val thy = Proof_Context.theory_of ctxt in
   2.180 +      if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
   2.181 +        case level of
   2.182 +          Noninf_Nonmono_Types (strictness, _) =>
   2.183 +          if exists (type_instance thy T) surely_infinite_Ts orelse
   2.184 +             member (type_equiv thy) maybe_finite_Ts T then
   2.185 +            mono
   2.186 +          else if is_type_kind_of_surely_infinite ctxt strictness
   2.187 +                                                  surely_infinite_Ts T then
   2.188 +            {maybe_finite_Ts = maybe_finite_Ts,
   2.189 +             surely_finite_Ts = surely_finite_Ts,
   2.190 +             maybe_infinite_Ts = maybe_infinite_Ts,
   2.191 +             surely_infinite_Ts = surely_infinite_Ts |> insert_type thy I T,
   2.192 +             maybe_nonmono_Ts = maybe_nonmono_Ts}
   2.193 +          else
   2.194 +            {maybe_finite_Ts = maybe_finite_Ts |> insert (type_equiv thy) T,
   2.195 +             surely_finite_Ts = surely_finite_Ts,
   2.196 +             maybe_infinite_Ts = maybe_infinite_Ts,
   2.197 +             surely_infinite_Ts = surely_infinite_Ts,
   2.198 +             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
   2.199 +        | Fin_Nonmono_Types _ =>
   2.200 +          if exists (type_instance thy T) surely_finite_Ts orelse
   2.201 +             member (type_equiv thy) maybe_infinite_Ts T then
   2.202 +            mono
   2.203 +          else if is_type_surely_finite ctxt T then
   2.204 +            {maybe_finite_Ts = maybe_finite_Ts,
   2.205 +             surely_finite_Ts = surely_finite_Ts |> insert_type thy I T,
   2.206 +             maybe_infinite_Ts = maybe_infinite_Ts,
   2.207 +             surely_infinite_Ts = surely_infinite_Ts,
   2.208 +             maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type thy I T}
   2.209 +          else
   2.210 +            {maybe_finite_Ts = maybe_finite_Ts,
   2.211 +             surely_finite_Ts = surely_finite_Ts,
   2.212 +             maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_equiv thy) T,
   2.213 +             surely_infinite_Ts = surely_infinite_Ts,
   2.214 +             maybe_nonmono_Ts = maybe_nonmono_Ts}
   2.215 +        | _ => mono
   2.216 +      else
   2.217 +        mono
   2.218 +    end
   2.219    | add_iterm_mononotonicity_info _ _ _ _ mono = mono
   2.220  fun add_fact_mononotonicity_info ctxt level
   2.221          ({kind, iformula, ...} : translated_formula) =
   2.222 @@ -2210,9 +2216,10 @@
   2.223  
   2.224  fun add_iformula_monotonic_types ctxt mono type_enc =
   2.225    let
   2.226 +    val thy = Proof_Context.theory_of ctxt
   2.227      val level = level_of_type_enc type_enc
   2.228      val should_encode = should_encode_type ctxt mono level
   2.229 -    fun add_type T = not (should_encode T) ? insert_type ctxt I T
   2.230 +    fun add_type T = not (should_encode T) ? insert_type thy I T
   2.231      fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
   2.232        | add_args _ = I
   2.233      and add_term tm = add_type (ityp_of tm) #> add_args tm
   2.234 @@ -2360,12 +2367,12 @@
   2.235  
   2.236  fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
   2.237  
   2.238 -fun rationalize_decls ctxt (decls as decl :: (decls' as _ :: _)) =
   2.239 +fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
   2.240      let
   2.241        val T = result_type_of_decl decl
   2.242                |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
   2.243      in
   2.244 -      if forall (type_generalization ctxt T o result_type_of_decl) decls' then
   2.245 +      if forall (type_generalization thy T o result_type_of_decl) decls' then
   2.246          [decl]
   2.247        else
   2.248          decls
   2.249 @@ -2378,7 +2385,8 @@
   2.250      Simple_Types _ => [decl_line_for_sym ctxt format mono type_enc s (hd decls)]
   2.251    | Guards (_, level) =>
   2.252      let
   2.253 -      val decls = decls |> rationalize_decls ctxt
   2.254 +      val thy = Proof_Context.theory_of ctxt
   2.255 +      val decls = decls |> rationalize_decls thy
   2.256        val n = length decls
   2.257        val decls =
   2.258          decls |> filter (should_encode_type ctxt mono level
   2.259 @@ -2517,10 +2525,9 @@
   2.260  
   2.261  fun undeclared_syms_in_problem type_enc problem =
   2.262    let
   2.263 -    val declared = declared_syms_in_problem problem
   2.264      fun do_sym (name as (s, _)) ty =
   2.265 -      if is_tptp_user_symbol s andalso not (member (op =) declared name) then
   2.266 -        AList.default (op =) (name, ty)
   2.267 +      if is_tptp_user_symbol s then
   2.268 +        Symtab.default (s, (name, ty))
   2.269        else
   2.270          I
   2.271      fun do_type (AType (name, tys)) =
   2.272 @@ -2539,17 +2546,19 @@
   2.273      fun do_problem_line (Decl (_, _, ty)) = do_type ty
   2.274        | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
   2.275    in
   2.276 -    fold (fold do_problem_line o snd) problem []
   2.277 -    |> filter_out (is_built_in_tptp_symbol o fst o fst)
   2.278 +    Symtab.empty
   2.279 +    |> fold (fn (s, _) => Symtab.default (s, (("", ""), K tvar_a_atype)))
   2.280 +            (declared_syms_in_problem problem)
   2.281 +    |> fold (fold do_problem_line o snd) problem
   2.282    end
   2.283  
   2.284  fun declare_undeclared_syms_in_atp_problem type_enc problem =
   2.285    let
   2.286      val decls =
   2.287 -      problem
   2.288 -      |> undeclared_syms_in_problem type_enc
   2.289 -      |> sort_wrt (fst o fst)
   2.290 -      |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
   2.291 +      Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
   2.292 +                    | (s, (sym, ty)) =>
   2.293 +                      cons (Decl (type_decl_prefix ^ s, sym, ty ())))
   2.294 +                  (undeclared_syms_in_problem type_enc problem) []
   2.295    in (implicit_declsN, decls) :: problem end
   2.296  
   2.297  fun exists_subdtype P =
   2.298 @@ -2622,7 +2631,7 @@
   2.299            conj_sym_kind mono type_enc uncurried_aliases sym_tab0 sym_tab
   2.300      val sym_decl_lines =
   2.301        (conjs, helpers @ facts, uncurried_alias_eq_tms)
   2.302 -      |> sym_decl_table_for_facts ctxt format type_enc sym_tab
   2.303 +      |> sym_decl_table_for_facts thy format type_enc sym_tab
   2.304        |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
   2.305                                                 type_enc mono_Ts
   2.306      val num_facts = length facts
     3.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
     3.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
     3.3 @@ -16,10 +16,10 @@
     3.4    val maybe_quote : string -> string
     3.5    val string_from_ext_time : bool * Time.time -> string
     3.6    val string_from_time : Time.time -> string
     3.7 -  val type_instance : Proof.context -> typ -> typ -> bool
     3.8 -  val type_generalization : Proof.context -> typ -> typ -> bool
     3.9 -  val type_intersect : Proof.context -> typ -> typ -> bool
    3.10 -  val type_equiv : Proof.context -> typ * typ -> bool
    3.11 +  val type_instance : theory -> typ -> typ -> bool
    3.12 +  val type_generalization : theory -> typ -> typ -> bool
    3.13 +  val type_intersect : theory -> typ -> typ -> bool
    3.14 +  val type_equiv : theory -> typ * typ -> bool
    3.15    val varify_type : Proof.context -> typ -> typ
    3.16    val instantiate_type : theory -> typ -> typ -> typ -> typ
    3.17    val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
    3.18 @@ -123,14 +123,12 @@
    3.19  
    3.20  val string_from_time = string_from_ext_time o pair false
    3.21  
    3.22 -fun type_instance ctxt T T' =
    3.23 -  Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
    3.24 -fun type_generalization ctxt T T' = type_instance ctxt T' T
    3.25 -fun type_intersect ctxt T T' =
    3.26 -  can (Sign.typ_unify (Proof_Context.theory_of ctxt)
    3.27 -                      (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
    3.28 +fun type_instance thy T T' = Sign.typ_instance thy (T, T')
    3.29 +fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
    3.30 +fun type_intersect thy T T' =
    3.31 +  can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
    3.32        (Vartab.empty, 0)
    3.33 -val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
    3.34 +val type_equiv = Sign.typ_equiv
    3.35  
    3.36  fun varify_type ctxt T =
    3.37    Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
    3.38 @@ -177,7 +175,7 @@
    3.39      fun aux slack avoid T =
    3.40        if member (op =) avoid T then
    3.41          0
    3.42 -      else case AList.lookup (type_equiv ctxt) assigns T of
    3.43 +      else case AList.lookup (type_equiv thy) assigns T of
    3.44          SOME k => k
    3.45        | NONE =>
    3.46          case T of