--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 10:33:31 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue May 03 14:27:21 2005 +0200
@@ -3,247 +3,76 @@
Copyright 2004 University of Cambridge
*)
-(* Get claset rules *)
+signature RES_CLASIMP =
+ sig
+ val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
+ end;
+
+structure ResClasimp : RES_CLASIMP =
+struct
fun has_name th = not((Thm.name_of_thm th)= "")
fun has_name_pair (a,b) = not_equal a "";
-fun good_pair c (a,b) = not_equal b c;
-
-
-
-val num_of_clauses = ref 0;
-val clause_arr = Array.array(3500, ("empty", 0));
-
-
-(*
-val foo_arr = Array.array(20, ("a",0));
-
-fill_cls_array foo_arr 0 [("b",1), ("c",2), ("d", 3), ("e", 4), ("f",5)];
-
-
-
-
-fun setupFork () = let
- (** pipes for communication between parent and watcher **)
- val p1 = Posix.IO.pipe ()
- val p2 = Posix.IO.pipe ()
- fun closep () = (
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p1);
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p2)
- )
- (***********************************************************)
- (****** fork a watcher process and get it set up and going *)
- (***********************************************************)
- fun startFork () =
- (case Posix.Process.fork() (***************************************)
- of SOME pid => pid (* parent - i.e. main Isabelle process *)
- (***************************************)
-
- (*************************)
- | NONE => let (* child - i.e. watcher *)
- val oldchildin = #infd p1 (*************************)
- val fromParent = Posix.FileSys.wordToFD 0w0
- val oldchildout = #outfd p2
- val toParent = Posix.FileSys.wordToFD 0w1
- val fromParentIOD = Posix.FileSys.fdToIOD fromParent
- val fromParentStr = openInFD ("_exec_in_parent", fromParent)
- val toParentStr = openOutFD ("_exec_out_parent", toParent)
- val fooax = fst(Array.sub(foo_arr, 3))
- val outfile = TextIO.openOut("/homes/clq20/Jia_Code/fork");
- val _ = TextIO.output (outfile, ("fooax 3 is: "^fooax))
- val _ = TextIO.closeOut outfile
- in
- (***************************)
- (*** Sort out pipes ********)
- (***************************)
-
- Posix.IO.close (#outfd p1);
- Posix.IO.close (#infd p2);
- Posix.IO.dup2{old = oldchildin, new = fromParent};
- Posix.IO.close oldchildin;
- Posix.IO.dup2{old = oldchildout, new = toParent};
- Posix.IO.close oldchildout;
-
- (***************************)
- (* start the watcher loop *)
- (***************************)
-
- (****************************************************************************)
- (* fake return value - actually want the watcher to loop until killed *)
- (****************************************************************************)
- Posix.Process.wordToPid 0w0
-
- end)
- val start = startFork()
- in
-
-
- (*******************************)
- (* close the child-side fds *)
- (*******************************)
- Posix.IO.close (#outfd p2);
- Posix.IO.close (#infd p1);
- (* set the fds close on exec *)
- Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
- Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
-
- (*******************************)
- (* return value *)
- (*******************************)
- ()
- end;
-
-
-
-*)
-
-
-
-
-fun multi x 0 xlist = xlist
- |multi x n xlist = multi x (n -1 ) (x::xlist);
-
-
-fun clause_numbering (name:string, cls) = let val num_of_cls = length cls
- val numbers = 0 upto (num_of_cls -1)
- val multi_name = multi name num_of_cls []
- in
- ListPair.zip (multi_name,numbers)
- end;
fun stick [] = []
| stick (x::xs) = x@(stick xs )
-
-
-fun fill_cls_array array n [] = ()
-| fill_cls_array array n (x::xs) = let val _ = Array.update (array, n,x)
- in
- fill_cls_array array (n+1) (xs)
- end;
-
-
-
-val nc = ref (Symtab.empty : (thm list) Symtab.table)
-
-
-
-fun memo_add_clauses (name:string, cls)=
- nc := Symtab.update((name , cls), !nc);
-
-
-
-fun memo_find_clause name = case Symtab.lookup (!nc,name) of
- NONE => []
- |SOME cls => cls ;
-
-
-fun get_simp_metas [] = [[]]
-| get_simp_metas (x::xs) = let val metas = ResAxioms.meta_cnf_axiom x
- in
- metas::(get_simp_metas xs)
- end
- handle THM _ => get_simp_metas xs
+(* changed, now it also finds out the name of the theorem. *)
+(* convert a theorem into CNF and then into Clause.clause format. *)
+fun clausify_axiom_pairs thm =
+ let val isa_clauses = ResAxioms.cnf_axiom thm (*"isa_clauses" are already "standard"ed. *)
+ val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
+ val thm_name = Thm.name_of_thm thm
+ val clauses_n = length isa_clauses
+ fun make_axiom_clauses _ [] []= []
+ | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
+ in
+ make_axiom_clauses 0 isa_clauses' isa_clauses
+ end;
-(* re-jig all these later as smaller functions for each bit *)
- val num_of_clauses = ref 0;
-val clause_arr = Array.array(3500, ("empty", 0));
-
-
-fun write_out_clasimp filename (clause_arr:(string * int) Array.array) = let
- val _= warning "in writeoutclasimp"
- (****************************************)
- (* add claset rules to array and write out as strings *)
- (****************************************)
- val clausifiable_rules = ResAxioms.claset_rules_of_thy (the_context())
- val name_fol_cs = List.filter has_name clausifiable_rules;
- (* length name_fol_cs is 93 *)
- val good_names = map Thm.name_of_thm name_fol_cs;
-
- (*******************************************)
- (* get (name, thm) pairs for claset rules *)
- (*******************************************)
+fun clausify_rules_pairs [] err_list = ([],err_list)
+ | clausify_rules_pairs (thm::thms) err_list =
+ let val (ts,es) = clausify_rules_pairs thms err_list
+ in
+ ((clausify_axiom_pairs thm)::ts,es) handle _ => (ts,(thm::es))
+ end;
- val names_rules = ListPair.zip (good_names,name_fol_cs);
-
- val new_clasrls = #1(ResAxioms.clausify_rules name_fol_cs[])
-
- val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
+fun write_out_clasimp filename = let
+ val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
+ val named_claset = List.filter has_name claset_rules;
+ val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
- (* list of lists of tptp string clauses *)
- val stick_clasrls = map stick claset_tptp_strs;
- (* stick stick_clasrls length is 172*)
-
- val name_stick = ListPair.zip (good_names,stick_clasrls);
+ val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
+ val named_simpset = map #2(List.filter has_name_pair simpset_rules);
+ val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
- val cl_name_nums =map clause_numbering name_stick;
-
- val cl_long_name_nums = stick cl_name_nums;
- (*******************************************)
- (* create array and put clausename, number pairs into it *)
- (*******************************************)
+ val cls_thms = (claset_cls_thms@simpset_cls_thms);
+ val cls_thms_list = stick cls_thms;
- val _ = fill_cls_array clause_arr 1 cl_long_name_nums;
- val _= num_of_clauses := (List.length cl_long_name_nums);
-
- (*************************************)
- (* write claset out as tptp file *)
- (*************************************)
-
- val claset_all_strs = stick stick_clasrls;
- val out = TextIO.openOut filename;
- val _= ResLib.writeln_strs out claset_all_strs;
- val _= TextIO.flushOut out;
- val _= TextIO.output (out,("\n \n"));
- val _= TextIO.flushOut out;
- (*val _= TextIO.closeOut out;*)
-
- (*********************)
- (* Get simpset rules *)
- (*********************)
+ (*********************************************************)
+ (* create array and put clausename, number pairs into it *)
+ (*********************************************************)
+ val num_of_clauses = 0;
+ val clause_arr = Array.fromList cls_thms_list;
+
+ val num_of_clauses= (List.length cls_thms_list);
- val (simpset_name_rules) = ResAxioms.simpset_rules_of_thy (the_context());
-
- val named_simps = List.filter has_name_pair simpset_name_rules;
-
- val simp_names = map #1 named_simps;
- val simp_rules = map #2 named_simps;
-
- (* 1137 clausif simps *)
-
- (* need to get names of claset_cluases so we can make sure we've*)
- (* got the same ones (ie. the named ones ) as the claset rules *)
- (* length 1374*)
- val new_simps = #1(ResAxioms.clausify_rules simp_rules []);
- val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
-
- val stick_strs = map stick simpset_tptp_strs;
- val name_stick = ListPair.zip (simp_names,stick_strs);
-
- val name_nums =map clause_numbering name_stick;
- (* length 2409*)
- val long_name_nums = stick name_nums;
+ (*************************************************)
+ (* Write out clauses as tptp strings to filename *)
+ (*************************************************)
+ val clauses = map #1(cls_thms_list);
+ val cls_tptp_strs = map ResClause.tptp_clause clauses;
+ (* list of lists of tptp string clauses *)
+ val stick_clasrls = stick cls_tptp_strs;
+ val out = TextIO.openOut filename;
+ val _= ResLib.writeln_strs out stick_clasrls;
+ val _= TextIO.flushOut out;
+ val _= TextIO.closeOut out
+ in
+ (clause_arr, num_of_clauses)
+ end;
- val _ =fill_cls_array clause_arr (!num_of_clauses + 1) long_name_nums;
- val _ =num_of_clauses := (!num_of_clauses) + (List.length long_name_nums);
-
-
-
- val tptplist = (stick stick_strs)
-
- in
- ResLib.writeln_strs out tptplist;
- TextIO.flushOut out;
- TextIO.closeOut out;
- clause_arr
- end;
-
-(*
-
- Array.sub(clause_arr, 2310);
-*)
+end;