reorganization of code to support DFG otuput
authorpaulson
Tue Jan 31 10:39:13 2006 +0100 (2006-01-31)
changeset 18863a113b6839df1
parent 18862 bd83590be0f7
child 18864 a87c0aeae92f
reorganization of code to support DFG otuput
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_atp_setup.ML
src/HOL/Tools/res_clause.ML
     1.1 --- a/src/HOL/Tools/res_atp.ML	Tue Jan 31 00:51:15 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Jan 31 10:39:13 2006 +0100
     1.3 @@ -13,7 +13,6 @@
     1.4    val helper_path: string -> string -> string
     1.5    val problem_name: string ref
     1.6    val time_limit: int ref
     1.7 -  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
     1.8  end;
     1.9  
    1.10  structure ResAtp: RES_ATP =
    1.11 @@ -49,39 +48,6 @@
    1.12  
    1.13  fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    1.14  
    1.15 -
    1.16 -(**** For running in Isar ****)
    1.17 -
    1.18 -fun writeln_strs _   []      = ()
    1.19 -  | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    1.20 -
    1.21 -(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
    1.22 -fun tptp_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) =
    1.23 -  let
    1.24 -    val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.25 -    val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    1.26 -    val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    1.27 -    val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    1.28 -    val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    1.29 -    val out = TextIO.openOut(pf n)
    1.30 -  in
    1.31 -    writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    1.32 -    writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    1.33 -    TextIO.closeOut out
    1.34 -  end;
    1.35 -
    1.36 -(* write out a subgoal in DFG format to the file "xxxx_N"*)
    1.37 -fun dfg_inputs_tfrees ths pf n (axclauses,classrel_clauses,arity_clauses) = 
    1.38 -    let val clss = ResClause.make_conjecture_clauses (map prop_of ths)
    1.39 -        (*FIXME: classrel_clauses and arity_clauses*)
    1.40 -        val probN = ResClause.clauses2dfg (!problem_name ^ "_" ^ Int.toString n)
    1.41 -                        axclauses clss 
    1.42 -	val out = TextIO.openOut(pf n)
    1.43 -    in
    1.44 -	writeln_strs out [probN]; TextIO.closeOut out
    1.45 -    end;
    1.46 -
    1.47 -
    1.48  (* call prover with settings and problem file for the current subgoal *)
    1.49  fun watcher_call_provers sign sg_terms (childin, childout, pid) =
    1.50    let
    1.51 @@ -145,14 +111,15 @@
    1.52        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.53        val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.54        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.55 -      val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    1.56 +      val write = if !prover = "spass" then ResClause.dfg_write_file 
    1.57 +                                       else ResClause.tptp_write_file
    1.58        fun writenext n =
    1.59  	if n=0 then []
    1.60  	 else
    1.61  	   (SELECT_GOAL
    1.62  	    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
    1.63  	      METAHYPS(fn negs => 
    1.64 -		(write (make_clauses negs) pf n 
    1.65 +		(write (make_clauses negs) (pf n) 
    1.66  		       (axclauses,classrel_clauses,arity_clauses);
    1.67  		 all_tac))]) n th;
    1.68  	    pf n :: writenext (n-1))
     2.1 --- a/src/HOL/Tools/res_atp_setup.ML	Tue Jan 31 00:51:15 2006 +0100
     2.2 +++ b/src/HOL/Tools/res_atp_setup.ML	Tue Jan 31 10:39:13 2006 +0100
     2.3 @@ -325,7 +325,7 @@
     2.4  	val (clss,errs) = tptp_ax_fn rules
     2.5  	val clss' = ResClause.union_all clss
     2.6      in
     2.7 -	ResAtp.writeln_strs out clss';
     2.8 +	ResClause.writeln_strs out clss';
     2.9  	TextIO.closeOut out;
    2.10  	([file],errs)
    2.11      end;
    2.12 @@ -353,11 +353,11 @@
    2.13  fun atp_conjectures_h_g filt_conj_fn hyp_cls =
    2.14      let val (tptp_h_clss,tfree_litss) = filt_conj_fn hyp_cls
    2.15  	val tfree_lits = ResClause.union_all tfree_litss
    2.16 -	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    2.17 +	val tfree_clss = map ResClause.tptp_tfree_clause tfree_lits 
    2.18  	val hypsfile = hyps_file ()
    2.19          val out = TextIO.openOut(hypsfile)
    2.20      in
    2.21 -        ResAtp.writeln_strs out (tfree_clss @ tptp_h_clss);
    2.22 +        ResClause.writeln_strs out (tfree_clss @ tptp_h_clss);
    2.23          TextIO.closeOut out; warning hypsfile;
    2.24          ([hypsfile],tfree_lits)
    2.25      end;
    2.26 @@ -368,11 +368,11 @@
    2.27  
    2.28  fun atp_conjectures_c_g filt_conj_fn conj_cls n tfrees =
    2.29      let val (tptp_c_clss,tfree_litss) = filt_conj_fn conj_cls
    2.30 -	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
    2.31 +	val tfree_clss = map ResClause.tptp_tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
    2.32  	val probfile = prob_file n
    2.33  	val out = TextIO.openOut(probfile)		 	
    2.34      in
    2.35 -	ResAtp.writeln_strs out (tfree_clss @ tptp_c_clss);
    2.36 +	ResClause.writeln_strs out (tfree_clss @ tptp_c_clss);
    2.37  	TextIO.closeOut out;
    2.38  	warning probfile; 
    2.39  	probfile 
    2.40 @@ -410,7 +410,7 @@
    2.41  	    let val tsfile = types_sorts_file ()
    2.42  		val out = TextIO.openOut(tsfile)
    2.43  	    in
    2.44 -		ResAtp.writeln_strs out (classrel_cls @ arity_cls);
    2.45 +		ResClause.writeln_strs out (classrel_cls @ arity_cls);
    2.46  		TextIO.closeOut out;
    2.47  		[tsfile]
    2.48  	    end
     3.1 --- a/src/HOL/Tools/res_clause.ML	Tue Jan 31 00:51:15 2006 +0100
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Tue Jan 31 10:39:13 2006 +0100
     3.3 @@ -25,9 +25,6 @@
     3.4    val isTaut : clause -> bool
     3.5    val num_of_clauses : clause -> int
     3.6  
     3.7 -  val clauses2dfg : string -> clause list -> clause list -> string
     3.8 -  val tfree_dfg_clause : string -> string
     3.9 -
    3.10    val arity_clause_thy: theory -> arityClause list 
    3.11    val classrel_clauses_thy: theory -> classrelClause list 
    3.12  
    3.13 @@ -35,7 +32,7 @@
    3.14    val tptp_classrelClause : classrelClause -> string
    3.15    val tptp_clause : clause -> string list
    3.16    val clause2tptp : clause -> string * string list
    3.17 -  val tfree_clause : string -> string
    3.18 +  val tptp_tfree_clause : string -> string
    3.19    val schematic_var_prefix : string
    3.20    val fixed_var_prefix : string
    3.21    val tvar_prefix : string
    3.22 @@ -76,9 +73,16 @@
    3.23    val types_ord : fol_type list * fol_type list -> order
    3.24    val string_of_fol_type : fol_type -> string
    3.25    val mk_fol_type: string * string * fol_type list -> fol_type
    3.26 -  val types_eq :fol_type list * fol_type list ->
    3.27 -   (string * string) list * (string * string) list -> bool * ((string * string) list * (string * string) list)
    3.28 +  val types_eq: fol_type list * fol_type list -> 
    3.29 +        (string*string) list * (string*string) list -> 
    3.30 +        bool * ((string*string) list * (string*string) list)
    3.31    val check_var_pairs: ''a * ''b -> (''a * ''b) list -> int
    3.32 +
    3.33 +  val dfg_write_file: thm list -> string -> 
    3.34 +        (clause list * classrelClause list * arityClause list) -> unit
    3.35 +  val tptp_write_file: thm list -> string -> 
    3.36 +        (clause list * classrelClause list * arityClause list) -> unit
    3.37 +  val writeln_strs: TextIO.outstream -> TextIO.vector list -> unit
    3.38    end;
    3.39  
    3.40  structure ResClause : RES_CLAUSE =
    3.41 @@ -794,17 +798,21 @@
    3.42  
    3.43  fun string_of_type_clsname (cls_id,ax_name,idx) = 
    3.44      string_of_clausename (cls_id,ax_name) ^ "_tcs" ^ (Int.toString idx);
    3.45 +
    3.46 +(*Write a list of strings to a file*)
    3.47 +fun writeln_strs os = List.app (fn s => TextIO.output (os,s));
    3.48 +
    3.49      
    3.50  
    3.51  (********************************)
    3.52  (* Code for producing DFG files *)
    3.53  (********************************)
    3.54  
    3.55 -fun dfg_literal (Literal(pol,pred,tag)) =
    3.56 -    let val pred_string = string_of_predicate pred
    3.57 -    in
    3.58 -	if pol then pred_string else "not(" ^pred_string ^ ")"  
    3.59 -    end;
    3.60 +(*Attach sign in DFG syntax: false means negate.*)
    3.61 +fun dfg_sign true s = s
    3.62 +  | dfg_sign false s = "not(" ^ s ^ ")"  
    3.63 +
    3.64 +fun dfg_literal (Literal(pol,pred,tag)) = dfg_sign pol (string_of_predicate pred)
    3.65  
    3.66  fun dfg_of_typeLit (LTVar (s,ty)) = "not(" ^ s ^ "(" ^ ty ^ "))"
    3.67    | dfg_of_typeLit (LTFree (s,ty)) = s ^ "(" ^ ty ^ ")";
    3.68 @@ -819,13 +827,13 @@
    3.69  fun gen_dfg_cls (cls_id,ax_name,knd,lits,tvars,vars) = 
    3.70      "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
    3.71      "or(" ^ lits ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
    3.72 -    string_of_clausename (cls_id,ax_name) ^  ").";
    3.73 +    string_of_clausename (cls_id,ax_name) ^  ").\n\n";
    3.74  
    3.75  (*FIXME: UNUSED*)
    3.76  fun gen_dfg_type_cls (cls_id,ax_name,knd,tfree_lit,idx,tvars,vars) = 
    3.77      "clause( %(" ^ knd ^ ")\n" ^ forall_open(vars,tvars) ^ 
    3.78      "or( " ^ tfree_lit ^ ")" ^ forall_close(vars,tvars) ^ ",\n" ^ 
    3.79 -    string_of_type_clsname (cls_id,ax_name,idx) ^  ").";
    3.80 +    string_of_type_clsname (cls_id,ax_name,idx) ^  ").\n\n";
    3.81  
    3.82  fun dfg_clause_aux (Clause cls) = 
    3.83    let val lits = map dfg_literal (#literals cls)
    3.84 @@ -887,35 +895,24 @@
    3.85  fun string_of_symbols predstr funcstr = 
    3.86    "list_of_symbols.\n" ^ predstr  ^ funcstr  ^ "end_of_list.\n\n";
    3.87  
    3.88 -fun string_of_axioms axstr = 
    3.89 -  "list_of_clauses(axioms,cnf).\n" ^ axstr ^ "end_of_list.\n\n";
    3.90 +fun write_axioms (out, strs) = 
    3.91 +  (TextIO.output (out, "list_of_clauses(axioms,cnf).\n");
    3.92 +   writeln_strs out strs;
    3.93 +   TextIO.output (out, "end_of_list.\n\n"));
    3.94  
    3.95 -fun string_of_conjectures conjstr = 
    3.96 -  "list_of_clauses(conjectures,cnf).\n" ^ conjstr ^ "end_of_list.\n\n";
    3.97 +fun write_conjectures (out, strs) = 
    3.98 +  (TextIO.output (out, "list_of_clauses(conjectures,cnf).\n");
    3.99 +   writeln_strs out strs;
   3.100 +   TextIO.output (out, "end_of_list.\n\n"));
   3.101  
   3.102  fun string_of_start name = "begin_problem(" ^ name ^ ").\n\n";
   3.103  
   3.104 -fun string_of_descrip name = "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   3.105 -
   3.106 -fun tfree_dfg_clause tfree_lit =
   3.107 -  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ")."
   3.108 +fun string_of_descrip name = 
   3.109 +  "list_of_descriptions.\nname({*" ^ name ^ "*}).\nauthor({*Isabelle*}).\nstatus(unknown).\ndescription({*auto-generated*}).\nend_of_list.\n\n"
   3.110  
   3.111 -fun gen_dfg_file probname axioms conjectures funcs preds = 
   3.112 -    let val axstrs_tfrees = (map clause2dfg axioms)
   3.113 -	val (axstrs, atfrees) = ListPair.unzip axstrs_tfrees
   3.114 -        val axstr = (space_implode "\n" axstrs) ^ "\n\n"
   3.115 -	val (conjstrs, atfrees) = ListPair.unzip (map clause2dfg conjectures)
   3.116 -        val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
   3.117 -        val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
   3.118 -        val funcstr = string_of_funcs funcs
   3.119 -        val predstr = string_of_preds preds
   3.120 -    in
   3.121 -       string_of_start probname ^ string_of_descrip probname ^
   3.122 -       string_of_symbols funcstr predstr ^  
   3.123 -       string_of_axioms axstr ^
   3.124 -       string_of_conjectures conjstr ^ "end_problem.\n"
   3.125 -    end;
   3.126 -   
   3.127 +fun dfg_tfree_clause tfree_lit =
   3.128 +  "clause( %(conjecture)\n" ^ "or( " ^ tfree_lit ^ "),\n" ^ "tfree_tcs" ^ ").\n\n"
   3.129 +
   3.130  
   3.131  (*** Find all occurrences of predicates in types, terms, literals... ***)
   3.132  
   3.133 @@ -969,42 +966,34 @@
   3.134  
   3.135  val funcs_of_clauses = Symtab.dest o (foldl add_clause_funcs Symtab.empty)
   3.136  
   3.137 -
   3.138 -fun clauses2dfg probname axioms conjectures = 
   3.139 -  let val clss = conjectures @ axioms
   3.140 -  in
   3.141 -     gen_dfg_file probname axioms conjectures 
   3.142 -       (funcs_of_clauses clss) (preds_of_clauses clss)
   3.143 -  end
   3.144 -
   3.145 -
   3.146  fun string_of_arClauseID (ArityClause {clause_id,axiom_name,...}) =
   3.147      arclause_prefix ^ ascii_of axiom_name ^ "_" ^ Int.toString clause_id;
   3.148  
   3.149  fun string_of_arKind (ArityClause arcls) = name_of_kind(#kind arcls);
   3.150  
   3.151 -(*FIXME!!! currently is TPTP format!*)
   3.152 -fun dfg_of_arLit (TConsLit(b,(c,t,args))) =
   3.153 -      let val pol = if b then "++" else "--"
   3.154 -	  val arg_strs = paren_pack args
   3.155 -      in 
   3.156 -	  pol ^ c ^ "(" ^ t ^ arg_strs ^ ")"
   3.157 -      end
   3.158 -  | dfg_of_arLit (TVarLit(b,(c,str))) =
   3.159 -      let val pol = if b then "++" else "--"
   3.160 -      in
   3.161 -	  pol ^ c ^ "(" ^ str ^ ")"
   3.162 -      end;
   3.163 +fun dfg_of_arLit (TConsLit(pol,(c,t,args))) =
   3.164 +      dfg_sign pol (c ^ "(" ^ t ^ paren_pack args ^ ")")
   3.165 +  | dfg_of_arLit (TVarLit(pol,(c,str))) =
   3.166 +      dfg_sign pol (c ^ "(" ^ str ^ ")")
   3.167      
   3.168 -
   3.169  fun dfg_of_conclLit (ArityClause arcls) = dfg_of_arLit (#conclLit arcls);
   3.170       
   3.171 -
   3.172  fun dfg_of_premLits (ArityClause arcls) = map dfg_of_arLit (#premLits arcls);
   3.173  		
   3.174 -
   3.175 +fun dfg_classrelLits sub sup = 
   3.176 +    let val tvar = "(T)"
   3.177 +    in 
   3.178 +	"not(" ^ sub ^ tvar ^ "), " ^ sup ^ tvar
   3.179 +    end;
   3.180  
   3.181 -(*FIXME: would this have variables in a forall? *)
   3.182 +fun dfg_classrelClause (ClassrelClause {clause_id,subclass,superclass,...}) =
   3.183 +  let val relcls_id = clrelclause_prefix ^ ascii_of subclass ^ "_" ^ 
   3.184 +		      Int.toString clause_id
   3.185 +      val lits = dfg_classrelLits (make_type_class subclass) (make_type_class superclass)
   3.186 +  in
   3.187 +      "clause(\nor( " ^ lits ^ ")),\n" ^
   3.188 +      relcls_id ^ ").\n\n"
   3.189 +  end; 
   3.190  
   3.191  fun dfg_arity_clause arcls = 
   3.192    let val arcls_id = string_of_arClauseID arcls
   3.193 @@ -1013,8 +1002,35 @@
   3.194        val knd = string_of_arKind arcls
   3.195        val all_lits = concl_lit :: prems_lits
   3.196    in
   3.197 -      "clause( %(" ^ knd ^ ")\n" ^  "or( " ^ (bracket_pack all_lits) ^ ")),\n" ^
   3.198 -       arcls_id ^  ")."
   3.199 +      "clause( %(" ^ knd ^ ")\n" ^  "or( " ^ bracket_pack all_lits ^ ")),\n" ^
   3.200 +       arcls_id ^ ").\n\n"
   3.201 +  end;
   3.202 +
   3.203 +(* write out a subgoal in DFG format to the file "xxxx_N"*)
   3.204 +fun dfg_write_file ths filename (axclauses,classrel_clauses,arity_clauses) = 
   3.205 +  let 
   3.206 +    val conjectures = make_conjecture_clauses (map prop_of ths)
   3.207 +    val (dfg_clss,tfree_litss) = ListPair.unzip (map clause2dfg conjectures)
   3.208 +    val classrel_cls = map dfg_classrelClause classrel_clauses
   3.209 +    val arity_cls = map dfg_arity_clause arity_clauses
   3.210 +    val clss = conjectures @ axclauses
   3.211 +    val funcs = (funcs_of_clauses clss)
   3.212 +    and preds = (preds_of_clauses clss)
   3.213 +    val out = TextIO.openOut filename
   3.214 +    and probname = Path.pack (Path.base (Path.unpack filename))
   3.215 +    val axstrs_tfrees = (map clause2dfg axclauses)
   3.216 +    val (axstrs, _) = ListPair.unzip axstrs_tfrees
   3.217 +    val tfree_clss = map dfg_tfree_clause (union_all tfree_litss) 
   3.218 +    val funcstr = string_of_funcs funcs
   3.219 +    val predstr = string_of_preds preds
   3.220 +  in
   3.221 +      TextIO.output (out, string_of_start probname); 
   3.222 +      TextIO.output (out, string_of_descrip probname); 
   3.223 +      TextIO.output (out, string_of_symbols funcstr predstr); 
   3.224 +      write_axioms (out, axstrs); 
   3.225 +      write_conjectures (out, tfree_clss@dfg_clss); 
   3.226 +      TextIO.output (out, "end_problem.\n");
   3.227 +      TextIO.closeOut out
   3.228    end;
   3.229  
   3.230  
   3.231 @@ -1037,11 +1053,11 @@
   3.232  
   3.233  fun gen_tptp_cls (cls_id,ax_name,knd,lits) = 
   3.234      "input_clause(" ^ string_of_clausename (cls_id,ax_name) ^ "," ^ 
   3.235 -    knd ^ "," ^ lits ^ ").";
   3.236 +    knd ^ "," ^ lits ^ ").\n";
   3.237  
   3.238  fun gen_tptp_type_cls (cls_id,ax_name,knd,tfree_lit,idx) = 
   3.239      "input_clause(" ^ string_of_type_clsname (cls_id,ax_name,idx) ^ "," ^ 
   3.240 -    knd ^ ",[" ^ tfree_lit ^ "]).";
   3.241 +    knd ^ ",[" ^ tfree_lit ^ "]).\n";
   3.242  
   3.243  fun tptp_type_lits (Clause cls) = 
   3.244      let val lits = map tptp_literal (#literals cls)
   3.245 @@ -1086,8 +1102,8 @@
   3.246      end;
   3.247  
   3.248  
   3.249 -fun tfree_clause tfree_lit =
   3.250 -    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).";
   3.251 +fun tptp_tfree_clause tfree_lit =
   3.252 +    "input_clause(" ^ "tfree_tcs," ^ "conjecture" ^ ",[" ^ tfree_lit ^ "]).\n";
   3.253  
   3.254  
   3.255  fun tptp_of_arLit (TConsLit(b,(c,t,args))) =
   3.256 @@ -1115,7 +1131,7 @@
   3.257  	val all_lits = concl_lit :: prems_lits
   3.258      in
   3.259  	"input_clause(" ^ arcls_id ^ "," ^ knd ^ "," ^ 
   3.260 -	(bracket_pack all_lits) ^ ")."
   3.261 +	(bracket_pack all_lits) ^ ").\n"
   3.262      end;
   3.263  
   3.264  fun tptp_classrelLits sub sup = 
   3.265 @@ -1129,7 +1145,26 @@
   3.266                          Int.toString clause_id
   3.267  	val lits = tptp_classrelLits (make_type_class subclass) (make_type_class superclass)
   3.268      in
   3.269 -	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ")."
   3.270 +	"input_clause(" ^ relcls_id ^ ",axiom," ^ lits ^ ").\n"
   3.271      end; 
   3.272  
   3.273 +(* write out a subgoal as tptp clauses to the file "xxxx_N"*)
   3.274 +fun tptp_write_file ths filename (axclauses,classrel_clauses,arity_clauses) =
   3.275 +  let
   3.276 +    val clss = make_conjecture_clauses (map prop_of ths)
   3.277 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
   3.278 +    val tfree_clss = map tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
   3.279 +    val classrel_cls = map tptp_classrelClause classrel_clauses
   3.280 +    val arity_cls = map tptp_arity_clause arity_clauses
   3.281 +    val out = TextIO.openOut filename
   3.282 +  in
   3.283 +    List.app (writeln_strs out o tptp_clause) axclauses;
   3.284 +    writeln_strs out tfree_clss;
   3.285 +    writeln_strs out tptp_clss;
   3.286 +    writeln_strs out classrel_cls;
   3.287 +    writeln_strs out arity_cls;
   3.288 +    TextIO.closeOut out
   3.289 +  end;
   3.290 +
   3.291 +
   3.292  end;