diff -r 488046fdda59 -r cf43583f9bb9 src/HOL/Tools/ATP/atp_proof_reconstruct.ML --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 16:18:15 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Mon Jun 16 16:18:34 2014 +0200 @@ -130,6 +130,8 @@ 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 (ty as 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) @@ -188,46 +190,24 @@ (* Higher-order translation. Variables are typed (although we don't use that information). Lambdas - are typed. *) + are typed. + + The code is similar to term_of_atp_fo. *) fun term_of_atp_ho ctxt textual sym_tab = let val thy = Proof_Context.theory_of ctxt - fun norm_var_types var T' t = - let - fun norm_term (ATerm ((x, ty), l)) = - ATerm((x, if x = var then [T'] else ty), List.map norm_term l) - | norm_term (AAbs(((x, ty), term), l)) = AAbs(((x, ty), term), List.map norm_term l) - in - norm_term t - end - fun mk_op_of_tptp_operator s = - if s = tptp_or then HOLogic.mk_disj - else if s = tptp_and then HOLogic.mk_conj - else if s = tptp_implies then HOLogic.mk_imp - else if s = tptp_iff orelse s = tptp_equal then HOLogic.mk_eq - else if s = tptp_not_iff orelse s = tptp_not_equal then HOLogic.mk_eq #> HOLogic.mk_not - else if s = tptp_if then HOLogic.mk_imp #> HOLogic.mk_not - else if s = tptp_not_and then HOLogic.mk_conj #> HOLogic.mk_not - else if s = tptp_not_or then HOLogic.mk_disj #> HOLogic.mk_not - else raise Fail ("unknown operator: " ^ s) - fun mk_quant_of_tptp_quant s = - if s = tptp_ho_exists then HOLogic.mk_exists - else if s = tptp_ho_forall then HOLogic.mk_all - else raise Fail ("unknown quantifier: " ^ s) val var_index = if textual then 0 else 1 fun do_term opt_T u = (case u of AAbs(((var, ty), term), []) => let val typ = typ_of_atp_type ctxt ty in - absfree (repair_var_name textual var, typ) (do_term NONE (norm_var_types var ty term)) + absfree (repair_var_name textual var, typ) (do_term NONE term) end | ATerm ((s, tys), us) => if s = "" then 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 *) else if s = tptp_equal then let val ts = map (do_term NONE) us in if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then @@ -235,90 +215,65 @@ else list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts) end - else if s = tptp_app then - let val ts = map (do_term NONE) us in - hd ts $ List.last ts - end - else if s = tptp_not then - let val ts = map (do_term NONE) us in - List.last ts |> HOLogic.mk_not - end - else if s = tptp_ho_forall orelse s = tptp_ho_exists then - (case us of - [AAbs (((var, ty), term), [])] => - let val typ = typ_of_atp_type ctxt ty in - (repair_var_name textual var, typ , do_term NONE (norm_var_types var ty term)) - |> mk_quant_of_tptp_quant s - end - | [] => if s = tptp_ho_exists then HOLogic.exists_const dummyT - else HOLogic.all_const dummyT) - else if List.exists (curry (op=) s) tptp_binary_op_list then - let val ts = map (do_term NONE) us in - (mk_op_of_tptp_operator s) (hd ts, List.last ts) - end + else if not (null us) then + let + val args = List.map (do_term NONE) us + val opt_T' = SOME (map slack_fastype_of args ---> the_default dummyT opt_T) + val func = do_term opt_T' (ATerm ((s, tys), [])) + in foldl1 (op $) (func :: args) end + else if s = tptp_or then HOLogic.disj + else if s = tptp_and then HOLogic.conj + else if s = tptp_implies then HOLogic.imp + else if s = tptp_iff orelse s = tptp_equal then HOLogic.eq_const dummyT + else if s = tptp_not_iff orelse s = tptp_not_equal then @{term "% P Q. Q ~= P"} + else if s = tptp_if then @{term "% P Q. Q --> P"} + else if s = tptp_not_and then @{term "% P Q. ~ (P & Q)"} + else if s = tptp_not_or then @{term "% P Q. ~ (P | Q)"} + else if s = tptp_not then HOLogic.Not + else if s = tptp_ho_forall then HOLogic.all_const dummyT + else if s = tptp_ho_exists then HOLogic.exists_const dummyT else - if us <> [] then + (case unprefix_and_unascii const_prefix s of + SOME s' => let - val applicant_list = List.map (do_term NONE) us - val opt_typ = SOME (fold_rev - (fn t1 => fn t2 => slack_fastype_of t1 --> t2) - applicant_list (the_default dummyT opt_T)) - val func_name = do_term opt_typ (ATerm ((s, tys), [])) - in - foldl1 (op$) (func_name :: applicant_list) end - else (*FIXME: clean (remove stuff related to vampire and other provers)*) - (case unprefix_and_unascii const_prefix s of - SOME s' => - let - val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const - 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 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 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 - | NONE => - map slack_fastype_of term_ts ---> - the_default (Type_Infer.anyT @{sort type}) opt_T) - val t = - if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T) - else Const (unproxify_const s', T) - in list_comb (t, term_ts) end - | NONE => (* a free or schematic variable *) - let - (* This assumes that distinct names are mapped to distinct names by - "Variable.variant_frees". This does not hold in general but should hold for - ATP-generated Skolem function names, since these end with a digit and - "variant_frees" appends letters. *) - fun fresh_up s = - [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst - val ts = map (do_term NONE) us - val T = - (case opt_T of - SOME T => map slack_fastype_of ts ---> T - | NONE => - map slack_fastype_of ts ---> - (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT - @{sort type})) - val t = - (case unprefix_and_unascii fixed_var_prefix s of - SOME s => Free (s, T) - | NONE => - if textual andalso not (is_tptp_variable s) then - Free (s |> textual ? (repair_var_name_raw #> fresh_up), T) - else - Var ((repair_var_name textual s, var_index), T)) - in list_comb (t, ts) end)) + val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const + 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 Ts) andalso robust_const_num_type_args thy s' = length Ts then + if textual then try (Sign.const_instance thy) (s', Ts) else NONE + else + NONE) + |> (fn SOME T => T + | NONE => + map slack_fastype_of term_ts ---> + the_default (Type_Infer.anyT @{sort type}) opt_T) + val t = Const (unproxify_const s', T) + in list_comb (t, term_ts) end + | NONE => (* a free or schematic variable *) + let + fun fresh_up s = + [(s, ())] |> Variable.variant_frees ctxt [] |> hd |> fst + val ts = map (do_term NONE) us + val T = + (case opt_T of + SOME T => map slack_fastype_of ts ---> T + | NONE => + map slack_fastype_of ts ---> + (case tys of + [ty] => typ_of_atp_type ctxt ty + | _ => Type_Infer.anyT @{sort type})) + val t = + (case unprefix_and_unascii fixed_var_prefix s of + SOME s => Free (s, T) + | NONE => + if textual andalso not (is_tptp_variable s) then + Free (s |> textual ? (repair_var_name_raw #> fresh_up), T) + else + Var ((repair_var_name textual s, var_index), T)) + in list_comb (t, ts) end)) in do_term end (* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}" @@ -459,7 +414,7 @@ val vars = filter (fn ((s, _), _) => s = var_s) (Term.add_vars t []) val normTs = vars |> AList.group (op =) |> map (apsnd hd) fun norm_var_types (Var (x, T)) = - Var (x, (case AList.lookup (op =) normTs x of NONE => T | SOME T' => T')) + Var (x, the_default T (AList.lookup (op =) normTs x)) | norm_var_types t = t in t |> map_aterms norm_var_types |> fold_rev quant_of (map Var normTs) end @@ -623,7 +578,7 @@ t | t => t) -fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE +fun termify_line _ _ _ _ _ (_, Type_Role, _, _, _) = NONE | termify_line ctxt format type_enc lifted sym_tab (name, role, u, rule, deps) = let val thy = Proof_Context.theory_of ctxt @@ -656,7 +611,7 @@ #> nasty_atp_proof pool #> map_term_names_in_atp_proof repair_name #> map_filter (termify_line ctxt format type_enc lifted sym_tab) - #> prover = waldmeisterN ? repair_waldmeister_endgame + #> perhaps (try (unprefix remote_prefix)) 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