implemented new type system encoding "overload_args", which is more lightweight than "const_args" (the unsound default) and hopefully almost as sound

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -9,10 +9,11 @@
 signature SLEDGEHAMMER_ATP_RECONSTRUCT =
 sig
   type locality = Sledgehammer_Filter.locality
+  type type_system = Sledgehammer_ATP_Translate.type_system
   type minimize_command = string list -> string
   type metis_params =
-    string * bool * minimize_command * string * (string * locality) list vector
-    * thm * int
+    string * type_system * minimize_command * string
+    * (string * locality) list vector * thm * int
   type isar_params =
     string Symtab.table * bool * int * Proof.context * int list list
   type text_result = string * (string * locality) list
@@ -43,8 +44,8 @@
 
 type minimize_command = string list -> string
 type metis_params =
-  string * bool * minimize_command * string * (string * locality) list vector
-  * thm * int
+  string * type_system * minimize_command * string
+  * (string * locality) list vector * thm * int
 type isar_params =
   string Symtab.table * bool * int * Proof.context * int list list
 type text_result = string * (string * locality) list
@@ -125,12 +126,12 @@
 fun using_labels [] = ""
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name full_types = if full_types then "metisFT" else "metis"
-fun metis_call full_types ss = command_call (metis_name full_types) ss
-fun metis_command full_types i n (ls, ss) =
-  using_labels ls ^ apply_on_subgoal i n ^ metis_call full_types ss
-fun metis_line banner full_types i n ss =
-  try_command_line banner (metis_command full_types i n ([], ss))
+fun metis_name type_sys = if is_fully_typed type_sys then "metisFT" else "metis"
+fun metis_call type_sys ss = command_call (metis_name type_sys) ss
+fun metis_command type_sys i n (ls, ss) =
+  using_labels ls ^ apply_on_subgoal i n ^ metis_call type_sys ss
+fun metis_line banner type_sys i n ss =
+  try_command_line banner (metis_command type_sys i n ([], ss))
 fun minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
@@ -165,14 +166,14 @@
   List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
-fun metis_proof_text (banner, full_types, minimize_command,
-                      tstplike_proof, fact_names, goal, i) =
+fun metis_proof_text (banner, type_sys, minimize_command, tstplike_proof,
+                      fact_names, goal, i) =
   let
     val (chained_lemmas, other_lemmas) =
       split_used_facts (used_facts_in_tstplike_proof fact_names tstplike_proof)
     val n = Logic.count_prems (prop_of goal)
   in
-    (metis_line banner full_types i n (map fst other_lemmas) ^
+    (metis_line banner type_sys i n (map fst other_lemmas) ^
      minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
      other_lemmas @ chained_lemmas)
   end
@@ -303,7 +304,7 @@
 
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
-fun raw_term_from_pred thy full_types tfrees =
+fun raw_term_from_pred thy type_sys tfrees =
   let
     fun aux opt_T extra_us u =
       case u of
@@ -327,25 +328,26 @@
         | SOME b =>
           let
             val c = invert_const b
-            val num_type_args = num_type_args thy c
-            val (type_us, term_us) =
-              chop (if full_types then 0 else num_type_args) us
+            val num_ty_args = num_atp_type_args thy type_sys c
+            val (type_us, term_us) = chop num_ty_args us
             (* Extra args from "hAPP" come after any arguments given directly to
                the constant. *)
             val term_ts = map (aux NONE []) term_us
             val extra_ts = map (aux NONE []) extra_us
             val t =
-              Const (c, if full_types then
+              Const (c, if is_fully_typed type_sys then
                           case opt_T of
                             SOME T => map fastype_of term_ts ---> T
                           | NONE =>
-                            if num_type_args = 0 then
+                            if num_type_args thy c = 0 then
                               Sign.const_instance thy (c, [])
                             else
                               raise Fail ("no type information for " ^ quote c)
-                        else
+                        else if num_type_args thy c = length type_us then
                           Sign.const_instance thy (c,
-                              map (type_from_fo_term tfrees) type_us))
+                              map (type_from_fo_term tfrees) type_us)
+                        else
+                          HOLogic.typeT)
           in list_comb (t, term_ts @ extra_ts) end
         | NONE => (* a free or schematic variable *)
           let
@@ -366,12 +368,12 @@
           in list_comb (t, ts) end
   in aux (SOME HOLogic.boolT) [] end
 
-fun term_from_pred thy full_types tfrees pos (u as ATerm (s, _)) =
+fun term_from_pred thy type_sys tfrees pos (u as ATerm (s, _)) =
   if String.isPrefix class_prefix s then
     add_type_constraint (type_constraint_from_term pos tfrees u)
     #> pair @{const True}
   else
-    pair (raw_term_from_pred thy full_types tfrees u)
+    pair (raw_term_from_pred thy type_sys tfrees u)
 
 val combinator_table =
   [(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def_raw}),
@@ -412,7 +414,7 @@
 
 (* Interpret an ATP formula as a HOL term, extracting sort constraints as they
    appear in the formula. *)
-fun prop_from_formula thy full_types tfrees phi =
+fun prop_from_formula thy type_sys tfrees phi =
   let
     fun do_formula pos phi =
       case phi of
@@ -435,7 +437,7 @@
              | AIff => s_iff
              | ANotIff => s_not o s_iff
              | _ => raise Fail "unexpected connective")
-      | AAtom tm => term_from_pred thy full_types tfrees pos tm
+      | AAtom tm => term_from_pred thy type_sys tfrees pos tm
       | _ => raise FORMULA [phi]
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
 
@@ -449,14 +451,14 @@
 fun unvarify_term (Var ((s, 0), T)) = Free (s, T)
   | unvarify_term t = raise TERM ("unvarify_term: non-Var", [t])
 
-fun decode_line full_types tfrees (Definition (name, phi1, phi2)) ctxt =
+fun decode_line type_sys tfrees (Definition (name, phi1, phi2)) ctxt =
     let
       val thy = ProofContext.theory_of ctxt
-      val t1 = prop_from_formula thy full_types tfrees phi1
+      val t1 = prop_from_formula thy type_sys tfrees phi1
       val vars = snd (strip_comb t1)
       val frees = map unvarify_term vars
       val unvarify_args = subst_atomic (vars ~~ frees)
-      val t2 = prop_from_formula thy full_types tfrees phi2
+      val t2 = prop_from_formula thy type_sys tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
         |> unvarify_args |> uncombine_term |> check_formula ctxt
@@ -465,17 +467,17 @@
       (Definition (name, t1, t2),
        fold Variable.declare_term (maps OldTerm.term_frees [t1, t2]) ctxt)
     end
-  | decode_line full_types tfrees (Inference (name, u, deps)) ctxt =
+  | decode_line type_sys tfrees (Inference (name, u, deps)) ctxt =
     let
       val thy = ProofContext.theory_of ctxt
-      val t = u |> prop_from_formula thy full_types tfrees
+      val t = u |> prop_from_formula thy type_sys tfrees
                 |> uncombine_term |> check_formula ctxt
     in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)
     end
-fun decode_lines ctxt full_types tfrees lines =
-  fst (fold_map (decode_line full_types tfrees) lines ctxt)
+fun decode_lines ctxt type_sys tfrees lines =
+  fst (fold_map (decode_line type_sys tfrees) lines ctxt)
 
 fun is_same_inference _ (Definition _) = false
   | is_same_inference t (Inference (_, t', _)) = t aconv t'
@@ -605,16 +607,15 @@
     else
       s
 
-fun isar_proof_from_tstplike_proof pool ctxt full_types tfrees
-        isar_shrink_factor tstplike_proof conjecture_shape fact_names params
-        frees =
+fun isar_proof_from_tstplike_proof pool ctxt type_sys tfrees isar_shrink_factor
+        tstplike_proof conjecture_shape fact_names params frees =
   let
     val lines =
       tstplike_proof
       |> atp_proof_from_tstplike_string
       |> nasty_atp_proof pool
       |> map_term_names_in_atp_proof repair_name
-      |> decode_lines ctxt full_types tfrees
+      |> decode_lines ctxt type_sys tfrees
       |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
       |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
@@ -857,7 +858,7 @@
         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt0 full_types i n =
+fun string_for_proof ctxt0 type_sys i n =
   let
     val ctxt = ctxt0
       |> Config.put show_free_types false
@@ -879,7 +880,7 @@
          if member (op =) qs Show then "show" else "have")
     val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
     fun do_facts (ls, ss) =
-      metis_command full_types 1 1
+      metis_command type_sys 1 1
                     (ls |> sort_distinct (prod_ord string_ord int_ord),
                      ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
@@ -914,7 +915,7 @@
   in do_proof end
 
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-                    (metis_params as (_, full_types, _, tstplike_proof,
+                    (metis_params as (_, type_sys, _, tstplike_proof,
                                       fact_names, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
@@ -923,7 +924,7 @@
     val n = Logic.count_prems (prop_of goal)
     val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
-      case isar_proof_from_tstplike_proof pool ctxt full_types tfrees
+      case isar_proof_from_tstplike_proof pool ctxt type_sys tfrees
                isar_shrink_factor tstplike_proof conjecture_shape fact_names
                params frees
            |> redirect_proof hyp_ts concl_t
@@ -931,7 +932,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt full_types i n of
+           |> string_for_proof ctxt type_sys i n of
         "" => "\nNo structured proof available."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -20,6 +20,8 @@
 
   val fact_prefix : string
   val conjecture_prefix : string
+  val is_fully_typed : type_system -> bool
+  val num_atp_type_args : theory -> type_system -> string -> int
   val translate_atp_fact :
     Proof.context -> (string * 'a) * thm
     -> translated_formula option * ((string * 'a) * thm)
@@ -63,6 +65,24 @@
   | is_fully_typed (Preds full_types) = full_types
   | is_fully_typed _ = false
 
+(* This is an approximation. If it returns "true" for a constant that isn't
+   overloaded (i.e., that has one uniform definition), needless clutter is
+   generated; if it returns "false" for an overloaded constant, the ATP gets a
+   license to do unsound reasoning if the type system is "overloaded_args". *)
+fun is_overloaded thy s =
+  length (Defs.specifications_of (Theory.defs_of thy) s) > 1
+
+fun needs_type_args thy type_sys s =
+  case type_sys of
+    Tags full_types => not full_types
+  | Preds full_types => not full_types
+  | Const_Args => true
+  | Overload_Args => is_overloaded thy s
+  | No_Types => false
+
+fun num_atp_type_args thy type_sys s =
+  if needs_type_args thy type_sys s then num_type_args thy s else 0
+
 fun mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
 fun mk_ahorn [] phi = phi
@@ -308,7 +328,7 @@
 
 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
 
-fun fo_term_for_combterm type_sys =
+fun fo_term_for_combterm thy type_sys =
   let
     fun aux top_level u =
       let
@@ -316,18 +336,27 @@
         val (x, ty_args) =
           case head of
             CombConst (name as (s, s'), _, ty_args) =>
-            let val ty_args = if is_fully_typed type_sys then [] else ty_args in
-              if s = "equal" then
-                if top_level andalso length args = 2 then (name, [])
-                else (("c_fequal", @{const_name Metis.fequal}), ty_args)
-              else if top_level then
-                case s of
-                  "c_False" => (("$false", s'), [])
-                | "c_True" => (("$true", s'), [])
-                | _ => (name, ty_args)
-              else
-                (name, ty_args)
-            end
+            (case strip_prefix_and_unascii const_prefix s of
+               NONE =>
+               if s = "equal" then
+                 if top_level andalso length args = 2 then (name, [])
+                 else (("c_fequal", @{const_name Metis.fequal}), ty_args)
+               else
+                 (name, ty_args)
+             | SOME s'' =>
+               let
+                 val s'' = invert_const s''
+                 val ty_args =
+                   if needs_type_args thy type_sys s'' then ty_args else []
+                in
+                  if top_level then
+                    case s of
+                      "c_False" => (("$false", s'), [])
+                    | "c_True" => (("$true", s'), [])
+                    | _ => (name, ty_args)
+                  else
+                    (name, ty_args)
+                end)
           | CombVar (name, _) => (name, [])
           | CombApp _ => raise Fail "impossible \"CombApp\""
         val t = ATerm (x, map fo_term_for_combtyp ty_args @
@@ -340,21 +369,21 @@
     end
   in aux true end
 
-fun formula_for_combformula type_sys =
+fun formula_for_combformula thy type_sys =
   let
     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
       | aux (AConn (c, phis)) = AConn (c, map aux phis)
-      | aux (AAtom tm) = AAtom (fo_term_for_combterm type_sys tm)
+      | aux (AAtom tm) = AAtom (fo_term_for_combterm thy type_sys tm)
   in aux end
 
-fun formula_for_fact type_sys
+fun formula_for_fact thy type_sys
                      ({combformula, ctypes_sorts, ...} : translated_formula) =
   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
                 (type_literals_for_types ctypes_sorts))
-           (formula_for_combformula type_sys combformula)
+           (formula_for_combformula thy type_sys combformula)
 
-fun problem_line_for_fact prefix type_sys (formula as {name, kind, ...}) =
-  Fof (prefix ^ ascii_of name, kind, formula_for_fact type_sys formula)
+fun problem_line_for_fact thy prefix type_sys (formula as {name, kind, ...}) =
+  Fof (prefix ^ ascii_of name, kind, formula_for_fact thy type_sys formula)
 
 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
@@ -377,10 +406,10 @@
                 (formula_for_fo_literal
                      (fo_literal_for_arity_literal conclLit)))
 
-fun problem_line_for_conjecture type_sys
+fun problem_line_for_conjecture thy type_sys
         ({name, kind, combformula, ...} : translated_formula) =
   Fof (conjecture_prefix ^ name, kind,
-       formula_for_combformula type_sys combformula)
+       formula_for_combformula thy type_sys combformula)
 
 fun free_type_literals_for_conjecture
         ({ctypes_sorts, ...} : translated_formula) =
@@ -427,10 +456,8 @@
         String.isPrefix type_const_prefix s orelse
         String.isPrefix class_prefix s then
        16383 (* large number *)
-     else if is_fully_typed type_sys then
-       0
      else case strip_prefix_and_unascii const_prefix s of
-       SOME s' => num_type_args thy (invert_const s')
+       SOME s' => num_atp_type_args thy type_sys (invert_const s')
      | NONE => 0)
   | min_arity_of _ _ (SOME the_const_tab) s =
     case Symtab.lookup the_const_tab s of
@@ -528,11 +555,11 @@
     val (fact_names, (conjectures, facts, helper_facts, class_rel_clauses,
                       arity_clauses)) =
       translate_formulas ctxt type_sys hyp_ts concl_t facts
-    val fact_lines = map (problem_line_for_fact fact_prefix type_sys) facts
+    val fact_lines = map (problem_line_for_fact thy fact_prefix type_sys) facts
     val helper_lines =
-      map (problem_line_for_fact helper_prefix type_sys) helper_facts
+      map (problem_line_for_fact thy helper_prefix type_sys) helper_facts
     val conjecture_lines =
-      map (problem_line_for_conjecture type_sys) conjectures
+      map (problem_line_for_conjecture thy type_sys) conjectures
     val tfree_lines = problem_lines_for_free_types conjectures
     val class_rel_lines =
       map problem_line_for_class_rel_clause class_rel_clauses

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -99,7 +99,7 @@
    ("no_isar_proof", "isar_proof")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "full_types", "type_sys", "isar_proof",
+  ["debug", "verbose", "overlord", "type_sys", "full_types", "isar_proof",
    "isar_shrink_factor", "timeout"]
 
 val property_dependent_params = ["provers", "full_types", "timeout"]
@@ -221,8 +221,8 @@
     val overlord = lookup_bool "overlord"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
+    val type_sys = lookup_string "type_sys"
     val full_types = lookup_bool "full_types"
-    val type_sys = lookup_string "type_sys"
     val explicit_apply = lookup_bool "explicit_apply"
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
@@ -232,7 +232,7 @@
     val expect = lookup_string "expect"
   in
     {blocking = blocking, debug = debug, verbose = verbose, overlord = overlord,
-     provers = provers, full_types = full_types, type_sys = type_sys,
+     provers = provers, type_sys = type_sys, full_types = full_types,
      explicit_apply = explicit_apply,
      relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
      isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -20,8 +20,8 @@
      verbose: bool,
      overlord: bool,
      provers: string list,
+     type_sys: string,
      full_types: bool,
-     type_sys: string,
      explicit_apply: bool,
      relevance_thresholds: real * real,
      max_relevant: int option,
@@ -204,8 +204,8 @@
    verbose: bool,
    overlord: bool,
    provers: string list,
+   type_sys: string,
    full_types: bool,
-   type_sys: string,
    explicit_apply: bool,
    relevance_thresholds: real * real,
    max_relevant: int option,
@@ -271,7 +271,7 @@
 fun run_atp auto atp_name
         ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
          known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
-        ({debug, verbose, overlord, full_types, type_sys, explicit_apply,
+        ({debug, verbose, overlord, type_sys, full_types, explicit_apply,
           isar_proof, isar_shrink_factor, timeout, ...} : params)
         minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
   let
@@ -398,7 +398,7 @@
         NONE =>
         proof_text isar_proof
             (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-            (proof_banner auto, full_types, minimize_command, tstplike_proof,
+            (proof_banner auto, type_sys, minimize_command, tstplike_proof,
              fact_names, goal, subgoal)
         |>> (fn message =>
                 message ^