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