1.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Jul 01 15:53:37 2011 +0200
     1.3 @@ -415,10 +415,10 @@
     1.4    remotify_atp z3_atp "Z3" ["2.18"] (K (250, "mangled_preds?") (* FUDGE *))
     1.5  val remote_leo2 =
     1.6    remote_atp leo2N "LEO-II" ["1.2.6"] [] [] Axiom Hypothesis [THF]
     1.7 -             (K (100, "simple") (* FUDGE *))
     1.8 +             (K (100, "simple_higher") (* FUDGE *))
     1.9  val remote_satallax =
    1.10    remote_atp satallaxN "Satallax" ["2.0"] [] [] Axiom Hypothesis [THF]
    1.11 -             (K (64, "simple") (* FUDGE *))
    1.12 +             (K (64, "simple_higher") (* FUDGE *))
    1.13  val remote_sine_e =
    1.14    remote_atp sine_eN "SInE" ["0.4"] [] (#known_failures e_config) Axiom
    1.15               Conjecture [FOF] (K (500, "mangled_preds?") (* FUDGE *))

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Jul 01 15:53:37 2011 +0200
     2.3 @@ -19,6 +19,7 @@
     2.4      General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
     2.5      Chained
     2.6  
     2.7 +  datatype order = First_Order | Higher_Order
     2.8    datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     2.9    datatype type_level =
    2.10      All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    2.11 @@ -26,7 +27,7 @@
    2.12    datatype type_heaviness = Heavyweight | Lightweight
    2.13  
    2.14    datatype type_sys =
    2.15 -    Simple_Types of type_level |
    2.16 +    Simple_Types of order * type_level |
    2.17      Preds of polymorphism * type_level * type_heaviness |
    2.18      Tags of polymorphism * type_level * type_heaviness
    2.19  
    2.20 @@ -501,6 +502,7 @@
    2.21    | is_locality_global Chained = false
    2.22    | is_locality_global _ = true
    2.23  
    2.24 +datatype order = First_Order | Higher_Order
    2.25  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    2.26  datatype type_level =
    2.27    All_Types | Noninf_Nonmono_Types | Fin_Nonmono_Types | Const_Arg_Types |
    2.28 @@ -508,7 +510,7 @@
    2.29  datatype type_heaviness = Heavyweight | Lightweight
    2.30  
    2.31  datatype type_sys =
    2.32 -  Simple_Types of type_level |
    2.33 +  Simple_Types of order * type_level |
    2.34    Preds of polymorphism * type_level * type_heaviness |
    2.35    Tags of polymorphism * type_level * type_heaviness
    2.36  
    2.37 @@ -526,7 +528,8 @@
    2.38           SOME s => (SOME Mangled_Monomorphic, s)
    2.39         | NONE => (NONE, s))
    2.40    ||> (fn s =>
    2.41 -          (* "_query" and "_bang" are for the ASCII-challenged Mirabelle. *)
    2.42 +          (* "_query" and "_bang" are for the ASCII-challenged Metis and
    2.43 +             Mirabelle. *)
    2.44            case try_unsuffixes ["?", "_query"] s of
    2.45              SOME s => (Noninf_Nonmono_Types, s)
    2.46            | NONE =>
    2.47 @@ -539,7 +542,10 @@
    2.48                  | NONE => (Lightweight, s))
    2.49    |> (fn (poly, (level, (heaviness, core))) =>
    2.50           case (core, (poly, level, heaviness)) of
    2.51 -           ("simple", (NONE, _, Lightweight)) => Simple_Types level
    2.52 +           ("simple", (NONE, _, Lightweight)) =>
    2.53 +           Simple_Types (First_Order, level)
    2.54 +         | ("simple_higher", (NONE, _, Lightweight)) =>
    2.55 +           Simple_Types (Higher_Order, level)
    2.56           | ("preds", (SOME poly, _, _)) => Preds (poly, level, heaviness)
    2.57           | ("tags", (SOME Polymorphic, _, _)) =>
    2.58             Tags (Polymorphic, level, heaviness)
    2.59 @@ -551,11 +557,14 @@
    2.60           | _ => raise Same.SAME)
    2.61    handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
    2.62  
    2.63 +fun is_type_sys_higher_order (Simple_Types (Higher_Order, _)) = true
    2.64 +  | is_type_sys_higher_order _ = false
    2.65 +
    2.66  fun polymorphism_of_type_sys (Simple_Types _) = Mangled_Monomorphic
    2.67    | polymorphism_of_type_sys (Preds (poly, _, _)) = poly
    2.68    | polymorphism_of_type_sys (Tags (poly, _, _)) = poly
    2.69  
    2.70 -fun level_of_type_sys (Simple_Types level) = level
    2.71 +fun level_of_type_sys (Simple_Types (_, level)) = level
    2.72    | level_of_type_sys (Preds (_, level, _)) = level
    2.73    | level_of_type_sys (Tags (_, level, _)) = level
    2.74  
    2.75 @@ -572,13 +581,13 @@
    2.76    is_type_level_virtually_sound level orelse level = Fin_Nonmono_Types
    2.77  val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
    2.78  
    2.79 -fun is_setting_higher_order THF (Simple_Types _) = true
    2.80 -  | is_setting_higher_order _ _ = false
    2.81 -
    2.82 -fun choose_format formats (Simple_Types level) =
    2.83 -    if member (op =) formats THF then (THF, Simple_Types level)
    2.84 -    else if member (op =) formats TFF then (TFF, Simple_Types level)
    2.85 -    else choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
    2.86 +fun choose_format formats (Simple_Types (order, level)) =
    2.87 +    if member (op =) formats THF then
    2.88 +      (THF, Simple_Types (order, level))
    2.89 +    else if member (op =) formats TFF then
    2.90 +      (TFF, Simple_Types (First_Order, level))
    2.91 +    else
    2.92 +      choose_format formats (Preds (Mangled_Monomorphic, level, Heavyweight))
    2.93    | choose_format formats type_sys =
    2.94      (case hd formats of
    2.95         CNF_UEQ =>
    2.96 @@ -699,7 +708,7 @@
    2.97  fun fo_term_from_typ format type_sys =
    2.98    let
    2.99      fun term (Type (s, Ts)) =
   2.100 -      ATerm (case (is_setting_higher_order format type_sys, s) of
   2.101 +      ATerm (case (is_type_sys_higher_order type_sys, s) of
   2.102                 (true, @{type_name bool}) => `I tptp_bool_type
   2.103               | (true, @{type_name fun}) => `I tptp_fun_type
   2.104               | _ => if s = homo_infinite_type_name andalso
   2.105 @@ -733,7 +742,7 @@
   2.106    else
   2.107      simple_type_prefix ^ ascii_of s
   2.108  
   2.109 -fun ho_type_from_fo_term format type_sys pred_sym ary =
   2.110 +fun ho_type_from_fo_term type_sys pred_sym ary =
   2.111    let
   2.112      fun to_atype ty =
   2.113        AType ((make_simple_type (generic_mangled_type_name fst ty),
   2.114 @@ -743,10 +752,10 @@
   2.115        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   2.116      fun to_ho (ty as ATerm ((s, _), tys)) =
   2.117        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
   2.118 -  in if is_setting_higher_order format type_sys then to_ho else to_fo ary end
   2.119 +  in if is_type_sys_higher_order type_sys then to_ho else to_fo ary end
   2.120  
   2.121  fun mangled_type format type_sys pred_sym ary =
   2.122 -  ho_type_from_fo_term format type_sys pred_sym ary
   2.123 +  ho_type_from_fo_term type_sys pred_sym ary
   2.124    o fo_term_from_typ format type_sys
   2.125  
   2.126  fun mangled_const_name format type_sys T_args (s, s') =
   2.127 @@ -780,14 +789,14 @@
   2.128      (hd ss, map unmangled_type (tl ss))
   2.129    end
   2.130  
   2.131 -fun introduce_proxies format type_sys =
   2.132 +fun introduce_proxies type_sys =
   2.133    let
   2.134      fun intro top_level (CombApp (tm1, tm2)) =
   2.135          CombApp (intro top_level tm1, intro false tm2)
   2.136        | intro top_level (CombConst (name as (s, _), T, T_args)) =
   2.137          (case proxify_const s of
   2.138             SOME proxy_base =>
   2.139 -           if top_level orelse is_setting_higher_order format type_sys then
   2.140 +           if top_level orelse is_type_sys_higher_order type_sys then
   2.141               case (top_level, s) of
   2.142                 (_, "c_False") => (`I tptp_false, [])
   2.143               | (_, "c_True") => (`I tptp_true, [])
   2.144 @@ -806,11 +815,11 @@
   2.145        | intro _ tm = tm
   2.146    in intro true end
   2.147  
   2.148 -fun combformula_from_prop thy format type_sys eq_as_iff =
   2.149 +fun combformula_from_prop thy type_sys eq_as_iff =
   2.150    let
   2.151      fun do_term bs t atomic_types =
   2.152        combterm_from_term thy bs (Envir.eta_contract t)
   2.153 -      |>> (introduce_proxies format type_sys #> AAtom)
   2.154 +      |>> (introduce_proxies type_sys #> AAtom)
   2.155        ||> union (op =) atomic_types
   2.156      fun do_quant bs q s T t' =
   2.157        let val s = singleton (Name.variant_list (map fst bs)) s in
   2.158 @@ -931,10 +940,10 @@
   2.159    end
   2.160  
   2.161  (* making fact and conjecture formulas *)
   2.162 -fun make_formula thy format type_sys eq_as_iff name loc kind t =
   2.163 +fun make_formula thy type_sys eq_as_iff name loc kind t =
   2.164    let
   2.165      val (combformula, atomic_types) =
   2.166 -      combformula_from_prop thy format type_sys eq_as_iff t []
   2.167 +      combformula_from_prop thy type_sys eq_as_iff t []
   2.168    in
   2.169      {name = name, locality = loc, kind = kind, combformula = combformula,
   2.170       atomic_types = atomic_types}
   2.171 @@ -944,8 +953,8 @@
   2.172                ((name, loc), t) =
   2.173    let val thy = Proof_Context.theory_of ctxt in
   2.174      case t |> preproc ? preprocess_prop ctxt presimp_consts Axiom
   2.175 -           |> make_formula thy format type_sys (eq_as_iff andalso format <> CNF)
   2.176 -                           name loc Axiom of
   2.177 +           |> make_formula thy type_sys (eq_as_iff andalso format <> CNF) name
   2.178 +                           loc Axiom of
   2.179        formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
   2.180        if s = tptp_true then NONE else SOME formula
   2.181      | formula => SOME formula
   2.182 @@ -968,8 +977,8 @@
   2.183                in
   2.184                  t |> preproc ?
   2.185                       (preprocess_prop ctxt presimp_consts kind #> freeze_term)
   2.186 -                  |> make_formula thy format type_sys (format <> CNF)
   2.187 -                                  (string_of_int j) Local kind
   2.188 +                  |> make_formula thy type_sys (format <> CNF) (string_of_int j)
   2.189 +                                  Local kind
   2.190                    |> maybe_negate
   2.191                end)
   2.192           (0 upto last) ts
   2.193 @@ -1249,7 +1258,7 @@
   2.194    in aux 0 end
   2.195  
   2.196  fun repair_combterm ctxt format type_sys sym_tab =
   2.197 -  not (is_setting_higher_order format type_sys)
   2.198 +  not (is_type_sys_higher_order type_sys)
   2.199    ? (introduce_explicit_apps_in_combterm sym_tab
   2.200       #> introduce_predicators_in_combterm sym_tab)
   2.201    #> enforce_type_arg_policy_in_combterm ctxt format type_sys
   2.202 @@ -1477,7 +1486,7 @@
   2.203        term_from_combterm ctxt format nonmono_Ts type_sys (Top_Level pos)
   2.204      val do_bound_type =
   2.205        case type_sys of
   2.206 -        Simple_Types level =>
   2.207 +        Simple_Types (_, level) =>
   2.208          homogenized_type ctxt nonmono_Ts level 0
   2.209          #> mangled_type format type_sys false 0 #> SOME
   2.210        | _ => K NONE
   2.211 @@ -1649,7 +1658,7 @@
   2.212    let
   2.213      val (T_arg_Ts, level) =
   2.214        case type_sys of
   2.215 -        Simple_Types level => ([], level)
   2.216 +        Simple_Types (_, level) => ([], level)
   2.217        | _ => (replicate (length T_args) homo_infinite_type, No_Types)
   2.218    in
   2.219      Decl (sym_decl_prefix ^ s, (s, s'),