move type declarations to the front, for TFF-compliance
authorblanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 425418938507b2054
parent 42540 77d9915e6a11
child 42542 024920b65ce2
move type declarations to the front, for TFF-compliance
src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4    type type_system = Sledgehammer_ATP_Translate.type_system
     1.5    type minimize_command = string list -> string
     1.6    type metis_params =
     1.7 -    string * type_system * minimize_command * string proof
     1.8 +    string * type_system * minimize_command * string proof * int
     1.9      * (string * locality) list vector * thm * int
    1.10    type isar_params =
    1.11      string Symtab.table * bool * int * Proof.context * int list list
    1.12 @@ -23,9 +23,11 @@
    1.13      string -> int list list -> (string * locality) list vector
    1.14      -> int list list * (string * locality) list vector
    1.15    val used_facts_in_atp_proof :
    1.16 -    (string * locality) list vector -> string proof -> (string * locality) list
    1.17 +    int -> (string * locality) list vector -> string proof
    1.18 +    -> (string * locality) list
    1.19    val is_unsound_proof :
    1.20 -    int list list -> (string * locality) list vector -> string proof -> bool
    1.21 +    int list list -> int -> (string * locality) list vector -> string proof
    1.22 +    -> bool
    1.23    val apply_on_subgoal : string -> int -> int -> string
    1.24    val command_call : string -> string list -> string
    1.25    val try_command_line : string -> string -> string
    1.26 @@ -50,7 +52,7 @@
    1.27  
    1.28  type minimize_command = string list -> string
    1.29  type metis_params =
    1.30 -  string * type_system * minimize_command * string proof
    1.31 +  string * type_system * minimize_command * string proof * int
    1.32    * (string * locality) list vector * thm * int
    1.33  type isar_params =
    1.34    string Symtab.table * bool * int * Proof.context * int list list
    1.35 @@ -122,7 +124,7 @@
    1.36  
    1.37  val vampire_step_prefix = "f" (* grrr... *)
    1.38  
    1.39 -fun resolve_fact fact_names ((_, SOME s)) =
    1.40 +fun resolve_fact _ fact_names ((_, SOME s)) =
    1.41      (case try (unprefix fact_prefix) s of
    1.42         SOME s' =>
    1.43         let val s' = s' |> unprefix_fact_number |> unascii_of in
    1.44 @@ -131,13 +133,15 @@
    1.45           | NONE => []
    1.46         end
    1.47       | NONE => [])
    1.48 -  | resolve_fact fact_names (num, NONE) =
    1.49 +  | resolve_fact facts_offset fact_names (num, NONE) =
    1.50      case Int.fromString (perhaps (try (unprefix vampire_step_prefix)) num) of
    1.51        SOME j =>
    1.52 -      if j > 0 andalso j <= Vector.length fact_names then
    1.53 -        Vector.sub (fact_names, j - 1)
    1.54 -      else
    1.55 -        []
    1.56 +      let val j = j - facts_offset in
    1.57 +        if j > 0 andalso j <= Vector.length fact_names then
    1.58 +          Vector.sub (fact_names, j - 1)
    1.59 +        else
    1.60 +          []
    1.61 +      end
    1.62      | NONE => []
    1.63  
    1.64  fun resolve_conjecture conjecture_shape (num, s_opt) =
    1.65 @@ -150,25 +154,26 @@
    1.66                        | NONE => ~1
    1.67    in if k >= 0 then [k] else [] end
    1.68  
    1.69 -fun is_fact conjecture_shape = not o null o resolve_fact conjecture_shape
    1.70 +fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
    1.71  fun is_conjecture conjecture_shape =
    1.72    not o null o resolve_conjecture conjecture_shape
    1.73  
    1.74 -fun add_fact fact_names (Inference (name, _, [])) =
    1.75 -    append (resolve_fact fact_names name)
    1.76 -  | add_fact _ _ = I
    1.77 +fun add_fact facts_offset fact_names (Inference (name, _, [])) =
    1.78 +    append (resolve_fact facts_offset fact_names name)
    1.79 +  | add_fact _ _ _ = I
    1.80  
    1.81 -fun used_facts_in_atp_proof fact_names atp_proof =
    1.82 +fun used_facts_in_atp_proof facts_offset fact_names atp_proof =
    1.83    if null atp_proof then Vector.foldl (op @) [] fact_names
    1.84 -  else fold (add_fact fact_names) atp_proof []
    1.85 +  else fold (add_fact facts_offset fact_names) atp_proof []
    1.86  
    1.87  fun is_conjecture_referred_to_in_proof conjecture_shape =
    1.88    exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
    1.89             | _ => false)
    1.90  
    1.91 -fun is_unsound_proof conjecture_shape fact_names =
    1.92 -  (not o is_conjecture_referred_to_in_proof conjecture_shape) andf
    1.93 -  forall (is_global_locality o snd) o used_facts_in_atp_proof fact_names
    1.94 +fun is_unsound_proof conjecture_shape facts_offset fact_names =
    1.95 +  not o is_conjecture_referred_to_in_proof conjecture_shape andf
    1.96 +  forall (is_global_locality o snd)
    1.97 +  o used_facts_in_atp_proof facts_offset fact_names
    1.98  
    1.99  (** Soft-core proof reconstruction: Metis one-liner **)
   1.100  
   1.101 @@ -206,11 +211,12 @@
   1.102    List.partition (curry (op =) Chained o snd)
   1.103    #> pairself (sort_distinct (string_ord o pairself fst))
   1.104  
   1.105 -fun metis_proof_text (banner, type_sys, minimize_command, atp_proof, fact_names,
   1.106 -                      goal, i) =
   1.107 +fun metis_proof_text (banner, type_sys, minimize_command, atp_proof,
   1.108 +                      facts_offset, fact_names, goal, i) =
   1.109    let
   1.110      val (chained_lemmas, other_lemmas) =
   1.111 -      split_used_facts (used_facts_in_atp_proof fact_names atp_proof)
   1.112 +      atp_proof |> used_facts_in_atp_proof facts_offset fact_names
   1.113 +                |> split_used_facts
   1.114      val n = Logic.count_prems (prop_of goal)
   1.115    in
   1.116      (metis_line banner type_sys i n (map fst other_lemmas) ^
   1.117 @@ -606,20 +612,22 @@
   1.118  fun smart_case_split [] facts = ByMetis facts
   1.119    | smart_case_split proofs facts = CaseSplit (proofs, facts)
   1.120  
   1.121 -fun add_fact_from_dependency conjecture_shape fact_names name =
   1.122 +fun add_fact_from_dependency conjecture_shape facts_offset fact_names name =
   1.123    if is_fact fact_names name then
   1.124 -    apsnd (union (op =) (map fst (resolve_fact fact_names name)))
   1.125 +    apsnd (union (op =) (map fst (resolve_fact facts_offset fact_names name)))
   1.126    else
   1.127      apfst (insert (op =) (raw_label_for_name conjecture_shape name))
   1.128  
   1.129 -fun step_for_line _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.130 -  | step_for_line conjecture_shape _ _ (Inference (name, t, [])) =
   1.131 +fun step_for_line _ _ _ _ (Definition (_, t1, t2)) = Let (t1, t2)
   1.132 +  | step_for_line conjecture_shape _ _ _ (Inference (name, t, [])) =
   1.133      Assume (raw_label_for_name conjecture_shape name, t)
   1.134 -  | step_for_line conjecture_shape fact_names j (Inference (name, t, deps)) =
   1.135 +  | step_for_line conjecture_shape facts_offset fact_names j
   1.136 +                  (Inference (name, t, deps)) =
   1.137      Have (if j = 1 then [Show] else [],
   1.138            raw_label_for_name conjecture_shape name,
   1.139            fold_rev forall_of (map Var (Term.add_vars t [])) t,
   1.140 -          ByMetis (fold (add_fact_from_dependency conjecture_shape fact_names)
   1.141 +          ByMetis (fold (add_fact_from_dependency conjecture_shape facts_offset
   1.142 +                                                  fact_names)
   1.143                          deps ([], [])))
   1.144  
   1.145  fun repair_name "$true" = "c_True"
   1.146 @@ -633,7 +641,7 @@
   1.147        s
   1.148  
   1.149  fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.150 -        atp_proof conjecture_shape fact_names params frees =
   1.151 +        atp_proof conjecture_shape facts_offset fact_names params frees =
   1.152    let
   1.153      val lines =
   1.154        atp_proof
   1.155 @@ -647,8 +655,8 @@
   1.156        |> snd
   1.157    in
   1.158      (if null params then [] else [Fix params]) @
   1.159 -    map2 (step_for_line conjecture_shape fact_names) (length lines downto 1)
   1.160 -         lines
   1.161 +    map2 (step_for_line conjecture_shape facts_offset fact_names)
   1.162 +         (length lines downto 1) lines
   1.163    end
   1.164  
   1.165  (* When redirecting proofs, we keep information about the labels seen so far in
   1.166 @@ -939,7 +947,8 @@
   1.167    in do_proof end
   1.168  
   1.169  fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
   1.170 -        (metis_params as (_, type_sys, _, atp_proof, fact_names, goal, i)) =
   1.171 +        (metis_params as (_, type_sys, _, atp_proof, facts_offset, fact_names,
   1.172 +                          goal, i)) =
   1.173    let
   1.174      val (params, hyp_ts, concl_t) = strip_subgoal goal i
   1.175      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.176 @@ -948,8 +957,8 @@
   1.177      val (one_line_proof, lemma_names) = metis_proof_text metis_params
   1.178      fun isar_proof_for () =
   1.179        case isar_proof_from_atp_proof pool ctxt type_sys tfrees
   1.180 -               isar_shrink_factor atp_proof conjecture_shape fact_names params
   1.181 -               frees
   1.182 +               isar_shrink_factor atp_proof conjecture_shape facts_offset
   1.183 +               fact_names params frees
   1.184             |> redirect_proof hyp_ts concl_t
   1.185             |> kill_duplicate_assumptions_in_proof
   1.186             |> then_chain_proof
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
     2.3 @@ -33,7 +33,8 @@
     2.4    val prepare_atp_problem :
     2.5      Proof.context -> bool -> type_system -> bool -> term list -> term
     2.6      -> (translated_formula option * ((string * 'a) * thm)) list
     2.7 -    -> string problem * string Symtab.table * int * (string * 'a) list vector
     2.8 +    -> string problem * string Symtab.table * int * int
     2.9 +       * (string * 'a) list vector
    2.10    val atp_problem_weights : string problem -> (string * real) list
    2.11  end;
    2.12  
    2.13 @@ -798,11 +799,11 @@
    2.14                       `I tff_bool_type))
    2.15    | add_extra_type_decl_lines _ = I
    2.16  
    2.17 +val type_declsN = "Type declarations"
    2.18  val factsN = "Relevant facts"
    2.19  val class_relsN = "Class relationships"
    2.20  val aritiesN = "Arity declarations"
    2.21  val helpersN = "Helper facts"
    2.22 -val type_declsN = "Type declarations"
    2.23  val conjsN = "Conjectures"
    2.24  val free_typesN = "Type variables"
    2.25  
    2.26 @@ -820,12 +821,12 @@
    2.27      (* Reordering these might confuse the proof reconstruction code or the SPASS
    2.28         Flotter hack. *)
    2.29      val problem =
    2.30 -      [(factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
    2.31 +      [(type_declsN, []),
    2.32 +       (factsN, map (problem_line_for_fact ctxt fact_prefix type_sys)
    2.33                      (0 upto length facts - 1 ~~ facts)),
    2.34         (class_relsN, map problem_line_for_class_rel_clause class_rel_clauses),
    2.35         (aritiesN, map problem_line_for_arity_clause arity_clauses),
    2.36         (helpersN, []),
    2.37 -       (type_declsN, []),
    2.38         (conjsN, map (problem_line_for_conjecture ctxt type_sys) conjs),
    2.39         (free_typesN, problem_lines_for_free_types type_sys (facts @ conjs))]
    2.40      val sym_tab = sym_table_for_problem explicit_apply problem
    2.41 @@ -847,11 +848,12 @@
    2.42        |> op @
    2.43      val (problem, pool) =
    2.44        problem |> fold (AList.update (op =))
    2.45 -                      [(helpersN, helper_lines), (type_declsN, type_decl_lines)]
    2.46 +                      [(type_declsN, type_decl_lines), (helpersN, helper_lines)]
    2.47                |> nice_atp_problem readable_names
    2.48    in
    2.49      (problem,
    2.50       case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
    2.51 +     offset_of_heading_in_problem factsN problem 0,
    2.52       offset_of_heading_in_problem conjsN problem 0,
    2.53       fact_names |> Vector.fromList)
    2.54    end
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
     3.3 @@ -432,7 +432,8 @@
     3.4                      |> Output.urgent_message
     3.5                    else
     3.6                      ()
     3.7 -                val (atp_problem, pool, conjecture_offset, fact_names) =
     3.8 +                val (atp_problem, pool, conjecture_offset, facts_offset,
     3.9 +                     fact_names) =
    3.10                    prepare_atp_problem ctxt readable_names type_sys
    3.11                                        explicit_apply hyp_ts concl_t facts
    3.12                  fun weights () = atp_problem_weights atp_problem
    3.13 @@ -474,8 +475,8 @@
    3.14                  val outcome =
    3.15                    case outcome of
    3.16                      NONE => if not (is_type_system_sound type_sys) andalso
    3.17 -                               is_unsound_proof conjecture_shape fact_names
    3.18 -                                                atp_proof then
    3.19 +                               is_unsound_proof conjecture_shape facts_offset
    3.20 +                                                fact_names atp_proof then
    3.21                                SOME UnsoundProof
    3.22                              else
    3.23                                NONE
    3.24 @@ -484,7 +485,7 @@
    3.25                      else SOME IncompleteUnprovable
    3.26                    | _ => outcome
    3.27                in
    3.28 -                ((pool, conjecture_shape, fact_names),
    3.29 +                ((pool, conjecture_shape, facts_offset, fact_names),
    3.30                   (output, msecs, atp_proof, outcome))
    3.31                end
    3.32              val timer = Timer.startRealTimer ()
    3.33 @@ -503,9 +504,10 @@
    3.34                  end
    3.35                | maybe_run_slice _ _ result = result
    3.36              fun maybe_blacklist_facts_and_retry iter blacklist
    3.37 -                    (result as ((_, _, fact_names),
    3.38 +                    (result as ((_, _, facts_offset, fact_names),
    3.39                                  (_, _, atp_proof, SOME UnsoundProof))) =
    3.40 -                (case used_facts_in_atp_proof fact_names atp_proof of
    3.41 +                (case used_facts_in_atp_proof facts_offset fact_names
    3.42 +                                              atp_proof of
    3.43                     [] => result
    3.44                   | new_baddies =>
    3.45                     let val blacklist = new_baddies @ blacklist in
    3.46 @@ -516,7 +518,7 @@
    3.47                     end)
    3.48                | maybe_blacklist_facts_and_retry _ _ result = result
    3.49            in
    3.50 -            ((Symtab.empty, [], Vector.fromList []),
    3.51 +            ((Symtab.empty, [], 0, Vector.fromList []),
    3.52               ("", SOME 0, [], SOME InternalError))
    3.53              |> fold (maybe_run_slice []) actual_slices
    3.54                 (* The ATP found an unsound proof? Automatically try again
    3.55 @@ -535,7 +537,7 @@
    3.56          ()
    3.57        else
    3.58          File.write (Path.explode (Path.implode prob_file ^ "_proof")) output
    3.59 -    val ((pool, conjecture_shape, fact_names),
    3.60 +    val ((pool, conjecture_shape, facts_offset, fact_names),
    3.61           (output, msecs, atp_proof, outcome)) =
    3.62        with_path cleanup export run_on problem_path_name
    3.63      val important_message =
    3.64 @@ -556,8 +558,8 @@
    3.65           "")
    3.66      val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
    3.67      val metis_params =
    3.68 -      (proof_banner auto, type_sys, minimize_command, atp_proof, fact_names,
    3.69 -       goal, subgoal)
    3.70 +      (proof_banner auto, type_sys, minimize_command, atp_proof, facts_offset,
    3.71 +       fact_names, goal, subgoal)
    3.72      val (outcome, (message, used_facts)) =
    3.73        case outcome of
    3.74          NONE =>