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