src/HOL/Tools/ATP/atp_problem.ML

   val tptp_false : string
   val tptp_true : string
   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
   val spec_eqN : string
   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
   val is_tptp_user_symbol : string -> bool
   val atype_of_types : (string * string) ho_type

     -> connective * 'a list -> ('b, 'c, 'd) formula
   val formula_fold :
     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 :
     (string * string) problem -> (string * string) problem
   val declared_syms_in_problem : (string * ''a) problem -> (string * ''a) list

 val spec_eqN = "spec_eq"
 val rankN = "rank"
 
 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. *)
 fun isabelle_info (DFG DFG_Sorted) status rank =
     [] |> rank <> default_rank

   in fld pos end
 
 fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
   | 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
   | is_format_typed (THF _) = true

   | arity_of_type _ = 0
 
 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 =
       if top_level then
         case extract_isabelle_status info of

         str_for_conn top_level c ^ "(" ^
         commas (map (str_for_formula false) phis) ^ ")"
       | 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 =
       "predicate(" ^
       commas (sym :: map (string_for_type format) (binder_atypes ty)) ^ ")."

     fun sorts () =
       filt (fn Decl (_, sym, AType (s, [])) =>
                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
              | _ => NONE)
       |> flat

     list_of "formulae(axioms)" axioms @
     list_of "formulae(conjectures)" conjs @
     ["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
 
 
 (** CNF (Metis) and CNF UEQ (Waldmeister) **)