src/HOL/Tools/ATP/res_clasimpset.ML
changeset 15919 b30a35432f5a
parent 15907 f377ba412dba
child 15956 0da64b5a9a00
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 03 10:33:31 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 03 14:27:21 2005 +0200
     1.3 @@ -3,247 +3,76 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 -(* Get claset rules *)
     1.8 +signature RES_CLASIMP =
     1.9 +  sig
    1.10 +     val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
    1.11 +  end;
    1.12 +
    1.13 +structure ResClasimp : RES_CLASIMP =
    1.14 +struct
    1.15  
    1.16  fun has_name th = not((Thm.name_of_thm th)= "")
    1.17  
    1.18  fun has_name_pair (a,b) = not_equal a "";
    1.19 -fun good_pair c (a,b) = not_equal b c;
    1.20 -
    1.21 -
    1.22 -
    1.23 -val num_of_clauses = ref 0;
    1.24 -val clause_arr = Array.array(3500, ("empty", 0));
    1.25 -
    1.26 -
    1.27 -(*
    1.28 -val foo_arr = Array.array(20, ("a",0));
    1.29 -
    1.30 -fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
    1.31 -
    1.32 -
    1.33 -
    1.34 -
    1.35 -fun setupFork () = let
    1.36 -          (** pipes for communication between parent and watcher **)
    1.37 -          val p1 = Posix.IO.pipe ()
    1.38 -          val p2 = Posix.IO.pipe ()
    1.39 -	  fun closep () = (
    1.40 -                Posix.IO.close (#outfd p1); 
    1.41 -                Posix.IO.close (#infd p1);
    1.42 -                Posix.IO.close (#outfd p2); 
    1.43 -                Posix.IO.close (#infd p2)
    1.44 -              )
    1.45 -          (***********************************************************)
    1.46 -          (****** fork a watcher process and get it set up and going *)
    1.47 -          (***********************************************************)
    1.48 -          fun startFork () =
    1.49 -                   (case  Posix.Process.fork() (***************************************)
    1.50 -		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
    1.51 -                                               (***************************************)
    1.52 - 
    1.53 -                                                 (*************************)
    1.54 -                  | NONE => let                  (* child - i.e. watcher  *)
    1.55 -		      val oldchildin = #infd p1  (*************************)
    1.56 -		      val fromParent = Posix.FileSys.wordToFD 0w0
    1.57 -		      val oldchildout = #outfd p2
    1.58 -		      val toParent = Posix.FileSys.wordToFD 0w1
    1.59 -                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
    1.60 -                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
    1.61 -                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
    1.62 -                      val fooax = fst(Array.sub(foo_arr, 3))
    1.63 -                      val  outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");  
    1.64 -                      val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
    1.65 -                      val _ =  TextIO.closeOut outfile
    1.66 -                     in
    1.67 -                       (***************************)
    1.68 -                       (*** Sort out pipes ********)
    1.69 -                       (***************************)
    1.70 -
    1.71 -			Posix.IO.close (#outfd p1);
    1.72 -			Posix.IO.close (#infd p2);
    1.73 -			Posix.IO.dup2{old = oldchildin, new = fromParent};
    1.74 -                        Posix.IO.close oldchildin;
    1.75 -			Posix.IO.dup2{old = oldchildout, new = toParent};
    1.76 -                        Posix.IO.close oldchildout;
    1.77 -
    1.78 -                        (***************************)
    1.79 -                        (* start the watcher loop  *)
    1.80 -                        (***************************)
    1.81 -                        
    1.82 -                        (****************************************************************************)
    1.83 -                        (* fake return value - actually want the watcher to loop until killed       *)
    1.84 -                        (****************************************************************************)
    1.85 -                        Posix.Process.wordToPid 0w0
    1.86 -			
    1.87 -		      end)
    1.88 -            val start = startFork()
    1.89 -       in
    1.90 -
    1.91 -
    1.92 - (*******************************)
    1.93 -           (* close the child-side fds    *)
    1.94 -           (*******************************)
    1.95 -            Posix.IO.close (#outfd p2);
    1.96 -            Posix.IO.close (#infd p1);
    1.97 -            (* set the fds close on exec *)
    1.98 -            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
    1.99 -            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   1.100 -             
   1.101 -           (*******************************)
   1.102 -           (* return value                *)
   1.103 -           (*******************************)
   1.104 -          ()
   1.105 -         end;
   1.106 -
   1.107 -
   1.108 -
   1.109 -*)
   1.110 -
   1.111 -
   1.112 -
   1.113 -
   1.114 -fun multi x 0 xlist = xlist
   1.115 -   |multi x n xlist = multi x (n -1 ) (x::xlist);
   1.116 -
   1.117 -
   1.118 -fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
   1.119 -                                              val numbers = 0 upto (num_of_cls -1)
   1.120 -                                              val multi_name = multi name num_of_cls []
   1.121 -                                          in 
   1.122 -                                              ListPair.zip (multi_name,numbers)
   1.123 -                                          end;
   1.124  
   1.125  fun stick []  = []
   1.126  |   stick (x::xs)  = x@(stick xs )
   1.127  
   1.128 -
   1.129 -
   1.130 -fun fill_cls_array array n [] = ()
   1.131 -|   fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
   1.132 -                                     in
   1.133 -                                        fill_cls_array array (n+1) (xs)
   1.134 -                                     end;
   1.135 -
   1.136 -
   1.137 -   	      	    
   1.138 -val nc = ref (Symtab.empty : (thm list) Symtab.table)
   1.139 -
   1.140 - 
   1.141 -
   1.142 -fun memo_add_clauses (name:string, cls)=
   1.143 -                        nc := Symtab.update((name , cls), !nc);
   1.144 -      	       
   1.145 -
   1.146 -
   1.147 -fun memo_find_clause name = case Symtab.lookup (!nc,name) of
   1.148 -      	        NONE =>  []
   1.149 -                |SOME cls  => cls ;
   1.150 -
   1.151 -
   1.152 -fun get_simp_metas [] = [[]]
   1.153 -|   get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
   1.154 -                             in
   1.155 -                                 metas::(get_simp_metas xs)
   1.156 -                             end
   1.157 -                             handle THM _ => get_simp_metas xs
   1.158 +(* changed, now it also finds out the name of the theorem. *)
   1.159 +(* convert a theorem into CNF and then into Clause.clause format. *)
   1.160 +fun clausify_axiom_pairs thm =
   1.161 +    let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
   1.162 +        val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
   1.163 +        val thm_name = Thm.name_of_thm thm
   1.164 +	val clauses_n = length isa_clauses
   1.165 +	fun make_axiom_clauses _ [] []= []
   1.166 +	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
   1.167 +    in
   1.168 +	make_axiom_clauses 0 isa_clauses' isa_clauses		
   1.169 +    end;
   1.170  
   1.171  
   1.172 -(* re-jig all these later as smaller functions for each bit *)
   1.173 -  val num_of_clauses = ref 0;
   1.174 -val clause_arr = Array.array(3500, ("empty", 0));
   1.175 -                               
   1.176 -
   1.177 -fun write_out_clasimp filename (clause_arr:(string * int) Array.array)  = let 
   1.178 -                                   val _= warning "in writeoutclasimp"
   1.179 -                                   (****************************************)
   1.180 -                                   (* add claset rules to array and write out as strings *)
   1.181 -                                   (****************************************)
   1.182 -                                   val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
   1.183 -                                   val name_fol_cs = List.filter has_name clausifiable_rules;
   1.184 -                                   (* length name_fol_cs is 93 *)
   1.185 -                                   val good_names = map Thm.name_of_thm name_fol_cs;
   1.186 - 
   1.187 -                                   (*******************************************)
   1.188 -                                    (* get (name, thm) pairs for claset rules *)
   1.189 -                                   (*******************************************)
   1.190 +fun clausify_rules_pairs [] err_list = ([],err_list)
   1.191 +  | clausify_rules_pairs (thm::thms) err_list =
   1.192 +    let val (ts,es) = clausify_rules_pairs thms err_list
   1.193 +    in
   1.194 +	((clausify_axiom_pairs thm)::ts,es) handle  _ => (ts,(thm::es))
   1.195 +    end;
   1.196  
   1.197 -                                   val names_rules = ListPair.zip (good_names,name_fol_cs);
   1.198 -                                   
   1.199 -                                   val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
   1.200 -
   1.201 -                                   val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
   1.202 +fun write_out_clasimp filename = let
   1.203 +					val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
   1.204 +					val named_claset = List.filter has_name claset_rules;
   1.205 +					val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
   1.206  
   1.207 -                                   (* list of lists of tptp string clauses *)
   1.208 -                                   val stick_clasrls =  map stick claset_tptp_strs;
   1.209 -                                   (* stick stick_clasrls length is 172*)
   1.210 -
   1.211 -                                   val name_stick = ListPair.zip (good_names,stick_clasrls);
   1.212 +					val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
   1.213 +					val named_simpset = map #2(List.filter has_name_pair simpset_rules);
   1.214 +					val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
   1.215  
   1.216 -                                   val cl_name_nums =map clause_numbering name_stick;
   1.217 -                                       
   1.218 -                                   val cl_long_name_nums = stick cl_name_nums;
   1.219 -                                   (*******************************************)
   1.220 -                                  (* create array and put clausename, number pairs into it *)
   1.221 -                                   (*******************************************)
   1.222 +					val cls_thms = (claset_cls_thms@simpset_cls_thms);
   1.223 +					val cls_thms_list = stick cls_thms;
   1.224  
   1.225 -                                   val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
   1.226 -                                   val _= num_of_clauses := (List.length cl_long_name_nums);
   1.227 -                                   
   1.228 -                                   (*************************************)
   1.229 -                                   (* write claset out as tptp file      *)
   1.230 -                                    (*************************************)
   1.231 -                                  
   1.232 -                                    val claset_all_strs = stick stick_clasrls;
   1.233 -                                    val out = TextIO.openOut filename;
   1.234 -                                    val _=   ResLib.writeln_strs out claset_all_strs;
   1.235 -                                    val _= TextIO.flushOut out;
   1.236 -                                    val _=  TextIO.output (out,("\n \n"));
   1.237 -                                    val _= TextIO.flushOut out;
   1.238 -                                   (*val _= TextIO.closeOut out;*)
   1.239 -
   1.240 -                                  (*********************)
   1.241 -                                  (* Get simpset rules *)
   1.242 -                                  (*********************)
   1.243 +                                        (*********************************************************)
   1.244 +                                  	(* create array and put clausename, number pairs into it *)
   1.245 +                                   	(*********************************************************)
   1.246 +					val num_of_clauses =  0;
   1.247 +                                     	val clause_arr = Array.fromList cls_thms_list;
   1.248 +              
   1.249 +                                   	val  num_of_clauses= (List.length cls_thms_list);
   1.250  
   1.251 -                                  val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
   1.252 -
   1.253 -                                  val named_simps = List.filter has_name_pair simpset_name_rules;
   1.254 -
   1.255 -                                  val simp_names = map #1 named_simps;
   1.256 -                                  val simp_rules = map #2 named_simps;
   1.257 -                              
   1.258 -                                 (* 1137 clausif simps *)
   1.259 -                                   
   1.260 -                                    (* need to get names of claset_cluases so we can make sure we've*)
   1.261 -                                    (* got the same ones (ie. the named ones ) as the claset rules *)
   1.262 -                                    (* length 1374*)
   1.263 -                                    val new_simps = #1(ResAxioms.clausify_rules  simp_rules []);
   1.264 -                                    val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
   1.265 -
   1.266 -                                    val stick_strs = map stick simpset_tptp_strs;
   1.267 -                                    val name_stick = ListPair.zip (simp_names,stick_strs);
   1.268 -
   1.269 -                                    val name_nums =map clause_numbering name_stick;
   1.270 -                                    (* length 2409*)
   1.271 -                                    val long_name_nums = stick name_nums;
   1.272 +                                        (*************************************************)
   1.273 +					(* Write out clauses as tptp strings to filename *)
   1.274 + 					(*************************************************)
   1.275 +                                        val clauses = map #1(cls_thms_list);
   1.276 +          				val cls_tptp_strs = map ResClause.tptp_clause clauses;
   1.277 +                                        (* list of lists of tptp string clauses *)
   1.278 +                                        val stick_clasrls =   stick cls_tptp_strs;
   1.279 +    					val out = TextIO.openOut filename;
   1.280 +                                    	val _=   ResLib.writeln_strs out stick_clasrls;
   1.281 +                                    	val _= TextIO.flushOut out;
   1.282 +					val _= TextIO.closeOut out
   1.283 +                     		  in
   1.284 +					(clause_arr, num_of_clauses)
   1.285 +				  end;
   1.286  
   1.287  
   1.288 -                                    val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
   1.289 -                                    val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
   1.290 -
   1.291 -
   1.292 -
   1.293 -                                    val tptplist =  (stick stick_strs) 
   1.294 -
   1.295 -                              in 
   1.296 -                                   ResLib.writeln_strs out tptplist;
   1.297 -                                   TextIO.flushOut out;
   1.298 -                                   TextIO.closeOut out;
   1.299 -                                   clause_arr
   1.300 -                              end;
   1.301 -
   1.302 -(*
   1.303 -
   1.304 - Array.sub(clause_arr,  2310);
   1.305 -*)
   1.306 +end;