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