1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:07:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -11,13 +11,20 @@
     1.4    type 'a problem = 'a ATP_Problem.problem
     1.5    type translated_formula
     1.6  
     1.7 +  datatype type_system =
     1.8 +    Tags of bool |
     1.9 +    Preds of bool |
    1.10 +    Const_Args |
    1.11 +    Overload_Args |
    1.12 +    No_Types
    1.13 +
    1.14    val fact_prefix : string
    1.15    val conjecture_prefix : string
    1.16    val translate_atp_fact :
    1.17      Proof.context -> (string * 'a) * thm
    1.18      -> translated_formula option * ((string * 'a) * thm)
    1.19    val prepare_atp_problem :
    1.20 -    Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    1.21 +    Proof.context -> bool -> bool -> type_system -> bool -> term list -> term
    1.22      -> (translated_formula option * ((string * 'a) * thm)) list
    1.23      -> string problem * string Symtab.table * int * (string * 'a) list vector
    1.24  end;
    1.25 @@ -45,6 +52,17 @@
    1.26     combformula: (name, combterm) formula,
    1.27     ctypes_sorts: typ list}
    1.28  
    1.29 +datatype type_system =
    1.30 +  Tags of bool |
    1.31 +  Preds of bool |
    1.32 +  Const_Args |
    1.33 +  Overload_Args |
    1.34 +  No_Types
    1.35 +
    1.36 +fun is_fully_typed (Tags full_types) = full_types
    1.37 +  | is_fully_typed (Preds full_types) = full_types
    1.38 +  | is_fully_typed _ = false
    1.39 +
    1.40  fun mk_anot phi = AConn (ANot, [phi])
    1.41  fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    1.42  fun mk_ahorn [] phi = phi
    1.43 @@ -223,16 +241,16 @@
    1.44     (["c_COMBB"], @{thms Meson.COMBB_def}),
    1.45     (["c_COMBC"], @{thms Meson.COMBC_def}),
    1.46     (["c_COMBS"], @{thms Meson.COMBS_def})]
    1.47 -val optional_typed_helpers =
    1.48 +val optional_fully_typed_helpers =
    1.49    [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
    1.50     (["c_If"], @{thms if_True if_False})]
    1.51  val mandatory_helpers = @{thms Metis.fequal_def}
    1.52  
    1.53  val init_counters =
    1.54 -  [optional_helpers, optional_typed_helpers] |> maps (maps fst)
    1.55 +  [optional_helpers, optional_fully_typed_helpers] |> maps (maps fst)
    1.56    |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
    1.57  
    1.58 -fun get_helper_facts ctxt is_FO full_types conjectures facts =
    1.59 +fun get_helper_facts ctxt is_FO type_sys conjectures facts =
    1.60    let
    1.61      val ct =
    1.62        fold (fold count_translated_formula) [conjectures, facts] init_counters
    1.63 @@ -240,7 +258,7 @@
    1.64      fun baptize th = ((Thm.get_name_hint th, false), th)
    1.65    in
    1.66      (optional_helpers
    1.67 -     |> full_types ? append optional_typed_helpers
    1.68 +     |> is_fully_typed type_sys ? append optional_fully_typed_helpers
    1.69       |> maps (fn (ss, ths) =>
    1.70                   if exists is_needed ss then map baptize ths else [])) @
    1.71      (if is_FO then [] else map baptize mandatory_helpers)
    1.72 @@ -249,7 +267,7 @@
    1.73  
    1.74  fun translate_atp_fact ctxt = `(make_fact ctxt true)
    1.75  
    1.76 -fun translate_formulas ctxt full_types hyp_ts concl_t rich_facts =
    1.77 +fun translate_formulas ctxt type_sys hyp_ts concl_t rich_facts =
    1.78    let
    1.79      val thy = ProofContext.theory_of ctxt
    1.80      val fact_ts = map (prop_of o snd o snd) rich_facts
    1.81 @@ -268,7 +286,7 @@
    1.82      val tycons = type_consts_of_terms thy (goal_t :: fact_ts)
    1.83      (* TFrees in the conjecture; TVars in the facts *)
    1.84      val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
    1.85 -    val helper_facts = get_helper_facts ctxt is_FO full_types conjectures facts
    1.86 +    val helper_facts = get_helper_facts ctxt is_FO type_sys conjectures facts
    1.87      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    1.88      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    1.89    in
    1.90 @@ -290,7 +308,7 @@
    1.91  
    1.92  fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
    1.93  
    1.94 -fun fo_term_for_combterm full_types =
    1.95 +fun fo_term_for_combterm type_sys =
    1.96    let
    1.97      fun aux top_level u =
    1.98        let
    1.99 @@ -298,7 +316,7 @@
   1.100          val (x, ty_args) =
   1.101            case head of
   1.102              CombConst (name as (s, s'), _, ty_args) =>
   1.103 -            let val ty_args = if full_types then [] else ty_args in
   1.104 +            let val ty_args = if is_fully_typed type_sys then [] else ty_args in
   1.105                if s = "equal" then
   1.106                  if top_level andalso length args = 2 then (name, [])
   1.107                  else (("c_fequal", @{const_name Metis.fequal}), ty_args)
   1.108 @@ -315,25 +333,28 @@
   1.109          val t = ATerm (x, map fo_term_for_combtyp ty_args @
   1.110                            map (aux false) args)
   1.111      in
   1.112 -      if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   1.113 +      t |> (if type_sys = Tags true then
   1.114 +              wrap_type (fo_term_for_combtyp (combtyp_of u))
   1.115 +            else
   1.116 +              I)
   1.117      end
   1.118    in aux true end
   1.119  
   1.120 -fun formula_for_combformula full_types =
   1.121 +fun formula_for_combformula type_sys =
   1.122    let
   1.123      fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   1.124        | aux (AConn (c, phis)) = AConn (c, map aux phis)
   1.125 -      | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   1.126 +      | aux (AAtom tm) = AAtom (fo_term_for_combterm type_sys tm)
   1.127    in aux end
   1.128  
   1.129 -fun formula_for_fact full_types
   1.130 +fun formula_for_fact type_sys
   1.131                       ({combformula, ctypes_sorts, ...} : translated_formula) =
   1.132    mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   1.133                  (type_literals_for_types ctypes_sorts))
   1.134 -           (formula_for_combformula full_types combformula)
   1.135 +           (formula_for_combformula type_sys combformula)
   1.136  
   1.137 -fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   1.138 -  Fof (prefix ^ ascii_of name, kind, formula_for_fact full_types formula)
   1.139 +fun problem_line_for_fact prefix type_sys (formula as {name, kind, ...}) =
   1.140 +  Fof (prefix ^ ascii_of name, kind, formula_for_fact type_sys formula)
   1.141  
   1.142  fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   1.143                                                         superclass, ...}) =
   1.144 @@ -356,10 +377,10 @@
   1.145                  (formula_for_fo_literal
   1.146                       (fo_literal_for_arity_literal conclLit)))
   1.147  
   1.148 -fun problem_line_for_conjecture full_types
   1.149 +fun problem_line_for_conjecture type_sys
   1.150          ({name, kind, combformula, ...} : translated_formula) =
   1.151    Fof (conjecture_prefix ^ name, kind,
   1.152 -       formula_for_combformula full_types combformula)
   1.153 +       formula_for_combformula type_sys combformula)
   1.154  
   1.155  fun free_type_literals_for_conjecture
   1.156          ({ctypes_sorts, ...} : translated_formula) =
   1.157 @@ -401,12 +422,12 @@
   1.158    if explicit_apply then NONE
   1.159    else SOME (Symtab.empty |> consider_problem problem)
   1.160  
   1.161 -fun min_arity_of thy full_types NONE s =
   1.162 +fun min_arity_of thy type_sys NONE s =
   1.163      (if s = "equal" orelse s = type_wrapper_name orelse
   1.164          String.isPrefix type_const_prefix s orelse
   1.165          String.isPrefix class_prefix s then
   1.166         16383 (* large number *)
   1.167 -     else if full_types then
   1.168 +     else if is_fully_typed type_sys then
   1.169         0
   1.170       else case strip_prefix_and_unascii const_prefix s of
   1.171         SOME s' => num_type_args thy (invert_const s')
   1.172 @@ -429,7 +450,7 @@
   1.173        ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   1.174      end
   1.175  
   1.176 -fun repair_applications_in_term thy full_types const_tab =
   1.177 +fun repair_applications_in_term thy type_sys const_tab =
   1.178    let
   1.179      fun aux opt_ty (ATerm (name as (s, _), ts)) =
   1.180        if s = type_wrapper_name then
   1.181 @@ -439,7 +460,7 @@
   1.182        else
   1.183          let
   1.184            val ts = map (aux NONE) ts
   1.185 -          val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   1.186 +          val (ts1, ts2) = chop (min_arity_of thy type_sys const_tab s) ts
   1.187          in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   1.188    in aux NONE end
   1.189  
   1.190 @@ -481,37 +502,37 @@
   1.191      case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   1.192    end
   1.193  
   1.194 -fun repair_formula thy explicit_forall full_types const_tab =
   1.195 +fun repair_formula thy explicit_forall type_sys const_tab =
   1.196    let
   1.197      fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   1.198        | aux (AConn (c, phis)) = AConn (c, map aux phis)
   1.199        | aux (AAtom tm) =
   1.200 -        AAtom (tm |> repair_applications_in_term thy full_types const_tab
   1.201 +        AAtom (tm |> repair_applications_in_term thy type_sys const_tab
   1.202                    |> repair_predicates_in_term const_tab)
   1.203    in aux #> explicit_forall ? close_universally end
   1.204  
   1.205 -fun repair_problem_line thy explicit_forall full_types const_tab
   1.206 +fun repair_problem_line thy explicit_forall type_sys const_tab
   1.207                          (Fof (ident, kind, phi)) =
   1.208 -  Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   1.209 +  Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
   1.210  fun repair_problem_with_const_table thy =
   1.211    map o apsnd o map ooo repair_problem_line thy
   1.212  
   1.213 -fun repair_problem thy explicit_forall full_types explicit_apply problem =
   1.214 -  repair_problem_with_const_table thy explicit_forall full_types
   1.215 +fun repair_problem thy explicit_forall type_sys explicit_apply problem =
   1.216 +  repair_problem_with_const_table thy explicit_forall type_sys
   1.217        (const_table_for_problem explicit_apply problem) problem
   1.218  
   1.219 -fun prepare_atp_problem ctxt readable_names explicit_forall full_types
   1.220 +fun prepare_atp_problem ctxt readable_names explicit_forall type_sys
   1.221                          explicit_apply hyp_ts concl_t facts =
   1.222    let
   1.223      val thy = ProofContext.theory_of ctxt
   1.224      val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
   1.225                        arity_clauses)) =
   1.226 -      translate_formulas ctxt full_types hyp_ts concl_t facts
   1.227 -    val fact_lines = map (problem_line_for_fact fact_prefix full_types) facts
   1.228 +      translate_formulas ctxt type_sys hyp_ts concl_t facts
   1.229 +    val fact_lines = map (problem_line_for_fact fact_prefix type_sys) facts
   1.230      val helper_lines =
   1.231 -      map (problem_line_for_fact helper_prefix full_types) helper_facts
   1.232 +      map (problem_line_for_fact helper_prefix type_sys) helper_facts
   1.233      val conjecture_lines =
   1.234 -      map (problem_line_for_conjecture full_types) conjectures
   1.235 +      map (problem_line_for_conjecture type_sys) conjectures
   1.236      val tfree_lines = problem_lines_for_free_types conjectures
   1.237      val class_rel_lines =
   1.238        map problem_line_for_class_rel_clause class_rel_clauses
   1.239 @@ -525,7 +546,7 @@
   1.240         ("Helper facts", helper_lines),
   1.241         ("Conjectures", conjecture_lines),
   1.242         ("Type variables", tfree_lines)]
   1.243 -      |> repair_problem thy explicit_forall full_types explicit_apply
   1.244 +      |> repair_problem thy explicit_forall type_sys explicit_apply
   1.245      val (problem, pool) = nice_atp_problem readable_names problem
   1.246      val conjecture_offset =
   1.247        length fact_lines + length class_rel_lines + length arity_lines

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:07:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
     2.3 @@ -78,6 +78,7 @@
     2.4     ("debug", "false"),
     2.5     ("verbose", "false"),
     2.6     ("overlord", "false"),
     2.7 +   ("type_sys", "smart"),
     2.8     ("explicit_apply", "false"),
     2.9     ("relevance_thresholds", "0.45 0.85"),
    2.10     ("max_relevant", "smart"),
    2.11 @@ -98,7 +99,7 @@
    2.12     ("no_isar_proof", "isar_proof")]
    2.13  
    2.14  val params_for_minimize =
    2.15 -  ["debug", "verbose", "overlord", "full_types", "isar_proof",
    2.16 +  ["debug", "verbose", "overlord", "full_types", "type_sys", "isar_proof",
    2.17     "isar_shrink_factor", "timeout"]
    2.18  
    2.19  val property_dependent_params = ["provers", "full_types", "timeout"]
    2.20 @@ -221,6 +222,7 @@
    2.21      val provers = lookup_string "provers" |> space_explode " "
    2.22                    |> auto ? single o hd
    2.23      val full_types = lookup_bool "full_types"
    2.24 +    val type_sys = lookup_string "type_sys"
    2.25      val explicit_apply = lookup_bool "explicit_apply"
    2.26      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    2.27      val max_relevant = lookup_int_option "max_relevant"
    2.28 @@ -230,7 +232,7 @@
    2.29      val expect = lookup_string "expect"
    2.30    in
    2.31      {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
    2.32 -     provers = provers, full_types = full_types,
    2.33 +     provers = provers, full_types = full_types, type_sys = type_sys,
    2.34       explicit_apply = explicit_apply,
    2.35       relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    2.36       isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 15 11:07:13 2010 +0100
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Dec 15 11:26:28 2010 +0100
     3.3 @@ -48,14 +48,14 @@
     3.4  
     3.5  fun print silent f = if silent then () else Output.urgent_message (f ())
     3.6  
     3.7 -fun test_facts ({debug, overlord, provers, full_types, isar_proof,
     3.8 +fun test_facts ({debug, overlord, provers, full_types, type_sys, isar_proof,
     3.9                   isar_shrink_factor, ...} : params) silent (prover : prover)
    3.10                 explicit_apply timeout i n state facts =
    3.11    let
    3.12      val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
    3.13      val params =
    3.14        {blocking = true, debug = debug, verbose = false, overlord = overlord,
    3.15 -       provers = provers, full_types = full_types,
    3.16 +       provers = provers, full_types = full_types, type_sys = type_sys,
    3.17         explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
    3.18         max_relevant = NONE, isar_proof = isar_proof,
    3.19         isar_shrink_factor = isar_shrink_factor, timeout = timeout, expect = ""}

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:07:13 2010 +0100
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
     4.3 @@ -21,6 +21,7 @@
     4.4       overlord: bool,
     4.5       provers: string list,
     4.6       full_types: bool,
     4.7 +     type_sys: string,
     4.8       explicit_apply: bool,
     4.9       relevance_thresholds: real * real,
    4.10       max_relevant: int option,
    4.11 @@ -204,6 +205,7 @@
    4.12     overlord: bool,
    4.13     provers: string list,
    4.14     full_types: bool,
    4.15 +   type_sys: string,
    4.16     explicit_apply: bool,
    4.17     relevance_thresholds: real * real,
    4.18     max_relevant: int option,
    4.19 @@ -269,11 +271,21 @@
    4.20  fun run_atp auto atp_name
    4.21          ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
    4.22           known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
    4.23 -        ({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
    4.24 -          isar_shrink_factor, timeout, ...} : params)
    4.25 +        ({debug, verbose, overlord, full_types, type_sys, explicit_apply,
    4.26 +          isar_proof, isar_shrink_factor, timeout, ...} : params)
    4.27          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    4.28    let
    4.29      val ctxt = Proof.context_of state
    4.30 +    val type_sys =
    4.31 +      case (type_sys, full_types) of
    4.32 +        ("tags", _) => Tags full_types
    4.33 +      | ("preds", _) => Preds full_types
    4.34 +      | ("const_args", _) => Const_Args
    4.35 +      | ("overload_args", _) => Overload_Args
    4.36 +      | ("none", _) => No_Types
    4.37 +      | _ => (if type_sys = "smart" then ()
    4.38 +              else warning ("Unknown type system: " ^ quote type_sys ^ ".");
    4.39 +              if full_types then Tags true else Const_Args)
    4.40      val (_, hyp_ts, concl_t) = strip_subgoal goal subgoal
    4.41      val facts = facts |> map (atp_translated_fact ctxt)
    4.42      val dest_dir = if overlord then getenv "ISABELLE_HOME_USER"
    4.43 @@ -335,7 +347,7 @@
    4.44                in (output, msecs, tstplike_proof, outcome) end
    4.45              val readable_names = debug andalso overlord
    4.46              val (atp_problem, pool, conjecture_offset, fact_names) =
    4.47 -              prepare_atp_problem ctxt readable_names explicit_forall full_types
    4.48 +              prepare_atp_problem ctxt readable_names explicit_forall type_sys
    4.49                                    explicit_apply hyp_ts concl_t facts
    4.50              val ss = tptp_strings_for_atp_problem use_conjecture_for_hypotheses
    4.51                                                    atp_problem