# HG changeset patch
# User wenzelm
# Date 1304292028 -7200
# Node ID 20a99a0e65edc06098cd94cd06da53aff61f30b0
# Parent  13c7194a896a48369b9e85a7903a0f86b5350599# Parent  6c621a9d612a028c19dffb375969d9d1e3c1bf7c
merged;

diff -r 6c621a9d612a -r 20a99a0e65ed src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon May 02 01:20:28 2011 +0200
@@ -250,15 +250,15 @@
      >> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
 
 (* Generalized first-order terms, which include file names, numbers, etc. *)
-fun parse_annotation strict x =
+fun parse_annotation x =
   ((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
-      >> (strict ? filter (is_some o Int.fromString)))
-   -- Scan.optional (parse_annotation strict) [] >> op @
-   || $$ "(" |-- parse_annotations strict --| $$ ")"
-   || $$ "[" |-- parse_annotations strict --| $$ "]") x
-and parse_annotations strict x =
-  (Scan.optional (parse_annotation strict
-                  ::: Scan.repeat ($$ "," |-- parse_annotation strict)) []
+      >> filter (is_some o Int.fromString))
+   -- Scan.optional parse_annotation [] >> op @
+   || $$ "(" |-- parse_annotations --| $$ ")"
+   || $$ "[" |-- parse_annotations --| $$ "]") x
+and parse_annotations x =
+  (Scan.optional (parse_annotation
+                  ::: Scan.repeat ($$ "," |-- parse_annotation)) []
    >> flat) x
 
 (* Vampire proof lines sometimes contain needless information such as "(0:3)",
@@ -295,7 +295,9 @@
        >> (fn ((q, ts), phi) =>
               (* FIXME: TFF *)
               AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
-    || $$ "~" |-- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) >> mk_anot
+    || (Scan.repeat ($$ "~") >> length)
+       -- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom)
+       >> (fn (n, phi) => phi |> n div 2 = 1 ? mk_anot)
     || parse_atom)
    -- Scan.option ((Scan.this_string "=>" >> K AImplies
                     || Scan.this_string "<=>" >> K AIff
@@ -307,8 +309,8 @@
         | (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
 
 val parse_tstp_extra_arguments =
-  Scan.optional ($$ "," |-- parse_annotation false
-                 --| Scan.option ($$ "," |-- parse_annotations false)) []
+  Scan.optional ($$ "," |-- parse_annotation
+                 --| Scan.option ($$ "," |-- parse_annotations)) []
 
 val vampire_unknown_fact = "unknown"
 val tofof_fact_prefix = "fof_"
@@ -355,7 +357,7 @@
   scan_general_id --| $$ "." -- parse_formula
     --| Scan.option parse_vampire_braced_stuff
     --| Scan.option parse_vampire_parenthesized_detritus
-    -- parse_annotation true
+    -- parse_annotation
   >> (fn ((num, phi), deps) =>
          Inference ((num, NONE), phi, map (rpair NONE) deps))
 
diff -r 6c621a9d612a -r 20a99a0e65ed src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Mon May 02 01:20:28 2011 +0200
@@ -13,10 +13,11 @@
   type type_system = Sledgehammer_ATP_Translate.type_system
   type minimize_command = string list -> string
   type metis_params =
-    string * type_system * minimize_command * string proof * int
+    string * minimize_command * string proof * int
     * (string * locality) list vector * thm * int
   type isar_params =
-    string Symtab.table * bool * int * Proof.context * int list list
+     Proof.context * bool * type_system * int * string Symtab.table
+     * int list list
   type text_result = string * (string * locality) list
 
   val repair_conjecture_shape_and_fact_names :
@@ -53,10 +54,11 @@
 
 type minimize_command = string list -> string
 type metis_params =
-  string * type_system * minimize_command * string proof * int
+  string * minimize_command * string proof * int
   * (string * locality) list vector * thm * int
 type isar_params =
-  string Symtab.table * bool * int * Proof.context * int list list
+   Proof.context * bool * type_system * int * string Symtab.table
+   * int list list
 type text_result = string * (string * locality) list
 
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
@@ -193,13 +195,10 @@
 fun using_labels [] = ""
   | using_labels ls =
     "using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name type_sys =
-  if is_type_sys_fairly_sound 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 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 minimize_line _ [] = ""
   | minimize_line minimize_command ss =
     case minimize_command ss of
@@ -212,17 +211,17 @@
   List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
-fun metis_proof_text (banner, type_sys, minimize_command, atp_proof,
-                      facts_offset, fact_names, goal, i) =
+fun metis_proof_text (banner, minimize_command, atp_proof, facts_offset,
+                      fact_names, goal, i) =
   let
-    val (chained_lemmas, other_lemmas) =
+    val (chained, extra) =
       atp_proof |> used_facts_in_atp_proof facts_offset fact_names
                 |> split_used_facts
     val n = Logic.count_prems (prop_of goal)
   in
-    (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)
+    (try_command_line banner (metis_command false i n ([], map fst extra)) ^
+     minimize_line minimize_command (map fst (extra @ chained)),
+     extra @ chained)
   end
 
 (** Hard-core proof reconstruction: structured Isar proofs **)
@@ -955,9 +954,9 @@
         (if n <> 1 then "next" else "qed")
   in do_proof end
 
-fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-        (metis_params as (_, type_sys, _, atp_proof, facts_offset, fact_names,
-                          goal, i)) =
+fun isar_proof_text (ctxt, debug, type_sys, isar_shrink_factor, pool,
+                     conjecture_shape)
+        (metis_params as (_, _, atp_proof, facts_offset, fact_names, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
@@ -973,7 +972,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt type_sys i n of
+           |> string_for_proof ctxt (is_type_sys_fairly_sound type_sys) i n of
         "" => "\nNo structured proof available (proof too short)."
       | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
     val isar_proof =
diff -r 6c621a9d612a -r 20a99a0e65ed src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Mon May 02 01:20:28 2011 +0200
@@ -779,6 +779,8 @@
           if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
   end
 
+fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
+
 fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
   let
     val (arg_Ts, res_T) = n_ary_strip_type ary T
@@ -787,7 +789,8 @@
     val bound_tms =
       bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
     val bound_Ts =
-      arg_Ts |> map (if n > 1 then SOME else K NONE)
+      arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
+                             else NONE)
   in
     Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
              CombConst ((s, s'), T, T_args)
@@ -807,11 +810,13 @@
       val decls =
         case decls of
           decl :: (decls' as _ :: _) =>
-          if forall (curry (op =) (result_type_of_decl decl)
-                     o result_type_of_decl) decls' then
-            [decl]
-          else
-            decls
+          let val T = result_type_of_decl decl in
+            if forall ((fn T' => Type.raw_instance (T', T))
+                       o result_type_of_decl) decls' then
+              [decl]
+            else
+              decls
+          end
         | _ => decls
       val n = length decls
       val decls =
diff -r 6c621a9d612a -r 20a99a0e65ed src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 01:20:28 2011 +0200
@@ -582,10 +582,11 @@
          "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
        else
          "")
-    val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+    val isar_params =
+      (ctxt, debug, type_sys, isar_shrink_factor, pool, conjecture_shape)
     val metis_params =
-      (proof_banner auto, type_sys, minimize_command, atp_proof, facts_offset,
-       fact_names, goal, subgoal)
+      (proof_banner auto, minimize_command, atp_proof, facts_offset, fact_names,
+       goal, subgoal)
     val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>