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