# HG changeset patch # User fleury # Date 1402928314 -7200 # Node ID cf43583f9bb9de3ee0ff69b337e491c08ebb7b81 # Parent 488046fdda590ee780439c2c92aa0f78ee2cff35 imported patch leo2_skolem_simplication diff -r 488046fdda59 -r cf43583f9bb9 src/HOL/Tools/ATP/atp_problem.ML --- a/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 16:18:15 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_problem.ML Mon Jun 16 16:18:34 2014 +0200 @@ -94,7 +94,6 @@ val tptp_true : string val tptp_lambda : string val tptp_empty_list : string - val tptp_binary_op_list : string list val isabelle_info_prefix : string val isabelle_info : string -> int -> (string, 'a) atp_term list val extract_isabelle_status : (string, 'a) atp_term list -> string option @@ -249,8 +248,6 @@ val tptp_true = "$true" val tptp_lambda = "^" val tptp_empty_list = "[]" -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 isabelle_info_prefix = "isabelle_" val inductionN = "induction" diff -r 488046fdda59 -r cf43583f9bb9 src/HOL/Tools/ATP/atp_proof.ML --- a/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 16:18:15 2014 +0200 +++ b/src/HOL/Tools/ATP/atp_proof.ML Mon Jun 16 16:18:34 2014 +0200 @@ -438,13 +438,18 @@ | 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] + fun parse_binary_op x = - foldl1 (op||) (map Scan.this_string tptp_binary_op_list) x + foldl1 (op ||) (map Scan.this_string tptp_binary_op_list) x fun parse_thf0_type x = - ($$ "(" |-- parse_thf0_type --| $$ ")" - || parse_type --| $$ tptp_fun_type -- parse_thf0_type >> AFun - || parse_type) x + ($$ "(" |-- parse_thf0_type --| $$ ")" --| $$ tptp_fun_type -- parse_thf0_type >> AFun + || scan_general_id --| $$ tptp_fun_type -- +parse_thf0_type >> apfst (fn t => AType ((t, []), [])) >> AFun + || scan_general_id >> (fn t => AType ((t, []), [])) + || $$ "(" |-- parse_thf0_type --| $$ ")") x fun mk_ho_of_fo_quant q = if q = tptp_forall then tptp_ho_forall @@ -469,7 +474,7 @@ ((Scan.repeat ($$ tptp_not) >> length) -- ($$ "(" |-- parse_formula_hol_raw --| $$ ")" || scan_general_id >> mk_simple_aterm - || scan_general_id --| $$ ":" --| scan_general_id >> mk_simple_aterm + || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var,typ) => ATerm(((var,[typ]),[]))) || (Scan.this_string tptp_ho_forall || Scan.this_string tptp_ho_exists) >> mk_simple_aterm) >> (fn (n, phi) => phi |> n mod 2 = 1 ? mk_app (mk_simple_aterm tptp_not))) x @@ -503,7 +508,7 @@ ((Scan.this_string tptp_cnf || Scan.this_string tptp_fof || Scan.this_string tptp_tff || Scan.this_string tptp_thf) -- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ "," - -- parse_formula_hol -- parse_tstp_extra_arguments--| $$ ")" --| $$ "." + -- parse_formula_hol -- parse_tstp_extra_arguments --| $$ ")" --| $$ "." >> (fn (((num, role), phi), deps) => let val ((name, phi), rule, deps) = 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