# HG changeset patch # User blanchet # Date 1387461441 -3600 # Node ID a80bd631e57309e5fbd490dc2c550fbca605df4b # Parent e1da23db35a9025342dbaf3b3317c8ad72fd3b7c honor SPASS-Pirate type arguments diff -r e1da23db35a9 -r a80bd631e573 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 13:46:42 2013 +0100 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Thu Dec 19 14:57:21 2013 +0100 @@ -108,6 +108,7 @@ TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end +exception ATP_TYPE of string atp_type list exception ATP_TERM of (string, string atp_type) atp_term list exception ATP_FORMULA of (string, string, (string, string atp_type) atp_term, string) atp_formula list @@ -115,13 +116,13 @@ (* 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 +fun typ_of_atp_type ctxt (ty as AType (a, 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 us) then - raise ATP_TERM [u] (* only "tconst"s have type arguments *) + 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 @@ -129,13 +130,16 @@ (* 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. *) - (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS) - |> Type_Infer.param 0)) + Type_Infer.param 0 (a |> perhaps (unprefix_and_unascii tvar_prefix), HOLogic.typeS))) end +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 + (* Type class literal applied to a type. Returns triple of polarity, class, type. *) fun type_constraint_of_term ctxt (u as ATerm ((a, _), us)) = - (case (unprefix_and_unascii class_prefix a, map (typ_of_atp ctxt) us) of + (case (unprefix_and_unascii class_prefix a, map (typ_of_atp_term ctxt) us) of (SOME b, [T]) => (b, T) | _ => raise ATP_TERM [u]) @@ -190,7 +194,7 @@ val var_index = if textual then 0 else 1 fun do_term extra_ts opt_T u = (case u of - ATerm ((s, _), us) => + ATerm ((s, tys), us) => if s = "" then error "Isar proof reconstruction failed because the ATP proof \ \contains unparsable material." @@ -207,13 +211,10 @@ else (case unprefix_and_unascii const_prefix s of SOME s' => - let - val ((s', s''), mangled_us) = - s' |> unmangled_const |>> `invert_const - in + let val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const in if s' = type_tag_name then (case mangled_us @ us of - [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp ctxt typ_u)) term_u + [typ_u, term_u] => do_term extra_ts (SOME (typ_of_atp_term ctxt typ_u)) term_u | _ => raise ATP_TERM us) else if s' = predicator_name then do_term [] (SOME @{typ bool}) (hd us) @@ -230,22 +231,19 @@ else let val new_skolem = String.isPrefix new_skolem_const_prefix s'' - val num_ty_args = - length us - the_default 0 (Symtab.lookup sym_tab s) - val (type_us, term_us) = - chop num_ty_args us |>> append mangled_us + val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s) + val (type_us, term_us) = chop num_ty_args us |>> append mangled_us val term_ts = map (do_term [] NONE) term_us + + val Ts = map (typ_of_atp_type ctxt) tys @ map (typ_of_atp_term ctxt) type_us val T = - (if not (null type_us) andalso - robust_const_num_type_args thy s' = length type_us then - let val Ts = type_us |> map (typ_of_atp ctxt) in - if new_skolem then - SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts)) - else if textual then - try (Sign.const_instance thy) (s', Ts) - else - NONE - end + (if not (null Ts) andalso robust_const_num_type_args thy s' = length Ts then + if new_skolem then + SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts)) + else if textual then + try (Sign.const_instance thy) (s', Ts) + else + NONE else NONE) |> (fn SOME T => T @@ -377,8 +375,7 @@ fun add_non_rec_defs fact_names accum = Vector.foldl (fn (facts, facts') => - union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) - facts') + union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) facts') accum fact_names val isa_ext = Thm.get_name_hint @{thm ext} @@ -501,6 +498,7 @@ val thy = Proof_Context.theory_of ctxt val t = u |> prop_of_atp ctxt true sym_tab +|> tap (fn t => tracing ("termify_line: " ^ Syntax.string_of_term ctxt t)) (*###*) |> uncombine_term thy |> unlift_term lifted |> infer_formula_types ctxt diff -r e1da23db35a9 -r a80bd631e573 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 13:46:42 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 19 14:57:21 2013 +0100 @@ -727,22 +727,16 @@ handle UNRECOGNIZED_ATP_PROOF () => ([], SOME ProofIncomplete))) handle TimeLimit.TimeOut => (("", slice_timeout), ([], SOME TimedOut)) val outcome = - case outcome of + (case outcome of NONE => (case used_facts_in_unsound_atp_proof ctxt fact_names atp_proof |> Option.map (sort string_ord) of SOME facts => - let - val failure = - UnsoundProof (is_type_enc_sound type_enc, facts) - in - if debug then - (warning (string_of_atp_failure failure); NONE) - else - SOME failure + let val failure = UnsoundProof (is_type_enc_sound type_enc, facts) in + if debug then (warning (string_of_atp_failure failure); NONE) else SOME failure end | NONE => NONE) - | _ => outcome + | _ => outcome) in ((SOME key, value), (output, run_time, facts, atp_proof, outcome)) end @@ -756,10 +750,8 @@ result else run_slice time_left cache slice - |> (fn (cache, (output, run_time, used_from, atp_proof, - outcome)) => - (cache, (output, Time.+ (run_time0, run_time), used_from, - atp_proof, outcome))) + |> (fn (cache, (output, run_time, used_from, atp_proof, outcome)) => + (cache, (output, Time.+ (run_time0, run_time), used_from, atp_proof, outcome))) end | maybe_run_slice _ result = result in @@ -790,10 +782,8 @@ val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof val reconstrs = - bunch_of_reconstructors needs_full_types - (lam_trans_of_atp_proof atp_proof - o (fn desperate => if desperate then hide_lamsN - else default_metis_lam_trans)) + bunch_of_reconstructors needs_full_types (lam_trans_of_atp_proof atp_proof + o (fn desperate => if desperate then hide_lamsN else default_metis_lam_trans)) in (used_facts, Lazy.lazy (fn () =>