# HG changeset patch
# User blanchet
# Date 1304377443 -7200
# Node ID 59142dbfa3baca326f4e1fd9fe467927c575a86e
# Parent  4781fcd53572d9f361a0f2ab1c16e3e091200b1a
no need to generate fact numbers for polymorphic type systems -- this confuses the TPTP exporter

diff -r 4781fcd53572 -r 59142dbfa3ba src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 03 00:10:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Tue May 03 01:04:03 2011 +0200
@@ -13,22 +13,22 @@
   type type_system = Sledgehammer_ATP_Translate.type_system
   type minimize_command = string list -> string
   type metis_params =
-    string * minimize_command * string proof * int
+    string * minimize_command * type_system * string proof * int
     * (string * locality) list vector * thm * int
   type isar_params =
-     Proof.context * bool * type_system * int * string Symtab.table
-     * int list list
+     Proof.context * bool * int * string Symtab.table * int list list
   type text_result = string * (string * locality) list
 
   val repair_conjecture_shape_and_fact_names :
-    string -> int list list -> int -> (string * locality) list vector
+    type_system -> string -> int list list -> int
+    -> (string * locality) list vector
     -> int list list * int * (string * locality) list vector
   val used_facts_in_atp_proof :
-    int -> (string * locality) list vector -> string proof
+    type_system -> int -> (string * locality) list vector -> string proof
     -> (string * locality) list
   val is_unsound_proof :
-    int list list -> int -> (string * locality) list vector -> string proof
-    -> bool
+    type_system -> int list list -> int -> (string * locality) list vector
+    -> string proof -> bool
   val apply_on_subgoal : string -> int -> int -> string
   val command_call : string -> string list -> string
   val try_command_line : string -> string -> string
@@ -53,11 +53,10 @@
 
 type minimize_command = string list -> string
 type metis_params =
-  string * minimize_command * string proof * int
+  string * minimize_command * type_system * string proof * int
   * (string * locality) list vector * thm * int
 type isar_params =
-   Proof.context * bool * type_system * int * string Symtab.table
-   * int list list
+  Proof.context * bool * 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))
@@ -96,10 +95,12 @@
   #> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
   #> fst
 
-val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+fun maybe_unprefix_fact_number type_sys =
+  polymorphism_of_type_sys type_sys <> Polymorphic
+  ? (space_implode "_" o tl o space_explode "_")
 
-fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset
-                                           fact_names =
+fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
+                                           fact_offset fact_names =
   if String.isSubstring set_ClauseFormulaRelationN output then
     let
       val j0 = hd (hd conjecture_shape)
@@ -111,7 +112,7 @@
         |> map (fn s => find_index (curry (op =) s) seq + 1)
       fun names_for_number j =
         j |> AList.lookup (op =) name_map |> these
-          |> map_filter (try (unascii_of o unprefix_fact_number
+          |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys
                               o unprefix fact_prefix))
           |> map (fn name =>
                      (name, name |> find_first_in_list_vector fact_names |> the)
@@ -126,16 +127,16 @@
 
 val vampire_step_prefix = "f" (* grrr... *)
 
-fun resolve_fact _ fact_names ((_, SOME s)) =
+fun resolve_fact type_sys _ fact_names ((_, SOME s)) =
     (case try (unprefix fact_prefix) s of
        SOME s' =>
-       let val s' = s' |> unprefix_fact_number |> unascii_of in
+       let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
          case find_first_in_list_vector fact_names s' of
            SOME x => [(s', x)]
          | NONE => []
        end
      | NONE => [])
-  | resolve_fact facts_offset fact_names (num, 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
@@ -156,26 +157,27 @@
                       | NONE => ~1
   in if k >= 0 then [k] else [] end
 
-fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
+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 add_fact facts_offset fact_names (Inference (name, _, [])) =
-    append (resolve_fact facts_offset fact_names name)
-  | add_fact _ _ _ = I
+fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
+    append (resolve_fact type_sys facts_offset fact_names name)
+  | add_fact _ _ _ _ = I
 
-fun used_facts_in_atp_proof facts_offset fact_names atp_proof =
+fun used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof =
   if null atp_proof then Vector.foldl (op @) [] fact_names
-  else fold (add_fact facts_offset fact_names) atp_proof []
+  else fold (add_fact type_sys facts_offset fact_names) atp_proof []
 
 fun is_conjecture_referred_to_in_proof conjecture_shape =
   exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
            | _ => false)
 
-fun is_unsound_proof conjecture_shape facts_offset fact_names =
+fun is_unsound_proof type_sys conjecture_shape facts_offset fact_names =
   not o is_conjecture_referred_to_in_proof conjecture_shape andf
   forall (is_global_locality o snd)
-  o used_facts_in_atp_proof facts_offset fact_names
+  o used_facts_in_atp_proof type_sys facts_offset fact_names
 
 (** Soft-core proof reconstruction: Metis one-liner **)
 
@@ -210,11 +212,11 @@
   List.partition (curry (op =) Chained o snd)
   #> pairself (sort_distinct (string_ord o pairself fst))
 
-fun metis_proof_text (banner, minimize_command, atp_proof, facts_offset,
-                      fact_names, goal, i) =
+fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
+                      facts_offset, fact_names, goal, i) =
   let
     val (chained, extra) =
-      atp_proof |> used_facts_in_atp_proof facts_offset fact_names
+      atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
                 |> split_used_facts
     val n = Logic.count_prems (prop_of goal)
   in
@@ -528,11 +530,12 @@
 
 (* Discard facts; consolidate adjacent lines that prove the same formula, since
    they differ only in type information.*)
-fun add_line _ _ (line as Definition _) lines = line :: lines
-  | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
+fun add_line _ _ _ (line as Definition _) lines = line :: lines
+  | add_line type_sys conjecture_shape fact_names (Inference (name, t, []))
+             lines =
     (* No dependencies: fact, conjecture, or (for Vampire) internal facts or
        definitions. *)
-    if is_fact fact_names name then
+    if is_fact type_sys fact_names name then
       (* Facts are not proof lines. *)
       if is_only_type_information t then
         map (replace_dependencies_in_line (name, [])) lines
@@ -546,7 +549,7 @@
       Inference (name, s_not t, []) :: lines
     else
       map (replace_dependencies_in_line (name, [])) lines
-  | add_line _ _ (Inference (name, t, deps)) lines =
+  | add_line _ _ _ (Inference (name, t, deps)) lines =
     (* Type information will be deleted later; skip repetition test. *)
     if is_only_type_information t then
       Inference (name, t, deps) :: lines
@@ -574,12 +577,12 @@
 fun is_bad_free frees (Free x) = not (member (op =) frees x)
   | is_bad_free _ _ = false
 
-fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
     (j, line :: map (replace_dependencies_in_line (name, [])) lines)
-  | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
-                     (Inference (name, t, deps)) (j, lines) =
+  | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names
+                     frees (Inference (name, t, deps)) (j, lines) =
     (j + 1,
-     if is_fact fact_names name orelse
+     if is_fact type_sys fact_names name orelse
         is_conjecture conjecture_shape name orelse
         (* the last line must be kept *)
         j = 0 orelse
@@ -615,22 +618,24 @@
 fun smart_case_split [] facts = ByMetis facts
   | smart_case_split proofs facts = CaseSplit (proofs, facts)
 
-fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
-  if is_fact fact_names name then
-    apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
+fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names
+                             name =
+  if is_fact type_sys fact_names name then
+    apsnd (union (op =)
+          (map fst (resolve_fact type_sys facts_offset fact_names name)))
   else
     apfst (insert (op =) (raw_label_for_name conjecture_shape name))
 
-fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
-  | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) =
+fun step_for_line _ _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
+  | step_for_line _ conjecture_shape _ _ _ (Inference (name, t, [])) =
     Assume (raw_label_for_name conjecture_shape name, t)
-  | step_for_line conjecture_shape facts_offset fact_names j
-                  (Inference (name, t, deps)) =
+  | step_for_line type_sys conjecture_shape facts_offset
+                  fact_names j (Inference (name, t, deps)) =
     Have (if j = 1 then [Show] else [],
           raw_label_for_name conjecture_shape name,
           fold_rev forall_of (map Var (Term.add_vars t [])) t,
-          ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
-                                                  fact_names)
+          ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape
+                                                  facts_offset fact_names)
                         deps ([], [])))
 
 fun repair_name "$true" = "c_True"
@@ -651,14 +656,15 @@
       |> nasty_atp_proof pool
       |> map_term_names_in_atp_proof repair_name
       |> decode_lines ctxt type_sys tfrees
-      |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
+      |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names)
       |> rpair [] |-> fold_rev add_nontrivial_line
-      |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
-                                             conjecture_shape fact_names frees)
+      |> rpair (0, [])
+      |-> fold_rev (add_desired_line type_sys isar_shrink_factor
+                                     conjecture_shape fact_names frees)
       |> snd
   in
     (if null params then [] else [Fix params]) @
-    map2 (step_for_line conjecture_shape facts_offset fact_names)
+    map2 (step_for_line type_sys conjecture_shape facts_offset fact_names)
          (length lines downto 1) lines
   end
 
@@ -950,9 +956,9 @@
         (if n <> 1 then "next" else "qed")
   in do_proof end
 
-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)) =
+fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape)
+                    (metis_params as (_, _, type_sys, 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) []
diff -r 4781fcd53572 -r 59142dbfa3ba src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 00:10:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 01:04:03 2011 +0200
@@ -754,8 +754,11 @@
    the remote provers might care. *)
 fun formula_line_for_fact ctxt prefix type_sys
                           (j, formula as {name, locality, kind, ...}) =
-  Formula (prefix ^ string_of_int j ^ "_" ^ ascii_of name, kind,
-           formula_for_fact ctxt type_sys formula, NONE,
+  Formula (prefix ^
+           (if polymorphism_of_type_sys type_sys = Polymorphic then ""
+            else string_of_int j ^ "_") ^
+           ascii_of name,
+           kind, formula_for_fact ctxt type_sys formula, NONE,
            if generate_useful_info then
              case locality of
                Intro => useful_isabelle_info "intro"
diff -r 4781fcd53572 -r 59142dbfa3ba src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 00:10:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 03 01:04:03 2011 +0200
@@ -504,7 +504,7 @@
                   |>> atp_proof_from_tstplike_proof
                 val (conjecture_shape, facts_offset, fact_names) =
                   if is_none outcome then
-                    repair_conjecture_shape_and_fact_names output
+                    repair_conjecture_shape_and_fact_names type_sys output
                         conjecture_shape facts_offset fact_names
                   else
                     (* don't bother repairing *)
@@ -512,8 +512,8 @@
                 val outcome =
                   case outcome of
                     NONE =>
-                    if is_unsound_proof conjecture_shape facts_offset fact_names
-                                        atp_proof then
+                    if is_unsound_proof type_sys conjecture_shape facts_offset
+                                        fact_names atp_proof then
                       SOME (UnsoundProof (is_type_sys_virtually_sound type_sys))
                     else
                       NONE
@@ -543,7 +543,7 @@
             fun maybe_blacklist_facts_and_retry iter blacklist
                     (result as ((_, _, facts_offset, fact_names),
                                 (_, _, atp_proof, SOME (UnsoundProof false)))) =
-                (case used_facts_in_atp_proof facts_offset fact_names
+                (case used_facts_in_atp_proof type_sys facts_offset fact_names
                                               atp_proof of
                    [] => result
                  | new_baddies =>
@@ -594,11 +594,10 @@
          "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
        else
          "")
-    val isar_params =
-      (ctxt, debug, type_sys, isar_shrink_factor, pool, conjecture_shape)
+    val isar_params = (ctxt, debug, isar_shrink_factor, pool, conjecture_shape)
     val metis_params =
-      (proof_banner auto, minimize_command, atp_proof, facts_offset, fact_names,
-       goal, subgoal)
+      (proof_banner auto, minimize_command, type_sys, atp_proof, facts_offset,
+       fact_names, goal, subgoal)
     val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>