--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 09:36:30 2012 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 09 12:57:59 2012 +0100
@@ -76,6 +76,8 @@
val tptp_empty_list : string
val isabelle_info_prefix : string
val isabelle_info : atp_format -> string -> int -> (string, 'a) ho_term list
+ val extract_isabelle_status : (string, 'a) ho_term list -> string option
+ val extract_isabelle_rank : (string, 'a) ho_term list -> int
val introN : string
val elimN : string
val simpN : string
@@ -83,6 +85,7 @@
val rankN : string
val minimum_rank : int
val default_rank : int
+ val default_kbo_weight : int
val is_tptp_equal : string -> bool
val is_built_in_tptp_symbol : string -> bool
val is_tptp_variable : string -> bool
@@ -104,9 +107,12 @@
bool option -> (bool option -> 'c -> 'd -> 'd) -> ('a, 'b, 'c) formula
-> 'd -> 'd
val formula_map : ('c -> 'd) -> ('a, 'b, 'c) formula -> ('a, 'b, 'd) formula
+ val is_function_type : string ho_type -> bool
+ val is_predicate_type : string ho_type -> bool
val is_format_higher_order : atp_format -> bool
val is_format_typed : atp_format -> bool
- val lines_for_atp_problem : atp_format -> string problem -> string list
+ val lines_for_atp_problem :
+ atp_format -> (unit -> (string * int) list) -> string problem -> string list
val ensure_cnf_problem :
(string * string) problem -> (string * string) problem
val filter_cnf_ueq_problem :
@@ -205,6 +211,7 @@
val minimum_rank = 0
val default_rank = 1000
+val default_kbo_weight = 1
(* Currently, only newer versions of SPASS, with sorted DFG format support, can
process Isabelle metainformation. *)
@@ -273,6 +280,16 @@
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
+fun is_function_type (AFun (_, ty)) = is_function_type ty
+ | is_function_type (AType (s, _)) =
+ s <> tptp_type_of_types andalso s <> tptp_bool_type
+ | is_function_type _ = false
+fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
+ | is_predicate_type _ = false
+fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
+ | is_nontrivial_predicate_type _ = false
+
fun is_format_higher_order (THF _) = true
| is_format_higher_order _ = false
fun is_format_typed (TFF _) = true
@@ -443,17 +460,6 @@
fun binder_atypes (AFun (ty1, ty2)) = ty1 :: binder_atypes ty2
| binder_atypes _ = []
-fun is_function_type (AFun (_, ty)) = is_function_type ty
- | is_function_type (AType (s, _)) =
- s <> tptp_type_of_types andalso s <> tptp_bool_type
- | is_function_type _ = false
-
-fun is_predicate_type (AFun (_, ty)) = is_predicate_type ty
- | is_predicate_type (AType (s, _)) = (s = tptp_bool_type)
- | is_predicate_type _ = false
-fun is_nontrivial_predicate_type (AFun (_, ty)) = is_predicate_type ty
- | is_nontrivial_predicate_type _ = false
-
fun dfg_string_for_formula flavor info =
let
fun suffix_tag top_level s =
@@ -490,12 +496,12 @@
| str_for_formula top_level (AAtom tm) = str_for_term top_level tm
in str_for_formula true end
-fun dfg_lines flavor problem =
+fun dfg_lines flavor kbo_weights problem =
let
val sorted = (flavor = DFG_Sorted)
val format = DFG flavor
- fun ary sym ty =
- "(" ^ sym ^ ", " ^ string_of_int (arity_of_type ty) ^ ")"
+ fun spair (sym, k) = "(" ^ sym ^ ", " ^ string_of_int k ^ ")"
+ fun ary sym = curry spair sym o arity_of_type
fun fun_typ sym ty =
"function(" ^ sym ^ ", " ^ string_for_type format ty ^ ")."
fun pred_typ sym ty =
@@ -527,7 +533,11 @@
if s = tptp_type_of_types then SOME sym else NONE
| _ => NONE) @ [[dfg_individual_type]]
|> flat |> commas |> enclose "sorts [" "]."
- val syms = [func_aries, pred_aries] @ (if sorted then [sorts ()] else [])
+ fun do_kbo_weights () =
+ kbo_weights () |> map spair |> commas |> enclose "weights [" "]."
+ val syms =
+ [func_aries] @ (if sorted then [do_kbo_weights ()] else []) @
+ [pred_aries] @ (if sorted then [sorts ()] else [])
fun func_sigs () =
filt (fn Decl (_, sym, ty) =>
if is_function_type ty then SOME (fun_typ sym ty) else NONE
@@ -560,11 +570,11 @@
["end_problem.\n"]
end
-fun lines_for_atp_problem format problem =
+fun lines_for_atp_problem format kbo_weights problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
\% " ^ timestamp () ^ "\n" ::
(case format of
- DFG flavor => dfg_lines flavor
+ DFG flavor => dfg_lines flavor kbo_weights
| _ => tptp_lines format) problem