# HG changeset patch # User blanchet # Date 1411979979 -7200 # Node ID 8438bae06e63ff9420a1bd082250e57c3e5d3731 # Parent 6ade4c7109a8502beca440480abe1a845a557ad7 parse back type of SPASS proof variables diff -r 6ade4c7109a8 -r 8438bae06e63 src/HOL/Tools/ATP/atp_problem_generate.ML --- 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 diff -r 6ade4c7109a8 -r 8438bae06e63 src/HOL/Tools/ATP/atp_proof.ML --- 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 = diff -r 6ade4c7109a8 -r 8438bae06e63 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- 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