--- a/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon May 02 01:20:28 2011 +0200
@@ -250,15 +250,15 @@
>> (fn (ss1, ss2) => implode ss1 ^ implode ss2)
(* Generalized first-order terms, which include file names, numbers, etc. *)
-fun parse_annotation strict x =
+fun parse_annotation x =
((scan_general_id ::: Scan.repeat ($$ " " |-- scan_general_id)
- >> (strict ? filter (is_some o Int.fromString)))
- -- Scan.optional (parse_annotation strict) [] >> op @
- || $$ "(" |-- parse_annotations strict --| $$ ")"
- || $$ "[" |-- parse_annotations strict --| $$ "]") x
-and parse_annotations strict x =
- (Scan.optional (parse_annotation strict
- ::: Scan.repeat ($$ "," |-- parse_annotation strict)) []
+ >> filter (is_some o Int.fromString))
+ -- Scan.optional parse_annotation [] >> op @
+ || $$ "(" |-- parse_annotations --| $$ ")"
+ || $$ "[" |-- parse_annotations --| $$ "]") x
+and parse_annotations x =
+ (Scan.optional (parse_annotation
+ ::: Scan.repeat ($$ "," |-- parse_annotation)) []
>> flat) x
(* Vampire proof lines sometimes contain needless information such as "(0:3)",
@@ -295,7 +295,9 @@
>> (fn ((q, ts), phi) =>
(* FIXME: TFF *)
AQuant (q, map (rpair NONE o fo_term_head) ts, phi))
- || $$ "~" |-- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom) >> mk_anot
+ || (Scan.repeat ($$ "~") >> length)
+ -- ($$ "(" |-- parse_formula --| $$ ")" || parse_atom)
+ >> (fn (n, phi) => phi |> n div 2 = 1 ? mk_anot)
|| parse_atom)
-- Scan.option ((Scan.this_string "=>" >> K AImplies
|| Scan.this_string "<=>" >> K AIff
@@ -307,8 +309,8 @@
| (phi1, SOME (c, phi2)) => mk_aconn c (phi1, phi2))) x
val parse_tstp_extra_arguments =
- Scan.optional ($$ "," |-- parse_annotation false
- --| Scan.option ($$ "," |-- parse_annotations false)) []
+ Scan.optional ($$ "," |-- parse_annotation
+ --| Scan.option ($$ "," |-- parse_annotations)) []
val vampire_unknown_fact = "unknown"
val tofof_fact_prefix = "fof_"
@@ -355,7 +357,7 @@
scan_general_id --| $$ "." -- parse_formula
--| Scan.option parse_vampire_braced_stuff
--| Scan.option parse_vampire_parenthesized_detritus
- -- parse_annotation true
+ -- parse_annotation
>> (fn ((num, phi), deps) =>
Inference ((num, NONE), phi, map (rpair NONE) deps))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Mon May 02 01:20:28 2011 +0200
@@ -13,10 +13,11 @@
type type_system = Sledgehammer_ATP_Translate.type_system
type minimize_command = string list -> string
type metis_params =
- string * type_system * minimize_command * string proof * int
+ string * minimize_command * string proof * int
* (string * locality) list vector * thm * int
type isar_params =
- string Symtab.table * bool * int * Proof.context * int list list
+ Proof.context * bool * type_system * int * string Symtab.table
+ * int list list
type text_result = string * (string * locality) list
val repair_conjecture_shape_and_fact_names :
@@ -53,10 +54,11 @@
type minimize_command = string list -> string
type metis_params =
- string * type_system * minimize_command * string proof * int
+ string * minimize_command * string proof * int
* (string * locality) list vector * thm * int
type isar_params =
- string Symtab.table * bool * int * Proof.context * int list list
+ Proof.context * bool * type_system * 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))
@@ -193,13 +195,10 @@
fun using_labels [] = ""
| using_labels ls =
"using " ^ space_implode " " (map string_for_label ls) ^ " "
-fun metis_name type_sys =
- if is_type_sys_fairly_sound type_sys then "metisFT" else "metis"
-fun metis_call type_sys ss = command_call (metis_name type_sys) ss
-fun metis_command type_sys i n (ls, ss) =
- using_labels ls ^ apply_on_subgoal "" i n ^ metis_call type_sys ss
-fun metis_line banner type_sys i n ss =
- try_command_line banner (metis_command type_sys i n ([], ss))
+fun metis_name full_types = if full_types then "metisFT" else "metis"
+fun metis_call full_types ss = command_call (metis_name full_types) ss
+fun metis_command full_types i n (ls, ss) =
+ using_labels ls ^ apply_on_subgoal "" i n ^ metis_call full_types ss
fun minimize_line _ [] = ""
| minimize_line minimize_command ss =
case minimize_command ss of
@@ -212,17 +211,17 @@
List.partition (curry (op =) Chained o snd)
#> pairself (sort_distinct (string_ord o pairself fst))
-fun metis_proof_text (banner, type_sys, minimize_command, atp_proof,
- facts_offset, fact_names, goal, i) =
+fun metis_proof_text (banner, minimize_command, atp_proof, facts_offset,
+ fact_names, goal, i) =
let
- val (chained_lemmas, other_lemmas) =
+ val (chained, extra) =
atp_proof |> used_facts_in_atp_proof facts_offset fact_names
|> split_used_facts
val n = Logic.count_prems (prop_of goal)
in
- (metis_line banner type_sys i n (map fst other_lemmas) ^
- minimize_line minimize_command (map fst (other_lemmas @ chained_lemmas)),
- other_lemmas @ chained_lemmas)
+ (try_command_line banner (metis_command false i n ([], map fst extra)) ^
+ minimize_line minimize_command (map fst (extra @ chained)),
+ extra @ chained)
end
(** Hard-core proof reconstruction: structured Isar proofs **)
@@ -955,9 +954,9 @@
(if n <> 1 then "next" else "qed")
in do_proof end
-fun isar_proof_text (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (metis_params as (_, type_sys, _, atp_proof, facts_offset, fact_names,
- goal, i)) =
+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)) =
let
val (params, hyp_ts, concl_t) = strip_subgoal goal i
val frees = fold Term.add_frees (concl_t :: hyp_ts) []
@@ -973,7 +972,7 @@
|> then_chain_proof
|> kill_useless_labels_in_proof
|> relabel_proof
- |> string_for_proof ctxt type_sys i n of
+ |> string_for_proof ctxt (is_type_sys_fairly_sound type_sys) i n of
"" => "\nNo structured proof available (proof too short)."
| proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon May 02 01:20:28 2011 +0200
@@ -779,6 +779,8 @@
if pred_sym then `I tptp_tff_bool_type else mangled_type_name res_T)
end
+fun is_polymorphic_type T = fold_atyps (fn TVar _ => K true | _ => I) T false
+
fun formula_line_for_sym_decl ctxt type_sys n s j (s', T_args, T, _, ary) =
let
val (arg_Ts, res_T) = n_ary_strip_type ary T
@@ -787,7 +789,8 @@
val bound_tms =
bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
val bound_Ts =
- arg_Ts |> map (if n > 1 then SOME else K NONE)
+ arg_Ts |> map (fn T => if n > 1 orelse is_polymorphic_type T then SOME T
+ else NONE)
in
Formula (sym_decl_prefix ^ ascii_of s ^ "_" ^ string_of_int j, Axiom,
CombConst ((s, s'), T, T_args)
@@ -807,11 +810,13 @@
val decls =
case decls of
decl :: (decls' as _ :: _) =>
- if forall (curry (op =) (result_type_of_decl decl)
- o result_type_of_decl) decls' then
- [decl]
- else
- decls
+ let val T = result_type_of_decl decl in
+ if forall ((fn T' => Type.raw_instance (T', T))
+ o result_type_of_decl) decls' then
+ [decl]
+ else
+ decls
+ end
| _ => decls
val n = length decls
val decls =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 01:05:50 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 01:20:28 2011 +0200
@@ -582,10 +582,11 @@
"\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
else
"")
- val isar_params = (pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
+ val isar_params =
+ (ctxt, debug, type_sys, isar_shrink_factor, pool, conjecture_shape)
val metis_params =
- (proof_banner auto, type_sys, minimize_command, atp_proof, facts_offset,
- fact_names, goal, subgoal)
+ (proof_banner auto, minimize_command, atp_proof, facts_offset, fact_names,
+ goal, subgoal)
val (outcome, (message, used_facts)) =
case outcome of
NONE =>