--- a/src/HOL/Tools/ATP/atp_proof.ML Sun Jul 27 21:11:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jul 28 10:57:33 2014 +0200
@@ -2,6 +2,7 @@
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory
Author: Claire Quigley, Cambridge University Computer Laboratory
Author: Jasmin Blanchette, TU Muenchen
+ Author: Mathias Fleury, ENS Rennes
Abstract representation of ATP proofs and TSTP/SPASS syntax.
*)
@@ -295,7 +296,7 @@
val dummy_phi = AAtom (ATerm (("", []), []))
val dummy_inference = Inference_Source ("", [])
-val dummy_atype = AType(("", []), [])
+val dummy_atype = AType (("", []), [])
(* "skip_term" is there to cope with Waldmeister nonsense such as "theory(equality)". *)
fun parse_dependency x =
@@ -459,16 +460,17 @@
| role_of_tptp_string "type" = Type_Role
| role_of_tptp_string _ = Unknown
-val tptp_binary_op_list = [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if,
- tptp_iff, tptp_not_iff, tptp_equal, tptp_app]
+val tptp_binary_ops =
+ [tptp_and, tptp_not_and, tptp_or, tptp_not_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff,
+ tptp_equal, tptp_app]
fun parse_binary_op x =
- (foldl1 (op ||) (map Scan.this_string tptp_binary_op_list)
- >> (fn c => if c = tptp_equal then "equal" else c)) x
+ (foldl1 (op ||) (map Scan.this_string tptp_binary_ops)
+ >> (fn c => if c = tptp_equal then "equal" else c)) x
fun parse_thf0_type x =
(($$ "(" |-- parse_thf0_type --| $$ ")" || scan_general_id >> (fn t => AType ((t, []), [])))
- -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
+ -- Scan.option ($$ tptp_fun_type |-- parse_thf0_type)
>> (fn (a, NONE) => a
| (a, SOME b) => AFun (a, b))) x
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sun Jul 27 21:11:35 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jul 28 10:57:33 2014 +0200
@@ -116,25 +116,33 @@
(* 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_type ctxt (ty as AType ((a, clss), tys)) =
- let val Ts = map (typ_of_atp_type ctxt) tys in
- (case unprefix_and_unascii type_const_prefix a of
- SOME b => Type (invert_const b, Ts)
- | NONE =>
- if not (null tys) then
- raise ATP_TYPE [ty] (* only "tconst"s have type arguments *)
- else
- (case unprefix_and_unascii tfree_prefix a of
- SOME b => make_tfree ctxt b
- | NONE =>
- (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
- Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
- forces us to use a type parameter in all cases. *)
- Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
- (if null clss then @{sort type} else map class_of_atp_class clss))))
+ let val Ts = map (typ_of_atp_type ctxt) tys in
+ (case unprefix_and_unascii type_const_prefix a of
+ SOME b => Type (invert_const b, Ts)
+ | NONE =>
+ if not (null tys) then
+ raise ATP_TYPE [ty] (* only "tconst"s have type arguments *)
+ else
+ (case unprefix_and_unascii tfree_prefix a of
+ SOME b => make_tfree ctxt b
+ | NONE =>
+ (* The term could be an Isabelle variable or a variable from the ATP, say "X1" or "_5018".
+ Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
+ forces us to use a type parameter in all cases. *)
+ Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
+ (if null clss then @{sort type} else map class_of_atp_class clss))))
+ end
+ | typ_of_atp_type ctxt (AFun (ty1, ty2)) = typ_of_atp_type ctxt ty1 --> typ_of_atp_type ctxt ty2
+
+fun atp_type_of_atp_term (ATerm ((s, _), us)) =
+ let val tys = map atp_type_of_atp_term us in
+ if s = tptp_fun_type then
+ (case tys of
+ [ty1, ty2] => AFun (ty1, ty2)
+ | _ => raise ATP_TYPE tys)
+ else
+ AType ((s, []), tys)
end
- | typ_of_atp_type ctxt (AFun (a, tys)) = typ_of_atp_type ctxt a --> typ_of_atp_type ctxt tys
-
-fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
fun typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term