--- a/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML Tue May 24 10:00:38 2011 +0200
@@ -27,12 +27,13 @@
(* official TPTP syntax *)
val tptp_special_prefix : string
- val tptp_false : string
- val tptp_true : string
val tptp_type_of_types : string
val tptp_bool_type : string
val tptp_individual_type : string
val tptp_fun_type : string
+ val tptp_false : string
+ val tptp_true : string
+ val tptp_app_op : string
val is_atp_variable : string -> bool
val mk_anot : ('a, 'b, 'c) formula -> ('a, 'b, 'c) formula
val mk_aconn :
@@ -76,12 +77,13 @@
(* official TPTP syntax *)
val tptp_special_prefix = "$"
-val tptp_false = "$false"
-val tptp_true = "$true"
val tptp_type_of_types = "$tType"
val tptp_bool_type = "$o"
val tptp_individual_type = "$i"
val tptp_fun_type = ">"
+val tptp_false = "$false"
+val tptp_true = "$true"
+val tptp_app_op = "@"
fun is_atp_variable s = Char.isUpper (String.sub (s, 0))
--- a/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue May 24 10:00:38 2011 +0200
@@ -281,12 +281,21 @@
::: Scan.repeat ($$ "," |-- parse_annotation)) []
>> flat) x
-fun parse_term x =
+fun list_app (f, args) =
+ fold (fn arg => fn f => ATerm (tptp_app_op, [f, arg])) args f
+
+fun parse_arg x =
(scan_general_id
- --| Scan.option ($$ ":" -- scan_general_id) (* ignore TFF types for now *)
+ (* We ignore TFF and THF types for now. *)
+ --| Scan.repeat (($$ ":" || $$ ">") |-- parse_arg)
-- Scan.optional ($$ "(" |-- parse_terms --| $$ ")") []
>> ATerm) x
-and parse_terms x = (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
+and parse_app x =
+ (parse_arg -- Scan.repeat ($$ tptp_app_op |-- parse_arg) >> list_app) x
+and parse_term x =
+ (parse_app -- Scan.optional)
+and parse_terms x =
+ (parse_term ::: Scan.repeat ($$ "," |-- parse_term)) x
fun parse_atom x =
(parse_term -- Scan.option (Scan.option ($$ "!") --| $$ "=" -- parse_term)
@@ -320,7 +329,7 @@
(($$ "!" >> K AForall || $$ "?" >> K AExists)
--| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
>> (fn ((q, ts), phi) =>
- (* FIXME: TFF *)
+ (* We ignore TFF and THF types for now. *)
AQuant (q, map (rpair NONE o fo_term_head) ts, phi))) x
val parse_tstp_extra_arguments =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Tue May 24 10:00:38 2011 +0200
@@ -392,11 +392,11 @@
[typ_u, term_u] =>
aux (SOME (typ_from_fo_term tfrees typ_u)) extra_us term_u
| _ => raise FO_TERM us
- else if s' = predicator_base then
+ else if s' = predicator_name then
aux (SOME @{typ bool}) [] (hd us)
- else if s' = explicit_app_base then
+ else if s' = app_op_name then
aux opt_T (nth us 1 :: extra_us) (hd us)
- else if s' = type_pred_base then
+ else if s' = type_pred_name then
@{const True} (* ignore type predicates *)
else
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 24 10:00:38 2011 +0200
@@ -31,9 +31,9 @@
val conjecture_prefix : string
val helper_prefix : string
val typed_helper_suffix : string
- val predicator_base : string
- val explicit_app_base : string
- val type_pred_base : string
+ val predicator_name : string
+ val app_op_name : string
+ val type_pred_name : string
val simple_type_prefix : string
val type_sys_from_string : string -> type_system
val polymorphism_of_type_sys : type_system -> polymorphism
@@ -93,9 +93,9 @@
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
-val predicator_base = "hBOOL"
-val explicit_app_base = "hAPP"
-val type_pred_base = "is"
+val predicator_name = "hBOOL"
+val app_op_name = "hAPP"
+val type_pred_name = "is"
val simple_type_prefix = "ty_"
fun make_simple_type s =
@@ -236,8 +236,7 @@
fun type_arg_policy type_sys s =
if s = @{const_name HOL.eq} orelse
- (s = explicit_app_base andalso
- level_of_type_sys type_sys = Const_Arg_Types) then
+ (s = app_op_name andalso level_of_type_sys type_sys = Const_Arg_Types) then
No_Type_Args
else
general_type_arg_policy type_sys
@@ -597,7 +596,7 @@
val default_sym_table_entries : (string * sym_info) list =
[("equal", {pred_sym = true, min_ary = 2, max_ary = 2, typ = NONE}),
- (make_fixed_const predicator_base,
+ (make_fixed_const predicator_name,
{pred_sym = true, min_ary = 1, max_ary = 1, typ = NONE})] @
([tptp_false, tptp_true]
|> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, typ = NONE}))
@@ -613,9 +612,9 @@
case strip_prefix_and_unascii const_prefix s of
SOME s =>
let val s = s |> unmangled_const_name |> invert_const in
- if s = predicator_base then 1
- else if s = explicit_app_base then 2
- else if s = type_pred_base then 1
+ if s = predicator_name then 1
+ else if s = app_op_name then 2
+ else if s = type_pred_name then 1
else 0
end
| NONE => 0
@@ -631,7 +630,7 @@
| NONE => false
val predicator_combconst =
- CombConst (`make_fixed_const predicator_base, @{typ "bool => bool"}, [])
+ CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
fun predicator tm = CombApp (predicator_combconst, tm)
fun introduce_predicators_in_combterm sym_tab tm =
@@ -647,7 +646,7 @@
val head_T = combtyp_of head
val (arg_T, res_T) = dest_funT head_T
val explicit_app =
- CombConst (`make_fixed_const explicit_app_base, head_T --> head_T,
+ CombConst (`make_fixed_const app_op_name, head_T --> head_T,
[arg_T, res_T])
in list_app explicit_app [head, arg] end
fun list_explicit_app head args = fold explicit_app args head
@@ -673,7 +672,7 @@
| filter_type_args thy s arity T_args =
let
(* will throw "TYPE" for pseudo-constants *)
- val U = if s = explicit_app_base then
+ val U = if s = app_op_name then
@{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
else
s |> Sign.the_const_type thy
@@ -705,7 +704,7 @@
anyway, by distinguishing overloads only on the homogenized
result type. Don't do it for lightweight type systems, though,
since it leads to too many unsound proofs. *)
- if s = const_prefix ^ explicit_app_base andalso
+ if s = const_prefix ^ app_op_name andalso
length T_args = 2 andalso
not (is_type_sys_virtually_sound type_sys) andalso
heaviness_of_type_sys type_sys = Heavy then
@@ -834,7 +833,7 @@
fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
fun type_pred_combterm ctxt format nonmono_Ts type_sys T tm =
- CombApp (CombConst (`make_fixed_const type_pred_base, T --> @{typ bool}, [T])
+ CombApp (CombConst (`make_fixed_const type_pred_name, T --> @{typ bool}, [T])
|> enforce_type_arg_policy_in_combterm ctxt format nonmono_Ts
type_sys,
tm)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 10:00:38 2011 +0200
@@ -44,7 +44,7 @@
val auto_minimize_min_facts =
Attrib.setup_config_int @{binding sledgehammer_auto_minimize_min_facts}
- (fn generic => Config.get_generic generic binary_min_facts)
+ (fn generic => (* ### Config.get_generic generic binary_min_facts *) 10000 (*###*))
fun get_minimizing_prover ctxt auto name
(params as {debug, verbose, explicit_apply, ...}) minimize_command