--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 03 00:10:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 03 01:04:03 2011 +0200
@@ -13,22 +13,22 @@
type type_system = Sledgehammer_ATP_Translate.type_system
type minimize_command = string list -> string
type metis_params =
- string * minimize_command * string proof * int
+ string * minimize_command * type_system * string proof * int
* (string * locality) list vector * thm * int
type isar_params =
- Proof.context * bool * type_system * int * string Symtab.table
- * int list list
+ Proof.context * bool * int * string Symtab.table * int list list
type text_result = string * (string * locality) list
val repair_conjecture_shape_and_fact_names :
- string -> int list list -> int -> (string * locality) list vector
+ type_system -> string -> int list list -> int
+ -> (string * locality) list vector
-> int list list * int * (string * locality) list vector
val used_facts_in_atp_proof :
- int -> (string * locality) list vector -> string proof
+ type_system -> int -> (string * locality) list vector -> string proof
-> (string * locality) list
val is_unsound_proof :
- int list list -> int -> (string * locality) list vector -> string proof
- -> bool
+ type_system -> 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
@@ -53,11 +53,10 @@
type minimize_command = string list -> string
type metis_params =
- string * minimize_command * string proof * int
+ string * minimize_command * type_system * string proof * int
* (string * locality) list vector * thm * int
type isar_params =
- Proof.context * bool * type_system * int * string Symtab.table
- * int list list
+ Proof.context * bool * int * string Symtab.table * int list list
type text_result = string * (string * locality) list
fun is_head_digit s = Char.isDigit (String.sub (s, 0))
@@ -96,10 +95,12 @@
#> raw_explode #> filter_out Symbol.is_blank #> parse_clause_formula_relation
#> fst
-val unprefix_fact_number = space_implode "_" o tl o space_explode "_"
+fun maybe_unprefix_fact_number type_sys =
+ polymorphism_of_type_sys type_sys <> Polymorphic
+ ? (space_implode "_" o tl o space_explode "_")
-fun repair_conjecture_shape_and_fact_names output conjecture_shape fact_offset
- fact_names =
+fun repair_conjecture_shape_and_fact_names type_sys output conjecture_shape
+ fact_offset fact_names =
if String.isSubstring set_ClauseFormulaRelationN output then
let
val j0 = hd (hd conjecture_shape)
@@ -111,7 +112,7 @@
|> map (fn s => find_index (curry (op =) s) seq + 1)
fun names_for_number j =
j |> AList.lookup (op =) name_map |> these
- |> map_filter (try (unascii_of o unprefix_fact_number
+ |> map_filter (try (unascii_of o maybe_unprefix_fact_number type_sys
o unprefix fact_prefix))
|> map (fn name =>
(name, name |> find_first_in_list_vector fact_names |> the)
@@ -126,16 +127,16 @@
val vampire_step_prefix = "f" (* grrr... *)
-fun resolve_fact _ fact_names ((_, SOME s)) =
+fun resolve_fact type_sys _ fact_names ((_, SOME s)) =
(case try (unprefix fact_prefix) s of
SOME s' =>
- let val s' = s' |> unprefix_fact_number |> unascii_of in
+ let val s' = s' |> maybe_unprefix_fact_number type_sys |> unascii_of in
case find_first_in_list_vector fact_names s' of
SOME x => [(s', x)]
| NONE => []
end
| NONE => [])
- | resolve_fact facts_offset 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 =>
let val j = j - facts_offset in
@@ -156,26 +157,27 @@
| NONE => ~1
in if k >= 0 then [k] else [] end
-fun is_fact conjecture_shape = not o null o resolve_fact 0 conjecture_shape
+fun is_fact type_sys conjecture_shape =
+ not o null o resolve_fact type_sys 0 conjecture_shape
fun is_conjecture conjecture_shape =
not o null o resolve_conjecture conjecture_shape
-fun add_fact facts_offset fact_names (Inference (name, _, [])) =
- append (resolve_fact facts_offset fact_names name)
- | add_fact _ _ _ = I
+fun add_fact type_sys facts_offset fact_names (Inference (name, _, [])) =
+ append (resolve_fact type_sys facts_offset fact_names name)
+ | add_fact _ _ _ _ = I
-fun used_facts_in_atp_proof facts_offset fact_names atp_proof =
+fun used_facts_in_atp_proof type_sys facts_offset fact_names atp_proof =
if null atp_proof then Vector.foldl (op @) [] fact_names
- else fold (add_fact facts_offset fact_names) atp_proof []
+ else fold (add_fact type_sys 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 facts_offset fact_names =
+fun is_unsound_proof type_sys 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
+ o used_facts_in_atp_proof type_sys facts_offset fact_names
(** Soft-core proof reconstruction: Metis one-liner **)
@@ -210,11 +212,11 @@
List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
-fun metis_proof_text (banner, minimize_command, atp_proof, facts_offset,
- fact_names, goal, i) =
+fun metis_proof_text (banner, minimize_command, type_sys, atp_proof,
+ facts_offset, fact_names, goal, i) =
let
val (chained, extra) =
- atp_proof |> used_facts_in_atp_proof facts_offset fact_names
+ atp_proof |> used_facts_in_atp_proof type_sys facts_offset fact_names
|> split_used_facts
val n = Logic.count_prems (prop_of goal)
in
@@ -528,11 +530,12 @@
(* Discard facts; consolidate adjacent lines that prove the same formula, since
they differ only in type information.*)
-fun add_line _ _ (line as Definition _) lines = line :: lines
- | add_line conjecture_shape fact_names (Inference (name, t, [])) lines =
+fun add_line _ _ _ (line as Definition _) lines = line :: lines
+ | add_line type_sys conjecture_shape fact_names (Inference (name, t, []))
+ lines =
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or
definitions. *)
- if is_fact fact_names name then
+ if is_fact type_sys fact_names name then
(* Facts are not proof lines. *)
if is_only_type_information t then
map (replace_dependencies_in_line (name, [])) lines
@@ -546,7 +549,7 @@
Inference (name, s_not t, []) :: lines
else
map (replace_dependencies_in_line (name, [])) lines
- | add_line _ _ (Inference (name, t, deps)) lines =
+ | add_line _ _ _ (Inference (name, t, deps)) lines =
(* Type information will be deleted later; skip repetition test. *)
if is_only_type_information t then
Inference (name, t, deps) :: lines
@@ -574,12 +577,12 @@
fun is_bad_free frees (Free x) = not (member (op =) frees x)
| is_bad_free _ _ = false
-fun add_desired_line _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
+fun add_desired_line _ _ _ _ _ (line as Definition (name, _, _)) (j, lines) =
(j, line :: map (replace_dependencies_in_line (name, [])) lines)
- | add_desired_line isar_shrink_factor conjecture_shape fact_names frees
- (Inference (name, t, deps)) (j, lines) =
+ | add_desired_line type_sys isar_shrink_factor conjecture_shape fact_names
+ frees (Inference (name, t, deps)) (j, lines) =
(j + 1,
- if is_fact fact_names name orelse
+ if is_fact type_sys fact_names name orelse
is_conjecture conjecture_shape name orelse
(* the last line must be kept *)
j = 0 orelse
@@ -615,22 +618,24 @@
fun smart_case_split [] facts = ByMetis facts
| smart_case_split proofs facts = CaseSplit (proofs, facts)
-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 facts_offset fact_names name)))
+fun add_fact_from_dependency type_sys conjecture_shape facts_offset fact_names
+ name =
+ if is_fact type_sys fact_names name then
+ apsnd (union (op =)
+ (map fst (resolve_fact type_sys 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 facts_offset fact_names j
- (Inference (name, t, deps)) =
+ | step_for_line type_sys 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 facts_offset
- fact_names)
+ ByMetis (fold (add_fact_from_dependency type_sys conjecture_shape
+ facts_offset fact_names)
deps ([], [])))
fun repair_name "$true" = "c_True"
@@ -651,14 +656,15 @@
|> nasty_atp_proof pool
|> map_term_names_in_atp_proof repair_name
|> decode_lines ctxt type_sys tfrees
- |> rpair [] |-> fold_rev (add_line conjecture_shape fact_names)
+ |> rpair [] |-> fold_rev (add_line type_sys conjecture_shape fact_names)
|> rpair [] |-> fold_rev add_nontrivial_line
- |> rpair (0, []) |-> fold_rev (add_desired_line isar_shrink_factor
- conjecture_shape fact_names frees)
+ |> rpair (0, [])
+ |-> fold_rev (add_desired_line type_sys isar_shrink_factor
+ conjecture_shape fact_names frees)
|> snd
in
(if null params then [] else [Fix params]) @
- map2 (step_for_line conjecture_shape facts_offset fact_names)
+ map2 (step_for_line type_sys conjecture_shape facts_offset fact_names)
(length lines downto 1) lines
end
@@ -950,9 +956,9 @@
(if n <> 1 then "next" else "qed")
in do_proof end
-fun isar_proof_text (ctxt, debug, type_sys, isar_shrink_factor, pool,
- conjecture_shape)
- (metis_params as (_, _, atp_proof, facts_offset, fact_names, goal, i)) =
+fun isar_proof_text (ctxt, debug, isar_shrink_factor, pool, conjecture_shape)
+ (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) []