src/HOL/Tools/ATP/res_clasimpset.ML
author paulson
Thu Apr 28 17:56:58 2005 +0200 (2005-04-28)
changeset 15872 8336ff711d80
parent 15789 4cb16144c81b
child 15907 f377ba412dba
permissions -rw-r--r--
fixed treatment of higher-order simprules
     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 get_simp_metas [] = [[]]
   174 |   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
   175                              in
   176                                  metas::(get_simp_metas xs)
   177                              end
   178                              handle THM _ => get_simp_metas xs
   179 
   180 
   181 (* re-jig all these later as smaller functions for each bit *)
   182   val num_of_clauses = ref 0;
   183 val clause_arr = Array.array(3500, ("empty", 0));
   184                                
   185 
   186 fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
   187                                   val  outfile = TextIO.openOut("wibble");                                  val _ = TextIO.output (outfile, ("in write_out_clasimpset"))
   188                                   val _ =  TextIO.closeOut outfile
   189                                    val _= (warning ("in writeoutclasimp"))
   190                                    (****************************************)
   191                                    (* add claset rules to array and write out as strings *)
   192                                    (****************************************)
   193                                    val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
   194                                    val claset = ResAxioms.clausify_classical_rules_thy (the_context())
   195                                    val (claset_clauses,badthms) =  claset;
   196                                    val clausifiable_rules = remove_all badthms claset_rules;
   197                                    val named_claset = List.filter has_name clausifiable_rules;
   198                                    val name_fol_cs = List.filter rule_is_fol  named_claset;
   199                                    (* length name_fol_cs is 93 *)
   200                                    val good_names = map Thm.name_of_thm name_fol_cs;
   201  
   202                                    (*******************************************)
   203                                     (* get (name, thm) pairs for claset rules *)
   204                                    (*******************************************)
   205 
   206                                    val names_rules = ListPair.zip (good_names,name_fol_cs);
   207                                    
   208                                    val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
   209 
   210                                    val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
   211 
   212                                    (* list of lists of tptp string clauses *)
   213                                    val stick_clasrls =  map stick claset_tptp_strs;
   214                                    (* stick stick_clasrls length is 172*)
   215 
   216                                    val name_stick = ListPair.zip (good_names,stick_clasrls);
   217 
   218                                    val cl_name_nums =map clause_numbering name_stick;
   219                                        
   220                                    val cl_long_name_nums = stick cl_name_nums;
   221                                    (*******************************************)
   222                                   (* create array and put clausename, number pairs into it *)
   223                                    (*******************************************)
   224 
   225                                    val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   226                                    val _= num_of_clauses := (List.length cl_long_name_nums);
   227                                    
   228                                    (*************************************)
   229                                    (* write claset out as tptp file      *)
   230                                     (*************************************)
   231                                   
   232                                     val claset_all_strs = stick stick_clasrls;
   233                                     val out = TextIO.openOut filename;
   234                                     val _=   ResLib.writeln_strs out claset_all_strs;
   235                                     val _= TextIO.flushOut out;
   236                                     val _=  TextIO.output (out,("\n \n"));
   237                                     val _= TextIO.flushOut out;
   238                                    (*val _= TextIO.closeOut out;*)
   239 
   240                                   (*********************)
   241                                   (* Get simpset rules *)
   242                                   (*********************)
   243 
   244                                   val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
   245 
   246                                   val named_simps = List.filter has_name_pair simpset_name_rules;
   247 
   248                                   val simp_names = map #1 named_simps;
   249                                   val simp_rules = map #2 named_simps;
   250                               
   251                                   val (simpset_cls,badthms) = ResAxioms.clausify_rules  simp_rules [];
   252                                  (* 1137 clausif simps *)
   253                                   val name_fol_simps = remove_all_simps badthms named_simps;
   254                                    
   255                                     val simp_names = map #1 name_fol_simps;
   256                                     val simp_rules = map #2 name_fol_simps;
   257                                     
   258                                      (* 995 of these *)
   259                                     (* need to get names of claset_cluases so we can make sure we've*)
   260                                     (* got the same ones (ie. the named ones ) as the claset rules *)
   261                                     (* length 1374*)
   262                                     val new_simps = #1(ResAxioms.clausify_rules  simp_rules []);
   263                                     val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
   264 
   265                                     val stick_strs = map stick simpset_tptp_strs;
   266                                     val name_stick = ListPair.zip (simp_names,stick_strs);
   267 
   268                                     val name_nums =map clause_numbering name_stick;
   269                                     (* length 2409*)
   270                                     val long_name_nums = stick name_nums;
   271 
   272 
   273                                     val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
   274                                     val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
   275 
   276 
   277 
   278                                     val tptplist =  (stick stick_strs) 
   279 
   280                               in 
   281                                    ResLib.writeln_strs out tptplist;
   282                                    TextIO.flushOut out;
   283                                    TextIO.closeOut out;
   284                                    clause_arr
   285                               end;
   286 
   287 (*
   288 
   289  Array.sub(clause_arr,  2310);
   290 *)