Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
authorquigley
Tue May 03 14:27:21 2005 +0200 (2005-05-03)
changeset 15919b30a35432f5a
parent 15918 6d6d3fabef02
child 15920 c79fa63504c8
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
Rewrote res_clasimpset.ML. Now produces an array of (thm, clause) in addition to writing out clasimpset as tptp strings. C.Q.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/ATP/watcher.sig
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Tue May 03 10:33:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Tue May 03 14:27:21 2005 +0200
     1.3 @@ -19,7 +19,6 @@
     1.4  				TextIO.output (fd, thisLine); logSpassInput (instr,fd))
     1.5   			 end;
     1.6  
     1.7 -
     1.8  (**********************************************************************)
     1.9  (*  Reconstruct the Spass proof w.r.t. thmstring (string version of   *)
    1.10  (*  Isabelle goal to be proved), then transfer the reconstruction     *)
    1.11 @@ -38,16 +37,16 @@
    1.12       end);
    1.13  
    1.14  
    1.15 -fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num = 
    1.16 +fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num clause_arr  (num_of_clauses:int ) = 
    1.17   let val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar3")));
    1.18   in
    1.19  SELECT_GOAL
    1.20    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.21 -  METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs))]) sg_num
    1.22 +  METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs clause_arr  num_of_clauses ))]) sg_num
    1.23   end ;
    1.24  
    1.25  
    1.26 -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
    1.27 +fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num,clause_arr,  num_of_clauses) = let 
    1.28                           val thisLine = TextIO.inputLine fromChild 
    1.29  			 in 
    1.30                              if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    1.31 @@ -58,51 +57,18 @@
    1.32  			            in 
    1.33  
    1.34                                          TextIO.output(foo,(proofextract));TextIO.closeOut foo;
    1.35 -                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num thm
    1.36 +                                        reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  clause_arr  num_of_clauses thm
    1.37                                                 
    1.38                                      end
    1.39                                    )
    1.40        			    else (
    1.41  				
    1.42 -                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
    1.43 +                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num, clause_arr,  num_of_clauses)
    1.44                                  )
    1.45   			 end;
    1.46  
    1.47  
    1.48 -(*
    1.49  
    1.50 -fun transferSpassInput (fromChild, toParent, ppid,thmstring,goalstring, currentString, thm, sg_num) = let 
    1.51 -                         val thisLine = TextIO.inputLine fromChild 
    1.52 -			 in 
    1.53 -                            if (thisLine = "--------------------------SPASS-STOP------------------------------\n" )
    1.54 -			    then ( 
    1.55 -                                    let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
    1.56 -                                        val reconstr = Recon_Transfer.spassString_to_reconString (currentString^thisLine) thmstring thm sg_num
    1.57 -                                        val foo =   TextIO.openOut( File.sysify_path(File.tmp_path (Path.basic"foobar2")));
    1.58 -                               in
    1.59 -                                         TextIO.output(foo,(reconstr^thmstring));TextIO.closeOut foo;
    1.60 -                                   
    1.61 -                                         TextIO.output (toParent, reconstr^"\n");
    1.62 -                                         TextIO.flushOut toParent;
    1.63 -                                         TextIO.output (toParent, thmstring^"\n");
    1.64 -                                         TextIO.flushOut toParent;
    1.65 -                                         TextIO.output (toParent, goalstring^"\n");
    1.66 -                                         TextIO.flushOut toParent;
    1.67 -                                          
    1.68 -                                         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.69 -                                         (* Attempt to prevent several signals from turning up simultaneously *)
    1.70 -                                         Posix.Process.sleep(Time.fromSeconds 1); ()
    1.71 -                                               
    1.72 -                                    end
    1.73 -                                      
    1.74 -                                  )
    1.75 -      			    else (
    1.76 -				
    1.77 -                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,(currentString^thisLine), thm, sg_num)
    1.78 -                                )
    1.79 - 			 end;
    1.80 -
    1.81 -*)
    1.82  
    1.83  (*********************************************************************************)
    1.84  (*  Inspect the output of a Spass   process to see if it has found a proof,      *)
    1.85 @@ -110,7 +76,7 @@
    1.86  (*********************************************************************************)
    1.87  
    1.88   
    1.89 -fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num) = 
    1.90 +fun startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,thm, sg_num,clause_arr, num_of_clauses) = 
    1.91                                        (*let val _ = Posix.Process.wait ()
    1.92                                        in*)
    1.93                                         
    1.94 @@ -127,20 +93,22 @@
    1.95                                                 val _=  TextIO.output (outfile, "about to transfer proof, thm is: "^(string_of_thm thm));
    1.96                                                 val _ =  TextIO.closeOut outfile;
    1.97                                                 in
    1.98 -                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num);
    1.99 +                                                transferSpassInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, thm, sg_num,clause_arr,  num_of_clauses);
   1.100                                                  true
   1.101                                                 end)
   1.102                                               
   1.103                                               else 
   1.104                                                  (
   1.105 -                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num)
   1.106 +                                                 startSpassTransfer (fromChild, toParent, ppid, thmstring, goalstring,childCmd, thm, sg_num,clause_arr, num_of_clauses)
   1.107                                                  )
   1.108                                              end
   1.109                                             )
   1.110                                           else (false)
   1.111                                       (*  end*)
   1.112  
   1.113 -fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num) = 
   1.114 +
   1.115 +
   1.116 +fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
   1.117                                         let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
   1.118                                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
   1.119                                              val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
   1.120 @@ -159,7 +127,7 @@
   1.121                                               
   1.122                                                       val _ =  TextIO.closeOut outfile
   1.123                                                   in 
   1.124 -                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num) 
   1.125 +                                                    startSpassTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses) 
   1.126                                                   end
   1.127                                                 )   
   1.128                                                 else if (thisLine= "SPASS beiseite: Completion found.\n" )
   1.129 @@ -215,7 +183,7 @@
   1.130                                                      else
   1.131                                                         (TextIO.output (spass_proof_file, (thisLine));
   1.132                                                         TextIO.flushOut spass_proof_file;
   1.133 -                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num))
   1.134 +                                                       checkSpassProofFound  (fromChild, toParent, ppid, thmstring,goalstring,childCmd, thm, sg_num, clause_arr,  num_of_clauses))
   1.135  
   1.136                                                end
   1.137                                            )
   1.138 @@ -229,36 +197,6 @@
   1.139  (***********************************************************************)
   1.140  
   1.141  
   1.142 -(***********************************************************************)
   1.143 -(*  Function used by the Isabelle process to read in a vampire proof   *)
   1.144 -(***********************************************************************)
   1.145 -
   1.146 -(*fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
   1.147 -			 in 
   1.148 -                           if (thisLine = "%==============  End of proof. ==================\n" )
   1.149 -			    then
   1.150 -                               (
   1.151 -                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
   1.152 -                               )
   1.153 -                             else if (thisLine = "% Unprovable.\n" ) 
   1.154 -                                  then 
   1.155 -                                     (
   1.156 -                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
   1.157 -                                      )
   1.158 -                                   else if (thisLine = "% Proof not found.\n")
   1.159 -                                        then 
   1.160 -                                            (
   1.161 -                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
   1.162 -                                             )
   1.163 -
   1.164 -
   1.165 -                                         else 
   1.166 -                                            (
   1.167 -				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
   1.168 -                                             )
   1.169 - 			 end;
   1.170 -
   1.171 -*)
   1.172  
   1.173  fun getSpassInput instr = if (isSome (TextIO.canInput(instr, 2)))
   1.174                            then
     2.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 03 10:33:31 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 03 14:27:21 2005 +0200
     2.3 @@ -242,7 +242,7 @@
     2.4                      (* resulting thm, clause-strs in spass order, vars *)
     2.5  
     2.6  fun rearrange_clause thm res_strlist allvars = 
     2.7 -                          let val isa_strlist = get_meta_lits thm
     2.8 +                          let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *)
     2.9                                val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
    2.10                                val symmed = apply_rule sym symlist thm
    2.11                                val not_symmed = apply_rule not_sym not_symlist symmed
     3.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Tue May 03 10:33:31 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Tue May 03 14:27:21 2005 +0200
     3.3 @@ -405,10 +405,20 @@
     3.4  
     3.5   val clause =  term
     3.6  
     3.7 - val line = number ++ justification ++ a (Other "|") ++ 
     3.8 +
     3.9 +
    3.10 + (*val line = number ++ justification ++ a (Other "|") ++ 
    3.11              a (Other "|") ++ clause ++ a (Other ".")
    3.12 -          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))
    3.13 -    
    3.14 +          >> (fn (a, (z, (_,( _, (c, _))))) => (a, z, c))*)
    3.15 +
    3.16 +
    3.17 +(* not entirely sure nterm is right here, but I don't think you get negative things before the ||s *)
    3.18 + val line = number ++ justification ++ many( nterm) ++ a (Other "|") ++ 
    3.19 +            a (Other "|") ++ clause ++ a (Other ".")
    3.20 +          >> (fn (a, (z, (w, (_,( _, (c, _)))))) => (a, z,(w@ c)))
    3.21 +       
    3.22 +
    3.23 +
    3.24   val lines = many line
    3.25   val alllines = (lines ++ finished) >> fst
    3.26      
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 03 10:33:31 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 03 14:27:21 2005 +0200
     4.3 @@ -17,6 +17,39 @@
     4.4  
     4.5  
     4.6  
     4.7 +(*
     4.8 +fun fill_cls_array array n [] = ()
     4.9 +|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
    4.10 +                                     in
    4.11 +                                        fill_cls_array array (n+1) (xs)
    4.12 +                                     end;
    4.13 +
    4.14 +
    4.15 +
    4.16 +fun memo_add_clauses ((name:string, (cls:Thm.thm list)), symtable)=
    4.17 +                        symtable := Symtab.update((name , cls), !symtable);
    4.18 +      	       
    4.19 +
    4.20 +fun memo_add_all ([], symtable) = ()
    4.21 +|   memo_add_all ((x::xs),symtable) = let val _ = memo_add_clauses (x, symtable)
    4.22 +                           in
    4.23 +                               memo_add_all (xs, symtable)
    4.24 +                           end
    4.25 +
    4.26 +fun memo_find_clause (name, (symtable: Thm.thm list Symtab.table ref)) = case Symtab.lookup (!symtable,name) of
    4.27 +      	        NONE =>  []
    4.28 +                |SOME cls  => cls ;
    4.29 +      	        	
    4.30 +
    4.31 +fun retrieve_clause array symtable clausenum = let
    4.32 +                                                  val (name, clnum) = Array.sub(array, clausenum)
    4.33 +                                                  val clauses = memo_find_clause (name, symtable)
    4.34 +                                                  val clause = get_nth clnum clauses
    4.35 +                                               in
    4.36 +                                                  (name, clause)
    4.37 +                                               end
    4.38 + *)                                             
    4.39 +
    4.40  (* Versions that include type information *)
    4.41   
    4.42  fun string_of_thm thm = let val _ = set show_sorts
    4.43 @@ -146,8 +179,30 @@
    4.44  fun thmstrings [] str = str
    4.45  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    4.46  
    4.47 +fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
    4.48  
    4.49 - fun get_axioms_used proof_steps thms = let 
    4.50 +
    4.51 +
    4.52 +fun retrieve_axioms clause_arr  [] = []
    4.53 +|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
    4.54 + 						     (retrieve_axioms clause_arr  xs)
    4.55 +
    4.56 +
    4.57 +(* retrieve the axioms that were obtained from the clasimpset *)
    4.58 +
    4.59 +fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    4.60 +                                let val clasimp_nums = List.filter (is_clasimp_ax clasimp_num) step_nums
    4.61 +                                in
    4.62 +                                    retrieve_axioms clause_arr  clasimp_nums
    4.63 +                                end
    4.64 +
    4.65 +
    4.66 +
    4.67 +
    4.68 +(* add array and table here, so can retrieve clasimp axioms *)
    4.69 +
    4.70 + fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    4.71 +                                         let 
    4.72                                               (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    4.73                                               val _ = TextIO.output (outfile, thmstring)
    4.74                                               
    4.75 @@ -157,9 +212,21 @@
    4.76                                              val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    4.77                                              val axioms = get_init_axioms proof_steps
    4.78                                              val step_nums = get_step_nums axioms []
    4.79 -                                      
    4.80 -                                           
    4.81 -                                            val clauses = make_clauses thms
    4.82 +
    4.83 +                                           (***********************************************)
    4.84 +                                           (* here need to add the clauses from clause_arr*)
    4.85 +                                           (***********************************************)
    4.86 +
    4.87 +                                           (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    4.88 +                                            val clasimp_names = map #1 clasimp_names_cls
    4.89 +                                            val clasimp_cls = map #2 clasimp_names_cls
    4.90 +                                            val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    4.91 +                                             val _ = TextIO.output (outfile,clasimp_namestr)
    4.92 +                                             
    4.93 +                                             val _ =  TextIO.closeOut outfile
    4.94 +*)
    4.95 +
    4.96 +                                            val clauses =(*(clasimp_cls)@*)( make_clauses thms)
    4.97                                              
    4.98                                              val vars = map thm_vars clauses
    4.99                                             
   4.100 @@ -215,7 +282,7 @@
   4.101                                             val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   4.102                                             
   4.103                                           in
   4.104 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
   4.105 +                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   4.106                                           end
   4.107                                          
   4.108  fun numclstr (vars, []) str = str
   4.109 @@ -293,9 +360,12 @@
   4.110  
   4.111  *)
   4.112  
   4.113 +
   4.114 +
   4.115 +
   4.116  val dummy_tac = PRIMITIVE(fn thm => thm );
   4.117  
   4.118 -fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms= 
   4.119 +fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   4.120                                                let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   4.121                                                    (* val sign = sign_of_thm thm
   4.122                                                   val prems = prems_of thm
   4.123 @@ -307,7 +377,8 @@
   4.124  
   4.125                                                    val tokens = #1(lex proofstr)
   4.126  
   4.127 -                                                     
   4.128 +                                                    
   4.129 +
   4.130                                                (***********************************)
   4.131                                                (* parse spass proof into datatype *)
   4.132                                                (***********************************)
   4.133 @@ -327,7 +398,9 @@
   4.134                                                    (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   4.135                                                    (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   4.136                                                    (* subgoal this is, and turn it into meta_clauses *)
   4.137 -                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms
   4.138 +                                                  (* should prob add array and table here, so that we can get axioms*)
   4.139 +                                                  (* produced from the clasimpset rather than the problem *)
   4.140 +                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   4.141                                                    
   4.142                                                    (*val numcls_string = numclstr ( vars, numcls) ""*)
   4.143                                                    val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
     5.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 03 10:33:31 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 03 14:27:21 2005 +0200
     5.3 @@ -67,9 +67,10 @@
     5.4  
     5.5  fun reconstruction_failed fname = error (fname ^ ": reconstruction failed")
     5.6  
     5.7 -(****************************************)
     5.8 -(* Reconstruct an axiom resolution step *)
     5.9 -(****************************************)
    5.10 +(************************************************)
    5.11 +(* Reconstruct an axiom resolution step         *)
    5.12 +(* clauses is a list of (clausenum,clause) pairs*)
    5.13 +(************************************************)
    5.14  
    5.15  fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    5.16                                       let val this_axiom = valOf (assoc (clauses,clausenum))
     6.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 03 10:33:31 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 03 14:27:21 2005 +0200
     6.3 @@ -3,247 +3,76 @@
     6.4      Copyright   2004  University of Cambridge
     6.5  *)
     6.6  
     6.7 -(* Get claset rules *)
     6.8 +signature RES_CLASIMP =
     6.9 +  sig
    6.10 +     val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
    6.11 +  end;
    6.12 +
    6.13 +structure ResClasimp : RES_CLASIMP =
    6.14 +struct
    6.15  
    6.16  fun has_name th = not((Thm.name_of_thm th)= "")
    6.17  
    6.18  fun has_name_pair (a,b) = not_equal a "";
    6.19 -fun good_pair c (a,b) = not_equal b c;
    6.20 -
    6.21 -
    6.22 -
    6.23 -val num_of_clauses = ref 0;
    6.24 -val clause_arr = Array.array(3500, ("empty", 0));
    6.25 -
    6.26 -
    6.27 -(*
    6.28 -val foo_arr = Array.array(20, ("a",0));
    6.29 -
    6.30 -fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
    6.31 -
    6.32 -
    6.33 -
    6.34 -
    6.35 -fun setupFork () = let
    6.36 -          (** pipes for communication between parent and watcher **)
    6.37 -          val p1 = Posix.IO.pipe ()
    6.38 -          val p2 = Posix.IO.pipe ()
    6.39 -	  fun closep () = (
    6.40 -                Posix.IO.close (#outfd p1); 
    6.41 -                Posix.IO.close (#infd p1);
    6.42 -                Posix.IO.close (#outfd p2); 
    6.43 -                Posix.IO.close (#infd p2)
    6.44 -              )
    6.45 -          (***********************************************************)
    6.46 -          (****** fork a watcher process and get it set up and going *)
    6.47 -          (***********************************************************)
    6.48 -          fun startFork () =
    6.49 -                   (case  Posix.Process.fork() (***************************************)
    6.50 -		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
    6.51 -                                               (***************************************)
    6.52 - 
    6.53 -                                                 (*************************)
    6.54 -                  | NONE => let                  (* child - i.e. watcher  *)
    6.55 -		      val oldchildin = #infd p1  (*************************)
    6.56 -		      val fromParent = Posix.FileSys.wordToFD 0w0
    6.57 -		      val oldchildout = #outfd p2
    6.58 -		      val toParent = Posix.FileSys.wordToFD 0w1
    6.59 -                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    6.60 -                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    6.61 -                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
    6.62 -                      val fooax = fst(Array.sub(foo_arr, 3))
    6.63 -                      val  outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");  
    6.64 -                      val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
    6.65 -                      val _ =  TextIO.closeOut outfile
    6.66 -                     in
    6.67 -                       (***************************)
    6.68 -                       (*** Sort out pipes ********)
    6.69 -                       (***************************)
    6.70 -
    6.71 -			Posix.IO.close (#outfd p1);
    6.72 -			Posix.IO.close (#infd p2);
    6.73 -			Posix.IO.dup2{old = oldchildin, new = fromParent};
    6.74 -                        Posix.IO.close oldchildin;
    6.75 -			Posix.IO.dup2{old = oldchildout, new = toParent};
    6.76 -                        Posix.IO.close oldchildout;
    6.77 -
    6.78 -                        (***************************)
    6.79 -                        (* start the watcher loop  *)
    6.80 -                        (***************************)
    6.81 -                        
    6.82 -                        (****************************************************************************)
    6.83 -                        (* fake return value - actually want the watcher to loop until killed       *)
    6.84 -                        (****************************************************************************)
    6.85 -                        Posix.Process.wordToPid 0w0
    6.86 -			
    6.87 -		      end)
    6.88 -            val start = startFork()
    6.89 -       in
    6.90 -
    6.91 -
    6.92 - (*******************************)
    6.93 -           (* close the child-side fds    *)
    6.94 -           (*******************************)
    6.95 -            Posix.IO.close (#outfd p2);
    6.96 -            Posix.IO.close (#infd p1);
    6.97 -            (* set the fds close on exec *)
    6.98 -            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
    6.99 -            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.100 -             
   6.101 -           (*******************************)
   6.102 -           (* return value                *)
   6.103 -           (*******************************)
   6.104 -          ()
   6.105 -         end;
   6.106 -
   6.107 -
   6.108 -
   6.109 -*)
   6.110 -
   6.111 -
   6.112 -
   6.113 -
   6.114 -fun multi x 0 xlist = xlist
   6.115 -   |multi x n xlist = multi x (n -1 ) (x::xlist);
   6.116 -
   6.117 -
   6.118 -fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
   6.119 -                                              val numbers = 0 upto (num_of_cls -1)
   6.120 -                                              val multi_name = multi name num_of_cls []
   6.121 -                                          in 
   6.122 -                                              ListPair.zip (multi_name,numbers)
   6.123 -                                          end;
   6.124  
   6.125  fun stick []  = []
   6.126  |   stick (x::xs)  = x@(stick xs )
   6.127  
   6.128 -
   6.129 -
   6.130 -fun fill_cls_array array n [] = ()
   6.131 -|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
   6.132 -                                     in
   6.133 -                                        fill_cls_array array (n+1) (xs)
   6.134 -                                     end;
   6.135 -
   6.136 -
   6.137 -   	      	    
   6.138 -val nc = ref (Symtab.empty : (thm list) Symtab.table)
   6.139 -
   6.140 - 
   6.141 -
   6.142 -fun memo_add_clauses (name:string, cls)=
   6.143 -                        nc := Symtab.update((name , cls), !nc);
   6.144 -      	       
   6.145 -
   6.146 -
   6.147 -fun memo_find_clause name = case Symtab.lookup (!nc,name) of
   6.148 -      	        NONE =>  []
   6.149 -                |SOME cls  => cls ;
   6.150 -
   6.151 -
   6.152 -fun get_simp_metas [] = [[]]
   6.153 -|   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
   6.154 -                             in
   6.155 -                                 metas::(get_simp_metas xs)
   6.156 -                             end
   6.157 -                             handle THM _ => get_simp_metas xs
   6.158 +(* changed, now it also finds out the name of the theorem. *)
   6.159 +(* convert a theorem into CNF and then into Clause.clause format. *)
   6.160 +fun clausify_axiom_pairs thm =
   6.161 +    let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
   6.162 +        val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
   6.163 +        val thm_name = Thm.name_of_thm thm
   6.164 +	val clauses_n = length isa_clauses
   6.165 +	fun make_axiom_clauses _ [] []= []
   6.166 +	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
   6.167 +    in
   6.168 +	make_axiom_clauses 0 isa_clauses' isa_clauses		
   6.169 +    end;
   6.170  
   6.171  
   6.172 -(* re-jig all these later as smaller functions for each bit *)
   6.173 -  val num_of_clauses = ref 0;
   6.174 -val clause_arr = Array.array(3500, ("empty", 0));
   6.175 -                               
   6.176 -
   6.177 -fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
   6.178 -                                   val _= warning "in writeoutclasimp"
   6.179 -                                   (****************************************)
   6.180 -                                   (* add claset rules to array and write out as strings *)
   6.181 -                                   (****************************************)
   6.182 -                                   val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
   6.183 -                                   val name_fol_cs = List.filter has_name clausifiable_rules;
   6.184 -                                   (* length name_fol_cs is 93 *)
   6.185 -                                   val good_names = map Thm.name_of_thm name_fol_cs;
   6.186 - 
   6.187 -                                   (*******************************************)
   6.188 -                                    (* get (name, thm) pairs for claset rules *)
   6.189 -                                   (*******************************************)
   6.190 +fun clausify_rules_pairs [] err_list = ([],err_list)
   6.191 +  | clausify_rules_pairs (thm::thms) err_list =
   6.192 +    let val (ts,es) = clausify_rules_pairs thms err_list
   6.193 +    in
   6.194 +	((clausify_axiom_pairs thm)::ts,es) handle  _ => (ts,(thm::es))
   6.195 +    end;
   6.196  
   6.197 -                                   val names_rules = ListPair.zip (good_names,name_fol_cs);
   6.198 -                                   
   6.199 -                                   val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
   6.200 -
   6.201 -                                   val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
   6.202 +fun write_out_clasimp filename = let
   6.203 +					val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
   6.204 +					val named_claset = List.filter has_name claset_rules;
   6.205 +					val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
   6.206  
   6.207 -                                   (* list of lists of tptp string clauses *)
   6.208 -                                   val stick_clasrls =  map stick claset_tptp_strs;
   6.209 -                                   (* stick stick_clasrls length is 172*)
   6.210 -
   6.211 -                                   val name_stick = ListPair.zip (good_names,stick_clasrls);
   6.212 +					val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
   6.213 +					val named_simpset = map #2(List.filter has_name_pair simpset_rules);
   6.214 +					val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
   6.215  
   6.216 -                                   val cl_name_nums =map clause_numbering name_stick;
   6.217 -                                       
   6.218 -                                   val cl_long_name_nums = stick cl_name_nums;
   6.219 -                                   (*******************************************)
   6.220 -                                  (* create array and put clausename, number pairs into it *)
   6.221 -                                   (*******************************************)
   6.222 +					val cls_thms = (claset_cls_thms@simpset_cls_thms);
   6.223 +					val cls_thms_list = stick cls_thms;
   6.224  
   6.225 -                                   val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   6.226 -                                   val _= num_of_clauses := (List.length cl_long_name_nums);
   6.227 -                                   
   6.228 -                                   (*************************************)
   6.229 -                                   (* write claset out as tptp file      *)
   6.230 -                                    (*************************************)
   6.231 -                                  
   6.232 -                                    val claset_all_strs = stick stick_clasrls;
   6.233 -                                    val out = TextIO.openOut filename;
   6.234 -                                    val _=   ResLib.writeln_strs out claset_all_strs;
   6.235 -                                    val _= TextIO.flushOut out;
   6.236 -                                    val _=  TextIO.output (out,("\n \n"));
   6.237 -                                    val _= TextIO.flushOut out;
   6.238 -                                   (*val _= TextIO.closeOut out;*)
   6.239 -
   6.240 -                                  (*********************)
   6.241 -                                  (* Get simpset rules *)
   6.242 -                                  (*********************)
   6.243 +                                        (*********************************************************)
   6.244 +                                  	(* create array and put clausename, number pairs into it *)
   6.245 +                                   	(*********************************************************)
   6.246 +					val num_of_clauses =  0;
   6.247 +                                     	val clause_arr = Array.fromList cls_thms_list;
   6.248 +              
   6.249 +                                   	val  num_of_clauses= (List.length cls_thms_list);
   6.250  
   6.251 -                                  val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
   6.252 -
   6.253 -                                  val named_simps = List.filter has_name_pair simpset_name_rules;
   6.254 -
   6.255 -                                  val simp_names = map #1 named_simps;
   6.256 -                                  val simp_rules = map #2 named_simps;
   6.257 -                              
   6.258 -                                 (* 1137 clausif simps *)
   6.259 -                                   
   6.260 -                                    (* need to get names of claset_cluases so we can make sure we've*)
   6.261 -                                    (* got the same ones (ie. the named ones ) as the claset rules *)
   6.262 -                                    (* length 1374*)
   6.263 -                                    val new_simps = #1(ResAxioms.clausify_rules  simp_rules []);
   6.264 -                                    val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
   6.265 -
   6.266 -                                    val stick_strs = map stick simpset_tptp_strs;
   6.267 -                                    val name_stick = ListPair.zip (simp_names,stick_strs);
   6.268 -
   6.269 -                                    val name_nums =map clause_numbering name_stick;
   6.270 -                                    (* length 2409*)
   6.271 -                                    val long_name_nums = stick name_nums;
   6.272 +                                        (*************************************************)
   6.273 +					(* Write out clauses as tptp strings to filename *)
   6.274 + 					(*************************************************)
   6.275 +                                        val clauses = map #1(cls_thms_list);
   6.276 +          				val cls_tptp_strs = map ResClause.tptp_clause clauses;
   6.277 +                                        (* list of lists of tptp string clauses *)
   6.278 +                                        val stick_clasrls =   stick cls_tptp_strs;
   6.279 +    					val out = TextIO.openOut filename;
   6.280 +                                    	val _=   ResLib.writeln_strs out stick_clasrls;
   6.281 +                                    	val _= TextIO.flushOut out;
   6.282 +					val _= TextIO.closeOut out
   6.283 +                     		  in
   6.284 +					(clause_arr, num_of_clauses)
   6.285 +				  end;
   6.286  
   6.287  
   6.288 -                                    val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
   6.289 -                                    val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
   6.290 -
   6.291 -
   6.292 -
   6.293 -                                    val tptplist =  (stick stick_strs) 
   6.294 -
   6.295 -                              in 
   6.296 -                                   ResLib.writeln_strs out tptplist;
   6.297 -                                   TextIO.flushOut out;
   6.298 -                                   TextIO.closeOut out;
   6.299 -                                   clause_arr
   6.300 -                              end;
   6.301 -
   6.302 -(*
   6.303 -
   6.304 - Array.sub(clause_arr,  2310);
   6.305 -*)
   6.306 +end;
     7.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue May 03 10:33:31 2005 +0200
     7.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue May 03 14:27:21 2005 +0200
     7.3 @@ -92,7 +92,7 @@
     7.4                                                           val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
     7.5                                                           (*** only include problem and clasimp for the moment, not sure how to refer to ***)
     7.6                                                           (*** hyps/local axioms just now                                                ***)
     7.7 -                                                         val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile, axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
     7.8 +                                                         val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
     7.9                                                           val dfg_create =if File.exists dfg_dir 
    7.10                                                                           then
    7.11                                                                               ((warning("dfg dir exists"));())
    7.12 @@ -112,7 +112,8 @@
    7.13                       					(warning ("probfile is: "^probfile));
    7.14                                                           (warning("dfg file is: "^newfile));
    7.15                                                           (warning ("wholefile is: "^(File.sysify_path wholefile)));
    7.16 -                                                         sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    7.17 +                                                        sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    7.18 +(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    7.19                                                           TextIO.flushOut toWatcherStr;
    7.20                                                           Unix.reap exec_tptp2x; 
    7.21                                                           
    7.22 @@ -244,7 +245,7 @@
    7.23  
    7.24  
    7.25  
    7.26 -fun setupWatcher (thm) = let
    7.27 +fun setupWatcher (thm,clause_arr, num_of_clauses) = let
    7.28            (** pipes for communication between parent and watcher **)
    7.29            val p1 = Posix.IO.pipe ()
    7.30            val p2 = Posix.IO.pipe ()
    7.31 @@ -275,6 +276,14 @@
    7.32                        val prems = prems_of thm
    7.33                        val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    7.34                        val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
    7.35 +                     (* tracing *)
    7.36 +		    (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    7.37 +                      val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
    7.38 +                      val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    7.39 +                      val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
    7.40 +                      val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
    7.41 +                      val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
    7.42 +                               *)
    7.43                        (*val goalstr = string_of_thm (the_goal)
    7.44                         val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
    7.45                        val _ = TextIO.output (outfile,goalstr )
    7.46 @@ -374,7 +383,7 @@
    7.47                                                  val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
    7.48                                                  val _ =  TextIO.closeOut outfile
    7.49                                                val childDone = (case prover of
    7.50 -                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num)     ) )
    7.51 +                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
    7.52                                                     in
    7.53                                                      if childDone      (**********************************************)
    7.54                                                      then              (* child has found a proof and transferred it *)
    7.55 @@ -475,7 +484,7 @@
    7.56                                               )
    7.57                                            else
    7.58                                              ( 
    7.59 -                                              if ((length procList)<2)    (********************)
    7.60 +                                              if ((length procList)<10)    (********************)
    7.61                                                then                        (* Execute locally  *)
    7.62                                                   (                        (********************)
    7.63                                                    let 
    7.64 @@ -587,7 +596,7 @@
    7.65  (**********************************************************)
    7.66  fun killWatcher pid= killChild pid;
    7.67  
    7.68 -fun createWatcher (thm) = let val mychild = childInfo (setupWatcher(thm))
    7.69 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    7.70  			   val streams =snd mychild
    7.71                             val childin = fst streams
    7.72                             val childout = snd streams
     8.1 --- a/src/HOL/Tools/ATP/watcher.sig	Tue May 03 10:33:31 2005 +0200
     8.2 +++ b/src/HOL/Tools/ATP/watcher.sig	Tue May 03 14:27:21 2005 +0200
     8.3 @@ -36,7 +36,7 @@
     8.4  (* Start a watcher and set up signal handlers             *)
     8.5  (**********************************************************)
     8.6  
     8.7 -val createWatcher : Thm.thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid
     8.8 +val createWatcher : Thm.thm*(ResClause.clause * Thm.thm) Array.array *  int -> TextIO.instream * TextIO.outstream * Posix.Process.pid
     8.9  
    8.10  
    8.11  
     9.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 03 10:33:31 2005 +0200
     9.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 03 14:27:21 2005 +0200
     9.3 @@ -180,22 +180,28 @@
     9.4                               val _ = TextIO.output(outfile, "prob file path is "^probfile^" thmstring is "^thmstr^" goalstring is "^goalstring);
     9.5                               val _ = TextIO.flushOut outfile;
     9.6                               val _ =  TextIO.closeOut outfile
     9.7 +                             val spass_home = getenv "SPASS_HOME"
     9.8                            in
     9.9                             (* without paramodulation *)
    9.10                             (warning ("goalstring in call_res_tac is: "^goalstring));
    9.11                             (warning ("prob file in cal_res_tac is: "^probfile));
    9.12 +                                                       Watcher.callResProvers(childout,
    9.13 +                            [("spass",thmstr,goalstring,spass_home,  
    9.14 +                             "-DocProof", 
    9.15 +                             clasimpfile, axfile, hypsfile, probfile)]);
    9.16 +
    9.17                              Watcher.callResProvers(childout,
    9.18 -                            [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",  
    9.19 +                            [("spass",thmstr,goalstring,spass_home,  
    9.20                               "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    9.21                               clasimpfile, axfile, hypsfile, probfile)]);
    9.22  
    9.23                             (* with paramodulation *)
    9.24                             (*Watcher.callResProvers(childout,
    9.25 -                                  [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS",
    9.26 +                                  [("spass",thmstr,goalstring,spass_home,
    9.27                                    "-FullRed=0%-ISPm=1%-Split=0%-PObv=0%-DocProof", 
    9.28                                      prob_path)]); *)
    9.29                            (* Watcher.callResProvers(childout,
    9.30 -                           [("spass",thmstr,goalstring,"/homes/clq20/bin/SPASS", 
    9.31 +                           [("spass",thmstr,goalstring,spass_home, 
    9.32                             "-DocProof",  prob_path)]);*)
    9.33                             dummy_tac
    9.34                           end
    9.35 @@ -282,24 +288,32 @@
    9.36  (******************************************************************)
    9.37  (*FIX changed to clasimp_file *)
    9.38  fun isar_atp' (thms, thm) =
    9.39 -    let val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    9.40 +    let 
    9.41 +	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    9.42          val _= (warning ("in isar_atp'"))
    9.43          val prems  = prems_of thm
    9.44          val sign = sign_of_thm thm
    9.45          val thms_string = Meson.concat_with_and (map string_of_thm thms) 
    9.46          val thmstring = string_of_thm thm
    9.47          val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    9.48 -        (* set up variables for writing out the clasimps to a tptp file *)
    9.49 +        
    9.50 +	(* set up variables for writing out the clasimps to a tptp file *)
    9.51 +	val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp (File.sysify_path clasimp_file) 
    9.52 +        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    9.53  
    9.54 -         val clause_arr = write_out_clasimp (File.sysify_path clasimp_file) clause_arr
    9.55 -        val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
    9.56          (* cq: add write out clasimps to file *)
    9.57 -        (* cq:create watcher and pass to isar_atp_aux *) 
    9.58 -        (*val tenth_ax = fst( Array.sub(clause_arr, 10))  
    9.59 -        val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
    9.60 -        val _ = (warning ("num_of_clauses is: "^(string_of_int (!num_of_clauses))) )  *)      
    9.61 -                               
    9.62 -        val (childin,childout,pid) = Watcher.createWatcher(thm)
    9.63 +        (* cq:create watcher and pass to isar_atp_aux *)
    9.64 +        (* tracing *) 
    9.65 +        (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
    9.66 +         val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab)
    9.67 +         val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
    9.68 +         val _ = (warning ("tenth axiom in array is: "^tenth_ax))         
    9.69 +         val _ = (warning ("tenth axiom in table is: "^clause_str))         
    9.70 +                 
    9.71 +         val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) )     
    9.72 +         *)             
    9.73 +        
    9.74 +        val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses)
    9.75          val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid )))
    9.76      in
    9.77  	case prems of [] => ()