--- a/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML Wed Dec 18 22:55:20 2013 +0100
@@ -8,6 +8,7 @@
signature ATP_PROOF =
sig
+ type 'a atp_type = 'a ATP_Problem.atp_type
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
type atp_formula_role = ATP_Problem.atp_formula_role
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
@@ -38,8 +39,7 @@
type ('a, 'b) atp_step =
atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
- type 'a atp_proof =
- (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
+ type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
val agsyhol_core_rule : string
val satallax_core_rule : string
@@ -50,23 +50,18 @@
val short_output : bool -> string -> string
val string_of_atp_failure : atp_failure -> string
val extract_important_message : string -> string
- val extract_known_atp_failure :
- (atp_failure * string) list -> string -> atp_failure option
+ val extract_known_atp_failure : (atp_failure * string) list -> string -> atp_failure option
val extract_tstplike_proof_and_outcome :
bool -> (string * string) list -> (atp_failure * string) list -> string
-> string * atp_failure option
val is_same_atp_step : atp_step_name -> atp_step_name -> bool
val scan_general_id : string list -> string * string list
- val parse_formula :
- string list
- -> (string, 'a, (string, 'a) atp_term, string) atp_formula * string list
- val atp_proof_of_tstplike_proof :
- string atp_problem -> string -> string atp_proof
+ val parse_formula : string list ->
+ (string, string atp_type, (string, string atp_type) atp_term, string) atp_formula * string list
+ val atp_proof_of_tstplike_proof : string atp_problem -> string -> string atp_proof
val clean_up_atp_proof_dependencies : string atp_proof -> string atp_proof
- val map_term_names_in_atp_proof :
- (string -> string) -> string atp_proof -> string atp_proof
- val nasty_atp_proof :
- string Symtab.table -> string atp_proof -> string atp_proof
+ val map_term_names_in_atp_proof : (string -> string) -> string atp_proof -> string atp_proof
+ val nasty_atp_proof : string Symtab.table -> string atp_proof -> string atp_proof
end;
structure ATP_Proof : ATP_PROOF =
@@ -203,11 +198,9 @@
| _ => raise Fail "not Vampire")
end
-type ('a, 'b) atp_step =
- atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
+type ('a, 'b) atp_step = atp_step_name * atp_formula_role * 'a * 'b * atp_step_name list
-type 'a atp_proof =
- (('a, 'a, ('a, 'a) atp_term, 'a) atp_formula, string) atp_step list
+type 'a atp_proof = (('a, 'a, ('a, 'a atp_type) atp_term, 'a) atp_formula, string) atp_step list
(**** PARSING OF TSTP FORMAT ****)
@@ -245,8 +238,7 @@
(parse_inference_source >> snd
|| scan_general_id --| skip_term >> single) x
and parse_dependencies x =
- (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency)
- >> flat) x
+ (parse_dependency ::: Scan.repeat ($$ "," |-- parse_dependency) >> flat) x
and parse_file_source x =
(Scan.this_string "file" |-- $$ "(" |-- scan_general_id
-- Scan.option ($$ "," |-- scan_general_id) --| $$ ")") x
@@ -266,19 +258,28 @@
fun list_app (f, args) = fold (fn arg => fn f => ATerm ((tptp_app, []), [f, arg])) args f
+fun parse_sort x = scan_general_id x
+and parse_sorts x = (parse_sort ::: Scan.repeat ($$ "&" |-- parse_sort)) x
+
+fun parse_type x =
+ (scan_general_id --| Scan.option ($$ "{" |-- parse_sorts --| $$ "}")
+ -- Scan.optional ($$ "(" |-- parse_types --| $$ ")") []
+ >> AType) x
+and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
+
(* We currently ignore TFF and THF types. *)
-fun parse_type_stuff x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
+fun parse_type_signature x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
and parse_arg x =
- ($$ "(" |-- parse_term --| $$ ")" --| parse_type_stuff
- || scan_general_id --| parse_type_stuff
- -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
- >> (ATerm o apfst (rpair []))) x
+ ($$ "(" |-- parse_term --| $$ ")" --| parse_type_signature
+ || scan_general_id --| parse_type_signature
+ -- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
+ -- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
+ >> ATerm) x
and parse_term x = (parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg) >> list_app) x
and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
fun parse_atom x =
- (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal
- -- parse_term)
+ (parse_term -- Scan.option (Scan.option ($$ tptp_not_infix) --| $$ tptp_equal -- parse_term)
>> (fn (u1, NONE) => AAtom u1
| (u1, SOME (neg, u2)) =>
AAtom (ATerm (("equal", []), [u1, u2])) |> is_some neg ? mk_anot)) x
@@ -424,8 +425,7 @@
val parse_dot_name = scan_general_id --| $$ "." --| scan_general_id
val parse_spass_annotations =
- Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name
- --| Scan.option ($$ ","))) []
+ Scan.optional ($$ ":" |-- Scan.repeat (parse_dot_name --| Scan.option ($$ ","))) []
(* It is not clear why some literals are followed by sequences of stars and/or
pluses. We ignore them. *)
@@ -460,7 +460,7 @@
fun parse_spass_pirate_dependency x = (Scan.option ($$ "-") |-- scan_general_id) x
fun parse_spass_pirate_dependencies x =
- (parse_spass_pirate_dependency ::: Scan.repeat ($$ "," |-- parse_spass_pirate_dependency)) x
+ Scan.repeat (parse_spass_pirate_dependency --| Scan.option ($$ "," || $$ " ")) x
fun parse_spass_pirate_file_source x =
((Scan.this_string "Input" || Scan.this_string "Conj") |-- $$ "(" |-- scan_general_id
--| $$ ")") x
@@ -517,28 +517,37 @@
(case core_of_agsyhol_proof tstp of
SOME facts => facts |> map (core_inference agsyhol_core_rule)
| NONE =>
- tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
+ tstp ^ "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
|> parse_proof problem
|> perhaps (try (sort (vampire_step_name_ord o pairself #1))))
fun clean_up_dependencies _ [] = []
| clean_up_dependencies seen ((name, role, u, rule, deps) :: steps) =
- (name, role, u, rule,
- map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
+ (name, role, u, rule, map_filter (fn dep => find_first (is_same_atp_step dep) seen) deps) ::
clean_up_dependencies (name :: seen) steps
fun clean_up_atp_proof_dependencies proof = clean_up_dependencies [] proof
fun map_term_names_in_atp_proof f =
let
- fun do_term (ATerm ((s, tys), ts)) = ATerm ((f s, tys), map do_term ts)
- fun do_formula (AQuant (q, xs, phi)) =
- AQuant (q, map (apfst f) xs, do_formula phi)
- | do_formula (AConn (c, phis)) = AConn (c, map do_formula phis)
- | do_formula (AAtom t) = AAtom (do_term t)
- fun do_step (name, role, phi, rule, deps) =
- (name, role, do_formula phi, rule, deps)
- in map do_step end
+ fun map_type (AType (s, tys)) = AType (f s, map map_type tys)
+ | map_type (AFun (ty, ty')) = AFun (map_type ty, map_type ty')
+ | map_type (APi (ss, ty)) = APi (map f ss, map_type ty)
+
+ fun map_term (ATerm ((s, tys), ts)) = ATerm ((f s, map map_type tys), map map_term ts)
+ | map_term (AAbs (((s, ty), tm), args)) =
+ AAbs (((f s, map_type ty), map_term tm), map map_term args)
+
+ fun map_formula (AQuant (q, xs, phi)) =
+ AQuant (q, map (apfst f) xs, map_formula phi)
+ | map_formula (AConn (c, phis)) = AConn (c, map map_formula phis)
+ | map_formula (AAtom t) = AAtom (map_term t)
+
+ fun map_step (name, role, phi, rule, deps) =
+ (name, role, map_formula phi, rule, deps)
+ in
+ map map_step
+ end
fun nasty_name pool s = s |> Symtab.lookup pool |> the_default s
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Wed Dec 18 22:55:20 2013 +0100
@@ -8,6 +8,7 @@
signature ATP_PROOF_RECONSTRUCT =
sig
+ type 'a atp_type = 'a ATP_Problem.atp_type
type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
type stature = ATP_Problem_Generate.stature
@@ -32,9 +33,9 @@
val exists_of : term -> term -> term
val unalias_type_enc : string -> string list
val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
- (string, string) atp_term -> term
+ (string, string atp_type) atp_term -> term
val prop_of_atp : Proof.context -> bool -> int Symtab.table ->
- (string, string, (string, string) atp_term, string) atp_formula -> term
+ (string, string, (string, string atp_type) atp_term, string) atp_formula -> term
val used_facts_in_atp_proof :
Proof.context -> (string * stature) list vector -> string atp_proof -> (string * stature) list
@@ -107,20 +108,20 @@
TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
end
-exception ATP_TERM of (string, string) atp_term list
+exception ATP_TERM of (string, string atp_type) atp_term list
exception ATP_FORMULA of
- (string, string, (string, string) atp_term, string) atp_formula list
+ (string, string, (string, string atp_type) atp_term, string) atp_formula list
exception SAME of unit
-(* Type variables are given the basic sort "HOL.type". Some will later be
- constrained by information from type literals, or by type inference. *)
+(* Type variables are given the basic sort "HOL.type". Some will later be constrained by information
+ from type literals, or by type inference. *)
fun typ_of_atp ctxt (u as ATerm ((a, _), us)) =
let val Ts = map (typ_of_atp ctxt) us in
(case unprefix_and_unascii type_const_prefix a of
SOME b => Type (invert_const b, Ts)
| NONE =>
if not (null us) then
- raise ATP_TERM [u] (* only "tconst"s have type arguments *)
+ raise ATP_TERM [u] (* only "tconst"s have type arguments *)
else
(case unprefix_and_unascii tfree_prefix a of
SOME b => make_tfree ctxt b
@@ -320,8 +321,8 @@
| norm_var_types t = t
in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end
-(* Interpret an ATP formula as a HOL term, extracting sort constraints as they
- appear in the formula. *)
+(* Interpret an ATP formula as a HOL term, extracting sort constraints as they appear in the
+ formula. *)
fun prop_of_atp ctxt textual sym_tab phi =
let
fun do_formula pos phi =
@@ -337,11 +338,11 @@
do_formula (pos |> c = AImplies ? not) phi1
##>> do_formula pos phi2
#>> (case c of
- AAnd => s_conj
- | AOr => s_disj
- | AImplies => s_imp
- | AIff => s_iff
- | ANot => raise Fail "impossible connective")
+ AAnd => s_conj
+ | AOr => s_disj
+ | AImplies => s_imp
+ | AIff => s_iff
+ | ANot => raise Fail "impossible connective")
| AAtom tm => term_of_atom ctxt textual sym_tab pos tm
| _ => raise ATP_FORMULA [phi])
in
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 18 17:27:17 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Wed Dec 18 22:55:20 2013 +0100
@@ -84,8 +84,7 @@
val SledgehammerN : string
val plain_metis : reconstructor
val select_smt_solver : string -> Proof.context -> Proof.context
- val extract_reconstructor :
- params -> reconstructor -> string * (string * string list) list
+ val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
val is_reconstructor : string -> bool
val is_atp : theory -> string -> bool
val is_smt_prover : Proof.context -> string -> bool
@@ -719,8 +718,7 @@
val ord = effective_term_order ctxt name
val full_proof = isar_proofs |> the_default (mode = Minimize)
val args =
- arguments ctxt full_proof extra
- (slice_timeout |> the_default one_day)
+ arguments ctxt full_proof extra (slice_timeout |> the_default one_day)
(File.shell_path prob_path) (ord, ord_info, sel_weights)
val command =
"(exec 2>&1; " ^ File.shell_path command0 ^ " " ^ args ^ " " ^ ")"
@@ -728,26 +726,18 @@
val _ =
atp_problem
|> lines_of_atp_problem format ord ord_info
- |> cons ("% " ^ command ^ "\n" ^
- (if comment = "" then "" else "% " ^ comment ^ "\n"))
+ |> cons ("% " ^ command ^ "\n" ^ (if comment = "" then "" else "% " ^ comment ^ "\n"))
|> File.write_list prob_path
val ((output, run_time), (atp_proof, outcome)) =
- time_limit generous_slice_timeout Isabelle_System.bash_output
- command
- |>> (if overlord then
- prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n")
- else
- I)
+ time_limit generous_slice_timeout Isabelle_System.bash_output command
+ |>> (if overlord then prefix ("% " ^ command ^ "\n% " ^ timestamp () ^ "\n") else I)
|> fst |> split_time
|> (fn accum as (output, _) =>
(accum,
- extract_tstplike_proof_and_outcome verbose proof_delims
- known_failures output
+ extract_tstplike_proof_and_outcome verbose proof_delims known_failures output
|>> atp_proof_of_tstplike_proof atp_problem
- handle UNRECOGNIZED_ATP_PROOF () =>
- ([], SOME ProofIncomplete)))
- handle TimeLimit.TimeOut =>
- (("", the slice_timeout), ([], SOME TimedOut))
+ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete)))
+ handle TimeLimit.TimeOut => (("", the slice_timeout), ([], SOME TimedOut))
val outcome =
case outcome of
NONE =>