--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Mon Sep 29 10:39:39 2014 +0200
@@ -104,6 +104,7 @@
val mk_aconns :
atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
-> ('a, 'b, 'c, 'd) atp_formula
+ val unmangled_type : string -> (string, 'a) ATP_Problem.atp_term
val unmangled_const : string -> string * (string, 'b) atp_term list
val unmangled_const_name : string -> string list
val helper_table : ((string * bool) * (status * thm) list) list
--- a/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Sep 29 10:39:39 2014 +0200
@@ -348,17 +348,22 @@
>> AType) x
and parse_types x = (parse_type ::: Scan.repeat ($$ "," |-- parse_type)) x
-(* We currently ignore TFF and THF types. *)
-fun parse_type_signature x = Scan.repeat (($$ tptp_has_type || $$ tptp_fun_type) |-- parse_arg) x
+(* We currently half ignore types. *)
+fun parse_optional_type_signature x =
+ Scan.option ($$ tptp_has_type |-- parse_type) x
and parse_arg x =
- ($$ "(" |-- parse_term --| $$ ")" --| parse_type_signature
- || scan_general_id --| parse_type_signature
+ ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature
+ || scan_general_id -- parse_optional_type_signature
-- Scan.optional ($$ "<" |-- parse_types --| $$ ">") []
-- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
- >> ATerm) x
+ >> (fn (((s, ty_opt), tyargs), args) =>
+ if is_tptp_variable s andalso null tyargs andalso null args andalso is_some ty_opt then
+ ATerm ((s, the_list ty_opt), [])
+ else
+ ATerm ((s, tyargs), args))) x
and parse_term x =
(parse_arg -- Scan.repeat ($$ tptp_app |-- parse_arg)
- --| Scan.option parse_type_signature >> list_app) x
+ --| parse_optional_type_signature >> list_app) x
and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
fun parse_atom x =
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 29 10:39:39 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Sep 29 10:39:39 2014 +0200
@@ -156,27 +156,6 @@
SOME s => s
| NONE => raise ATP_CLASS [cls])
-(* 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))))
- 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
@@ -187,6 +166,30 @@
AType ((s, []), tys)
end
+(* 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 native_type_prefix a of
+ SOME b => typ_of_atp_type ctxt (atp_type_of_atp_term (unmangled_type b))
+ | NONE =>
+ (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 typ_of_atp_term ctxt = typ_of_atp_type ctxt o atp_type_of_atp_term
(* Type class literal applied to a type. Returns triple of polarity, class, type. *)
@@ -337,7 +340,7 @@
error "Isar proof reconstruction failed because the ATP proof contains unparsable \
\material."
else if String.isPrefix native_type_prefix s then
- @{const True} (* ignore TPTP type information *)
+ @{const True} (* ignore TPTP type information (needed?) *)
else if s = tptp_equal then
list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}),
map (do_term [] NONE) us)
@@ -620,10 +623,6 @@
#> map_proof_terms (infer_formulas_types ctxt #> map HOLogic.mk_Trueprop)
#> local_prover = waldmeisterN ? repair_waldmeister_endgame
-fun take_distinct_vars seen ((t as Var _) :: ts) =
- if member (op aconv) seen t then rev seen else take_distinct_vars (t :: seen) ts
- | take_distinct_vars seen _ = rev seen
-
fun unskolemize_term skos =
let
val is_skolem = member (op =) skos