# HG changeset patch
# User blanchet
# Date 1305888479 -7200
# Node ID dbdfe2d5b6ab6c2c6c1d453fe994ddef96377eec
# Parent  221af561ebf9c23cab531a537ada5bec90f30ccb
automatically use "metisFT" when typed helpers are necessary

diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 20 12:47:59 2011 +0200
@@ -14,7 +14,7 @@
   type minimize_command = string list -> string
   type metis_params =
     string * minimize_command * type_system * string proof * int
-    * (string * locality) list vector * thm * int
+    * (string * locality) list vector * int list * thm * int
   type isar_params =
     Proof.context * bool * int * string Symtab.table * int list list
     * int Symtab.table
@@ -22,8 +22,8 @@
 
   val repair_conjecture_shape_and_fact_names :
     type_system -> string -> int list list -> int
-    -> (string * locality) list vector
-    -> int list list * int * (string * locality) list vector
+    -> (string * locality) list vector -> int list
+    -> int list list * int * (string * locality) list vector * int list
   val used_facts_in_atp_proof :
     type_system -> int -> (string * locality) list vector -> string proof
     -> (string * locality) list
@@ -55,7 +55,7 @@
 type minimize_command = string list -> string
 type metis_params =
   string * minimize_command * type_system * string proof * int
-  * (string * locality) list vector * thm * int
+  * (string * locality) list vector * int list * thm * int
 type isar_params =
   Proof.context * bool * int * string Symtab.table * int list list
   * int Symtab.table
@@ -64,6 +64,9 @@
 fun is_head_digit s = Char.isDigit (String.sub (s, 0))
 val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
 
+val is_typed_helper_name =
+  String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix
+
 fun find_first_in_list_vector vec key =
   Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
                  | (_, value) => value) NONE vec
@@ -102,7 +105,7 @@
   ? (space_implode "_" o tl o space_explode "_")
 
 fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
-                                           fact_offset fact_names =
+        fact_offset fact_names typed_helpers =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
       val j0 = hd (hd conjecture_shape)
@@ -122,13 +125,17 @@
                             error ("No such fact: " ^ quote name ^ "."))
     in
       (conjecture_shape |> map (maps renumber_conjecture), 0,
-       seq |> map names_for_number |> Vector.fromList)
+       seq |> map names_for_number |> Vector.fromList,
+       name_map |> filter (forall is_typed_helper_name o snd) |> map fst)
     end
   else
-    (conjecture_shape, fact_offset, fact_names)
+    (conjecture_shape, fact_offset, fact_names, typed_helpers)
 
 val vampire_step_prefix = "f" (* grrr... *)
 
+val extract_step_number =
+  Int.fromString o perhaps (try (unprefix vampire_step_prefix))
+
 fun resolve_fact type_sys _ fact_names (_, SOME s) =
     (case try (unprefix fact_prefix) s of
        SOME s' =>
@@ -139,15 +146,18 @@
        end
      | NONE => [])
   | resolve_fact _ facts_offset fact_names (num, NONE) =
-    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
-      SOME j =>
-      let val j = j - facts_offset in
-        if j > 0 andalso j <= Vector.length fact_names then
-          Vector.sub (fact_names, j - 1)
-        else
-          []
-      end
-    | NONE => []
+    (case extract_step_number num of
+       SOME j =>
+       let val j = j - facts_offset in
+         if j > 0 andalso j <= Vector.length fact_names then
+           Vector.sub (fact_names, j - 1)
+         else
+           []
+       end
+     | NONE => [])
+
+fun is_fact type_sys conjecture_shape =
+  not o null o resolve_fact type_sys 0 conjecture_shape
 
 fun resolve_conjecture _ (_, SOME s) =
     (case try (unprefix conjecture_prefix) s of
@@ -157,18 +167,21 @@
         | NONE => [])
      | NONE => [])
   | resolve_conjecture conjecture_shape (num, NONE) =
-    case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
-      SOME i =>
-      (case find_index (exists (curry (op =) i)) conjecture_shape of
-         ~1 => []
-       | j => [j])
+    case extract_step_number num of
+      SOME i => (case find_index (exists (curry (op =) i)) conjecture_shape of
+                   ~1 => []
+                 | j => [j])
     | NONE => []
 
-fun is_fact type_sys conjecture_shape =
-  not o null o resolve_fact type_sys 0 conjecture_shape
 fun is_conjecture conjecture_shape =
   not o null o resolve_conjecture conjecture_shape
 
+fun is_typed_helper _ (_, SOME s) = is_typed_helper_name s
+  | is_typed_helper typed_helpers (num, NONE) =
+    (case extract_step_number num of
+       SOME i => member (op =) typed_helpers i
+     | NONE => false)
+
 fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
     append (resolve_fact type_sys facts_offset fact_names name)
   | add_fact _ _ _ _ = I
@@ -227,15 +240,21 @@
   List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
+fun uses_typed_helpers typed_helpers =
+  exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
+           | _ => false)
+
 fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
-                      facts_offset, fact_names, goal, i) =
+                      facts_offset, fact_names, typed_helpers, goal, i) =
   let
     val (chained, extra) =
       atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
                 |> split_used_facts
+    val full_types = uses_typed_helpers typed_helpers atp_proof
     val n = Logic.count_prems (prop_of goal)
+    val metis = metis_command full_types i n ([], map fst extra)
   in
-    (try_command_line banner (metis_command false i n ([], map fst extra)) ^
+    (try_command_line banner metis ^
      minimize_line minimize_command (map fst (extra @ chained)),
      extra @ chained)
   end
@@ -919,7 +938,7 @@
         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
-fun string_for_proof ctxt0 i n =
+fun string_for_proof ctxt0 full_types i n =
   let
     val ctxt =
       ctxt0 |> Config.put show_free_types false
@@ -942,7 +961,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 false 1 1
+      metis_command full_types 1 1
                     (ls |> sort_distinct (prod_ord string_ord int_ord),
                      ss |> sort_distinct string_ord)
     and do_step ind (Fix xs) =
@@ -979,11 +998,12 @@
 fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape,
                      sym_tab)
                     (metis_params as (_, _, type_sys, atp_proof, facts_offset,
-                                      fact_names, goal, i)) =
+                                      fact_names, typed_helpers, goal, i)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal i
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
+    val full_types = uses_typed_helpers typed_helpers atp_proof
     val n = Logic.count_prems (prop_of goal)
     val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
@@ -995,7 +1015,7 @@
            |> then_chain_proof
            |> kill_useless_labels_in_proof
            |> relabel_proof
-           |> string_for_proof ctxt i n of
+           |> string_for_proof ctxt full_types 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 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri May 20 12:47:59 2011 +0200
@@ -28,6 +28,8 @@
   val readable_names : bool Config.T
   val fact_prefix : string
   val conjecture_prefix : string
+  val helper_prefix : string
+  val typed_helper_suffix : string
   val predicator_base : string
   val explicit_app_base : string
   val type_pred_base : string
@@ -46,7 +48,7 @@
     -> term list -> term
     -> (translated_formula option * ((string * 'a) * thm)) list
     -> string problem * string Symtab.table * int * int
-       * (string * 'a) list vector * int Symtab.table
+       * (string * 'a) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
 end;
 
@@ -87,6 +89,9 @@
 val arity_clause_prefix = "arity_"
 val tfree_prefix = "tfree_"
 
+val typed_helper_suffix = "_T"
+val untyped_helper_suffix = "_U"
+
 val predicator_base = "hBOOL"
 val explicit_app_base = "hAPP"
 val type_pred_base = "is"
@@ -487,7 +492,7 @@
                     if prem_kind = Conjecture then update_combformula mk_anot
                     else I)
               in
-                make_formula ctxt true true (string_of_int j) Chained kind t
+                make_formula ctxt true true (string_of_int j) General kind t
                 |> maybe_negate
               end)
          (0 upto last) ts
@@ -734,8 +739,10 @@
       val thy = Proof_Context.theory_of ctxt
       val unmangled_s = mangled_s |> unmangled_const_name
       fun dub_and_inst c needs_some_types (th, j) =
-        ((c ^ "_" ^ string_of_int j ^ (if needs_some_types then "T" else ""),
-          Chained),
+        ((c ^ "_" ^ string_of_int j ^
+          (if needs_some_types then typed_helper_suffix
+           else untyped_helper_suffix),
+          General),
          let val t = th |> prop_of in
            t |> ((case general_type_arg_policy type_sys of
                     Mangled_Type_Args _ => true
@@ -1203,6 +1210,10 @@
       (conjs, helpers @ facts)
       |> sym_decl_table_for_facts type_sys repaired_sym_tab
       |> problem_lines_for_sym_decl_table ctxt conj_sym_kind nonmono_Ts type_sys
+    val helper_lines =
+      map (formula_line_for_fact ctxt helper_prefix nonmono_Ts type_sys)
+          (0 upto length helpers - 1 ~~ helpers)
+      |> should_add_ti_ti_helper type_sys ? cons (ti_ti_helper_fact ())
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =
@@ -1211,11 +1222,7 @@
                     (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map formula_line_for_arity_clause arity_clauses),
-       (helpersN, map (formula_line_for_fact ctxt helper_prefix nonmono_Ts
-                                             type_sys)
-                      (0 upto length helpers - 1 ~~ helpers)
-                  |> should_add_ti_ti_helper type_sys
-                     ? cons (ti_ti_helper_fact ())),
+       (helpersN, helper_lines),
        (conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)
                     conjs),
        (free_typesN, formula_lines_for_free_types type_sys (facts @ conjs))]
@@ -1228,6 +1235,13 @@
           | _ => I)
     val (problem, pool) =
       problem |> nice_atp_problem (Config.get ctxt readable_names)
+    val helpers_offset = offset_of_heading_in_problem helpersN problem 0
+    val typed_helpers =
+      map_filter (fn (j, {name, ...}) =>
+                     if String.isSuffix typed_helper_suffix name then SOME j
+                     else NONE)
+                 ((helpers_offset + 1 upto helpers_offset + length helpers)
+                  ~~ helpers)
     fun add_sym_arity (s, {min_ary, ...} : sym_info) =
       if min_ary > 0 then
         case strip_prefix_and_unascii const_prefix s of
@@ -1241,6 +1255,7 @@
      offset_of_heading_in_problem conjsN problem 0,
      offset_of_heading_in_problem factsN problem 0,
      fact_names |> Vector.fromList,
+     typed_helpers,
      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
   end
 
diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 20 12:47:59 2011 +0200
@@ -534,7 +534,7 @@
                   else
                     ()
                 val (atp_problem, pool, conjecture_offset, facts_offset,
-                     fact_names, sym_tab) =
+                     fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt conj_sym_kind prem_kind type_sys
                                       explicit_apply hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
@@ -567,13 +567,14 @@
                   extract_tstplike_proof_and_outcome verbose complete res_code
                       proof_delims known_failures output
                   |>> atp_proof_from_tstplike_proof
-                val (conjecture_shape, facts_offset, fact_names) =
+                val (conjecture_shape, facts_offset, fact_names,
+                     typed_helpers) =
                   if is_none outcome then
                     repair_conjecture_shape_and_fact_names type_sys output
-                        conjecture_shape facts_offset fact_names
+                        conjecture_shape facts_offset fact_names typed_helpers
                   else
                     (* don't bother repairing *)
-                    (conjecture_shape, facts_offset, fact_names)
+                    (conjecture_shape, facts_offset, fact_names, typed_helpers)
                 val outcome =
                   case outcome of
                     NONE =>
@@ -587,7 +588,8 @@
                     else SOME IncompleteUnprovable
                   | _ => outcome
               in
-                ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+                ((pool, conjecture_shape, facts_offset, fact_names,
+                  typed_helpers, sym_tab),
                  (output, msecs, type_sys, atp_proof, outcome))
               end
             val timer = Timer.startRealTimer ()
@@ -607,7 +609,7 @@
                 end
               | maybe_run_slice _ _ result = result
             fun maybe_blacklist_facts_and_retry iter blacklist
-                    (result as ((_, _, facts_offset, fact_names, _),
+                    (result as ((_, _, facts_offset, fact_names, _, _),
                                 (_, _, type_sys, atp_proof,
                                  SOME (UnsoundProof (false, _))))) =
                 (case used_facts_in_atp_proof type_sys facts_offset fact_names
@@ -624,7 +626,7 @@
                      result)
               | maybe_blacklist_facts_and_retry _ _ result = result
           in
-            ((Symtab.empty, [], 0, Vector.fromList [], Symtab.empty),
+            ((Symtab.empty, [], 0, Vector.fromList [], [], Symtab.empty),
              ("", SOME 0, hd fallback_best_type_systems, [],
               SOME InternalError))
             |> fold (maybe_run_slice []) actual_slices
@@ -644,7 +646,8 @@
         ()
       else
         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
-    val ((pool, conjecture_shape, facts_offset, fact_names, sym_tab),
+    val ((pool, conjecture_shape, facts_offset, fact_names, typed_helpers,
+          sym_tab),
          (output, msecs, type_sys, atp_proof, outcome)) =
       with_path cleanup export run_on problem_path_name
     val important_message =
@@ -668,7 +671,7 @@
       (ctxt, debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
     val metis_params =
       (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
-       fact_names, goal, subgoal)
+       fact_names, typed_helpers, goal, subgoal)
     val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>
diff -r 221af561ebf9 -r dbdfe2d5b6ab src/HOL/ex/tptp_export.ML
--- a/src/HOL/ex/tptp_export.ML	Fri May 20 12:47:58 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Fri May 20 12:47:59 2011 +0200
@@ -103,7 +103,7 @@
            else Sledgehammer_ATP_Translate.Const_Arg_Types,
            Sledgehammer_ATP_Translate.Heavy)
     val explicit_apply = false
-    val (atp_problem, _, _, _, _, _) =
+    val (atp_problem, _, _, _, _, _, _) =
       Sledgehammer_ATP_Translate.prepare_atp_problem ctxt ATP_Problem.Axiom
           ATP_Problem.Axiom type_sys explicit_apply [] @{prop False} facts
     val infers =