move type declarations to the front, for TFF-compliance

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
@@ -13,7 +13,7 @@
   type type_system = Sledgehammer_ATP_Translate.type_system
   type minimize_command = string list -> string
   type metis_params =
-    string * type_system * minimize_command * string proof
+    string * type_system * minimize_command * string proof * int
     * (string * locality) list vector * thm * int
   type isar_params =
     string Symtab.table * bool * int * Proof.context * int list list
@@ -23,9 +23,11 @@
     string -> int list list -> (string * locality) list vector
     -> int list list * (string * locality) list vector
   val used_facts_in_atp_proof :
-    (string * locality) list vector -> string proof -> (string * locality) list
+    int -> (string * locality) list vector -> string proof
+    -> (string * locality) list
   val is_unsound_proof :
-    int list list -> (string * locality) list vector -> string proof -> bool
+    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
@@ -50,7 +52,7 @@
 
 type minimize_command = string list -> string
 type metis_params =
-  string * type_system * minimize_command * string proof
+  string * type_system * minimize_command * string proof * int
   * (string * locality) list vector * thm * int
 type isar_params =
   string Symtab.table * bool * int * Proof.context * int list list
@@ -122,7 +124,7 @@
 
 val vampire_step_prefix = "f" (* grrr... *)
 
-fun resolve_fact fact_names ((_, SOME s)) =
+fun resolve_fact _ fact_names ((_, SOME s)) =
     (case try (unprefix fact_prefix) s of
        SOME s' =>
        let val s' = s' |> unprefix_fact_number |> unascii_of in
@@ -131,13 +133,15 @@
          | NONE => []
        end
      | NONE => [])
-  | resolve_fact 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 =>
-      if j > 0 andalso j <= Vector.length fact_names then
-        Vector.sub (fact_names, j - 1)
-      else
-        []
+      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 resolve_conjecture conjecture_shape (num, s_opt) =
@@ -150,25 +154,26 @@
                       | NONE => ~1
   in if k >= 0 then [k] else [] end
 
-fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
+fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
 fun is_conjecture conjecture_shape =
   not o null o resolve_conjecture conjecture_shape
 
-fun add_fact fact_names (Inference (name, _, [])) =
-    append (resolve_fact fact_names name)
-  | add_fact _ _ = I
+fun add_fact facts_offset fact_names (Inference (name, _, [])) =
+    append (resolve_fact facts_offset fact_names name)
+  | add_fact _ _ _ = I
 
-fun used_facts_in_atp_proof fact_names atp_proof =
+fun used_facts_in_atp_proof facts_offset fact_names atp_proof =
   if null atp_proof then Vector.foldl (op @) [] fact_names
-  else fold (add_fact fact_names) atp_proof []
+  else fold (add_fact 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 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 fact_names
+fun is_unsound_proof 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
 
 (** Soft-core proof reconstruction: Metis one-liner **)
 
@@ -206,11 +211,12 @@
   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, fact_names,
-                      goal, i) =
+fun metis_proof_text (banner, type_sys, minimize_command, atp_proof,
+                      facts_offset, fact_names, goal, i) =
   let
     val (chained_lemmas, other_lemmas) =
-      split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
+      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) ^
@@ -606,20 +612,22 @@
 fun smart_case_split [] facts = ByMetis facts
   | smart_case_split proofs facts = CaseSplit (proofs, facts)
 
-fun add_fact_from_dependency conjecture_shape fact_names name =
+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 fact_names name)))
+    apsnd (union (op =) (map fst (resolve_fact 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 fact_names j (Inference (name, t, deps)) =
+  | step_for_line 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 fact_names)
+          ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
+                                                  fact_names)
                         deps ([], [])))
 
 fun repair_name "$true" = "c_True"
@@ -633,7 +641,7 @@
       s
 
 fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
-        atp_proof conjecture_shape fact_names params frees =
+        atp_proof conjecture_shape facts_offset fact_names params frees =
   let
     val lines =
       atp_proof
@@ -647,8 +655,8 @@
       |> snd
   in
     (if null params then [] else [Fix params]) @
-    map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
-         lines
+    map2 (step_for_line conjecture_shape facts_offset fact_names)
+         (length lines downto 1) lines
   end
 
 (* When redirecting proofs, we keep information about the labels seen so far in
@@ -939,7 +947,8 @@
   in do_proof end
 
 fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
-        (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
+        (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) []
@@ -948,8 +957,8 @@
     val (one_line_proof, lemma_names) = metis_proof_text metis_params
     fun isar_proof_for () =
       case isar_proof_from_atp_proof pool ctxt type_sys tfrees
-               isar_shrink_factor atp_proof conjecture_shape fact_names params
-               frees
+               isar_shrink_factor atp_proof conjecture_shape facts_offset
+               fact_names params frees
            |> redirect_proof hyp_ts concl_t
            |> kill_duplicate_assumptions_in_proof
            |> then_chain_proof

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -33,7 +33,8 @@
   val prepare_atp_problem :
     Proof.context -> bool -> type_system -> bool -> term list -> term
     -> (translated_formula option * ((string * 'a) * thm)) list
-    -> string problem * string Symtab.table * int * (string * 'a) list vector
+    -> string problem * string Symtab.table * int * int
+       * (string * 'a) list vector
   val atp_problem_weights : string problem -> (string * real) list
 end;
 
@@ -798,11 +799,11 @@
                      `I tff_bool_type))
   | add_extra_type_decl_lines _ = I
 
+val type_declsN = "Type declarations"
 val factsN = "Relevant facts"
 val class_relsN = "Class relationships"
 val aritiesN = "Arity declarations"
 val helpersN = "Helper facts"
-val type_declsN = "Type declarations"
 val conjsN = "Conjectures"
 val free_typesN = "Type variables"
 
@@ -820,12 +821,12 @@
     (* Reordering these might confuse the proof reconstruction code or the SPASS
        Flotter hack. *)
     val problem =
-      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
+      [(type_declsN, []),
+       (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
                     (0 upto length facts - 1 ~~ facts)),
        (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
        (aritiesN, map problem_line_for_arity_clause arity_clauses),
        (helpersN, []),
-       (type_declsN, []),
        (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
        (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
     val sym_tab = sym_table_for_problem explicit_apply problem
@@ -847,11 +848,12 @@
       |> op @
     val (problem, pool) =
       problem |> fold (AList.update (op =))
-                      [(helpersN, helper_lines), (type_declsN, type_decl_lines)]
+                      [(type_declsN, type_decl_lines), (helpersN, helper_lines)]
               |> nice_atp_problem readable_names
   in
     (problem,
      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+     offset_of_heading_in_problem factsN problem 0,
      offset_of_heading_in_problem conjsN problem 0,
      fact_names |> Vector.fromList)
   end

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
@@ -432,7 +432,8 @@
                     |> Output.urgent_message
                   else
                     ()
-                val (atp_problem, pool, conjecture_offset, fact_names) =
+                val (atp_problem, pool, conjecture_offset, facts_offset,
+                     fact_names) =
                   prepare_atp_problem ctxt readable_names type_sys
                                       explicit_apply hyp_ts concl_t facts
                 fun weights () = atp_problem_weights atp_problem
@@ -474,8 +475,8 @@
                 val outcome =
                   case outcome of
                     NONE => if not (is_type_system_sound type_sys) andalso
-                               is_unsound_proof conjecture_shape fact_names
-                                                atp_proof then
+                               is_unsound_proof conjecture_shape facts_offset
+                                                fact_names atp_proof then
                               SOME UnsoundProof
                             else
                               NONE
@@ -484,7 +485,7 @@
                     else SOME IncompleteUnprovable
                   | _ => outcome
               in
-                ((pool, conjecture_shape, fact_names),
+                ((pool, conjecture_shape, facts_offset, fact_names),
                  (output, msecs, atp_proof, outcome))
               end
             val timer = Timer.startRealTimer ()
@@ -503,9 +504,10 @@
                 end
               | maybe_run_slice _ _ result = result
             fun maybe_blacklist_facts_and_retry iter blacklist
-                    (result as ((_, _, fact_names),
+                    (result as ((_, _, facts_offset, fact_names),
                                 (_, _, atp_proof, SOME UnsoundProof))) =
-                (case used_facts_in_atp_proof fact_names atp_proof of
+                (case used_facts_in_atp_proof facts_offset fact_names
+                                              atp_proof of
                    [] => result
                  | new_baddies =>
                    let val blacklist = new_baddies @ blacklist in
@@ -516,7 +518,7 @@
                    end)
               | maybe_blacklist_facts_and_retry _ _ result = result
           in
-            ((Symtab.empty, [], Vector.fromList []),
+            ((Symtab.empty, [], 0, Vector.fromList []),
              ("", SOME 0, [], SOME InternalError))
             |> fold (maybe_run_slice []) actual_slices
                (* The ATP found an unsound proof? Automatically try again
@@ -535,7 +537,7 @@
         ()
       else
         File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
-    val ((pool, conjecture_shape, fact_names),
+    val ((pool, conjecture_shape, facts_offset, fact_names),
          (output, msecs, atp_proof, outcome)) =
       with_path cleanup export run_on problem_path_name
     val important_message =
@@ -556,8 +558,8 @@
          "")
     val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
     val metis_params =
-      (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names,
-       goal, subgoal)
+      (proof_banner auto, type_sys, minimize_command, atp_proof, facts_offset,
+       fact_names, goal, subgoal)
     val (outcome, (message, used_facts)) =
       case outcome of
         NONE =>