improve SPASS hack, when a clause comes from several facts
authorblanchet
Thu Aug 26 14:05:22 2010 +0200 (2010-08-26)
changeset 3881861cf050f8b2e
parent 38817 bf27c24ba224
child 38819 71c9f61516cd
improve SPASS hack, when a clause comes from several facts
src/HOL/Tools/Sledgehammer/sledgehammer.ML
src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 26 13:55:30 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 26 14:05:22 2010 +0200
     1.3 @@ -38,7 +38,7 @@
     1.4       atp_run_time_in_msecs: int,
     1.5       output: string,
     1.6       proof: string,
     1.7 -     axiom_names: (string * locality) vector,
     1.8 +     axiom_names: (string * locality) list vector,
     1.9       conjecture_shape: int list list}
    1.10    type prover = params -> minimize_command -> problem -> prover_result
    1.11  
    1.12 @@ -107,7 +107,7 @@
    1.13     atp_run_time_in_msecs: int,
    1.14     output: string,
    1.15     proof: string,
    1.16 -   axiom_names: (string * locality) vector,
    1.17 +   axiom_names: (string * locality) list vector,
    1.18     conjecture_shape: int list list}
    1.19  
    1.20  type prover = params -> minimize_command -> problem -> prover_result
    1.21 @@ -175,6 +175,7 @@
    1.22    #> snd #> Substring.string #> strip_spaces_except_between_ident_chars
    1.23    #> explode #> parse_clause_formula_relation #> fst
    1.24  
    1.25 +(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *)
    1.26  fun repair_conjecture_shape_and_theorem_names output conjecture_shape
    1.27                                                axiom_names =
    1.28    if String.isSubstring set_ClauseFormulaRelationN output then
    1.29 @@ -189,19 +190,17 @@
    1.30          conjecture_prefix ^ string_of_int (j - j0)
    1.31          |> AList.find (fn (s, ss) => member (op =) ss s) name_map
    1.32          |> map (fn s => find_index (curry (op =) s) seq + 1)
    1.33 -      fun name_for_number j =
    1.34 -        let
    1.35 -          val axioms =
    1.36 -            j |> AList.lookup (op =) name_map |> these
    1.37 -              |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    1.38 -          val loc =
    1.39 -            case axioms of
    1.40 -              [axiom] => find_first_in_vector axiom_names axiom General
    1.41 -            | _ => General
    1.42 -        in (axioms |> space_implode " ", loc) end
    1.43 +      fun names_for_number j =
    1.44 +        j |> AList.lookup (op =) name_map |> these
    1.45 +          |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of
    1.46 +          |> map (fn name =>
    1.47 +                     (name, name |> find_first_in_list_vector axiom_names
    1.48 +                                 |> the)
    1.49 +                     handle Option.Option =>
    1.50 +                            error ("No such fact: " ^ quote name ^ "."))
    1.51      in
    1.52        (conjecture_shape |> map (maps renumber_conjecture),
    1.53 -       seq |> map name_for_number |> Vector.fromList)
    1.54 +       seq |> map names_for_number |> Vector.fromList)
    1.55      end
    1.56    else
    1.57      (conjecture_shape, axiom_names)
    1.58 @@ -253,7 +252,7 @@
    1.59          if the_dest_dir = "" then File.tmp_path probfile
    1.60          else if File.exists (Path.explode the_dest_dir)
    1.61          then Path.append (Path.explode the_dest_dir) probfile
    1.62 -        else error ("No such directory: " ^ the_dest_dir ^ ".")
    1.63 +        else error ("No such directory: " ^ quote the_dest_dir ^ ".")
    1.64        end;
    1.65  
    1.66      val measure_run_time = verbose orelse Config.get ctxt measure_runtime
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 13:55:30 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Aug 26 14:05:22 2010 +0200
     2.3 @@ -586,9 +586,8 @@
     2.4      val local_facts = ProofContext.facts_of ctxt
     2.5      val named_locals = local_facts |> Facts.dest_static []
     2.6      val is_chained = member Thm.eq_thm chained_ths
     2.7 -    (* Unnamed, not chained formulas with schematic variables are omitted,
     2.8 -       because they are rejected by the backticks (`...`) parser for some
     2.9 -       reason. *)
    2.10 +    (* Unnamed nonchained formulas with schematic variables are omitted, because
    2.11 +       they are rejected by the backticks (`...`) parser for some reason. *)
    2.12      fun is_good_unnamed_local th =
    2.13        forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
    2.14        andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 13:55:30 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Aug 26 14:05:22 2010 +0200
     3.3 @@ -10,18 +10,16 @@
     3.4  sig
     3.5    type locality = Sledgehammer_Fact_Filter.locality
     3.6    type minimize_command = string list -> string
     3.7 -
     3.8 -  val metis_proof_text:
     3.9 -    bool * minimize_command * string * (string * locality) vector * thm * int
    3.10 -    -> string * (string * locality) list
    3.11 -  val isar_proof_text:
    3.12 +  type metis_params =
    3.13 +    bool * minimize_command * string * (string * locality) list vector * thm
    3.14 +    * int
    3.15 +  type isar_params =
    3.16      string Symtab.table * bool * int * Proof.context * int list list
    3.17 -    -> bool * minimize_command * string * (string * locality) vector * thm * int
    3.18 -    -> string * (string * locality) list
    3.19 -  val proof_text:
    3.20 -    bool -> string Symtab.table * bool * int * Proof.context * int list list
    3.21 -    -> bool * minimize_command * string * (string * locality) vector * thm * int
    3.22 -    -> string * (string * locality) list
    3.23 +  type text_result = string * (string * locality) list
    3.24 +
    3.25 +  val metis_proof_text : metis_params -> text_result
    3.26 +  val isar_proof_text : isar_params -> metis_params -> text_result
    3.27 +  val proof_text : bool -> isar_params -> metis_params -> text_result
    3.28  end;
    3.29  
    3.30  structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
    3.31 @@ -34,6 +32,11 @@
    3.32  open Sledgehammer_Translate
    3.33  
    3.34  type minimize_command = string list -> string
    3.35 +type metis_params =
    3.36 +  bool * minimize_command * string * (string * locality) list vector * thm * int
    3.37 +type isar_params =
    3.38 +  string Symtab.table * bool * int * Proof.context * int list list
    3.39 +type text_result = string * (string * locality) list
    3.40  
    3.41  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    3.42     spurious "True"s. *)
    3.43 @@ -61,7 +64,7 @@
    3.44  fun index_in_shape x = find_index (exists (curry (op =) x))
    3.45  fun is_axiom_number axiom_names num =
    3.46    num > 0 andalso num <= Vector.length axiom_names andalso
    3.47 -  fst (Vector.sub (axiom_names, num - 1)) <> ""
    3.48 +  not (null (Vector.sub (axiom_names, num - 1)))
    3.49  fun is_conjecture_number conjecture_shape num =
    3.50    index_in_shape num conjecture_shape >= 0
    3.51  
    3.52 @@ -565,12 +568,10 @@
    3.53     "108. ... [input]". *)
    3.54  fun used_facts_in_atp_proof axiom_names atp_proof =
    3.55    let
    3.56 -    fun axiom_name_at_index num =
    3.57 +    fun axiom_names_at_index num =
    3.58        let val j = Int.fromString num |> the_default ~1 in
    3.59 -        if is_axiom_number axiom_names j then
    3.60 -          SOME (Vector.sub (axiom_names, j - 1))
    3.61 -        else
    3.62 -          NONE
    3.63 +        if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1)
    3.64 +        else []
    3.65        end
    3.66      val tokens_of =
    3.67        String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
    3.68 @@ -579,17 +580,19 @@
    3.69            (case strip_prefix_and_unascii axiom_prefix (List.last rest) of
    3.70               SOME name =>
    3.71               if member (op =) rest "file" then
    3.72 -               SOME (name, find_first_in_vector axiom_names name General)
    3.73 +               ([(name, name |> find_first_in_list_vector axiom_names |> the)]
    3.74 +                handle Option.Option =>
    3.75 +                       error ("No such fact: " ^ quote name ^ "."))
    3.76               else
    3.77 -               axiom_name_at_index num
    3.78 -           | NONE => axiom_name_at_index num)
    3.79 +               axiom_names_at_index num
    3.80 +           | NONE => axiom_names_at_index num)
    3.81          else
    3.82 -          NONE
    3.83 -      | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num
    3.84 +          []
    3.85 +      | do_line (num :: "0" :: "Inp" :: _) = axiom_names_at_index num
    3.86        | do_line (num :: rest) =
    3.87 -        (case List.last rest of "input" => axiom_name_at_index num | _ => NONE)
    3.88 -      | do_line _ = NONE
    3.89 -  in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end
    3.90 +        (case List.last rest of "input" => axiom_names_at_index num | _ => [])
    3.91 +      | do_line _ = []
    3.92 +  in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end
    3.93  
    3.94  val indent_size = 2
    3.95  val no_label = ("", ~1)
    3.96 @@ -663,7 +666,7 @@
    3.97  
    3.98  fun add_fact_from_dep axiom_names num =
    3.99    if is_axiom_number axiom_names num then
   3.100 -    apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1))))
   3.101 +    apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1))))
   3.102    else
   3.103      apfst (insert (op =) (raw_prefix, num))
   3.104  
     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 13:55:30 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Thu Aug 26 14:05:22 2010 +0200
     4.3 @@ -19,7 +19,7 @@
     4.4    val prepare_problem :
     4.5      Proof.context -> bool -> bool -> bool -> bool -> term list -> term
     4.6      -> ((string * 'a) * thm) list
     4.7 -    -> string problem * string Symtab.table * int * (string * 'a) vector
     4.8 +    -> string problem * string Symtab.table * int * (string * 'a) list vector
     4.9  end;
    4.10  
    4.11  structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    4.12 @@ -271,7 +271,7 @@
    4.13      val (supers', arity_clauses) = make_arity_clauses thy tycons supers
    4.14      val class_rel_clauses = make_class_rel_clauses thy subs supers'
    4.15    in
    4.16 -    (Vector.fromList axiom_names,
    4.17 +    (axiom_names |> map single |> Vector.fromList,
    4.18       (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
    4.19    end
    4.20  
     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 13:55:30 2010 +0200
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 14:05:22 2010 +0200
     5.3 @@ -6,7 +6,7 @@
     5.4  
     5.5  signature SLEDGEHAMMER_UTIL =
     5.6  sig
     5.7 -  val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
     5.8 +  val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option
     5.9    val plural_s : int -> string
    5.10    val serial_commas : string -> string list -> string list
    5.11    val simplify_spaces : string -> string
    5.12 @@ -29,9 +29,9 @@
    5.13  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    5.14  struct
    5.15  
    5.16 -fun find_first_in_vector vec key default =
    5.17 -  Vector.foldl (fn ((key', value'), value) =>
    5.18 -                   if key' = key then value' else value) default vec
    5.19 +fun find_first_in_list_vector vec key =
    5.20 +  Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key
    5.21 +                 | (_, value) => value) NONE vec
    5.22  
    5.23  fun plural_s n = if n = 1 then "" else "s"
    5.24