src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Mon May 02 13:30:48 2005 +0200 (2005-05-02)
changeset 15907 f377ba412dba
parent 15872 8336ff711d80
child 15919 b30a35432f5a
permissions -rw-r--r--
deleted redundant code
paulson@15789
     1
(*  ID:         $Id$
paulson@15789
     2
    Author:     Claire Quigley
paulson@15789
     3
    Copyright   2004  University of Cambridge
paulson@15789
     4
*)
paulson@15789
     5
quigley@15643
     6
(* Get claset rules *)
quigley@15643
     7
quigley@15643
     8
fun has_name th = not((Thm.name_of_thm th)= "")
quigley@15643
     9
quigley@15643
    10
fun has_name_pair (a,b) = not_equal a "";
quigley@15643
    11
fun good_pair c (a,b) = not_equal b c;
quigley@15643
    12
quigley@15643
    13
quigley@15643
    14
quigley@15643
    15
val num_of_clauses = ref 0;
quigley@15643
    16
val clause_arr = Array.array(3500, ("empty", 0));
quigley@15643
    17
quigley@15643
    18
paulson@15907
    19
(*
quigley@15782
    20
val foo_arr = Array.array(20, ("a",0));
quigley@15782
    21
quigley@15782
    22
fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
quigley@15782
    23
quigley@15782
    24
quigley@15782
    25
quigley@15782
    26
quigley@15782
    27
fun setupFork () = let
quigley@15782
    28
          (** pipes for communication between parent and watcher **)
quigley@15782
    29
          val p1 = Posix.IO.pipe ()
quigley@15782
    30
          val p2 = Posix.IO.pipe ()
quigley@15782
    31
	  fun closep () = (
quigley@15782
    32
                Posix.IO.close (#outfd p1); 
quigley@15782
    33
                Posix.IO.close (#infd p1);
quigley@15782
    34
                Posix.IO.close (#outfd p2); 
quigley@15782
    35
                Posix.IO.close (#infd p2)
quigley@15782
    36
              )
quigley@15782
    37
          (***********************************************************)
quigley@15782
    38
          (****** fork a watcher process and get it set up and going *)
quigley@15782
    39
          (***********************************************************)
quigley@15782
    40
          fun startFork () =
quigley@15782
    41
                   (case  Posix.Process.fork() (***************************************)
quigley@15782
    42
		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
quigley@15782
    43
                                               (***************************************)
quigley@15782
    44
 
quigley@15782
    45
                                                 (*************************)
quigley@15782
    46
                  | NONE => let                  (* child - i.e. watcher  *)
quigley@15782
    47
		      val oldchildin = #infd p1  (*************************)
quigley@15782
    48
		      val fromParent = Posix.FileSys.wordToFD 0w0
quigley@15782
    49
		      val oldchildout = #outfd p2
quigley@15782
    50
		      val toParent = Posix.FileSys.wordToFD 0w1
quigley@15782
    51
                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
quigley@15782
    52
                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
quigley@15782
    53
                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
quigley@15782
    54
                      val fooax = fst(Array.sub(foo_arr, 3))
quigley@15782
    55
                      val  outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");  
quigley@15782
    56
                      val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
quigley@15782
    57
                      val _ =  TextIO.closeOut outfile
quigley@15782
    58
                     in
quigley@15782
    59
                       (***************************)
quigley@15782
    60
                       (*** Sort out pipes ********)
quigley@15782
    61
                       (***************************)
quigley@15782
    62
quigley@15782
    63
			Posix.IO.close (#outfd p1);
quigley@15782
    64
			Posix.IO.close (#infd p2);
quigley@15782
    65
			Posix.IO.dup2{old = oldchildin, new = fromParent};
quigley@15782
    66
                        Posix.IO.close oldchildin;
quigley@15782
    67
			Posix.IO.dup2{old = oldchildout, new = toParent};
quigley@15782
    68
                        Posix.IO.close oldchildout;
quigley@15782
    69
quigley@15782
    70
                        (***************************)
quigley@15782
    71
                        (* start the watcher loop  *)
quigley@15782
    72
                        (***************************)
quigley@15782
    73
                        
quigley@15782
    74
                        (****************************************************************************)
quigley@15782
    75
                        (* fake return value - actually want the watcher to loop until killed       *)
quigley@15782
    76
                        (****************************************************************************)
quigley@15782
    77
                        Posix.Process.wordToPid 0w0
quigley@15782
    78
			
quigley@15782
    79
		      end)
quigley@15782
    80
            val start = startFork()
quigley@15782
    81
       in
quigley@15782
    82
quigley@15782
    83
quigley@15782
    84
 (*******************************)
quigley@15782
    85
           (* close the child-side fds    *)
quigley@15782
    86
           (*******************************)
quigley@15782
    87
            Posix.IO.close (#outfd p2);
quigley@15782
    88
            Posix.IO.close (#infd p1);
quigley@15782
    89
            (* set the fds close on exec *)
quigley@15782
    90
            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
quigley@15782
    91
            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
quigley@15782
    92
             
quigley@15782
    93
           (*******************************)
quigley@15782
    94
           (* return value                *)
quigley@15782
    95
           (*******************************)
quigley@15782
    96
          ()
quigley@15782
    97
         end;
quigley@15782
    98
quigley@15782
    99
quigley@15782
   100
quigley@15782
   101
*)
quigley@15782
   102
quigley@15782
   103
quigley@15782
   104
quigley@15643
   105
quigley@15643
   106
fun multi x 0 xlist = xlist
quigley@15643
   107
   |multi x n xlist = multi x (n -1 ) (x::xlist);
quigley@15643
   108
quigley@15643
   109
quigley@15643
   110
fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
quigley@15643
   111
                                              val numbers = 0 upto (num_of_cls -1)
quigley@15643
   112
                                              val multi_name = multi name num_of_cls []
quigley@15643
   113
                                          in 
paulson@15774
   114
                                              ListPair.zip (multi_name,numbers)
quigley@15643
   115
                                          end;
quigley@15643
   116
quigley@15643
   117
fun stick []  = []
quigley@15643
   118
|   stick (x::xs)  = x@(stick xs )
quigley@15643
   119
quigley@15643
   120
quigley@15643
   121
quigley@15643
   122
fun fill_cls_array array n [] = ()
quigley@15643
   123
|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
quigley@15643
   124
                                     in
quigley@15643
   125
                                        fill_cls_array array (n+1) (xs)
quigley@15643
   126
                                     end;
quigley@15643
   127
quigley@15643
   128
quigley@15643
   129
   	      	    
quigley@15643
   130
val nc = ref (Symtab.empty : (thm list) Symtab.table)
quigley@15643
   131
quigley@15643
   132
 
quigley@15643
   133
quigley@15643
   134
fun memo_add_clauses (name:string, cls)=
quigley@15643
   135
                        nc := Symtab.update((name , cls), !nc);
quigley@15643
   136
      	       
quigley@15643
   137
quigley@15643
   138
quigley@15643
   139
fun memo_find_clause name = case Symtab.lookup (!nc,name) of
quigley@15643
   140
      	        NONE =>  []
quigley@15643
   141
                |SOME cls  => cls ;
quigley@15643
   142
quigley@15643
   143
quigley@15643
   144
fun get_simp_metas [] = [[]]
quigley@15643
   145
|   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
quigley@15643
   146
                             in
quigley@15643
   147
                                 metas::(get_simp_metas xs)
quigley@15643
   148
                             end
quigley@15643
   149
                             handle THM _ => get_simp_metas xs
quigley@15643
   150
quigley@15643
   151
quigley@15643
   152
(* re-jig all these later as smaller functions for each bit *)
quigley@15643
   153
  val num_of_clauses = ref 0;
quigley@15643
   154
val clause_arr = Array.array(3500, ("empty", 0));
quigley@15643
   155
                               
quigley@15643
   156
quigley@15782
   157
fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
paulson@15907
   158
                                   val _= warning "in writeoutclasimp"
quigley@15643
   159
                                   (****************************************)
quigley@15643
   160
                                   (* add claset rules to array and write out as strings *)
quigley@15643
   161
                                   (****************************************)
paulson@15907
   162
                                   val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
paulson@15907
   163
                                   val name_fol_cs = List.filter has_name clausifiable_rules;
quigley@15643
   164
                                   (* length name_fol_cs is 93 *)
quigley@15643
   165
                                   val good_names = map Thm.name_of_thm name_fol_cs;
quigley@15643
   166
 
quigley@15643
   167
                                   (*******************************************)
quigley@15643
   168
                                    (* get (name, thm) pairs for claset rules *)
quigley@15643
   169
                                   (*******************************************)
quigley@15643
   170
paulson@15774
   171
                                   val names_rules = ListPair.zip (good_names,name_fol_cs);
quigley@15643
   172
                                   
paulson@15872
   173
                                   val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
quigley@15643
   174
quigley@15643
   175
                                   val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
quigley@15643
   176
quigley@15643
   177
                                   (* list of lists of tptp string clauses *)
quigley@15643
   178
                                   val stick_clasrls =  map stick claset_tptp_strs;
quigley@15643
   179
                                   (* stick stick_clasrls length is 172*)
quigley@15643
   180
paulson@15774
   181
                                   val name_stick = ListPair.zip (good_names,stick_clasrls);
quigley@15643
   182
quigley@15643
   183
                                   val cl_name_nums =map clause_numbering name_stick;
quigley@15643
   184
                                       
quigley@15643
   185
                                   val cl_long_name_nums = stick cl_name_nums;
quigley@15643
   186
                                   (*******************************************)
quigley@15643
   187
                                  (* create array and put clausename, number pairs into it *)
quigley@15643
   188
                                   (*******************************************)
quigley@15643
   189
quigley@15782
   190
                                   val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
quigley@15643
   191
                                   val _= num_of_clauses := (List.length cl_long_name_nums);
quigley@15643
   192
                                   
quigley@15643
   193
                                   (*************************************)
quigley@15643
   194
                                   (* write claset out as tptp file      *)
quigley@15643
   195
                                    (*************************************)
quigley@15643
   196
                                  
quigley@15643
   197
                                    val claset_all_strs = stick stick_clasrls;
quigley@15643
   198
                                    val out = TextIO.openOut filename;
quigley@15643
   199
                                    val _=   ResLib.writeln_strs out claset_all_strs;
quigley@15643
   200
                                    val _= TextIO.flushOut out;
quigley@15643
   201
                                    val _=  TextIO.output (out,("\n \n"));
quigley@15643
   202
                                    val _= TextIO.flushOut out;
quigley@15643
   203
                                   (*val _= TextIO.closeOut out;*)
quigley@15643
   204
quigley@15643
   205
                                  (*********************)
quigley@15643
   206
                                  (* Get simpset rules *)
quigley@15643
   207
                                  (*********************)
quigley@15782
   208
paulson@15736
   209
                                  val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
quigley@15782
   210
quigley@15643
   211
                                  val named_simps = List.filter has_name_pair simpset_name_rules;
quigley@15643
   212
paulson@15736
   213
                                  val simp_names = map #1 named_simps;
paulson@15736
   214
                                  val simp_rules = map #2 named_simps;
quigley@15643
   215
                              
quigley@15643
   216
                                 (* 1137 clausif simps *)
quigley@15643
   217
                                   
quigley@15643
   218
                                    (* need to get names of claset_cluases so we can make sure we've*)
quigley@15643
   219
                                    (* got the same ones (ie. the named ones ) as the claset rules *)
quigley@15643
   220
                                    (* length 1374*)
paulson@15872
   221
                                    val new_simps = #1(ResAxioms.clausify_rules  simp_rules []);
quigley@15643
   222
                                    val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
quigley@15643
   223
quigley@15643
   224
                                    val stick_strs = map stick simpset_tptp_strs;
paulson@15774
   225
                                    val name_stick = ListPair.zip (simp_names,stick_strs);
quigley@15643
   226
quigley@15643
   227
                                    val name_nums =map clause_numbering name_stick;
quigley@15643
   228
                                    (* length 2409*)
quigley@15643
   229
                                    val long_name_nums = stick name_nums;
quigley@15643
   230
quigley@15643
   231
quigley@15643
   232
                                    val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
quigley@15643
   233
                                    val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
quigley@15643
   234
quigley@15643
   235
quigley@15643
   236
quigley@15643
   237
                                    val tptplist =  (stick stick_strs) 
quigley@15643
   238
quigley@15643
   239
                              in 
quigley@15643
   240
                                   ResLib.writeln_strs out tptplist;
quigley@15643
   241
                                   TextIO.flushOut out;
quigley@15782
   242
                                   TextIO.closeOut out;
quigley@15782
   243
                                   clause_arr
quigley@15643
   244
                              end;
quigley@15643
   245
quigley@15643
   246
(*
quigley@15643
   247
quigley@15643
   248
 Array.sub(clause_arr,  2310);
quigley@15643
   249
*)