src/HOL/Tools/res_hol_clause.ML
changeset 24311 d6864b34eecd
parent 24215 5458fbf18276
child 24323 9aa7b5708eac
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Aug 17 23:10:41 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Aug 17 23:10:42 2007 +0200
     1.3 @@ -1,15 +1,44 @@
     1.4 -(* ID: $Id$ 
     1.5 +(* ID: $Id$
     1.6     Author: Jia Meng, NICTA
     1.7  
     1.8 -FOL clauses translated from HOL formulae.  
     1.9 +FOL clauses translated from HOL formulae.
    1.10  
    1.11  The combinator code needs to be deleted after the translation paper has been published.
    1.12  It cannot be used with proof reconstruction because combinators are not introduced by proof.
    1.13  The Turner combinators (B', C', S') yield no improvement and should be deleted.
    1.14  *)
    1.15  
    1.16 -structure ResHolClause =
    1.17 +signature RES_HOL_CLAUSE =
    1.18 +sig
    1.19 +  val ext: thm
    1.20 +  val comb_I: thm
    1.21 +  val comb_K: thm
    1.22 +  val comb_B: thm
    1.23 +  val comb_C: thm
    1.24 +  val comb_S: thm
    1.25 +  datatype type_level = T_FULL | T_PARTIAL | T_CONST
    1.26 +  val typ_level: type_level ref
    1.27 +  val minimize_applies: bool ref
    1.28 +  val init: theory -> unit
    1.29 +  type axiom_name = string
    1.30 +  type polarity = bool
    1.31 +  type clause_id = int
    1.32 +  datatype combterm =
    1.33 +      CombConst of string * ResClause.fol_type * ResClause.fol_type list (*Const and Free*)
    1.34 +    | CombVar of string * ResClause.fol_type
    1.35 +    | CombApp of combterm * combterm
    1.36 +  datatype literal = Literal of polarity * combterm
    1.37 +  val strip_comb: combterm -> combterm * combterm list
    1.38 +  val literals_of_term: term -> literal list * (ResClause.typ_var * sort) list
    1.39 +  val tptp_write_file: bool -> thm list -> string ->
    1.40 +    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    1.41 +      ResClause.arityClause list -> string list -> axiom_name list
    1.42 +  val dfg_write_file: bool -> thm list -> string ->
    1.43 +    (thm * (axiom_name * clause_id)) list * ResClause.classrelClause list *
    1.44 +      ResClause.arityClause list -> string list -> axiom_name list
    1.45 +end
    1.46  
    1.47 +structure ResHolClause: RES_HOL_CLAUSE =
    1.48  struct
    1.49  
    1.50  structure RC = ResClause;
    1.51 @@ -38,7 +67,7 @@
    1.52  fun const_types_only () = (typ_level:=T_CONST);
    1.53  
    1.54  (*If true, each function will be directly applied to as many arguments as possible, avoiding
    1.55 -  use of the "apply" operator. Use of hBOOL is also minimized. It only works for the 
    1.56 +  use of the "apply" operator. Use of hBOOL is also minimized. It only works for the
    1.57    constant-typed translation, though it could be tried for the partially-typed one.*)
    1.58  val minimize_applies = ref true;
    1.59  
    1.60 @@ -58,7 +87,7 @@
    1.61  fun init thy = (const_typargs := Sign.const_typargs thy);
    1.62  
    1.63  (**********************************************************************)
    1.64 -(* convert a Term.term with lambdas into a Term.term with combinators *) 
    1.65 +(* convert a Term.term with lambdas into a Term.term with combinators *)
    1.66  (**********************************************************************)
    1.67  
    1.68  fun is_free (Bound(a)) n = (a = n)
    1.69 @@ -68,58 +97,58 @@
    1.70  
    1.71  fun compact_comb t bnds = t;
    1.72  
    1.73 -fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp) 
    1.74 -  | lam2comb (Abs(x,tp,Bound n)) bnds = 
    1.75 +fun lam2comb (Abs(x,tp,Bound 0)) _ = Const("ATP_Linkup.COMBI",tp-->tp)
    1.76 +  | lam2comb (Abs(x,tp,Bound n)) bnds =
    1.77        let val tb = List.nth(bnds,n-1)
    1.78        in  Const("ATP_Linkup.COMBK", [tb,tp] ---> tb) $ Bound (n-1)  end
    1.79 -  | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2) 
    1.80 +  | lam2comb (Abs(x,t1,Const(c,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Const(c,t2)
    1.81    | lam2comb (Abs(x,t1,Free(v,t2))) _ = Const("ATP_Linkup.COMBK",[t2,t1] ---> t2) $ Free(v,t2)
    1.82    | lam2comb (Abs(x,t1,Var(ind,t2))) _ = Const("ATP_Linkup.COMBK", [t2,t1] ---> t2) $ Var(ind,t2)
    1.83    | lam2comb (t as (Abs(x,t1,P$(Bound 0)))) bnds =
    1.84 -      if is_free P 0 then 
    1.85 -	  let val tI = [t1] ---> t1
    1.86 -	      val P' = lam2comb (Abs(x,t1,P)) bnds
    1.87 -	      val tp' = Term.type_of1(bnds,P')
    1.88 -	      val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P)
    1.89 -	  in
    1.90 -	      compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ 
    1.91 -	                     Const("ATP_Linkup.COMBI",tI)) bnds
    1.92 -	  end
    1.93 +      if is_free P 0 then
    1.94 +          let val tI = [t1] ---> t1
    1.95 +              val P' = lam2comb (Abs(x,t1,P)) bnds
    1.96 +              val tp' = Term.type_of1(bnds,P')
    1.97 +              val tS = [tp',tI] ---> Term.type_of1(t1::bnds,P)
    1.98 +          in
    1.99 +              compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $
   1.100 +                             Const("ATP_Linkup.COMBI",tI)) bnds
   1.101 +          end
   1.102        else incr_boundvars ~1 P
   1.103    | lam2comb (t as (Abs(x,t1,P$Q))) bnds =
   1.104        let val nfreeP = not(is_free P 0)
   1.105 -	  and nfreeQ = not(is_free Q 0)
   1.106 -	  val tpq = Term.type_of1(t1::bnds, P$Q) 
   1.107 +          and nfreeQ = not(is_free Q 0)
   1.108 +          val tpq = Term.type_of1(t1::bnds, P$Q)
   1.109        in
   1.110 -	  if nfreeP andalso nfreeQ 
   1.111 -	  then 
   1.112 -	    let val tK = [tpq,t1] ---> tpq
   1.113 -	    in  Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q)  end
   1.114 -	  else if nfreeP then 
   1.115 -	    let val Q' = lam2comb (Abs(x,t1,Q)) bnds
   1.116 -		val P' = incr_boundvars ~1 P
   1.117 -		val tp = Term.type_of1(bnds,P')
   1.118 -		val tq' = Term.type_of1(bnds, Q')
   1.119 -		val tB = [tp,tq',t1] ---> tpq
   1.120 -	    in  compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds  end
   1.121 -	  else if nfreeQ then 
   1.122 -	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.123 -		val Q' = incr_boundvars ~1 Q
   1.124 -		val tq = Term.type_of1(bnds,Q')
   1.125 -		val tp' = Term.type_of1(bnds, P')
   1.126 -		val tC = [tp',tq,t1] ---> tpq
   1.127 -	    in  compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds  end
   1.128 +          if nfreeP andalso nfreeQ
   1.129 +          then
   1.130 +            let val tK = [tpq,t1] ---> tpq
   1.131 +            in  Const("ATP_Linkup.COMBK",tK) $ incr_boundvars ~1 (P $ Q)  end
   1.132 +          else if nfreeP then
   1.133 +            let val Q' = lam2comb (Abs(x,t1,Q)) bnds
   1.134 +                val P' = incr_boundvars ~1 P
   1.135 +                val tp = Term.type_of1(bnds,P')
   1.136 +                val tq' = Term.type_of1(bnds, Q')
   1.137 +                val tB = [tp,tq',t1] ---> tpq
   1.138 +            in  compact_comb (Const("ATP_Linkup.COMBB",tB) $ P' $ Q') bnds  end
   1.139 +          else if nfreeQ then
   1.140 +            let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.141 +                val Q' = incr_boundvars ~1 Q
   1.142 +                val tq = Term.type_of1(bnds,Q')
   1.143 +                val tp' = Term.type_of1(bnds, P')
   1.144 +                val tC = [tp',tq,t1] ---> tpq
   1.145 +            in  compact_comb (Const("ATP_Linkup.COMBC",tC) $ P' $ Q') bnds  end
   1.146            else
   1.147 -	    let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.148 -		val Q' = lam2comb (Abs(x,t1,Q)) bnds 
   1.149 -		val tp' = Term.type_of1(bnds,P')
   1.150 -		val tq' = Term.type_of1(bnds,Q')
   1.151 -		val tS = [tp',tq',t1] ---> tpq
   1.152 -	    in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
   1.153 +            let val P' = lam2comb (Abs(x,t1,P)) bnds
   1.154 +                val Q' = lam2comb (Abs(x,t1,Q)) bnds
   1.155 +                val tp' = Term.type_of1(bnds,P')
   1.156 +                val tq' = Term.type_of1(bnds,Q')
   1.157 +                val tS = [tp',tq',t1] ---> tpq
   1.158 +            in  compact_comb (Const("ATP_Linkup.COMBS",tS) $ P' $ Q') bnds  end
   1.159        end
   1.160    | lam2comb (t as (Abs(x,t1,_))) _ = raise RC.CLAUSE("HOL CLAUSE",t);
   1.161  
   1.162 -fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds 
   1.163 +fun to_comb (Abs(x,tp,b)) bnds = lam2comb (Abs(x, tp, to_comb b (tp::bnds))) bnds
   1.164    | to_comb (P $ Q) bnds = (to_comb P bnds) $ (to_comb Q bnds)
   1.165    | to_comb t _ = t;
   1.166  
   1.167 @@ -133,19 +162,19 @@
   1.168  type clause_id = int;
   1.169  
   1.170  datatype combterm = CombConst of string * RC.fol_type * RC.fol_type list (*Const and Free*)
   1.171 -		  | CombVar of string * RC.fol_type
   1.172 -		  | CombApp of combterm * combterm
   1.173 -		  
   1.174 +                  | CombVar of string * RC.fol_type
   1.175 +                  | CombApp of combterm * combterm
   1.176 +
   1.177  datatype literal = Literal of polarity * combterm;
   1.178  
   1.179 -datatype clause = 
   1.180 -	 Clause of {clause_id: clause_id,
   1.181 -		    axiom_name: axiom_name,
   1.182 -		    th: thm,
   1.183 -		    kind: RC.kind,
   1.184 -		    literals: literal list,
   1.185 -		    ctypes_sorts: (RC.typ_var * Term.sort) list, 
   1.186 -                    ctvar_type_literals: RC.type_literal list, 
   1.187 +datatype clause =
   1.188 +         Clause of {clause_id: clause_id,
   1.189 +                    axiom_name: axiom_name,
   1.190 +                    th: thm,
   1.191 +                    kind: RC.kind,
   1.192 +                    literals: literal list,
   1.193 +                    ctypes_sorts: (RC.typ_var * Term.sort) list,
   1.194 +                    ctvar_type_literals: RC.type_literal list,
   1.195                      ctfree_type_literals: RC.type_literal list};
   1.196  
   1.197  
   1.198 @@ -162,8 +191,8 @@
   1.199        (pol andalso c = "c_True") orelse
   1.200        (not pol andalso c = "c_False")
   1.201    | isTrue _ = false;
   1.202 -  
   1.203 -fun isTaut (Clause {literals,...}) = exists isTrue literals;  
   1.204 +
   1.205 +fun isTaut (Clause {literals,...}) = exists isTrue literals;
   1.206  
   1.207  fun type_of (Type (a, Ts)) =
   1.208        let val (folTypes,ts) = types_of Ts
   1.209 @@ -177,7 +206,7 @@
   1.210        in  (folTyps, RC.union_all ts)  end;
   1.211  
   1.212  (* same as above, but no gathering of sort information *)
   1.213 -fun simp_type_of (Type (a, Ts)) = 
   1.214 +fun simp_type_of (Type (a, Ts)) =
   1.215        RC.Comp(RC.make_fixed_type_const a, map simp_type_of Ts)
   1.216    | simp_type_of (TFree (a,s)) = RC.AtomF(RC.make_fixed_type_var a)
   1.217    | simp_type_of (TVar (v,s)) = RC.AtomV(RC.make_schematic_type_var v);
   1.218 @@ -190,32 +219,32 @@
   1.219  (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
   1.220  fun combterm_of (Const(c,t)) =
   1.221        let val (tp,ts,tvar_list) = const_type_of (c,t)
   1.222 -	  val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
   1.223 +          val c' = CombConst(RC.make_fixed_const c, tp, tvar_list)
   1.224        in  (c',ts)  end
   1.225    | combterm_of (Free(v,t)) =
   1.226        let val (tp,ts) = type_of t
   1.227 -	  val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
   1.228 -		   else CombConst(RC.make_fixed_var v, tp, [])
   1.229 +          val v' = if RC.isMeta v then CombVar(RC.make_schematic_var(v,0),tp)
   1.230 +                   else CombConst(RC.make_fixed_var v, tp, [])
   1.231        in  (v',ts)  end
   1.232    | combterm_of (Var(v,t)) =
   1.233        let val (tp,ts) = type_of t
   1.234 -	  val v' = CombVar(RC.make_schematic_var v,tp)
   1.235 +          val v' = CombVar(RC.make_schematic_var v,tp)
   1.236        in  (v',ts)  end
   1.237    | combterm_of (t as (P $ Q)) =
   1.238        let val (P',tsP) = combterm_of P
   1.239 -	  val (Q',tsQ) = combterm_of Q
   1.240 +          val (Q',tsQ) = combterm_of Q
   1.241        in  (CombApp(P',Q'), tsP union tsQ)  end;
   1.242  
   1.243  fun predicate_of ((Const("Not",_) $ P), polarity) = predicate_of (P, not polarity)
   1.244    | predicate_of (t,polarity) = (combterm_of t, polarity);
   1.245  
   1.246  fun literals_of_term1 args (Const("Trueprop",_) $ P) = literals_of_term1 args P
   1.247 -  | literals_of_term1 args (Const("op |",_) $ P $ Q) = 
   1.248 +  | literals_of_term1 args (Const("op |",_) $ P $ Q) =
   1.249        literals_of_term1 (literals_of_term1 args P) Q
   1.250    | literals_of_term1 (lits,ts) P =
   1.251        let val ((pred,ts'),pol) = predicate_of (P,true)
   1.252        in
   1.253 -	  (Literal(pol,pred)::lits, ts union ts')
   1.254 +          (Literal(pol,pred)::lits, ts union ts')
   1.255        end;
   1.256  
   1.257  fun literals_of_term P = literals_of_term1 ([],[]) P;
   1.258 @@ -223,15 +252,15 @@
   1.259  (* making axiom and conjecture clauses *)
   1.260  fun make_clause(clause_id,axiom_name,kind,th) =
   1.261      let val (lits,ctypes_sorts) = literals_of_term (to_comb (prop_of th) [])
   1.262 -	val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   1.263 +        val (ctvar_lits,ctfree_lits) = RC.add_typs_aux ctypes_sorts
   1.264      in
   1.265 -	if forall isFalse lits
   1.266 -	then error "Problem too trivial for resolution (empty clause)"
   1.267 -	else
   1.268 -	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
   1.269 -		    literals = lits, ctypes_sorts = ctypes_sorts, 
   1.270 -		    ctvar_type_literals = ctvar_lits,
   1.271 -		    ctfree_type_literals = ctfree_lits}
   1.272 +        if forall isFalse lits
   1.273 +        then error "Problem too trivial for resolution (empty clause)"
   1.274 +        else
   1.275 +            Clause {clause_id = clause_id, axiom_name = axiom_name, th = th, kind = kind,
   1.276 +                    literals = lits, ctypes_sorts = ctypes_sorts,
   1.277 +                    ctvar_type_literals = ctvar_lits,
   1.278 +                    ctfree_type_literals = ctfree_lits}
   1.279      end;
   1.280  
   1.281  
   1.282 @@ -276,26 +305,26 @@
   1.283  fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c
   1.284    | head_needs_hBOOL _ = true;
   1.285  
   1.286 -fun wrap_type (s, tp) = 
   1.287 +fun wrap_type (s, tp) =
   1.288    if !typ_level=T_FULL then
   1.289        type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
   1.290    else s;
   1.291 -    
   1.292 +
   1.293  fun apply ss = "hAPP" ^ RC.paren_pack ss;
   1.294  
   1.295  (*Full (non-optimized) and partial-typed transations*)
   1.296 -fun string_of_combterm1 (CombConst(c,tp,_)) = 
   1.297 +fun string_of_combterm1 (CombConst(c,tp,_)) =
   1.298        let val c' = if c = "equal" then "c_fequal" else c
   1.299        in  wrap_type (c',tp)  end
   1.300    | string_of_combterm1 (CombVar(v,tp)) = wrap_type (v,tp)
   1.301    | string_of_combterm1 (CombApp(t1,t2)) =
   1.302        let val s1 = string_of_combterm1 t1
   1.303 -	  and s2 = string_of_combterm1 t2
   1.304 +          and s2 = string_of_combterm1 t2
   1.305        in
   1.306 -	  case !typ_level of
   1.307 -	      T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1))
   1.308 -	    | T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   1.309 -	    | T_CONST => raise ERROR "string_of_combterm1"
   1.310 +          case !typ_level of
   1.311 +              T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1))
   1.312 +            | T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)]
   1.313 +            | T_CONST => raise ERROR "string_of_combterm1"
   1.314        end;
   1.315  
   1.316  fun rev_apply (v, []) = v
   1.317 @@ -310,28 +339,28 @@
   1.318            val nargs = min_arity_of c
   1.319            val args1 = List.take(args, nargs)
   1.320              handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^
   1.321 -					     Int.toString nargs ^ " but is applied to " ^ 
   1.322 -					     space_implode ", " args) 
   1.323 +                                             Int.toString nargs ^ " but is applied to " ^
   1.324 +                                             space_implode ", " args)
   1.325            val args2 = List.drop(args, nargs)
   1.326            val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
   1.327                        else []
   1.328        in
   1.329 -	  string_apply (c ^ RC.paren_pack (args1@targs), args2)
   1.330 +          string_apply (c ^ RC.paren_pack (args1@targs), args2)
   1.331        end
   1.332    | string_of_applic (CombVar(v,tp), args) = string_apply (v, args)
   1.333    | string_of_applic _ = raise ERROR "string_of_applic";
   1.334  
   1.335  fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s;
   1.336 -    
   1.337 +
   1.338  (*Full (if optimized) and constant-typed transations*)
   1.339 -fun string_of_combterm2 t = 
   1.340 +fun string_of_combterm2 t =
   1.341    let val (head, args) = strip_comb t
   1.342 -  in  wrap_type_if (head, 
   1.343 -                    string_of_applic (head, map string_of_combterm2 args), 
   1.344 +  in  wrap_type_if (head,
   1.345 +                    string_of_applic (head, map string_of_combterm2 args),
   1.346                      type_of_combterm t)
   1.347    end;
   1.348  
   1.349 -fun string_of_combterm t = 
   1.350 +fun string_of_combterm t =
   1.351      case (!typ_level,!minimize_applies) of
   1.352           (T_PARTIAL, _) => string_of_combterm1 t
   1.353         | (T_FULL, false) => string_of_combterm1 t
   1.354 @@ -340,20 +369,20 @@
   1.355  (*Boolean-valued terms are here converted to literals.*)
   1.356  fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t];
   1.357  
   1.358 -fun string_of_predicate t = 
   1.359 +fun string_of_predicate t =
   1.360    case t of
   1.361        (CombApp(CombApp(CombConst("equal",_,_), t1), t2)) =>
   1.362 -	  (*DFG only: new TPTP prefers infix equality*)
   1.363 -	  ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.364 -    | _ => 
   1.365 +          (*DFG only: new TPTP prefers infix equality*)
   1.366 +          ("equal" ^ RC.paren_pack [string_of_combterm t1, string_of_combterm t2])
   1.367 +    | _ =>
   1.368            case #1 (strip_comb t) of
   1.369                CombConst(c,_,_) => if needs_hBOOL c then boolify t else string_of_combterm t
   1.370              | _ => boolify t;
   1.371  
   1.372 -fun string_of_clausename (cls_id,ax_name) = 
   1.373 +fun string_of_clausename (cls_id,ax_name) =
   1.374      RC.clause_prefix ^ RC.ascii_of ax_name ^ "_" ^ Int.toString cls_id;
   1.375  
   1.376 -fun string_of_type_clsname (cls_id,ax_name,idx) = 
   1.377 +fun string_of_type_clsname (cls_id,ax_name,idx) =
   1.378      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
   1.379  
   1.380  
   1.381 @@ -363,26 +392,26 @@
   1.382    let val eqop = if pol then " = " else " != "
   1.383    in  string_of_combterm t1 ^ eqop ^ string_of_combterm t2  end;
   1.384  
   1.385 -fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) = 
   1.386 +fun tptp_literal (Literal(pol, CombApp(CombApp(CombConst("equal",_,_), t1), t2))) =
   1.387        tptp_of_equality pol (t1,t2)
   1.388 -  | tptp_literal (Literal(pol,pred)) = 
   1.389 +  | tptp_literal (Literal(pol,pred)) =
   1.390        RC.tptp_sign pol (string_of_predicate pred);
   1.391 - 
   1.392 +
   1.393  (*Given a clause, returns its literals paired with a list of literals concerning TFrees;
   1.394    the latter should only occur in conjecture clauses.*)
   1.395 -fun tptp_type_lits (Clause cls) = 
   1.396 +fun tptp_type_lits (Clause cls) =
   1.397      let val lits = map tptp_literal (#literals cls)
   1.398 -	val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
   1.399 -	val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
   1.400 +        val ctvar_lits_strs = map RC.tptp_of_typeLit (#ctvar_type_literals cls)
   1.401 +        val ctfree_lits = map RC.tptp_of_typeLit (#ctfree_type_literals cls)
   1.402      in
   1.403 -	(ctvar_lits_strs @ lits, ctfree_lits)
   1.404 -    end; 
   1.405 -    
   1.406 +        (ctvar_lits_strs @ lits, ctfree_lits)
   1.407 +    end;
   1.408 +
   1.409  fun clause2tptp (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.410      let val (lits,ctfree_lits) = tptp_type_lits cls
   1.411 -	val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   1.412 +        val cls_str = RC.gen_tptp_cls(clause_id,axiom_name,kind,lits)
   1.413      in
   1.414 -	(cls_str,ctfree_lits)
   1.415 +        (cls_str,ctfree_lits)
   1.416      end;
   1.417  
   1.418  
   1.419 @@ -390,14 +419,14 @@
   1.420  
   1.421  fun dfg_literal (Literal(pol,pred)) = RC.dfg_sign pol (string_of_predicate pred);
   1.422  
   1.423 -fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) = 
   1.424 +fun dfg_clause_aux (Clause{literals, ctypes_sorts, ...}) =
   1.425    let val lits = map dfg_literal literals
   1.426        val (tvar_lits,tfree_lits) = RC.add_typs_aux ctypes_sorts
   1.427        val tvar_lits_strs = map RC.dfg_of_typeLit tvar_lits
   1.428 -      val tfree_lits = map RC.dfg_of_typeLit tfree_lits 
   1.429 +      val tfree_lits = map RC.dfg_of_typeLit tfree_lits
   1.430    in
   1.431        (tvar_lits_strs @ lits, tfree_lits)
   1.432 -  end; 
   1.433 +  end;
   1.434  
   1.435  fun get_uvars (CombConst _) vars = vars
   1.436    | get_uvars (CombVar(v,_)) vars = (v::vars)
   1.437 @@ -406,14 +435,14 @@
   1.438  fun get_uvars_l (Literal(_,c)) = get_uvars c [];
   1.439  
   1.440  fun dfg_vars (Clause {literals,...}) = RC.union_all (map get_uvars_l literals);
   1.441 - 
   1.442 +
   1.443  fun clause2dfg (cls as Clause{axiom_name,clause_id,kind,ctypes_sorts,...}) =
   1.444 -    let val (lits,tfree_lits) = dfg_clause_aux cls 
   1.445 +    let val (lits,tfree_lits) = dfg_clause_aux cls
   1.446          val vars = dfg_vars cls
   1.447          val tvars = RC.get_tvar_strs ctypes_sorts
   1.448 -	val knd = RC.name_of_kind kind
   1.449 -	val lits_str = commas lits
   1.450 -	val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars) 
   1.451 +        val knd = RC.name_of_kind kind
   1.452 +        val lits_str = commas lits
   1.453 +        val cls_str = RC.gen_dfg_cls(clause_id, axiom_name, knd, lits_str, tvars@vars)
   1.454      in (cls_str, tfree_lits) end;
   1.455  
   1.456  (** For DFG format: accumulate function and predicate declarations **)
   1.457 @@ -423,17 +452,17 @@
   1.458  fun add_decls (CombConst(c,tp,tvars), (funcs,preds)) =
   1.459        if c = "equal" then (addtypes tvars funcs, preds)
   1.460        else
   1.461 -	(case !typ_level of
   1.462 +        (case !typ_level of
   1.463              T_PARTIAL => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds)
   1.464 -	  | _ => 
   1.465 -               let val arity = min_arity_of c 
   1.466 +          | _ =>
   1.467 +               let val arity = min_arity_of c
   1.468                     val ntys = if !typ_level = T_CONST then length tvars else 0
   1.469 -                   val addit = Symtab.update(c, arity+ntys) 
   1.470 +                   val addit = Symtab.update(c, arity+ntys)
   1.471                 in
   1.472                     if needs_hBOOL c then (addtypes tvars (addit funcs), preds)
   1.473                     else (addtypes tvars funcs, addit preds)
   1.474                 end)
   1.475 -  | add_decls (CombVar(_,ctp), (funcs,preds)) = 
   1.476 +  | add_decls (CombVar(_,ctp), (funcs,preds)) =
   1.477        (RC.add_foltype_funcs (ctp,funcs), preds)
   1.478    | add_decls (CombApp(P,Q),decls) = add_decls(P,add_decls (Q,decls));
   1.479  
   1.480 @@ -449,7 +478,7 @@
   1.481        val init_predtab = Symtab.update ("hBOOL",1) Symtab.empty
   1.482        val (functab,predtab) = (foldl add_clause_decls (init_functab, init_predtab) clauses)
   1.483    in
   1.484 -      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses), 
   1.485 +      (Symtab.dest (foldl RC.add_arityClause_funcs functab arity_clauses),
   1.486         Symtab.dest predtab)
   1.487    end;
   1.488  
   1.489 @@ -458,13 +487,13 @@
   1.490    handle Symtab.DUP a => raise ERROR ("predicate " ^ a ^ " has multiple arities")
   1.491  
   1.492  (*Higher-order clauses have only the predicates hBOOL and type classes.*)
   1.493 -fun preds_of_clauses clauses clsrel_clauses arity_clauses = 
   1.494 +fun preds_of_clauses clauses clsrel_clauses arity_clauses =
   1.495      Symtab.dest
   1.496 -	(foldl RC.add_classrelClause_preds 
   1.497 -	       (foldl RC.add_arityClause_preds
   1.498 -		      (foldl add_clause_preds Symtab.empty clauses) 
   1.499 -		      arity_clauses)
   1.500 -	       clsrel_clauses)
   1.501 +        (foldl RC.add_classrelClause_preds
   1.502 +               (foldl RC.add_arityClause_preds
   1.503 +                      (foldl add_clause_preds Symtab.empty clauses)
   1.504 +                      arity_clauses)
   1.505 +               clsrel_clauses)
   1.506  
   1.507  
   1.508  
   1.509 @@ -475,11 +504,11 @@
   1.510  
   1.511  val init_counters =
   1.512      Symtab.make [("c_COMBI", 0), ("c_COMBK", 0),
   1.513 -		 ("c_COMBB", 0), ("c_COMBC", 0),
   1.514 -		 ("c_COMBS", 0), ("c_COMBB_e", 0),
   1.515 -		 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
   1.516 -                
   1.517 -fun count_combterm (CombConst(c,tp,_), ct) = 
   1.518 +                 ("c_COMBB", 0), ("c_COMBC", 0),
   1.519 +                 ("c_COMBS", 0), ("c_COMBB_e", 0),
   1.520 +                 ("c_COMBC_e", 0), ("c_COMBS_e", 0)];
   1.521 +
   1.522 +fun count_combterm (CombConst(c,tp,_), ct) =
   1.523       (case Symtab.lookup ct c of NONE => ct  (*no counter*)
   1.524                                 | SOME n => Symtab.update (c,n+1) ct)
   1.525    | count_combterm (CombVar(v,tp), ct) = ct
   1.526 @@ -489,7 +518,7 @@
   1.527  
   1.528  fun count_clause (Clause{literals,...}, ct) = foldl count_literal ct literals;
   1.529  
   1.530 -fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) = 
   1.531 +fun count_user_clause user_lemmas (Clause{axiom_name,literals,...}, ct) =
   1.532    if axiom_name mem_string user_lemmas then foldl count_literal ct literals
   1.533    else ct;
   1.534  
   1.535 @@ -501,24 +530,24 @@
   1.536      let val ct0 = foldl count_clause init_counters conjectures
   1.537          val ct = foldl (count_user_clause user_lemmas) ct0 axclauses
   1.538          fun needed c = valOf (Symtab.lookup ct c) > 0
   1.539 -        val IK = if needed "c_COMBI" orelse needed "c_COMBK" 
   1.540 -                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K]) 
   1.541 +        val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   1.542 +                 then (Output.debug (fn () => "Include combinator I K"); cnf_helper_thms [comb_I,comb_K])
   1.543 +                 else []
   1.544 +        val BC = if needed "c_COMBB" orelse needed "c_COMBC"
   1.545 +                 then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C])
   1.546                   else []
   1.547 -	val BC = if needed "c_COMBB" orelse needed "c_COMBC" 
   1.548 -	         then (Output.debug (fn () => "Include combinator B C"); cnf_helper_thms [comb_B,comb_C]) 
   1.549 -	         else []
   1.550 -	val S = if needed "c_COMBS" 
   1.551 -	        then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S]) 
   1.552 -	        else []
   1.553 -	val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e" 
   1.554 -	           then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C']) 
   1.555 -	           else []
   1.556 -	val S' = if needed "c_COMBS_e" 
   1.557 -	         then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S']) 
   1.558 -	         else []
   1.559 -	val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.560 +        val S = if needed "c_COMBS"
   1.561 +                then (Output.debug (fn () => "Include combinator S"); cnf_helper_thms [comb_S])
   1.562 +                else []
   1.563 +        val B'C' = if needed "c_COMBB_e" orelse needed "c_COMBC_e"
   1.564 +                   then (Output.debug (fn () => "Include combinator B' C'"); cnf_helper_thms [comb_B', comb_C'])
   1.565 +                   else []
   1.566 +        val S' = if needed "c_COMBS_e"
   1.567 +                 then (Output.debug (fn () => "Include combinator S'"); cnf_helper_thms [comb_S'])
   1.568 +                 else []
   1.569 +        val other = cnf_helper_thms [ext,fequal_imp_equal,equal_imp_fequal]
   1.570      in
   1.571 -	map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   1.572 +        map #2 (make_axiom_clauses (other @ IK @ BC @ S @ B'C' @ S'))
   1.573      end;
   1.574  
   1.575  (*Find the minimal arity of each function mentioned in the term. Also, note which uses
   1.576 @@ -529,14 +558,14 @@
   1.577        val _ = List.app (count_constants_term false) args
   1.578    in
   1.579        case head of
   1.580 -	  CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   1.581 -	    let val a = if a="equal" andalso not toplev then "c_fequal" else a
   1.582 -	    in  
   1.583 -	      const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
   1.584 -	      if toplev then ()
   1.585 -	      else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
   1.586 -	    end
   1.587 -	| ts => ()
   1.588 +          CombConst (a,_,_) => (*predicate or function version of "equal"?*)
   1.589 +            let val a = if a="equal" andalso not toplev then "c_fequal" else a
   1.590 +            in
   1.591 +              const_min_arity := Symtab.map_default (a,n) (curry Int.min n) (!const_min_arity);
   1.592 +              if toplev then ()
   1.593 +              else const_needs_hBOOL := Symtab.update (a,true) (!const_needs_hBOOL)
   1.594 +            end
   1.595 +        | ts => ()
   1.596    end;
   1.597  
   1.598  (*A literal is a top-level term*)
   1.599 @@ -545,12 +574,12 @@
   1.600  fun count_constants_clause (Clause{literals,...}) = List.app count_constants_lit literals;
   1.601  
   1.602  fun display_arity (c,n) =
   1.603 -  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^ 
   1.604 +  Output.debug (fn () => "Constant: " ^ c ^ " arity:\t" ^ Int.toString n ^
   1.605                  (if needs_hBOOL c then " needs hBOOL" else ""));
   1.606  
   1.607 -fun count_constants (conjectures, axclauses, helper_clauses) = 
   1.608 +fun count_constants (conjectures, axclauses, helper_clauses) =
   1.609    if !minimize_applies andalso !typ_level<>T_PARTIAL then
   1.610 -    (const_min_arity := Symtab.empty; 
   1.611 +    (const_min_arity := Symtab.empty;
   1.612       const_needs_hBOOL := Symtab.empty;
   1.613       List.app count_constants_clause conjectures;
   1.614       List.app count_constants_clause axclauses;
   1.615 @@ -559,27 +588,27 @@
   1.616    else ();
   1.617  
   1.618  (* tptp format *)
   1.619 -						  
   1.620 +
   1.621  (* write TPTP format to a single file *)
   1.622  fun tptp_write_file isFO thms filename (ax_tuples,classrel_clauses,arity_clauses) user_lemmas =
   1.623      let val _ = Output.debug (fn () => ("Preparing to write the TPTP file " ^ filename))
   1.624          val _ = RC.dfg_format := false
   1.625          val conjectures = make_conjecture_clauses thms
   1.626          val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.627 -	val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.628 -	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.629 -	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.630 -	val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.631 +        val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.632 +        val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.633 +        val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp conjectures)
   1.634 +        val tfree_clss = map RC.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   1.635          val out = TextIO.openOut filename
   1.636      in
   1.637 -	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.638 -	RC.writeln_strs out tfree_clss;
   1.639 -	RC.writeln_strs out tptp_clss;
   1.640 -	List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   1.641 -	List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   1.642 -	List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   1.643 -	TextIO.closeOut out;
   1.644 -	clnames
   1.645 +        List.app (curry TextIO.output out o #1 o clause2tptp) axclauses;
   1.646 +        RC.writeln_strs out tfree_clss;
   1.647 +        RC.writeln_strs out tptp_clss;
   1.648 +        List.app (curry TextIO.output out o RC.tptp_classrelClause) classrel_clauses;
   1.649 +        List.app (curry TextIO.output out o RC.tptp_arity_clause) arity_clauses;
   1.650 +        List.app (curry TextIO.output out o #1 o clause2tptp) helper_clauses;
   1.651 +        TextIO.closeOut out;
   1.652 +        clnames
   1.653      end;
   1.654  
   1.655  
   1.656 @@ -591,36 +620,36 @@
   1.657          val _ = RC.dfg_format := true
   1.658          val conjectures = make_conjecture_clauses thms
   1.659          val (clnames,axclauses) = ListPair.unzip (make_axiom_clauses ax_tuples)
   1.660 -	val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.661 -	val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.662 -	val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.663 -	and probname = Path.implode (Path.base (Path.explode filename))
   1.664 -	val axstrs = map (#1 o clause2dfg) axclauses
   1.665 -	val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   1.666 -	val out = TextIO.openOut filename
   1.667 -	val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   1.668 -	val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.669 -	and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.670 +        val helper_clauses = get_helper_clauses isFO (conjectures, axclauses, user_lemmas)
   1.671 +        val _ = count_constants (conjectures, axclauses, helper_clauses);
   1.672 +        val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   1.673 +        and probname = Path.implode (Path.base (Path.explode filename))
   1.674 +        val axstrs = map (#1 o clause2dfg) axclauses
   1.675 +        val tfree_clss = map RC.dfg_tfree_clause (RC.union_all tfree_litss)
   1.676 +        val out = TextIO.openOut filename
   1.677 +        val helper_clauses_strs = map (#1 o clause2dfg) helper_clauses
   1.678 +        val (funcs,cl_preds) = decls_of_clauses (helper_clauses @ conjectures @ axclauses) arity_clauses
   1.679 +        and ty_preds = preds_of_clauses axclauses classrel_clauses arity_clauses
   1.680      in
   1.681 -	TextIO.output (out, RC.string_of_start probname); 
   1.682 -	TextIO.output (out, RC.string_of_descrip probname); 
   1.683 -	TextIO.output (out, RC.string_of_symbols 
   1.684 -	                      (RC.string_of_funcs funcs) 
   1.685 -	                      (RC.string_of_preds (cl_preds @ ty_preds))); 
   1.686 -	TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   1.687 -	RC.writeln_strs out axstrs;
   1.688 -	List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   1.689 -	List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   1.690 -	RC.writeln_strs out helper_clauses_strs;
   1.691 -	TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.692 -	RC.writeln_strs out tfree_clss;
   1.693 -	RC.writeln_strs out dfg_clss;
   1.694 -	TextIO.output (out, "end_of_list.\n\n");
   1.695 -	(*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   1.696 -	TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   1.697 -	TextIO.output (out, "end_problem.\n");
   1.698 -	TextIO.closeOut out;
   1.699 -	clnames
   1.700 +        TextIO.output (out, RC.string_of_start probname);
   1.701 +        TextIO.output (out, RC.string_of_descrip probname);
   1.702 +        TextIO.output (out, RC.string_of_symbols
   1.703 +                              (RC.string_of_funcs funcs)
   1.704 +                              (RC.string_of_preds (cl_preds @ ty_preds)));
   1.705 +        TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
   1.706 +        RC.writeln_strs out axstrs;
   1.707 +        List.app (curry TextIO.output out o RC.dfg_classrelClause) classrel_clauses;
   1.708 +        List.app (curry TextIO.output out o RC.dfg_arity_clause) arity_clauses;
   1.709 +        RC.writeln_strs out helper_clauses_strs;
   1.710 +        TextIO.output (out, "end_of_list.\n\nlist_of_clauses(conjectures,cnf).\n");
   1.711 +        RC.writeln_strs out tfree_clss;
   1.712 +        RC.writeln_strs out dfg_clss;
   1.713 +        TextIO.output (out, "end_of_list.\n\n");
   1.714 +        (*VarWeight=3 helps the HO problems, probably by counteracting the presence of hAPP*)
   1.715 +        TextIO.output (out, "list_of_settings(SPASS).\n{*\nset_flag(VarWeight,3).\n*}\nend_of_list.\n\n");
   1.716 +        TextIO.output (out, "end_problem.\n");
   1.717 +        TextIO.closeOut out;
   1.718 +        clnames
   1.719      end;
   1.720  
   1.721  end