1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jun 23 15:35:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Wed Jun 23 16:28:12 2010 +0200
     1.3 @@ -29,6 +29,8 @@
     1.4  open Sledgehammer_FOL_Clause
     1.5  open Sledgehammer_HOL_Clause
     1.6  
     1.7 +type const_info = {min_arity: int, max_arity: int, sub_level: bool}
     1.8 +
     1.9  val clause_prefix = "cls_"
    1.10  val arity_clause_prefix = "clsarity_"
    1.11  
    1.12 @@ -44,15 +46,19 @@
    1.13      in (s ^ paren_pack ss, pool) end
    1.14  
    1.15  (* True if the constant ever appears outside of the top-level position in
    1.16 -   literals. If false, the constant always receives all of its arguments and is
    1.17 -   used as a predicate. *)
    1.18 -fun needs_hBOOL explicit_apply const_needs_hBOOL c =
    1.19 -  explicit_apply orelse the_default false (Symtab.lookup const_needs_hBOOL c)
    1.20 +   literals, or if it appears with different arities (e.g., because of different
    1.21 +   type instantiations). If false, the constant always receives all of its
    1.22 +   arguments and is used as a predicate. *)
    1.23 +fun needs_hBOOL NONE _ = true
    1.24 +  | needs_hBOOL (SOME the_const_tab) c =
    1.25 +    case Symtab.lookup the_const_tab c of
    1.26 +      SOME ({min_arity, max_arity, sub_level} : const_info) =>
    1.27 +      sub_level orelse min_arity < max_arity
    1.28 +    | NONE => false
    1.29  
    1.30 -fun head_needs_hBOOL explicit_apply const_needs_hBOOL
    1.31 -                     (CombConst ((c, _), _, _)) =
    1.32 -    needs_hBOOL explicit_apply const_needs_hBOOL c
    1.33 -  | head_needs_hBOOL _ _ _ = true
    1.34 +fun head_needs_hBOOL const_tab (CombConst ((c, _), _, _)) =
    1.35 +    needs_hBOOL const_tab c
    1.36 +  | head_needs_hBOOL _ _ = true
    1.37  
    1.38  fun wrap_type full_types (s, ty) pool =
    1.39    if full_types then
    1.40 @@ -62,11 +68,9 @@
    1.41    else
    1.42      (s, pool)
    1.43  
    1.44 -fun wrap_type_if full_types explicit_apply const_needs_hBOOL (head, s, tp) =
    1.45 -  if head_needs_hBOOL explicit_apply const_needs_hBOOL head then
    1.46 -    wrap_type full_types (s, tp)
    1.47 -  else
    1.48 -    pair s
    1.49 +fun wrap_type_if (full_types, const_tab) (head, s, tp) =
    1.50 +  if head_needs_hBOOL const_tab head then wrap_type full_types (s, tp)
    1.51 +  else pair s
    1.52  
    1.53  fun apply ss = "hAPP" ^ paren_pack ss;
    1.54  
    1.55 @@ -75,15 +79,19 @@
    1.56  
    1.57  fun string_apply (v, args) = rev_apply (v, rev args)
    1.58  
    1.59 -fun min_arity_of const_min_arity = the_default 0 o Symtab.lookup const_min_arity
    1.60 +fun min_arity_of NONE _ = 0
    1.61 +  | min_arity_of (SOME the_const_tab) c =
    1.62 +    case Symtab.lookup the_const_tab c of
    1.63 +      SOME ({min_arity, ...} : const_info) => min_arity
    1.64 +    | NONE => 0
    1.65  
    1.66  (* Apply an operator to the argument strings, using either the "apply" operator
    1.67     or direct function application. *)
    1.68 -fun string_of_application full_types const_min_arity
    1.69 +fun string_of_application (full_types, const_tab)
    1.70                            (CombConst ((s, s'), _, tvars), args) pool =
    1.71      let
    1.72        val s = if s = "equal" then "c_fequal" else s
    1.73 -      val nargs = min_arity_of const_min_arity s
    1.74 +      val nargs = min_arity_of const_tab s
    1.75        val args1 = List.take (args, nargs)
    1.76          handle Subscript =>
    1.77                 raise Fail (quote s ^ " has arity " ^ Int.toString nargs ^
    1.78 @@ -93,31 +101,24 @@
    1.79                            else pool_map string_of_fol_type tvars pool
    1.80        val (s, pool) = nice_name (s, s') pool
    1.81      in (string_apply (s ^ paren_pack (args1 @ targs), args2), pool) end
    1.82 -  | string_of_application _ _ (CombVar (name, _), args) pool =
    1.83 +  | string_of_application _ (CombVar (name, _), args) pool =
    1.84      nice_name name pool |>> (fn s => string_apply (s, args))
    1.85  
    1.86 -fun string_of_combterm (params as (full_types, explicit_apply, const_min_arity,
    1.87 -                                   const_needs_hBOOL)) t pool =
    1.88 +fun string_of_combterm params t pool =
    1.89    let
    1.90      val (head, args) = strip_combterm_comb t
    1.91      val (ss, pool) = pool_map (string_of_combterm params) args pool
    1.92 -    val (s, pool) =
    1.93 -      string_of_application full_types const_min_arity (head, ss) pool
    1.94 -  in
    1.95 -    wrap_type_if full_types explicit_apply const_needs_hBOOL
    1.96 -                 (head, s, type_of_combterm t) pool
    1.97 -  end
    1.98 +    val (s, pool) = string_of_application params (head, ss) pool
    1.99 +  in wrap_type_if params (head, s, type_of_combterm t) pool end
   1.100  
   1.101  (*Boolean-valued terms are here converted to literals.*)
   1.102  fun boolify params c =
   1.103    string_of_combterm params c #>> prefix "hBOOL" o paren_pack o single
   1.104  
   1.105 -fun string_of_predicate (params as (_, explicit_apply, _, const_needs_hBOOL))
   1.106 -                        t =
   1.107 +fun string_of_predicate (params as (_, const_tab)) t =
   1.108    case #1 (strip_combterm_comb t) of
   1.109      CombConst ((s, _), _, _) =>
   1.110 -    (if needs_hBOOL explicit_apply const_needs_hBOOL s then boolify
   1.111 -     else string_of_combterm) params t
   1.112 +    (if needs_hBOOL const_tab s then boolify else string_of_combterm) params t
   1.113    | _ => boolify params t
   1.114  
   1.115  fun tptp_of_equality params pos (t1, t2) =
   1.116 @@ -188,36 +189,34 @@
   1.117    tptp_cnf (arity_clause_prefix ^ ascii_of axiom_name) "axiom"
   1.118             (tptp_raw_clause (map tptp_of_arity_literal (conclLit :: premLits)))
   1.119  
   1.120 -(*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.121 -  are not at top level, to see if hBOOL is needed.*)
   1.122 -fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
   1.123 +(* Find the minimal arity of each function mentioned in the term. Also, note
   1.124 +   which uses are not at top level, to see if "hBOOL" is needed. *)
   1.125 +fun count_constants_term top_level t the_const_tab =
   1.126    let
   1.127      val (head, args) = strip_combterm_comb t
   1.128      val n = length args
   1.129 -    val (const_min_arity, const_needs_hBOOL) =
   1.130 -      (const_min_arity, const_needs_hBOOL)
   1.131 -      |> fold (count_constants_term false) args
   1.132 +    val the_const_tab = the_const_tab |> fold (count_constants_term false) args
   1.133    in
   1.134      case head of
   1.135 -      CombConst ((a, _), _, _) => (*predicate or function version of "equal"?*)
   1.136 -        let val a = if a="equal" andalso not toplev then "c_fequal" else a
   1.137 -        in
   1.138 -          (const_min_arity |> Symtab.map_default (a, n) (Integer.min n),
   1.139 -           const_needs_hBOOL |> not toplev ? Symtab.update (a, true))
   1.140 -        end
   1.141 -      | _ => (const_min_arity, const_needs_hBOOL)
   1.142 +      CombConst ((a, _), _, ty) =>
   1.143 +      (* Predicate or function version of "equal"? *)
   1.144 +      let val a = if a = "equal" andalso not top_level then "c_fequal" else a in
   1.145 +        the_const_tab
   1.146 +        |> Symtab.map_default
   1.147 +               (a, {min_arity = n, max_arity = n, sub_level = false})
   1.148 +               (fn {min_arity, max_arity, sub_level} =>
   1.149 +                   {min_arity = Int.min (n, min_arity),
   1.150 +                    max_arity = Int.max (n, max_arity),
   1.151 +                    sub_level = sub_level orelse not top_level})
   1.152 +      end
   1.153 +      | _ => the_const_tab
   1.154    end
   1.155 -fun count_constants_lit (Literal (_, t)) = count_constants_term true t
   1.156 +fun count_constants_literal (Literal (_, t)) = count_constants_term true t
   1.157  fun count_constants_clause (HOLClause {literals, ...}) =
   1.158 -  fold count_constants_lit literals
   1.159 -fun count_constants explicit_apply
   1.160 -                    (conjectures, _, extra_clauses, helper_clauses, _, _) =
   1.161 -  (Symtab.empty, Symtab.empty)
   1.162 -  |> (if explicit_apply then
   1.163 -        I
   1.164 -      else
   1.165 -        fold (fold count_constants_clause)
   1.166 -             [conjectures, extra_clauses, helper_clauses])
   1.167 +  fold count_constants_literal literals
   1.168 +fun count_constants (conjectures, _, extra_clauses, helper_clauses, _, _) =
   1.169 +  fold (fold count_constants_clause)
   1.170 +       [conjectures, extra_clauses, helper_clauses]
   1.171  
   1.172  fun write_tptp_file readable_names full_types explicit_apply file clauses =
   1.173    let
   1.174 @@ -228,10 +227,9 @@
   1.175      val pool = empty_name_pool readable_names
   1.176      val (conjectures, axclauses, _, helper_clauses,
   1.177        classrel_clauses, arity_clauses) = clauses
   1.178 -    val (const_min_arity, const_needs_hBOOL) =
   1.179 -      count_constants explicit_apply clauses
   1.180 -    val params = (full_types, explicit_apply, const_min_arity,
   1.181 -                  const_needs_hBOOL)
   1.182 +    val const_tab = if explicit_apply then NONE
   1.183 +                    else SOME (Symtab.empty |> count_constants clauses)
   1.184 +    val params = (full_types, const_tab)
   1.185      val ((conjecture_clss, tfree_litss), pool) =
   1.186        pool_map (tptp_clause params) conjectures pool |>> ListPair.unzip
   1.187      val tfree_clss = map tptp_tfree_clause (fold (union (op =)) tfree_litss [])