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