# HG changeset patch # User blanchet # Date 1282824322 -7200 # Node ID 61cf050f8b2ef21c51ec9a3251d9cf3d5fc4a2fa # Parent bf27c24ba2240ea9705b0e831d3d3e82b9d0e7e3 improve SPASS hack, when a clause comes from several facts diff -r bf27c24ba224 -r 61cf050f8b2e src/HOL/Tools/Sledgehammer/sledgehammer.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 13:55:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Aug 26 14:05:22 2010 +0200 @@ -38,7 +38,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * locality) vector, + axiom_names: (string * locality) list vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -107,7 +107,7 @@ atp_run_time_in_msecs: int, output: string, proof: string, - axiom_names: (string * locality) vector, + axiom_names: (string * locality) list vector, conjecture_shape: int list list} type prover = params -> minimize_command -> problem -> prover_result @@ -175,6 +175,7 @@ #> snd #> Substring.string #> strip_spaces_except_between_ident_chars #> explode #> parse_clause_formula_relation #> fst +(* TODO: move to "Sledgehammer_Proof_Reconstruct.ML" *) fun repair_conjecture_shape_and_theorem_names output conjecture_shape axiom_names = if String.isSubstring set_ClauseFormulaRelationN output then @@ -189,19 +190,17 @@ conjecture_prefix ^ string_of_int (j - j0) |> AList.find (fn (s, ss) => member (op =) ss s) name_map |> map (fn s => find_index (curry (op =) s) seq + 1) - fun name_for_number j = - let - val axioms = - j |> AList.lookup (op =) name_map |> these - |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of - val loc = - case axioms of - [axiom] => find_first_in_vector axiom_names axiom General - | _ => General - in (axioms |> space_implode " ", loc) end + fun names_for_number j = + j |> AList.lookup (op =) name_map |> these + |> map_filter (try (unprefix axiom_prefix)) |> map unascii_of + |> map (fn name => + (name, name |> find_first_in_list_vector axiom_names + |> the) + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) in (conjecture_shape |> map (maps renumber_conjecture), - seq |> map name_for_number |> Vector.fromList) + seq |> map names_for_number |> Vector.fromList) end else (conjecture_shape, axiom_names) @@ -253,7 +252,7 @@ if the_dest_dir = "" then File.tmp_path probfile else if File.exists (Path.explode the_dest_dir) then Path.append (Path.explode the_dest_dir) probfile - else error ("No such directory: " ^ the_dest_dir ^ ".") + else error ("No such directory: " ^ quote the_dest_dir ^ ".") end; val measure_run_time = verbose orelse Config.get ctxt measure_runtime diff -r bf27c24ba224 -r 61cf050f8b2e src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 13:55:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML Thu Aug 26 14:05:22 2010 +0200 @@ -586,9 +586,8 @@ val local_facts = ProofContext.facts_of ctxt val named_locals = local_facts |> Facts.dest_static [] val is_chained = member Thm.eq_thm chained_ths - (* Unnamed, not chained formulas with schematic variables are omitted, - because they are rejected by the backticks (`...`) parser for some - reason. *) + (* Unnamed nonchained formulas with schematic variables are omitted, because + they are rejected by the backticks (`...`) parser for some reason. *) fun is_good_unnamed_local th = forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) diff -r bf27c24ba224 -r 61cf050f8b2e src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 13:55:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML Thu Aug 26 14:05:22 2010 +0200 @@ -10,18 +10,16 @@ sig type locality = Sledgehammer_Fact_Filter.locality type minimize_command = string list -> string - - val metis_proof_text: - bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list - val isar_proof_text: + type metis_params = + bool * minimize_command * string * (string * locality) list vector * thm + * int + type isar_params = string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list - val proof_text: - bool -> string Symtab.table * bool * int * Proof.context * int list list - -> bool * minimize_command * string * (string * locality) vector * thm * int - -> string * (string * locality) list + type text_result = string * (string * locality) list + + val metis_proof_text : metis_params -> text_result + val isar_proof_text : isar_params -> metis_params -> text_result + val proof_text : bool -> isar_params -> metis_params -> text_result end; structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = @@ -34,6 +32,11 @@ open Sledgehammer_Translate type minimize_command = string list -> string +type metis_params = + bool * minimize_command * string * (string * locality) list vector * thm * int +type isar_params = + string Symtab.table * bool * int * Proof.context * int list list +type text_result = string * (string * locality) list (* Simple simplifications to ensure that sort annotations don't leave a trail of spurious "True"s. *) @@ -61,7 +64,7 @@ fun index_in_shape x = find_index (exists (curry (op =) x)) fun is_axiom_number axiom_names num = num > 0 andalso num <= Vector.length axiom_names andalso - fst (Vector.sub (axiom_names, num - 1)) <> "" + not (null (Vector.sub (axiom_names, num - 1))) fun is_conjecture_number conjecture_shape num = index_in_shape num conjecture_shape >= 0 @@ -565,12 +568,10 @@ "108. ... [input]". *) fun used_facts_in_atp_proof axiom_names atp_proof = let - fun axiom_name_at_index num = + fun axiom_names_at_index num = let val j = Int.fromString num |> the_default ~1 in - if is_axiom_number axiom_names j then - SOME (Vector.sub (axiom_names, j - 1)) - else - NONE + if is_axiom_number axiom_names j then Vector.sub (axiom_names, j - 1) + else [] end val tokens_of = String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_") @@ -579,17 +580,19 @@ (case strip_prefix_and_unascii axiom_prefix (List.last rest) of SOME name => if member (op =) rest "file" then - SOME (name, find_first_in_vector axiom_names name General) + ([(name, name |> find_first_in_list_vector axiom_names |> the)] + handle Option.Option => + error ("No such fact: " ^ quote name ^ ".")) else - axiom_name_at_index num - | NONE => axiom_name_at_index num) + axiom_names_at_index num + | NONE => axiom_names_at_index num) else - NONE - | do_line (num :: "0" :: "Inp" :: _) = axiom_name_at_index num + [] + | do_line (num :: "0" :: "Inp" :: _) = axiom_names_at_index num | do_line (num :: rest) = - (case List.last rest of "input" => axiom_name_at_index num | _ => NONE) - | do_line _ = NONE - in atp_proof |> split_proof_lines |> map_filter (do_line o tokens_of) end + (case List.last rest of "input" => axiom_names_at_index num | _ => []) + | do_line _ = [] + in atp_proof |> split_proof_lines |> maps (do_line o tokens_of) end val indent_size = 2 val no_label = ("", ~1) @@ -663,7 +666,7 @@ fun add_fact_from_dep axiom_names num = if is_axiom_number axiom_names num then - apsnd (insert (op =) (fst (Vector.sub (axiom_names, num - 1)))) + apsnd (union (op =) (map fst (Vector.sub (axiom_names, num - 1)))) else apfst (insert (op =) (raw_prefix, num)) diff -r bf27c24ba224 -r 61cf050f8b2e src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 13:55:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Thu Aug 26 14:05:22 2010 +0200 @@ -19,7 +19,7 @@ val prepare_problem : Proof.context -> bool -> bool -> bool -> bool -> term list -> term -> ((string * 'a) * thm) list - -> string problem * string Symtab.table * int * (string * 'a) vector + -> string problem * string Symtab.table * int * (string * 'a) list vector end; structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE = @@ -271,7 +271,7 @@ val (supers', arity_clauses) = make_arity_clauses thy tycons supers val class_rel_clauses = make_class_rel_clauses thy subs supers' in - (Vector.fromList axiom_names, + (axiom_names |> map single |> Vector.fromList, (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses)) end diff -r bf27c24ba224 -r 61cf050f8b2e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 13:55:30 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Aug 26 14:05:22 2010 +0200 @@ -6,7 +6,7 @@ signature SLEDGEHAMMER_UTIL = sig - val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b + val find_first_in_list_vector : (''a * 'b) list vector -> ''a -> 'b option val plural_s : int -> string val serial_commas : string -> string list -> string list val simplify_spaces : string -> string @@ -29,9 +29,9 @@ structure Sledgehammer_Util : SLEDGEHAMMER_UTIL = struct -fun find_first_in_vector vec key default = - Vector.foldl (fn ((key', value'), value) => - if key' = key then value' else value) default vec +fun find_first_in_list_vector vec key = + Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key + | (_, value) => value) NONE vec fun plural_s n = if n = 1 then "" else "s"