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