src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15782 a1863ea9052b
parent 15774 9df37a0e935d
child 15789 4cb16144c81b
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Apr 20 17:19:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed Apr 20 18:01:50 2005 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  (* Get claset rules *)
     1.5  
     1.6 +
     1.7 +
     1.8  fun remove_all [] rules = rules
     1.9  |   remove_all (x::xs) rules = let val rules' = List.filter (not_equal x) rules
    1.10                                in
    1.11 @@ -23,6 +25,94 @@
    1.12  val clause_arr = Array.array(3500, ("empty", 0));
    1.13  
    1.14  
    1.15 +val foo_arr = Array.array(20, ("a",0));
    1.16 +
    1.17 +
    1.18 +(*
    1.19 +
    1.20 +fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
    1.21 +
    1.22 +
    1.23 +
    1.24 +
    1.25 +fun setupFork () = let
    1.26 +          (** pipes for communication between parent and watcher **)
    1.27 +          val p1 = Posix.IO.pipe ()
    1.28 +          val p2 = Posix.IO.pipe ()
    1.29 +	  fun closep () = (
    1.30 +                Posix.IO.close (#outfd p1); 
    1.31 +                Posix.IO.close (#infd p1);
    1.32 +                Posix.IO.close (#outfd p2); 
    1.33 +                Posix.IO.close (#infd p2)
    1.34 +              )
    1.35 +          (***********************************************************)
    1.36 +          (****** fork a watcher process and get it set up and going *)
    1.37 +          (***********************************************************)
    1.38 +          fun startFork () =
    1.39 +                   (case  Posix.Process.fork() (***************************************)
    1.40 +		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
    1.41 +                                               (***************************************)
    1.42 + 
    1.43 +                                                 (*************************)
    1.44 +                  | NONE => let                  (* child - i.e. watcher  *)
    1.45 +		      val oldchildin = #infd p1  (*************************)
    1.46 +		      val fromParent = Posix.FileSys.wordToFD 0w0
    1.47 +		      val oldchildout = #outfd p2
    1.48 +		      val toParent = Posix.FileSys.wordToFD 0w1
    1.49 +                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    1.50 +                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    1.51 +                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
    1.52 +                      val fooax = fst(Array.sub(foo_arr, 3))
    1.53 +                      val  outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");  
    1.54 +                      val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
    1.55 +                      val _ =  TextIO.closeOut outfile
    1.56 +                     in
    1.57 +                       (***************************)
    1.58 +                       (*** Sort out pipes ********)
    1.59 +                       (***************************)
    1.60 +
    1.61 +			Posix.IO.close (#outfd p1);
    1.62 +			Posix.IO.close (#infd p2);
    1.63 +			Posix.IO.dup2{old = oldchildin, new = fromParent};
    1.64 +                        Posix.IO.close oldchildin;
    1.65 +			Posix.IO.dup2{old = oldchildout, new = toParent};
    1.66 +                        Posix.IO.close oldchildout;
    1.67 +
    1.68 +                        (***************************)
    1.69 +                        (* start the watcher loop  *)
    1.70 +                        (***************************)
    1.71 +                        
    1.72 +                        (****************************************************************************)
    1.73 +                        (* fake return value - actually want the watcher to loop until killed       *)
    1.74 +                        (****************************************************************************)
    1.75 +                        Posix.Process.wordToPid 0w0
    1.76 +			
    1.77 +		      end)
    1.78 +            val start = startFork()
    1.79 +       in
    1.80 +
    1.81 +
    1.82 + (*******************************)
    1.83 +           (* close the child-side fds    *)
    1.84 +           (*******************************)
    1.85 +            Posix.IO.close (#outfd p2);
    1.86 +            Posix.IO.close (#infd p1);
    1.87 +            (* set the fds close on exec *)
    1.88 +            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
    1.89 +            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
    1.90 +             
    1.91 +           (*******************************)
    1.92 +           (* return value                *)
    1.93 +           (*******************************)
    1.94 +          ()
    1.95 +         end;
    1.96 +
    1.97 +
    1.98 +
    1.99 +*)
   1.100 +
   1.101 +
   1.102 +
   1.103  
   1.104  fun multi x 0 xlist = xlist
   1.105     |multi x n xlist = multi x (n -1 ) (x::xlist);
   1.106 @@ -91,7 +181,10 @@
   1.107  val clause_arr = Array.array(3500, ("empty", 0));
   1.108                                 
   1.109  
   1.110 -fun write_out_clasimp filename = let 
   1.111 +fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
   1.112 +                                  val  outfile = TextIO.openOut("wibble");                                  val _ = TextIO.output (outfile, ("in write_out_clasimpset"))
   1.113 +                                  val _ =  TextIO.closeOut outfile
   1.114 +                                   val _= (warning ("in writeoutclasimp"))
   1.115                                     (****************************************)
   1.116                                     (* add claset rules to array and write out as strings *)
   1.117                                     (****************************************)
   1.118 @@ -127,9 +220,7 @@
   1.119                                    (* create array and put clausename, number pairs into it *)
   1.120                                     (*******************************************)
   1.121  
   1.122 -                                        val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   1.123 -                                 
   1.124 -
   1.125 +                                   val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   1.126                                     val _= num_of_clauses := (List.length cl_long_name_nums);
   1.127                                     
   1.128                                     (*************************************)
   1.129 @@ -147,7 +238,9 @@
   1.130                                    (*********************)
   1.131                                    (* Get simpset rules *)
   1.132                                    (*********************)
   1.133 +
   1.134                                    val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
   1.135 +
   1.136                                    val named_simps = List.filter has_name_pair simpset_name_rules;
   1.137  
   1.138                                    val simp_names = map #1 named_simps;
   1.139 @@ -183,11 +276,11 @@
   1.140  
   1.141                                      val tptplist =  (stick stick_strs) 
   1.142  
   1.143 -
   1.144                                in 
   1.145                                     ResLib.writeln_strs out tptplist;
   1.146                                     TextIO.flushOut out;
   1.147 -                                   TextIO.closeOut out
   1.148 +                                   TextIO.closeOut out;
   1.149 +                                   clause_arr
   1.150                                end;
   1.151  
   1.152  (*