--- 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
--- 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))
--- 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))
--- 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
--- 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"