--- 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"
--- 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) =
--- 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