src/HOL/Tools/res_hol_clause.ML
author immler@in.tum.de
Sun Jun 28 15:01:28 2009 +0200 (2009-06-28)
changeset 31837 a50de97f1b08
parent 31800 477f2abf90a4
child 31838 607a984b70e3
permissions -rw-r--r--
whitelist for HOL problems with ext:
as a 'helper clause' ext was not passed to metis, but metis does not include ext
wenzelm@30190
     1
(*
mengj@17998
     2
   Author: Jia Meng, NICTA
mengj@17998
     3
wenzelm@24311
     4
FOL clauses translated from HOL formulae.
mengj@17998
     5
*)
mengj@17998
     6
wenzelm@24311
     7
signature RES_HOL_CLAUSE =
wenzelm@24311
     8
sig
wenzelm@24311
     9
  val ext: thm
wenzelm@24311
    10
  val comb_I: thm
wenzelm@24311
    11
  val comb_K: thm
wenzelm@24311
    12
  val comb_B: thm
wenzelm@24311
    13
  val comb_C: thm
wenzelm@24311
    14
  val comb_S: thm
wenzelm@30153
    15
  val minimize_applies: bool
wenzelm@24311
    16
  type axiom_name = string
wenzelm@24311
    17
  type polarity = bool
wenzelm@24311
    18
  type clause_id = int
wenzelm@24311
    19
  datatype combterm =
wenzelm@24311
    20
      CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
wenzelm@24311
    21
    | CombVar of string * ResClause.fol_type
wenzelm@24311
    22
    | CombApp of combterm * combterm
wenzelm@24311
    23
  datatype literal = Literal of polarity * combterm
immler@31409
    24
  datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm,
immler@31409
    25
                    kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list}
wenzelm@24311
    26
  val strip_comb: combterm -> combterm * combterm list
paulson@24940
    27
  val literals_of_term: theory -> term -> literal list * typ list
wenzelm@28835
    28
  exception TOO_TRIVIAL
immler@31752
    29
  val make_conjecture_clauses:  bool -> theory -> thm list -> clause list (* dfg thy ccls *)
immler@31752
    30
  val make_axiom_clauses: bool ->
immler@31752
    31
       theory ->
immler@31752
    32
       (thm * (axiom_name * clause_id)) list -> (axiom_name * clause) list (* dfg thy axcls *)
immler@31752
    33
  val get_helper_clauses: bool ->
immler@31752
    34
       theory ->
immler@31752
    35
       bool ->
immler@31752
    36
       clause list * (thm * (axiom_name * clause_id)) list * string list ->
immler@31752
    37
       clause list
nipkow@31791
    38
  val tptp_write_file: bool -> string ->
immler@31409
    39
    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
nipkow@31791
    40
  val dfg_write_file: bool -> string -> 
immler@31409
    41
    clause list * clause list * clause list * ResClause.classrelClause list * ResClause.arityClause list -> unit
wenzelm@24311
    42
end
mengj@17998
    43
wenzelm@24311
    44
structure ResHolClause: RES_HOL_CLAUSE =
mengj@17998
    45
struct
mengj@17998
    46
paulson@22078
    47
structure RC = ResClause;
paulson@22078
    48
mengj@20791
    49
(* theorems for combinators and function extensionality *)
mengj@20791
    50
val ext = thm "HOL.ext";
wenzelm@21254
    51
val comb_I = thm "ATP_Linkup.COMBI_def";
wenzelm@21254
    52
val comb_K = thm "ATP_Linkup.COMBK_def";
wenzelm@21254
    53
val comb_B = thm "ATP_Linkup.COMBB_def";
wenzelm@21254
    54
val comb_C = thm "ATP_Linkup.COMBC_def";
wenzelm@21254
    55
val comb_S = thm "ATP_Linkup.COMBS_def";
wenzelm@21254
    56
val fequal_imp_equal = thm "ATP_Linkup.fequal_imp_equal";
wenzelm@21254
    57
val equal_imp_fequal = thm "ATP_Linkup.equal_imp_fequal";
mengj@20791
    58
paulson@22825
    59
nipkow@31800
    60
(* Parameter t_full below indicates that full type information is to be
nipkow@31800
    61
exported *)
paulson@22825
    62
paulson@22064
    63
(*If true, each function will be directly applied to as many arguments as possible, avoiding
paulson@24385
    64
  use of the "apply" operator. Use of hBOOL is also minimized.*)
wenzelm@30153
    65
val minimize_applies = true;
paulson@22064
    66
immler@30149
    67
fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
paulson@22064
    68
paulson@22825
    69
(*True if the constant ever appears outside of the top-level position in literals.
paulson@22825
    70
  If false, the constant always receives all of its arguments and is used as a predicate.*)
wenzelm@30153
    71
fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
immler@30150
    72
                    getOpt (Symtab.lookup const_needs_hBOOL c, false);
paulson@22064
    73
mengj@19198
    74
mengj@17998
    75
(******************************************************)
mengj@17998
    76
(* data types for typed combinator expressions        *)
mengj@17998
    77
(******************************************************)
mengj@17998
    78
mengj@17998
    79
type axiom_name = string;
mengj@17998
    80
type polarity = bool;
mengj@17998
    81
type clause_id = int;
mengj@17998
    82
paulson@23386
    83
datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
wenzelm@24311
    84
                  | CombVar of string * RC.fol_type
wenzelm@24311
    85
                  | CombApp of combterm * combterm
wenzelm@24311
    86
mengj@17998
    87
datatype literal = Literal of polarity * combterm;
mengj@17998
    88
wenzelm@24311
    89
datatype clause =
wenzelm@24311
    90
         Clause of {clause_id: clause_id,
wenzelm@24311
    91
                    axiom_name: axiom_name,
wenzelm@24311
    92
                    th: thm,
wenzelm@24311
    93
                    kind: RC.kind,
wenzelm@24311
    94
                    literals: literal list,
paulson@24940
    95
                    ctypes_sorts: typ list};
mengj@17998
    96
mengj@17998
    97
mengj@17998
    98
(*********************************************************************)
mengj@17998
    99
(* convert a clause with type Term.term to a clause with type clause *)
mengj@17998
   100
(*********************************************************************)
mengj@17998
   101
paulson@21561
   102
fun isFalse (Literal(pol, CombConst(c,_,_))) =
paulson@20360
   103
      (pol andalso c = "c_False") orelse
paulson@20360
   104
      (not pol andalso c = "c_True")
mengj@17998
   105
  | isFalse _ = false;
mengj@17998
   106
paulson@21561
   107
fun isTrue (Literal (pol, CombConst(c,_,_))) =
mengj@17998
   108
      (pol andalso c = "c_True") orelse
mengj@17998
   109
      (not pol andalso c = "c_False")
mengj@17998
   110
  | isTrue _ = false;
wenzelm@24311
   111
wenzelm@24311
   112
fun isTaut (Clause {literals,...}) = exists isTrue literals;
mengj@17998
   113
immler@30151
   114
fun type_of dfg (Type (a, Ts)) =
immler@30151
   115
      let val (folTypes,ts) = types_of dfg Ts
immler@30151
   116
      in  (RC.Comp(RC.make_fixed_type_const dfg a, folTypes), ts)  end
immler@30151
   117
  | type_of dfg (tp as (TFree(a,s))) =
paulson@24940
   118
      (RC.AtomF (RC.make_fixed_type_var a), [tp])
immler@30151
   119
  | type_of dfg (tp as (TVar(v,s))) =
paulson@24940
   120
      (RC.AtomV (RC.make_schematic_type_var v), [tp])
immler@30151
   121
and types_of dfg Ts =
immler@30151
   122
      let val (folTyps,ts) = ListPair.unzip (map (type_of dfg) Ts)
paulson@22078
   123
      in  (folTyps, RC.union_all ts)  end;
mengj@17998
   124
mengj@17998
   125
(* same as above, but no gathering of sort information *)
immler@30151
   126
fun simp_type_of dfg (Type (a, Ts)) =
immler@30151
   127
      RC.Comp(RC.make_fixed_type_const dfg a, map (simp_type_of dfg) Ts)
immler@30151
   128
  | simp_type_of dfg (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
immler@30151
   129
  | simp_type_of dfg (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
mengj@18440
   130
mengj@18356
   131
immler@30151
   132
fun const_type_of dfg thy (c,t) =
immler@30151
   133
      let val (tp,ts) = type_of dfg t
immler@30151
   134
      in  (tp, ts, map (simp_type_of dfg) (Sign.const_typargs thy (c,t))) end;
mengj@18356
   135
mengj@17998
   136
(* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
immler@30151
   137
fun combterm_of dfg thy (Const(c,t)) =
immler@30151
   138
      let val (tp,ts,tvar_list) = const_type_of dfg thy (c,t)
immler@30151
   139
          val c' = CombConst(RC.make_fixed_const dfg c, tp, tvar_list)
paulson@22078
   140
      in  (c',ts)  end
immler@30151
   141
  | combterm_of dfg thy (Free(v,t)) =
immler@30151
   142
      let val (tp,ts) = type_of dfg t
paulson@25243
   143
          val v' = CombConst(RC.make_fixed_var v, tp, [])
paulson@22078
   144
      in  (v',ts)  end
immler@30151
   145
  | combterm_of dfg thy (Var(v,t)) =
immler@30151
   146
      let val (tp,ts) = type_of dfg t
wenzelm@24311
   147
          val v' = CombVar(RC.make_schematic_var v,tp)
paulson@22078
   148
      in  (v',ts)  end
immler@30151
   149
  | combterm_of dfg thy (P $ Q) =
immler@30151
   150
      let val (P',tsP) = combterm_of dfg thy P
immler@30151
   151
          val (Q',tsQ) = combterm_of dfg thy Q
paulson@24385
   152
      in  (CombApp(P',Q'), tsP union tsQ)  end
immler@30151
   153
  | combterm_of _ thy (t as Abs _) = raise RC.CLAUSE("HOL CLAUSE",t);
mengj@17998
   154
immler@30151
   155
fun predicate_of dfg thy ((Const("Not",_) $ P), polarity) = predicate_of dfg thy (P, not polarity)
immler@30151
   156
  | predicate_of dfg thy (t,polarity) = (combterm_of dfg thy (Envir.eta_contract t), polarity);
mengj@17998
   157
immler@30151
   158
fun literals_of_term1 dfg thy args (Const("Trueprop",_) $ P) = literals_of_term1 dfg thy args P
immler@30151
   159
  | literals_of_term1 dfg thy args (Const("op |",_) $ P $ Q) =
immler@30151
   160
      literals_of_term1 dfg thy (literals_of_term1 dfg thy args P) Q
immler@30151
   161
  | literals_of_term1 dfg thy (lits,ts) P =
immler@30151
   162
      let val ((pred,ts'),pol) = predicate_of dfg thy (P,true)
paulson@21509
   163
      in
wenzelm@24311
   164
          (Literal(pol,pred)::lits, ts union ts')
paulson@21509
   165
      end;
mengj@17998
   166
immler@30151
   167
fun literals_of_term_dfg dfg thy P = literals_of_term1 dfg thy ([],[]) P;
immler@30151
   168
val literals_of_term = literals_of_term_dfg false;
mengj@17998
   169
wenzelm@28835
   170
(* Problem too trivial for resolution (empty clause) *)
wenzelm@28835
   171
exception TOO_TRIVIAL;
wenzelm@28835
   172
mengj@17998
   173
(* making axiom and conjecture clauses *)
immler@30151
   174
fun make_clause dfg thy (clause_id,axiom_name,kind,th) =
immler@30151
   175
    let val (lits,ctypes_sorts) = literals_of_term_dfg dfg thy (prop_of th)
mengj@17998
   176
    in
wenzelm@24311
   177
        if forall isFalse lits
wenzelm@28835
   178
        then raise TOO_TRIVIAL
wenzelm@24311
   179
        else
wenzelm@24311
   180
            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
paulson@24937
   181
                    literals = lits, ctypes_sorts = ctypes_sorts}
mengj@17998
   182
    end;
mengj@17998
   183
mengj@20016
   184
immler@30151
   185
fun add_axiom_clause dfg thy ((th,(name,id)), pairs) =
immler@30151
   186
  let val cls = make_clause dfg thy (id, name, RC.Axiom, th)
paulson@21573
   187
  in
paulson@21573
   188
      if isTaut cls then pairs else (name,cls)::pairs
paulson@21573
   189
  end;
mengj@19354
   190
wenzelm@30190
   191
fun make_axiom_clauses dfg thy = List.foldl (add_axiom_clause dfg thy) [];
mengj@19354
   192
immler@30151
   193
fun make_conjecture_clauses_aux dfg _ _ [] = []
immler@30151
   194
  | make_conjecture_clauses_aux dfg thy n (th::ths) =
immler@30151
   195
      make_clause dfg thy (n,"conjecture", RC.Conjecture, th) ::
immler@30151
   196
      make_conjecture_clauses_aux dfg thy (n+1) ths;
mengj@17998
   197
immler@30151
   198
fun make_conjecture_clauses dfg thy = make_conjecture_clauses_aux dfg thy 0;
mengj@17998
   199
mengj@17998
   200
mengj@17998
   201
(**********************************************************************)
mengj@17998
   202
(* convert clause into ATP specific formats:                          *)
mengj@17998
   203
(* TPTP used by Vampire and E                                         *)
mengj@19720
   204
(* DFG used by SPASS                                                  *)
mengj@17998
   205
(**********************************************************************)
mengj@17998
   206
paulson@22078
   207
(*Result of a function type; no need to check that the argument type matches.*)
paulson@22078
   208
fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2
wenzelm@27187
   209
  | result_type _ = error "result_type"
paulson@22078
   210
paulson@21513
   211
fun type_of_combterm (CombConst(c,tp,_)) = tp
paulson@21513
   212
  | type_of_combterm (CombVar(v,tp)) = tp
paulson@22078
   213
  | type_of_combterm (CombApp(t1,t2)) = result_type (type_of_combterm t1);
mengj@17998
   214
paulson@22064
   215
(*gets the head of a combinator application, along with the list of arguments*)
paulson@22064
   216
fun strip_comb u =
paulson@22078
   217
    let fun stripc (CombApp(t,u), ts) = stripc (t, u::ts)
paulson@22064
   218
        |   stripc  x =  x
paulson@22064
   219
    in  stripc(u,[])  end;
paulson@22064
   220
paulson@22851
   221
val type_wrapper = "ti";
paulson@22851
   222
immler@30150
   223
fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
immler@30150
   224
  | head_needs_hBOOL const_needs_hBOOL _ = true;
paulson@22851
   225
nipkow@31791
   226
fun wrap_type t_full (s, tp) =
nipkow@31791
   227
  if t_full then
paulson@22851
   228
      type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
paulson@22851
   229
  else s;
wenzelm@24311
   230
paulson@22851
   231
fun apply ss = "hAPP" ^ RC.paren_pack ss;
paulson@22851
   232
paulson@22064
   233
fun rev_apply (v, []) = v
paulson@22851
   234
  | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg];
paulson@22064
   235
paulson@22064
   236
fun string_apply (v, args) = rev_apply (v, rev args);
paulson@22064
   237
paulson@22064
   238
(*Apply an operator to the argument strings, using either the "apply" operator or
paulson@22064
   239
  direct function application.*)
nipkow@31791
   240
fun string_of_applic t_full cma (CombConst(c,tp,tvars), args) =
paulson@22064
   241
      let val c = if c = "equal" then "c_fequal" else c
immler@30150
   242
          val nargs = min_arity_of cma c
paulson@22851
   243
          val args1 = List.take(args, nargs)
wenzelm@27187
   244
            handle Subscript => error ("string_of_applic: " ^ c ^ " has arity " ^
wenzelm@27187
   245
                                         Int.toString nargs ^ " but is applied to " ^
wenzelm@27187
   246
                                         space_implode ", " args)
paulson@22064
   247
          val args2 = List.drop(args, nargs)
nipkow@31791
   248
          val targs = if not t_full then map RC.string_of_fol_type tvars
paulson@22851
   249
                      else []
paulson@21513
   250
      in
wenzelm@24311
   251
          string_apply (c ^ RC.paren_pack (args1@targs), args2)
paulson@21513
   252
      end
nipkow@31791
   253
  | string_of_applic _ cma (CombVar(v,tp), args) = string_apply (v, args)
nipkow@31791
   254
  | string_of_applic _ _ _ = error "string_of_applic";
wenzelm@24311
   255
nipkow@31791
   256
fun wrap_type_if t_full cnh (head, s, tp) =
nipkow@31791
   257
  if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
nipkow@31791
   258
nipkow@31800
   259
fun string_of_combterm (params as (t_full, cma, cnh)) t =
paulson@22064
   260
  let val (head, args) = strip_comb t
nipkow@31791
   261
  in  wrap_type_if t_full cnh (head,
nipkow@31800
   262
                    string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
paulson@22851
   263
                    type_of_combterm t)
paulson@22851
   264
  end;
mengj@18356
   265
paulson@22064
   266
(*Boolean-valued terms are here converted to literals.*)
nipkow@31800
   267
fun boolify params t =
nipkow@31800
   268
  "hBOOL" ^ RC.paren_pack [string_of_combterm params t];
paulson@22064
   269
nipkow@31800
   270
fun string_of_predicate (params as (_,_,cnh)) 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*)
nipkow@31800
   274
          ("equal" ^ RC.paren_pack [string_of_combterm params t1, string_of_combterm params t2])
wenzelm@24311
   275
    | _ =>
paulson@22064
   276
          case #1 (strip_comb t) of
nipkow@31800
   277
              CombConst(c,_,_) => if needs_hBOOL cnh c then boolify params t else string_of_combterm params t
nipkow@31800
   278
            | _ => boolify params 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
nipkow@31800
   289
fun tptp_of_equality params pol (t1,t2) =
paulson@21513
   290
  let val eqop = if pol then " = " else " != "
nipkow@31800
   291
  in  string_of_combterm params t1 ^ eqop ^ string_of_combterm params t2  end;
paulson@21513
   292
nipkow@31800
   293
fun tptp_literal params (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
nipkow@31800
   294
      tptp_of_equality params pol (t1,t2)
nipkow@31800
   295
  | tptp_literal params (Literal(pol,pred)) =
nipkow@31800
   296
      RC.tptp_sign pol (string_of_predicate params 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.*)
nipkow@31800
   300
fun tptp_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
nipkow@31800
   301
      (map (tptp_literal params) literals, 
paulson@24937
   302
       map (RC.tptp_of_typeLit pos) (RC.add_typs ctypes_sorts));
wenzelm@24311
   303
nipkow@31800
   304
fun clause2tptp params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
nipkow@31800
   305
  let val (lits,tylits) = tptp_type_lits params (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
nipkow@31800
   313
fun dfg_literal params (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate params pred);
mengj@19720
   314
nipkow@31800
   315
fun dfg_type_lits params pos (Clause{literals, ctypes_sorts, ...}) =
nipkow@31800
   316
      (map (dfg_literal params) 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
nipkow@31800
   327
fun clause2dfg params (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
nipkow@31800
   328
  let val (lits,tylits) = dfg_type_lits params (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
wenzelm@30190
   338
fun addtypes tvars tab = List.foldl RC.add_foltype_funcs tab tvars;
mengj@19720
   339
nipkow@31800
   340
fun add_decls (t_full, cma, cnh) (CombConst(c,tp,tvars), (funcs,preds)) =
paulson@22064
   341
      if c = "equal" then (addtypes tvars funcs, preds)
paulson@21561
   342
      else
immler@30150
   343
	let val arity = min_arity_of cma c
nipkow@31791
   344
	    val ntys = if not t_full then length tvars else 0
paulson@24385
   345
	    val addit = Symtab.update(c, arity+ntys)
paulson@24385
   346
	in
immler@30150
   347
	    if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
paulson@24385
   348
	    else (addtypes tvars funcs, addit preds)
paulson@24385
   349
	end
nipkow@31800
   350
  | add_decls _ (CombVar(_,ctp), (funcs,preds)) =
paulson@22078
   351
      (RC.add_foltype_funcs (ctp,funcs), preds)
nipkow@31800
   352
  | add_decls params (CombApp(P,Q),decls) = add_decls params (P,add_decls params (Q,decls));
mengj@19720
   353
nipkow@31800
   354
fun add_literal_decls params (Literal(_,c), decls) = add_decls params (c,decls);
mengj@19720
   355
nipkow@31800
   356
fun add_clause_decls params (Clause {literals, ...}, decls) =
nipkow@31800
   357
    List.foldl (add_literal_decls params) decls literals
wenzelm@27187
   358
    handle Symtab.DUP a => error ("function " ^ a ^ " has multiple arities")
mengj@19720
   359
nipkow@31800
   360
fun decls_of_clauses params 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
nipkow@31800
   363
      val (functab,predtab) = (List.foldl (add_clause_decls params) (init_functab, init_predtab) clauses)
paulson@22064
   364
  in
wenzelm@30190
   365
      (Symtab.dest (List.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) =
wenzelm@30190
   370
  List.foldl RC.add_type_sort_preds preds ctypes_sorts
wenzelm@27187
   371
  handle Symtab.DUP a => 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@30190
   376
        (List.foldl RC.add_classrelClause_preds
wenzelm@30190
   377
               (List.foldl RC.add_arityClause_preds
wenzelm@30190
   378
                      (List.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),
paulson@24943
   390
                 ("c_COMBS", 0)];
wenzelm@24311
   391
wenzelm@24311
   392
fun count_combterm (CombConst(c,tp,_), ct) =
paulson@21573
   393
     (case Symtab.lookup ct c of NONE => ct  (*no counter*)
paulson@21573
   394
                               | SOME n => Symtab.update (c,n+1) ct)
paulson@21573
   395
  | count_combterm (CombVar(v,tp), ct) = ct
paulson@22078
   396
  | count_combterm (CombApp(t1,t2), ct) = count_combterm(t1, count_combterm(t2, ct));
paulson@21573
   397
paulson@21573
   398
fun count_literal (Literal(_,t), ct) = count_combterm(t,ct);
paulson@21573
   399
wenzelm@30190
   400
fun count_clause (Clause{literals,...}, ct) = List.foldl count_literal ct literals;
paulson@21573
   401
wenzelm@24311
   402
fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
wenzelm@30190
   403
  if axiom_name mem_string user_lemmas then List.foldl count_literal ct literals
paulson@21573
   404
  else ct;
paulson@21573
   405
wenzelm@27178
   406
fun cnf_helper_thms thy =
wenzelm@27178
   407
  ResAxioms.cnf_rules_pairs thy o map ResAxioms.pairname
mengj@20644
   408
immler@31752
   409
fun get_helper_clauses dfg thy isFO (conjectures, axcls, user_lemmas) =
paulson@23386
   410
  if isFO then []  (*first-order*)
paulson@23386
   411
  else
immler@31752
   412
    let
immler@31752
   413
        val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
immler@31752
   414
        val ct0 = List.foldl count_clause init_counters conjectures
wenzelm@30190
   415
        val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
paulson@22064
   416
        fun needed c = valOf (Symtab.lookup ct c) > 0
wenzelm@24311
   417
        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
wenzelm@27178
   418
                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms thy [comb_I,comb_K])
wenzelm@24311
   419
                 else []
wenzelm@24311
   420
        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
wenzelm@27178
   421
                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms thy [comb_B,comb_C])
paulson@21135
   422
                 else []
wenzelm@24311
   423
        val S = if needed "c_COMBS"
wenzelm@27178
   424
                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms thy [comb_S])
wenzelm@24311
   425
                else []
immler@31837
   426
        val other = cnf_helper_thms thy [fequal_imp_equal,equal_imp_fequal]
mengj@20791
   427
    in
immler@30151
   428
        map #2 (make_axiom_clauses dfg thy (other @ IK @ BC @ S))
paulson@23386
   429
    end;
mengj@20791
   430
paulson@22064
   431
(*Find the minimal arity of each function mentioned in the term. Also, note which uses
paulson@22064
   432
  are not at top level, to see if hBOOL is needed.*)
immler@30150
   433
fun count_constants_term toplev t (const_min_arity, const_needs_hBOOL) =
paulson@22064
   434
  let val (head, args) = strip_comb t
paulson@22064
   435
      val n = length args
immler@30150
   436
      val (const_min_arity, const_needs_hBOOL) = fold (count_constants_term false) args (const_min_arity, const_needs_hBOOL)
paulson@22064
   437
  in
paulson@22064
   438
      case head of
wenzelm@24311
   439
          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
wenzelm@24311
   440
            let val a = if a="equal" andalso not toplev then "c_fequal" else a
immler@30149
   441
            val const_min_arity = Symtab.map_default (a,n) (curry Int.min n) const_min_arity
wenzelm@24311
   442
            in
immler@30150
   443
              if toplev then (const_min_arity, const_needs_hBOOL)
immler@30150
   444
              else (const_min_arity, Symtab.update (a,true) (const_needs_hBOOL))
wenzelm@24311
   445
            end
immler@30150
   446
        | ts => (const_min_arity, const_needs_hBOOL)
paulson@22064
   447
  end;
paulson@22064
   448
paulson@22064
   449
(*A literal is a top-level term*)
immler@30150
   450
fun count_constants_lit (Literal (_,t)) (const_min_arity, const_needs_hBOOL) =
immler@30150
   451
  count_constants_term true t (const_min_arity, const_needs_hBOOL);
paulson@22064
   452
immler@30150
   453
fun count_constants_clause (Clause{literals,...}) (const_min_arity, const_needs_hBOOL) =
immler@30150
   454
  fold count_constants_lit literals (const_min_arity, const_needs_hBOOL);
paulson@22064
   455
immler@30150
   456
fun display_arity const_needs_hBOOL (c,n) =
wenzelm@24311
   457
  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
immler@30150
   458
                (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
paulson@22064
   459
immler@31409
   460
fun count_constants (conjectures, axclauses, helper_clauses, _, _) =
wenzelm@30153
   461
  if minimize_applies then
immler@30150
   462
     let val (const_min_arity, const_needs_hBOOL) =
immler@30150
   463
          fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
immler@30149
   464
       |> fold count_constants_clause axclauses
immler@30149
   465
       |> fold count_constants_clause helper_clauses
immler@30150
   466
     val _ = List.app (display_arity const_needs_hBOOL) (Symtab.dest (const_min_arity))
immler@30150
   467
     in (const_min_arity, const_needs_hBOOL) end
immler@30150
   468
  else (Symtab.empty, Symtab.empty);
paulson@22064
   469
immler@31749
   470
(* tptp format *)
immler@31749
   471
nipkow@31791
   472
fun tptp_write_file t_full filename clauses =
immler@31409
   473
  let
immler@31752
   474
    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
nipkow@31791
   475
    val (cma, cnh) = count_constants clauses
nipkow@31791
   476
    val params = (t_full, cma, cnh)
nipkow@31791
   477
    val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
immler@31409
   478
    val tfree_clss = map RC.tptp_tfree_clause (List.foldl (op union_string) [] tfree_litss)
immler@31409
   479
    val out = TextIO.openOut filename
immler@31409
   480
  in
nipkow@31791
   481
    List.app (curry TextIO.output out o #1 o (clause2tptp params)) axclauses;
immler@31409
   482
    RC.writeln_strs out tfree_clss;
immler@31409
   483
    RC.writeln_strs out tptp_clss;
immler@31409
   484
    List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
immler@31409
   485
    List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
nipkow@31791
   486
    List.app (curry TextIO.output out o #1 o (clause2tptp params)) helper_clauses;
immler@31409
   487
    TextIO.closeOut out
immler@31409
   488
  end;
mengj@19198
   489
mengj@19720
   490
mengj@19720
   491
(* dfg format *)
mengj@19720
   492
nipkow@31791
   493
fun dfg_write_file t_full filename clauses =
immler@31409
   494
  let
immler@31752
   495
    val (conjectures, axclauses, helper_clauses, classrel_clauses, arity_clauses) = clauses
nipkow@31791
   496
    val (cma, cnh) = count_constants clauses
nipkow@31791
   497
    val params = (t_full, cma, cnh)
nipkow@31791
   498
    val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
immler@31409
   499
    and probname = Path.implode (Path.base (Path.explode filename))
nipkow@31791
   500
    val axstrs = map (#1 o (clause2dfg params)) axclauses
immler@31409
   501
    val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
immler@31409
   502
    val out = TextIO.openOut filename
nipkow@31791
   503
    val helper_clauses_strs = map (#1 o (clause2dfg params)) helper_clauses
nipkow@31791
   504
    val (funcs,cl_preds) = decls_of_clauses params (helper_clauses @ conjectures @ axclauses) arity_clauses
immler@31409
   505
    and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
immler@31409
   506
  in
immler@31409
   507
    TextIO.output (out, RC.string_of_start probname);
immler@31409
   508
    TextIO.output (out, RC.string_of_descrip probname);
immler@31409
   509
    TextIO.output (out, RC.string_of_symbols
immler@31409
   510
                          (RC.string_of_funcs funcs)
immler@31409
   511
                          (RC.string_of_preds (cl_preds @ ty_preds)));
immler@31409
   512
    TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
immler@31409
   513
    RC.writeln_strs out axstrs;
immler@31409
   514
    List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
immler@31409
   515
    List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
immler@31409
   516
    RC.writeln_strs out helper_clauses_strs;
immler@31409
   517
    TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
immler@31409
   518
    RC.writeln_strs out tfree_clss;
immler@31409
   519
    RC.writeln_strs out dfg_clss;
immler@31409
   520
    TextIO.output (out, "end_of_list.\n\n");
immler@31409
   521
    (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
immler@31409
   522
    TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
immler@31409
   523
    TextIO.output (out, "end_problem.\n");
immler@31409
   524
    TextIO.closeOut out
immler@31409
   525
  end;
mengj@19720
   526
wenzelm@21254
   527
end