src/HOL/Tools/res_hol_clause.ML
author paulson
Tue Aug 21 18:27:14 2007 +0200 (2007-08-21)
changeset 24385 ab62948281a9
parent 24323 9aa7b5708eac
child 24937 340523598914
permissions -rw-r--r--
Deleted the partially-typed translation and the combinator code.
Minimize_applies now uses the same translation code, which handles both cases anyway.
wenzelm@24311
     1
(* ID: $Id$
mengj@17998
     2
   Author: Jia Meng, NICTA
mengj@17998
     3
wenzelm@24311
     4
FOL clauses translated from HOL formulae.
paulson@22825
     5
paulson@22825
     6
The combinator code needs to be deleted after the translation paper has been published.
paulson@22825
     7
It cannot be used with proof reconstruction because combinators are not introduced by proof.
paulson@22825
     8
The Turner combinators (B', C', S') yield no improvement and should be deleted.
mengj@17998
     9
*)
mengj@17998
    10
wenzelm@24311
    11
signature RES_HOL_CLAUSE =
wenzelm@24311
    12
sig
wenzelm@24311
    13
  val ext: thm
wenzelm@24311
    14
  val comb_I: thm
wenzelm@24311
    15
  val comb_K: thm
wenzelm@24311
    16
  val comb_B: thm
wenzelm@24311
    17
  val comb_C: thm
wenzelm@24311
    18
  val comb_S: thm
paulson@24385
    19
  datatype type_level = T_FULL | T_CONST
wenzelm@24311
    20
  val typ_level: type_level ref
wenzelm@24311
    21
  val minimize_applies: bool ref
wenzelm@24311
    22
  type axiom_name = string
wenzelm@24311
    23
  type polarity = bool
wenzelm@24311
    24
  type clause_id = int
wenzelm@24311
    25
  datatype combterm =
wenzelm@24311
    26
      CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
wenzelm@24311
    27
    | CombVar of string * ResClause.fol_type
wenzelm@24311
    28
    | CombApp of combterm * combterm
wenzelm@24311
    29
  datatype literal = Literal of polarity * combterm
wenzelm@24311
    30
  val strip_comb: combterm -> combterm * combterm list
wenzelm@24323
    31
  val literals_of_term: theory -> term -> literal list * (ResClause.typ_var * sort) list
wenzelm@24323
    32
  val tptp_write_file: theory -> bool -> thm list -> string ->
wenzelm@24311
    33
    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
wenzelm@24311
    34
      ResClause.arityClause list -> string list -> axiom_name list
wenzelm@24323
    35
  val dfg_write_file: theory -> bool -> thm list -> string ->
wenzelm@24311
    36
    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
wenzelm@24311
    37
      ResClause.arityClause list -> string list -> axiom_name list
wenzelm@24311
    38
end
mengj@17998
    39
wenzelm@24311
    40
structure ResHolClause: RES_HOL_CLAUSE =
mengj@17998
    41
struct
mengj@17998
    42
paulson@22078
    43
structure RC = ResClause;
paulson@22078
    44
mengj@20791
    45
(* theorems for combinators and function extensionality *)
mengj@20791
    46
val ext = thm "HOL.ext";
wenzelm@21254
    47
val comb_I = thm "ATP_Linkup.COMBI_def";
wenzelm@21254
    48
val comb_K = thm "ATP_Linkup.COMBK_def";
wenzelm@21254
    49
val comb_B = thm "ATP_Linkup.COMBB_def";
wenzelm@21254
    50
val comb_C = thm "ATP_Linkup.COMBC_def";
wenzelm@21254
    51
val comb_S = thm "ATP_Linkup.COMBS_def";
wenzelm@21254
    52
val comb_B' = thm "ATP_Linkup.COMBB'_def";
wenzelm@21254
    53
val comb_C' = thm "ATP_Linkup.COMBC'_def";
wenzelm@21254
    54
val comb_S' = thm "ATP_Linkup.COMBS'_def";
wenzelm@21254
    55
val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
wenzelm@21254
    56
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
mengj@20791
    57
paulson@22825
    58
paulson@22825
    59
(*The different translations of types*)
paulson@24385
    60
datatype type_level = T_FULL | T_CONST;
paulson@22825
    61
paulson@22825
    62
val typ_level = ref T_CONST;
paulson@22825
    63
paulson@22064
    64
(*If true, each function will be directly applied to as many arguments as possible, avoiding
paulson@24385
    65
  use of the "apply" operator. Use of hBOOL is also minimized.*)
paulson@22078
    66
val minimize_applies = ref true;
paulson@22064
    67
paulson@22064
    68
val const_min_arity = ref (Symtab.empty : int Symtab.table);
paulson@22064
    69
paulson@22064
    70
val const_needs_hBOOL = ref (Symtab.empty : bool Symtab.table);
paulson@22064
    71
paulson@22064
    72
fun min_arity_of c = getOpt (Symtab.lookup(!const_min_arity) c, 0);
paulson@22064
    73
paulson@22825
    74
(*True if the constant ever appears outside of the top-level position in literals.
paulson@22825
    75
  If false, the constant always receives all of its arguments and is used as a predicate.*)
paulson@24385
    76
fun needs_hBOOL c = not (!minimize_applies) orelse
paulson@22064
    77
                    getOpt (Symtab.lookup(!const_needs_hBOOL) c, false);
paulson@22064
    78
mengj@19198
    79
mengj@17998
    80
(******************************************************)
mengj@17998
    81
(* data types for typed combinator expressions        *)
mengj@17998
    82
(******************************************************)
mengj@17998
    83
mengj@17998
    84
type axiom_name = string;
mengj@17998
    85
type polarity = bool;
mengj@17998
    86
type clause_id = int;
mengj@17998
    87
paulson@23386
    88
datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
wenzelm@24311
    89
                  | CombVar of string * RC.fol_type
wenzelm@24311
    90
                  | CombApp of combterm * combterm
wenzelm@24311
    91
mengj@17998
    92
datatype literal = Literal of polarity * combterm;
mengj@17998
    93
wenzelm@24311
    94
datatype clause =
wenzelm@24311
    95
         Clause of {clause_id: clause_id,
wenzelm@24311
    96
                    axiom_name: axiom_name,
wenzelm@24311
    97
                    th: thm,
wenzelm@24311
    98
                    kind: RC.kind,
wenzelm@24311
    99
                    literals: literal list,
wenzelm@24311
   100
                    ctypes_sorts: (RC.typ_var * Term.sort) list,
wenzelm@24311
   101
                    ctvar_type_literals: RC.type_literal list,
paulson@22078
   102
                    ctfree_type_literals: RC.type_literal list};
mengj@17998
   103
mengj@17998
   104
mengj@17998
   105
(*********************************************************************)
mengj@17998
   106
(* convert a clause with type Term.term to a clause with type clause *)
mengj@17998
   107
(*********************************************************************)
mengj@17998
   108
paulson@21561
   109
fun isFalse (Literal(pol, CombConst(c,_,_))) =
paulson@20360
   110
      (pol andalso c = "c_False") orelse
paulson@20360
   111
      (not pol andalso c = "c_True")
mengj@17998
   112
  | isFalse _ = false;
mengj@17998
   113
paulson@21561
   114
fun isTrue (Literal (pol, CombConst(c,_,_))) =
mengj@17998
   115
      (pol andalso c = "c_True") orelse
mengj@17998
   116
      (not pol andalso c = "c_False")
mengj@17998
   117
  | isTrue _ = false;
wenzelm@24311
   118
wenzelm@24311
   119
fun isTaut (Clause {literals,...}) = exists isTrue literals;
mengj@17998
   120
mengj@18440
   121
fun type_of (Type (a, Ts)) =
paulson@21561
   122
      let val (folTypes,ts) = types_of Ts
paulson@22078
   123
      in  (RC.Comp(RC.make_fixed_type_const a, folTypes), ts)  end
mengj@18440
   124
  | type_of (tp as (TFree(a,s))) =
paulson@22078
   125
      (RC.AtomF (RC.make_fixed_type_var a), [RC.mk_typ_var_sort tp])
mengj@18440
   126
  | type_of (tp as (TVar(v,s))) =
paulson@22078
   127
      (RC.AtomV (RC.make_schematic_type_var v), [RC.mk_typ_var_sort tp])
mengj@18440
   128
and types_of Ts =
paulson@22078
   129
      let val (folTyps,ts) = ListPair.unzip (map type_of Ts)
paulson@22078
   130
      in  (folTyps, RC.union_all ts)  end;
mengj@17998
   131
mengj@17998
   132
(* same as above, but no gathering of sort information *)
wenzelm@24311
   133
fun simp_type_of (Type (a, Ts)) =
paulson@22078
   134
      RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
paulson@22078
   135
  | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
paulson@22078
   136
  | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
mengj@18440
   137
mengj@18356
   138
wenzelm@24323
   139
fun const_type_of thy (c,t) =
paulson@22078
   140
      let val (tp,ts) = type_of t
wenzelm@24323
   141
      in  (tp, ts, map simp_type_of (Sign.const_typargs thy (c,t))) end;
mengj@18356
   142
mengj@17998
   143
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
wenzelm@24323
   144
fun combterm_of thy (Const(c,t)) =
wenzelm@24323
   145
      let val (tp,ts,tvar_list) = const_type_of thy (c,t)
wenzelm@24311
   146
          val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
paulson@22078
   147
      in  (c',ts)  end
wenzelm@24323
   148
  | combterm_of thy (Free(v,t)) =
paulson@21513
   149
      let val (tp,ts) = type_of t
wenzelm@24311
   150
          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
wenzelm@24311
   151
                   else CombConst(RC.make_fixed_var v, tp, [])
paulson@22078
   152
      in  (v',ts)  end
wenzelm@24323
   153
  | combterm_of thy (Var(v,t)) =
paulson@21513
   154
      let val (tp,ts) = type_of t
wenzelm@24311
   155
          val v' = CombVar(RC.make_schematic_var v,tp)
paulson@22078
   156
      in  (v',ts)  end
paulson@24385
   157
  | combterm_of thy (P $ Q) =
wenzelm@24323
   158
      let val (P',tsP) = combterm_of thy P
wenzelm@24323
   159
          val (Q',tsQ) = combterm_of thy Q
paulson@24385
   160
      in  (CombApp(P',Q'), tsP union tsQ)  end
paulson@24385
   161
  | combterm_of thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
mengj@17998
   162
wenzelm@24323
   163
fun predicate_of thy ((Const("Not",_) $ P), polarity) = predicate_of thy (P, not polarity)
wenzelm@24323
   164
  | predicate_of thy (t,polarity) = (combterm_of thy t, polarity);
mengj@17998
   165
wenzelm@24323
   166
fun literals_of_term1 thy args (Const("Trueprop",_) $ P) = literals_of_term1 thy args P
wenzelm@24323
   167
  | literals_of_term1 thy args (Const("op |",_) $ P $ Q) =
wenzelm@24323
   168
      literals_of_term1 thy (literals_of_term1 thy args P) Q
wenzelm@24323
   169
  | literals_of_term1 thy (lits,ts) P =
wenzelm@24323
   170
      let val ((pred,ts'),pol) = predicate_of thy (P,true)
paulson@21509
   171
      in
wenzelm@24311
   172
          (Literal(pol,pred)::lits, ts union ts')
paulson@21509
   173
      end;
mengj@17998
   174
wenzelm@24323
   175
fun literals_of_term thy P = literals_of_term1 thy ([],[]) P;
mengj@17998
   176
mengj@17998
   177
(* making axiom and conjecture clauses *)
wenzelm@24323
   178
fun make_clause thy (clause_id,axiom_name,kind,th) =
paulson@24385
   179
    let val (lits,ctypes_sorts) = literals_of_term thy (prop_of th)
wenzelm@24311
   180
        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
mengj@17998
   181
    in
wenzelm@24311
   182
        if forall isFalse lits
wenzelm@24311
   183
        then error "Problem too trivial for resolution (empty clause)"
wenzelm@24311
   184
        else
wenzelm@24311
   185
            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
wenzelm@24311
   186
                    literals = lits, ctypes_sorts = ctypes_sorts,
wenzelm@24311
   187
                    ctvar_type_literals = ctvar_lits,
wenzelm@24311
   188
                    ctfree_type_literals = ctfree_lits}
mengj@17998
   189
    end;
mengj@17998
   190
mengj@20016
   191
wenzelm@24323
   192
fun add_axiom_clause thy ((th,(name,id)), pairs) =
wenzelm@24323
   193
  let val cls = make_clause thy (id, name, RC.Axiom, th)
paulson@21573
   194
  in
paulson@21573
   195
      if isTaut cls then pairs else (name,cls)::pairs
paulson@21573
   196
  end;
mengj@19354
   197
wenzelm@24323
   198
fun make_axiom_clauses thy = foldl (add_axiom_clause thy) [];
mengj@19354
   199
wenzelm@24323
   200
fun make_conjecture_clauses_aux _ _ [] = []
wenzelm@24323
   201
  | make_conjecture_clauses_aux thy n (th::ths) =
wenzelm@24323
   202
      make_clause thy (n,"conjecture", RC.Conjecture, th) ::
wenzelm@24323
   203
      make_conjecture_clauses_aux thy (n+1) ths;
mengj@17998
   204
wenzelm@24323
   205
fun make_conjecture_clauses thy = make_conjecture_clauses_aux thy 0;
mengj@17998
   206
mengj@17998
   207
mengj@17998
   208
(**********************************************************************)
mengj@17998
   209
(* convert clause into ATP specific formats:                          *)
mengj@17998
   210
(* TPTP used by Vampire and E                                         *)
mengj@19720
   211
(* DFG used by SPASS                                                  *)
mengj@17998
   212
(**********************************************************************)
mengj@17998
   213
paulson@22078
   214
(*Result of a function type; no need to check that the argument type matches.*)
paulson@22078
   215
fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
paulson@22078
   216
  | result_type _ = raise ERROR "result_type"
paulson@22078
   217
paulson@21513
   218
fun type_of_combterm (CombConst(c,tp,_)) = tp
paulson@21513
   219
  | type_of_combterm (CombVar(v,tp)) = tp
paulson@22078
   220
  | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
mengj@17998
   221
paulson@22064
   222
(*gets the head of a combinator application, along with the list of arguments*)
paulson@22064
   223
fun strip_comb u =
paulson@22078
   224
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
paulson@22064
   225
        |   stripc  x =  x
paulson@22064
   226
    in  stripc(u,[])  end;
paulson@22064
   227
paulson@22851
   228
val type_wrapper = "ti";
paulson@22851
   229
paulson@22851
   230
fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
paulson@22851
   231
  | head_needs_hBOOL _ = true;
paulson@22851
   232
wenzelm@24311
   233
fun wrap_type (s, tp) =
paulson@22851
   234
  if !typ_level=T_FULL then
paulson@22851
   235
      type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
paulson@22851
   236
  else s;
wenzelm@24311
   237
paulson@22851
   238
fun apply ss = "hAPP" ^ RC.paren_pack ss;
paulson@22851
   239
paulson@22064
   240
fun rev_apply (v, []) = v
paulson@22851
   241
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
paulson@22064
   242
paulson@22064
   243
fun string_apply (v, args) = rev_apply (v, rev args);
paulson@22064
   244
paulson@22064
   245
(*Apply an operator to the argument strings, using either the "apply" operator or
paulson@22064
   246
  direct function application.*)
paulson@22851
   247
fun string_of_applic (CombConst(c,tp,tvars), args) =
paulson@22064
   248
      let val c = if c = "equal" then "c_fequal" else c
paulson@22064
   249
          val nargs = min_arity_of c
paulson@22851
   250
          val args1 = List.take(args, nargs)
paulson@22064
   251
            handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
wenzelm@24311
   252
                                             Int.toString nargs ^ " but is applied to " ^
wenzelm@24311
   253
                                             space_implode ", " args)
paulson@22064
   254
          val args2 = List.drop(args, nargs)
paulson@22851
   255
          val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
paulson@22851
   256
                      else []
paulson@21513
   257
      in
wenzelm@24311
   258
          string_apply (c ^ RC.paren_pack (args1@targs), args2)
paulson@21513
   259
      end
paulson@22851
   260
  | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
paulson@22064
   261
  | string_of_applic _ = raise ERROR "string_of_applic";
paulson@22064
   262
paulson@22851
   263
fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
wenzelm@24311
   264
paulson@24385
   265
fun string_of_combterm t =
paulson@22064
   266
  let val (head, args) = strip_comb t
wenzelm@24311
   267
  in  wrap_type_if (head,
paulson@24385
   268
                    string_of_applic (head, map string_of_combterm args),
paulson@22851
   269
                    type_of_combterm t)
paulson@22851
   270
  end;
mengj@18356
   271
paulson@22064
   272
(*Boolean-valued terms are here converted to literals.*)
paulson@22078
   273
fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
paulson@22064
   274
wenzelm@24311
   275
fun string_of_predicate t =
paulson@22064
   276
  case t of
paulson@22078
   277
      (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
wenzelm@24311
   278
          (*DFG only: new TPTP prefers infix equality*)
wenzelm@24311
   279
          ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
wenzelm@24311
   280
    | _ =>
paulson@22064
   281
          case #1 (strip_comb t) of
paulson@22064
   282
              CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
paulson@22064
   283
            | _ => boolify t;
mengj@18356
   284
wenzelm@24311
   285
fun string_of_clausename (cls_id,ax_name) =
paulson@22078
   286
    RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
mengj@17998
   287
wenzelm@24311
   288
fun string_of_type_clsname (cls_id,ax_name,idx) =
mengj@17998
   289
    string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
mengj@17998
   290
mengj@17998
   291
paulson@21561
   292
(*** tptp format ***)
mengj@19720
   293
paulson@21513
   294
fun tptp_of_equality pol (t1,t2) =
paulson@21513
   295
  let val eqop = if pol then " = " else " != "
paulson@21513
   296
  in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
paulson@21513
   297
wenzelm@24311
   298
fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
paulson@21513
   299
      tptp_of_equality pol (t1,t2)
wenzelm@24311
   300
  | tptp_literal (Literal(pol,pred)) =
paulson@22078
   301
      RC.tptp_sign pol (string_of_predicate pred);
wenzelm@24311
   302
paulson@22064
   303
(*Given a clause, returns its literals paired with a list of literals concerning TFrees;
paulson@22064
   304
  the latter should only occur in conjecture clauses.*)
wenzelm@24311
   305
fun tptp_type_lits (Clause cls) =
mengj@17998
   306
    let val lits = map tptp_literal (#literals cls)
wenzelm@24311
   307
        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
wenzelm@24311
   308
        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
mengj@17998
   309
    in
wenzelm@24311
   310
        (ctvar_lits_strs @ lits, ctfree_lits)
wenzelm@24311
   311
    end;
wenzelm@24311
   312
paulson@21509
   313
fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
mengj@17998
   314
    let val (lits,ctfree_lits) = tptp_type_lits cls
wenzelm@24311
   315
        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
mengj@17998
   316
    in
wenzelm@24311
   317
        (cls_str,ctfree_lits)
mengj@17998
   318
    end;
mengj@17998
   319
mengj@17998
   320
paulson@21561
   321
(*** dfg format ***)
paulson@21561
   322
paulson@22078
   323
fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
mengj@19720
   324
wenzelm@24311
   325
fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
mengj@19720
   326
  let val lits = map dfg_literal literals
paulson@22078
   327
      val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
paulson@22825
   328
      val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
wenzelm@24311
   329
      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
mengj@19720
   330
  in
mengj@19720
   331
      (tvar_lits_strs @ lits, tfree_lits)
wenzelm@24311
   332
  end;
mengj@19720
   333
paulson@22078
   334
fun get_uvars (CombConst _) vars = vars
paulson@22078
   335
  | get_uvars (CombVar(v,_)) vars = (v::vars)
paulson@22078
   336
  | get_uvars (CombApp(P,Q)) vars = get_uvars P (get_uvars Q vars);
mengj@19720
   337
mengj@19720
   338
fun get_uvars_l (Literal(_,c)) = get_uvars c [];
mengj@19720
   339
paulson@22078
   340
fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
wenzelm@24311
   341
mengj@19720
   342
fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
wenzelm@24311
   343
    let val (lits,tfree_lits) = dfg_clause_aux cls
mengj@19720
   344
        val vars = dfg_vars cls
paulson@22078
   345
        val tvars = RC.get_tvar_strs ctypes_sorts
wenzelm@24311
   346
        val knd = RC.name_of_kind kind
wenzelm@24311
   347
        val lits_str = commas lits
wenzelm@24311
   348
        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
mengj@19720
   349
    in (cls_str, tfree_lits) end;
mengj@19720
   350
paulson@22064
   351
(** For DFG format: accumulate function and predicate declarations **)
mengj@19720
   352
paulson@22078
   353
fun addtypes tvars tab = foldl RC.add_foltype_funcs tab tvars;
mengj@19720
   354
paulson@22825
   355
fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
paulson@22064
   356
      if c = "equal" then (addtypes tvars funcs, preds)
paulson@21561
   357
      else
paulson@24385
   358
	let val arity = min_arity_of c
paulson@24385
   359
	    val ntys = if !typ_level = T_CONST then length tvars else 0
paulson@24385
   360
	    val addit = Symtab.update(c, arity+ntys)
paulson@24385
   361
	in
paulson@24385
   362
	    if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
paulson@24385
   363
	    else (addtypes tvars funcs, addit preds)
paulson@24385
   364
	end
wenzelm@24311
   365
  | add_decls (CombVar(_,ctp), (funcs,preds)) =
paulson@22078
   366
      (RC.add_foltype_funcs (ctp,funcs), preds)
paulson@22078
   367
  | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
mengj@19720
   368
paulson@22064
   369
fun add_literal_decls (Literal(_,c), decls) = add_decls (c,decls);
mengj@19720
   370
paulson@22064
   371
fun add_clause_decls (Clause {literals, ...}, decls) =
paulson@22064
   372
    foldl add_literal_decls decls literals
mengj@19720
   373
    handle Symtab.DUP a => raise ERROR ("function " ^ a ^ " has multiple arities")
mengj@19720
   374
paulson@22064
   375
fun decls_of_clauses clauses arity_clauses =
paulson@24385
   376
  let val init_functab = Symtab.update (type_wrapper,2) (Symtab.update ("hAPP",2) RC.init_functab)
paulson@22064
   377
      val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
paulson@22064
   378
      val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
paulson@22064
   379
  in
wenzelm@24311
   380
      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
paulson@22064
   381
       Symtab.dest predtab)
paulson@22064
   382
  end;
mengj@19720
   383
paulson@21398
   384
fun add_clause_preds (Clause {ctypes_sorts, ...}, preds) =
paulson@22078
   385
  foldl RC.add_type_sort_preds preds ctypes_sorts
paulson@21398
   386
  handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
paulson@21398
   387
paulson@21398
   388
(*Higher-order clauses have only the predicates hBOOL and type classes.*)
wenzelm@24311
   389
fun preds_of_clauses clauses clsrel_clauses arity_clauses =
mengj@19720
   390
    Symtab.dest
wenzelm@24311
   391
        (foldl RC.add_classrelClause_preds
wenzelm@24311
   392
               (foldl RC.add_arityClause_preds
wenzelm@24311
   393
                      (foldl add_clause_preds Symtab.empty clauses)
wenzelm@24311
   394
                      arity_clauses)
wenzelm@24311
   395
               clsrel_clauses)
mengj@19720
   396
mengj@18440
   397
mengj@18440
   398
(**********************************************************************)
mengj@19198
   399
(* write clauses to files                                             *)
mengj@19198
   400
(**********************************************************************)
mengj@19198
   401
paulson@21573
   402
val init_counters =
paulson@21573
   403
    Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
wenzelm@24311
   404
                 ("c_COMBB", 0), ("c_COMBC", 0),
wenzelm@24311
   405
                 ("c_COMBS", 0), ("c_COMBB_e", 0),
wenzelm@24311
   406
                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
wenzelm@24311
   407
wenzelm@24311
   408
fun count_combterm (CombConst(c,tp,_), ct) =
paulson@21573
   409
     (case Symtab.lookup ct c of NONE => ct  (*no counter*)
paulson@21573
   410
                               | SOME n => Symtab.update (c,n+1) ct)
paulson@21573
   411
  | count_combterm (CombVar(v,tp), ct) = ct
paulson@22078
   412
  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
paulson@21573
   413
paulson@21573
   414
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
paulson@21573
   415
paulson@21573
   416
fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
paulson@21573
   417
wenzelm@24311
   418
fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
paulson@21573
   419
  if axiom_name mem_string user_lemmas then foldl count_literal ct literals
paulson@21573
   420
  else ct;
paulson@21573
   421
mengj@20791
   422
val cnf_helper_thms = ResAxioms.cnf_rules_pairs o (map ResAxioms.pairname)
mengj@20644
   423
wenzelm@24323
   424
fun get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas) =
paulson@23386
   425
  if isFO then []  (*first-order*)
paulson@23386
   426
  else
paulson@22064
   427
    let val ct0 = foldl count_clause init_counters conjectures
paulson@22064
   428
        val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
paulson@22064
   429
        fun needed c = valOf (Symtab.lookup ct c) > 0
wenzelm@24311
   430
        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
wenzelm@24311
   431
                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
wenzelm@24311
   432
                 else []
wenzelm@24311
   433
        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
wenzelm@24311
   434
                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
paulson@21135
   435
                 else []
wenzelm@24311
   436
        val S = if needed "c_COMBS"
wenzelm@24311
   437
                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
wenzelm@24311
   438
                else []
wenzelm@24311
   439
        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
wenzelm@24311
   440
                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
wenzelm@24311
   441
                   else []
wenzelm@24311
   442
        val S' = if needed "c_COMBS_e"
wenzelm@24311
   443
                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
wenzelm@24311
   444
                 else []
wenzelm@24311
   445
        val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
mengj@20791
   446
    in
wenzelm@24323
   447
        map #2 (make_axiom_clauses thy (other @ IK @ BC @ S @ B'C' @ S'))
paulson@23386
   448
    end;
mengj@20791
   449
paulson@22064
   450
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
paulson@22064
   451
  are not at top level, to see if hBOOL is needed.*)
paulson@22064
   452
fun count_constants_term toplev t =
paulson@22064
   453
  let val (head, args) = strip_comb t
paulson@22064
   454
      val n = length args
paulson@22064
   455
      val _ = List.app (count_constants_term false) args
paulson@22064
   456
  in
paulson@22064
   457
      case head of
wenzelm@24311
   458
          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
wenzelm@24311
   459
            let val a = if a="equal" andalso not toplev then "c_fequal" else a
wenzelm@24311
   460
            in
wenzelm@24311
   461
              const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
wenzelm@24311
   462
              if toplev then ()
wenzelm@24311
   463
              else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
wenzelm@24311
   464
            end
wenzelm@24311
   465
        | ts => ()
paulson@22064
   466
  end;
paulson@22064
   467
paulson@22064
   468
(*A literal is a top-level term*)
paulson@22064
   469
fun count_constants_lit (Literal (_,t)) = count_constants_term true t;
paulson@22064
   470
paulson@22064
   471
fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
paulson@22064
   472
paulson@22064
   473
fun display_arity (c,n) =
wenzelm@24311
   474
  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
paulson@22064
   475
                (if needs_hBOOL c then " needs hBOOL" else ""));
paulson@22064
   476
wenzelm@24311
   477
fun count_constants (conjectures, axclauses, helper_clauses) =
paulson@24385
   478
  if !minimize_applies then
wenzelm@24311
   479
    (const_min_arity := Symtab.empty;
paulson@23386
   480
     const_needs_hBOOL := Symtab.empty;
paulson@23386
   481
     List.app count_constants_clause conjectures;
paulson@22064
   482
     List.app count_constants_clause axclauses;
paulson@22064
   483
     List.app count_constants_clause helper_clauses;
paulson@22064
   484
     List.app display_arity (Symtab.dest (!const_min_arity)))
paulson@22064
   485
  else ();
paulson@22064
   486
mengj@20791
   487
(* tptp format *)
wenzelm@24311
   488
mengj@19198
   489
(* write TPTP format to a single file *)
wenzelm@24323
   490
fun tptp_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
paulson@23386
   491
    let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
paulson@23386
   492
        val _ = RC.dfg_format := false
wenzelm@24323
   493
        val conjectures = make_conjecture_clauses thy thms
wenzelm@24323
   494
        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
wenzelm@24323
   495
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
wenzelm@24311
   496
        val _ = count_constants (conjectures, axclauses, helper_clauses);
wenzelm@24311
   497
        val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
wenzelm@24311
   498
        val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
paulson@22064
   499
        val out = TextIO.openOut filename
mengj@19198
   500
    in
wenzelm@24311
   501
        List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
wenzelm@24311
   502
        RC.writeln_strs out tfree_clss;
wenzelm@24311
   503
        RC.writeln_strs out tptp_clss;
wenzelm@24311
   504
        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
wenzelm@24311
   505
        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
wenzelm@24311
   506
        List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
wenzelm@24311
   507
        TextIO.closeOut out;
wenzelm@24311
   508
        clnames
mengj@19198
   509
    end;
mengj@19198
   510
mengj@19720
   511
mengj@20644
   512
mengj@19720
   513
(* dfg format *)
mengj@19720
   514
wenzelm@24323
   515
fun dfg_write_file thy isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
paulson@23386
   516
    let val _ = Output.debug (fn () => ("Preparing to write the DFG file " ^ filename))
paulson@23386
   517
        val _ = RC.dfg_format := true
wenzelm@24323
   518
        val conjectures = make_conjecture_clauses thy thms
wenzelm@24323
   519
        val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses thy ax_tuples)
wenzelm@24323
   520
        val helper_clauses = get_helper_clauses thy isFO (conjectures, axclauses, user_lemmas)
wenzelm@24311
   521
        val _ = count_constants (conjectures, axclauses, helper_clauses);
wenzelm@24323
   522
        val (dfg_clss, tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
wenzelm@24311
   523
        and probname = Path.implode (Path.base (Path.explode filename))
wenzelm@24311
   524
        val axstrs = map (#1 o clause2dfg) axclauses
wenzelm@24311
   525
        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
wenzelm@24311
   526
        val out = TextIO.openOut filename
wenzelm@24311
   527
        val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
wenzelm@24311
   528
        val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
wenzelm@24311
   529
        and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
mengj@19720
   530
    in
wenzelm@24311
   531
        TextIO.output (out, RC.string_of_start probname);
wenzelm@24311
   532
        TextIO.output (out, RC.string_of_descrip probname);
wenzelm@24311
   533
        TextIO.output (out, RC.string_of_symbols
wenzelm@24311
   534
                              (RC.string_of_funcs funcs)
wenzelm@24311
   535
                              (RC.string_of_preds (cl_preds @ ty_preds)));
wenzelm@24311
   536
        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
wenzelm@24311
   537
        RC.writeln_strs out axstrs;
wenzelm@24311
   538
        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
wenzelm@24311
   539
        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
wenzelm@24311
   540
        RC.writeln_strs out helper_clauses_strs;
wenzelm@24311
   541
        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
wenzelm@24311
   542
        RC.writeln_strs out tfree_clss;
wenzelm@24311
   543
        RC.writeln_strs out dfg_clss;
wenzelm@24311
   544
        TextIO.output (out, "end_of_list.\n\n");
wenzelm@24311
   545
        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
wenzelm@24311
   546
        TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
wenzelm@24311
   547
        TextIO.output (out, "end_problem.\n");
wenzelm@24311
   548
        TextIO.closeOut out;
wenzelm@24311
   549
        clnames
mengj@19720
   550
    end;
mengj@19720
   551
wenzelm@21254
   552
end