# HG changeset patch # User paulson # Date 1113296905 -7200 # Node ID 970e0293dfb3068325e4f690fac3d082b5310b70 # Parent 7d91dd712ff8b4c0744435e5baa4e3b6207e473b tweaks mainly to achieve sml/nj compatibility diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Reconstruction.thy --- 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" diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/ATP/modUnix.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; diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/ATP/recon_order_clauses.ML --- 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)) diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/ATP/recon_transfer_proof.ML --- 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 *) diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/ATP/res_clasimpset.ML --- 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; diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/meson.ML --- 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) diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/recfun_codegen.ML --- 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; diff -r 7d91dd712ff8 -r 970e0293dfb3 src/HOL/Tools/res_atp.ML --- 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()