--- a/src/HOL/Reconstruction.thy Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Reconstruction.thy Tue Apr 12 11:08:25 2005 +0200
@@ -25,6 +25,7 @@
"Tools/ATP/modUnix.ML"
"Tools/ATP/watcher.sig"
"Tools/ATP/watcher.ML"
+ "Tools/ATP/res_clasimpset.ML"
"Tools/res_atp.ML"
"Tools/reconstruction.ML"
--- a/src/HOL/Tools/ATP/modUnix.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/ATP/modUnix.ML Tue Apr 12 11:08:25 2005 +0200
@@ -8,33 +8,7 @@
val fromStatus = Posix.Process.fromStatus
-
-
-(* Internal function - inverse of Posix.Process.fromStatus. *)
-local
- val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific
- in
- fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0))
- | toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w))
- | toStatus(W_SIGNALED s) =
- doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s)))
- | toStatus(W_STOPPED s) =
- doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s)))
- end
-
-(* fun reap{pid, infd, outfd} =
- let
- val u = Posix.IO.close infd;
- val u = Posix.IO.close outfd;
- val (_, status) =
- Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
- in
- toStatus status
- end
-
-*)
-
- fun reap(pid, instr, outstr) =
+fun reap(pid, instr, outstr) =
let
val u = TextIO.closeIn instr;
val u = TextIO.closeOut outstr;
@@ -42,14 +16,14 @@
val (_, status) =
Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
in
- toStatus status
+ status
end
fun fdReader (name : string, fd : Posix.IO.file_desc) =
- Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
+ Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
fun fdWriter (name, fd) =
- Posix.IO.mkWriter {
+ Posix.IO.mkTextWriter {
appendMode = false,
initBlkMode = true,
name = name,
@@ -292,4 +266,4 @@
instr = instr,
outstr = outstr
})::procList))
- end;
\ No newline at end of file
+ end;
--- a/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_order_clauses.ML Tue Apr 12 11:08:25 2005 +0200
@@ -16,139 +16,8 @@
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
- fun literals (Const("Trueprop",_) $ P) = literals P
- | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
- | literals (Const("Not",_) $ P) = [(false,P)]
- | literals P = [(true,P)];
-
- (*number of literals in a term*)
- val nliterals = length o literals;
-
exception Not_in_list;
-
-(*
-(* gives horn clause with kth disj as concl (starting at 1) *)
-fun rots (0,th) = (Meson.make_horn Meson.crules th)
- | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
-
-
-
-Goal " (~~P) == P";
-by Auto_tac;
-qed "notnotEq";
-
-Goal "A | A ==> A";
-by Auto_tac;
-qed "rem_dup_disj";
-
-
-
-
-(* New Meson code Versions of make_neg_rule and make_pos_rule that don't insert new *)
-(* assumptions, for ordinary resolution. *)
-
-
-
-
- val not_conjD = thm "meson_not_conjD";
- val not_disjD = thm "meson_not_disjD";
- val not_notD = thm "meson_not_notD";
- val not_allD = thm "meson_not_allD";
- val not_exD = thm "meson_not_exD";
- val imp_to_disjD = thm "meson_imp_to_disjD";
- val not_impD = thm "meson_not_impD";
- val iff_to_disjD = thm "meson_iff_to_disjD";
- val not_iffD = thm "meson_not_iffD";
- val conj_exD1 = thm "meson_conj_exD1";
- val conj_exD2 = thm "meson_conj_exD2";
- val disj_exD = thm "meson_disj_exD";
- val disj_exD1 = thm "meson_disj_exD1";
- val disj_exD2 = thm "meson_disj_exD2";
- val disj_assoc = thm "meson_disj_assoc";
- val disj_comm = thm "meson_disj_comm";
- val disj_FalseD1 = thm "meson_disj_FalseD1";
- val disj_FalseD2 = thm "meson_disj_FalseD2";
-
-
- fun literals (Const("Trueprop",_) $ P) = literals P
- | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
- | literals (Const("Not",_) $ P) = [(false,P)]
- | literals P = [(true,P)];
-
- (*number of literals in a term*)
- val nliterals = length o literals;
-
-exception Not_in_list;
-
-
-(* get a meta-clause for resolution with correct order of literals *)
-fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
- val contra = if lits = 1
- then
- th
- else
- rots (n,th)
- in
- if lits = 1
- then
-
- contra
- else
- rotate_prems (lits - n) contra
- end
-
-
-
-fun zip xs [] = []
-| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
-
-
-fun unzip [] = ([],[])
- | unzip((x,y)::pairs) =
- let val (xs,ys) = unzip pairs
- in (x::xs, y::ys) end;
-
-fun numlist 0 = []
-| numlist n = (numlist (n - 1))@[n]
-
-
-
-
-fun last(x::xs) = if xs=[] then x else last xs
-fun butlast []= []
-| butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
-
-
-fun minus a b = b - a;
-
-
-
-
-(* gives meta clause with kth disj as concl (starting at 1) *)
-(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules th)
- | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
-
-
-(* get a meta-clause for resolution with correct order of literals *)
-fun get_meta_cl (th,n) = let val lits = nliterals(prop_of th)
- val contra = if lits = 1
- then
- th
- else
- rots (n,th)
- in
- if lits = 1
- then
-
- contra
- else
- rotate_prems (lits - n) contra
- end
-*)
-
-
-
fun zip xs [] = []
| zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Tue Apr 12 11:08:25 2005 +0200
@@ -149,8 +149,8 @@
add_if_not_inlist ys xs (y::newlist)
else add_if_not_inlist ys xs (newlist)
-fun onestr [] str = str
-| onestr (x::xs) str = onestr xs (str^(concat x))
+(*Flattens a list of list of strings to one string*)
+fun onestr ls = String.concat (map String.concat ls);
fun thmstrings [] str = str
| thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
@@ -159,11 +159,6 @@
| onelist (x::xs) newlist = onelist xs (newlist@x)
-
-val prop_of = #prop o rep_thm;
-
-
-
fun get_axioms_used proof_steps thmstring = let
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))
val _ = TextIO.output (outfile, thmstring)
@@ -194,11 +189,11 @@
val metas_and_strs = zip metas meta_strs
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));
- val _ = TextIO.output (outfile, (onestr ax_strs ""))
+ val _ = TextIO.output (outfile, onestr ax_strs)
val _ = TextIO.closeOut outfile
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));
- val _ = TextIO.output (outfile, (onestr meta_strs ""))
+ val _ = TextIO.output (outfile, onestr meta_strs)
val _ = TextIO.closeOut outfile
(* get list of axioms as thms with their variables *)
--- a/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML Tue Apr 12 11:08:25 2005 +0200
@@ -109,8 +109,8 @@
(****************************************)
(* add claset rules to array and write out as strings *)
(****************************************)
- val claset_rules =claset_rules_of_thy Main.thy
- val claset = clausify_classical_rules_thy Main.thy
+ val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
+ val claset = ResAxioms.clausify_classical_rules_thy (the_context())
val (claset_clauses,badthms) = claset;
val clausifiable_rules = remove_all badthms claset_rules;
val named_claset = List.filter has_name clausifiable_rules;
@@ -124,7 +124,7 @@
val names_rules = zip good_names name_fol_cs;
- val new_clasrls = (fst(clausify_classical_rules name_fol_cs[]));
+ val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
@@ -161,13 +161,13 @@
(*********************)
(* Get simpset rules *)
(*********************)
- val (simpset_name_rules) =simpset_rules_of_thy Main.thy;
+ val (simpset_name_rules) =simpset_rules_of_thy (the_context());
val named_simps = List.filter has_name_pair simpset_name_rules;
val simp_names = map fst named_simps;
val simp_rules = map snd named_simps;
- val (simpset_cls,badthms) = clausify_simpset_rules simp_rules [];
+ val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
(* 1137 clausif simps *)
val clausifiable_simps = remove_all_simps badthms named_simps;
@@ -179,7 +179,7 @@
(* 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 = fst(clausify_simpset_rules simp_rules []);
+ val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
val stick_strs = map stick simpset_tptp_strs;
--- a/src/HOL/Tools/meson.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/meson.ML Tue Apr 12 11:08:25 2005 +0200
@@ -67,8 +67,6 @@
fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
| tryres (th, []) = raise THM("tryres", 0, [th]);
-val prop_of = #prop o rep_thm;
-
(*Permits forward proof from rules that discharge assumptions*)
fun forward_res nf st =
case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
--- a/src/HOL/Tools/recfun_codegen.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Apr 12 11:08:25 2005 +0200
@@ -29,7 +29,6 @@
structure CodegenData = TheoryDataFun(CodegenArgs);
-val prop_of = #prop o rep_thm;
val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
val lhs_of = fst o dest_eqn o prop_of;
val const_of = dest_Const o head_of o fst o dest_eqn;
--- a/src/HOL/Tools/res_atp.ML Tue Apr 12 11:07:42 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Apr 12 11:08:25 2005 +0200
@@ -309,7 +309,7 @@
val thmstring = string_of_thm thm
val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
(* set up variables for writing out the clasimps to a tptp file *)
- (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
+ val _ = write_out_clasimp (File.sysify_path axiom_file)
(* cq: add write out clasimps to file *)
(* cq:create watcher and pass to isar_atp_aux *)
val (childin,childout,pid) = Watcher.createWatcher()