# HG changeset patch # User blanchet # Date 1306224038 -7200 # Node ID 4e2d6c1e5392f9ab6e00dba2a652e0cddd057897 # Parent 1403595ec38cd3e7a38ccbd5880fd289307c7e48 more work on parsing LEO-II proofs without lambdas diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/ATP/atp_problem.ML --- 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)) diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/ATP/atp_proof.ML --- 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 = diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML --- 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 diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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) diff -r 1403595ec38c -r 4e2d6c1e5392 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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