tweaks mainly to achieve sml/nj compatibility
authorpaulson
Tue Apr 12 11:08:25 2005 +0200 (2005-04-12)
changeset 15700970e0293dfb3
parent 15699 7d91dd712ff8
child 15701 63f6614f95dc
tweaks mainly to achieve sml/nj compatibility
src/HOL/Reconstruction.thy
src/HOL/Tools/ATP/modUnix.ML
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Reconstruction.thy	Tue Apr 12 11:07:42 2005 +0200
     1.2 +++ b/src/HOL/Reconstruction.thy	Tue Apr 12 11:08:25 2005 +0200
     1.3 @@ -25,6 +25,7 @@
     1.4  	  "Tools/ATP/modUnix.ML"
     1.5  	  "Tools/ATP/watcher.sig"
     1.6  	  "Tools/ATP/watcher.ML"
     1.7 +	  "Tools/ATP/res_clasimpset.ML"
     1.8  	  "Tools/res_atp.ML"
     1.9  
    1.10            "Tools/reconstruction.ML"
     2.1 --- a/src/HOL/Tools/ATP/modUnix.ML	Tue Apr 12 11:07:42 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/modUnix.ML	Tue Apr 12 11:08:25 2005 +0200
     2.3 @@ -8,33 +8,7 @@
     2.4  
     2.5  val fromStatus = Posix.Process.fromStatus
     2.6  
     2.7 -
     2.8 -
     2.9 -(* Internal function - inverse of Posix.Process.fromStatus. *)
    2.10 -local
    2.11 -	val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific
    2.12 -	in
    2.13 -		fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0))
    2.14 -		 |  toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w))
    2.15 -		 |  toStatus(W_SIGNALED s) =
    2.16 -		 	doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s)))
    2.17 -		 |  toStatus(W_STOPPED s) = 
    2.18 -		 	doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s)))
    2.19 -	end
    2.20 -
    2.21 -(*	fun reap{pid, infd, outfd} =
    2.22 -	let
    2.23 -		val u = Posix.IO.close infd;
    2.24 -		val u = Posix.IO.close outfd;
    2.25 -		val (_, status) =
    2.26 -			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    2.27 -	in
    2.28 -		toStatus status
    2.29 -	end
    2.30 -
    2.31 -*)
    2.32 -
    2.33 -	fun reap(pid, instr, outstr) =
    2.34 +fun reap(pid, instr, outstr) =
    2.35  	let
    2.36  		val u = TextIO.closeIn instr;
    2.37  	        val u = TextIO.closeOut outstr;
    2.38 @@ -42,14 +16,14 @@
    2.39  		val (_, status) =
    2.40  			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    2.41  	in
    2.42 -		toStatus status
    2.43 +		status
    2.44  	end
    2.45  
    2.46  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    2.47 -	  Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
    2.48 +	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    2.49  
    2.50  fun fdWriter (name, fd) =
    2.51 -          Posix.IO.mkWriter {
    2.52 +          Posix.IO.mkTextWriter {
    2.53  	      appendMode = false,
    2.54                initBlkMode = true,
    2.55                name = name,  
    2.56 @@ -292,4 +266,4 @@
    2.57                instr = instr,
    2.58                outstr = outstr
    2.59              })::procList))
    2.60 -          end;
    2.61 \ No newline at end of file
    2.62 +          end;
     3.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 11:07:42 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue Apr 12 11:08:25 2005 +0200
     3.3 @@ -16,139 +16,8 @@
     3.4  fun get_nth n (x::xs) = hd (drop (n-1) (x::xs))
     3.5  
     3.6  
     3.7 - fun literals (Const("Trueprop",_) $ P) = literals P
     3.8 -   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
     3.9 -   | literals (Const("Not",_) $ P) = [(false,P)]
    3.10 -   | literals P = [(true,P)];
    3.11 -
    3.12 - (*number of literals in a term*)
    3.13 - val nliterals = length o literals; 
    3.14 -     
    3.15  exception Not_in_list;  
    3.16  
    3.17 -             
    3.18 -(*
    3.19 -(* gives horn clause with kth disj as concl (starting at 1) *)
    3.20 -fun rots (0,th) =  (Meson.make_horn Meson.crules th)
    3.21 -         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))
    3.22 -
    3.23 -
    3.24 -                
    3.25 -Goal " (~~P) == P";
    3.26 -by Auto_tac;
    3.27 -qed "notnotEq";
    3.28 -
    3.29 -Goal "A | A ==> A";
    3.30 -by Auto_tac;
    3.31 -qed "rem_dup_disj";
    3.32 -
    3.33 -
    3.34 -
    3.35 -
    3.36 -(* New Meson code  Versions of make_neg_rule and make_pos_rule that don't insert new *)
    3.37 -(* assumptions, for ordinary resolution. *)
    3.38 -
    3.39 -
    3.40 -
    3.41 -
    3.42 - val not_conjD = thm "meson_not_conjD";
    3.43 - val not_disjD = thm "meson_not_disjD";
    3.44 - val not_notD = thm "meson_not_notD";
    3.45 - val not_allD = thm "meson_not_allD";
    3.46 - val not_exD = thm "meson_not_exD";
    3.47 - val imp_to_disjD = thm "meson_imp_to_disjD";
    3.48 - val not_impD = thm "meson_not_impD";
    3.49 - val iff_to_disjD = thm "meson_iff_to_disjD";
    3.50 - val not_iffD = thm "meson_not_iffD";
    3.51 - val conj_exD1 = thm "meson_conj_exD1";
    3.52 - val conj_exD2 = thm "meson_conj_exD2";
    3.53 - val disj_exD = thm "meson_disj_exD";
    3.54 - val disj_exD1 = thm "meson_disj_exD1";
    3.55 - val disj_exD2 = thm "meson_disj_exD2";
    3.56 - val disj_assoc = thm "meson_disj_assoc";
    3.57 - val disj_comm = thm "meson_disj_comm";
    3.58 - val disj_FalseD1 = thm "meson_disj_FalseD1";
    3.59 - val disj_FalseD2 = thm "meson_disj_FalseD2";
    3.60 -
    3.61 -
    3.62 - fun literals (Const("Trueprop",_) $ P) = literals P
    3.63 -   | literals (Const("op |",_) $ P $ Q) = literals P @ literals Q
    3.64 -   | literals (Const("Not",_) $ P) = [(false,P)]
    3.65 -   | literals P = [(true,P)];
    3.66 -
    3.67 - (*number of literals in a term*)
    3.68 - val nliterals = length o literals; 
    3.69 -     
    3.70 -exception Not_in_list;  
    3.71 -
    3.72 -
    3.73 -(* get a meta-clause for resolution with correct order of literals *)
    3.74 -fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
    3.75 -                              val contra =  if lits = 1 
    3.76 -                                                 then
    3.77 -                                                     th
    3.78 -                                                 else
    3.79 -                                                     rots (n,th)   
    3.80 -                          in 
    3.81 -                               if lits = 1 
    3.82 -                               then
    3.83 -                                            
    3.84 -                                  contra
    3.85 -                               else
    3.86 -                                  rotate_prems (lits - n) contra
    3.87 -                          end
    3.88 -
    3.89 -
    3.90 -
    3.91 -fun zip xs [] = []
    3.92 -|   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
    3.93 -
    3.94 -
    3.95 -fun unzip [] = ([],[])
    3.96 -    | unzip((x,y)::pairs) =
    3.97 -	  let val (xs,ys) = unzip pairs
    3.98 -	  in  (x::xs, y::ys)  end;
    3.99 -
   3.100 -fun numlist 0 = []
   3.101 -|   numlist n = (numlist (n - 1))@[n]
   3.102 -
   3.103 -
   3.104 -
   3.105 -
   3.106 -fun last(x::xs) = if xs=[] then x else last xs
   3.107 -fun butlast []= []
   3.108 -|   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
   3.109 -
   3.110 -
   3.111 -fun minus a b = b - a;
   3.112 -
   3.113 -
   3.114 -
   3.115 -
   3.116 -(* gives meta clause with kth disj as concl (starting at 1) *)
   3.117 -(*fun rots (0,th) = negate_nead (make_horn resolution_clause_rules  th)
   3.118 -         | rots (k,th) = rots(k-1, assoc_right (th RS disj_comm))*)
   3.119 -
   3.120 -
   3.121 -(* get a meta-clause for resolution with correct order of literals *)
   3.122 -fun get_meta_cl  (th,n) = let val lits = nliterals(prop_of th)
   3.123 -                                   val contra =  if lits = 1 
   3.124 -                                                 then
   3.125 -                                                     th
   3.126 -                                                 else
   3.127 -                                                     rots (n,th)   
   3.128 -                                in 
   3.129 -                                   if lits = 1 
   3.130 -                                   then
   3.131 -                                            
   3.132 -                                     contra
   3.133 -                                   else
   3.134 -                                     rotate_prems (lits - n) contra
   3.135 -                               end
   3.136 -*)
   3.137 -
   3.138 -
   3.139 -
   3.140  
   3.141  fun zip xs [] = []
   3.142  |   zip xs (y::ys) = (case xs of [] => [] | (z::zs) => ((z,y)::zip zs ys))
     4.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 12 11:07:42 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Apr 12 11:08:25 2005 +0200
     4.3 @@ -149,8 +149,8 @@
     4.4                                        add_if_not_inlist ys xs (y::newlist)
     4.5                                          else add_if_not_inlist ys xs (newlist)
     4.6  
     4.7 -fun onestr [] str = str
     4.8 -|   onestr (x::xs) str = onestr xs (str^(concat x))
     4.9 +(*Flattens a list of list of strings to one string*)
    4.10 +fun onestr ls = String.concat (map String.concat ls);
    4.11  
    4.12  fun thmstrings [] str = str
    4.13  |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
    4.14 @@ -159,11 +159,6 @@
    4.15  |   onelist (x::xs) newlist = onelist xs (newlist@x)
    4.16  
    4.17  
    4.18 -
    4.19 -val prop_of = #prop o rep_thm;
    4.20 -
    4.21 -
    4.22 -
    4.23   fun get_axioms_used proof_steps thmstring = let 
    4.24                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    4.25                                               val _ = TextIO.output (outfile, thmstring)
    4.26 @@ -194,11 +189,11 @@
    4.27                                             
    4.28                                              val metas_and_strs = zip  metas meta_strs
    4.29                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
    4.30 -                                             val _ = TextIO.output (outfile, (onestr ax_strs ""))
    4.31 +                                             val _ = TextIO.output (outfile, onestr ax_strs)
    4.32                                               
    4.33                                               val _ =  TextIO.closeOut outfile
    4.34                                               val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
    4.35 -                                             val _ = TextIO.output (outfile, (onestr meta_strs ""))
    4.36 +                                             val _ = TextIO.output (outfile, onestr meta_strs)
    4.37                                               val _ =  TextIO.closeOut outfile
    4.38  
    4.39                                              (* get list of axioms as thms with their variables *)
     5.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 12 11:07:42 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue Apr 12 11:08:25 2005 +0200
     5.3 @@ -109,8 +109,8 @@
     5.4                                     (****************************************)
     5.5                                     (* add claset rules to array and write out as strings *)
     5.6                                     (****************************************)
     5.7 -                                   val claset_rules =claset_rules_of_thy Main.thy
     5.8 -                                   val claset = clausify_classical_rules_thy Main.thy
     5.9 +                                   val claset_rules = ResAxioms.claset_rules_of_thy (the_context())
    5.10 +                                   val claset = ResAxioms.clausify_classical_rules_thy (the_context())
    5.11                                     val (claset_clauses,badthms) =  claset;
    5.12                                     val clausifiable_rules = remove_all badthms claset_rules;
    5.13                                     val named_claset = List.filter has_name clausifiable_rules;
    5.14 @@ -124,7 +124,7 @@
    5.15  
    5.16                                     val names_rules = zip good_names name_fol_cs;
    5.17                                     
    5.18 -                                   val new_clasrls = (fst(clausify_classical_rules name_fol_cs[]));
    5.19 +                                   val new_clasrls = (fst(ResAxioms.clausify_classical_rules name_fol_cs[]));
    5.20  
    5.21                                     val claset_tptp_strs = map ( map ResClause.tptp_clause) new_clasrls;
    5.22  
    5.23 @@ -161,13 +161,13 @@
    5.24                                    (*********************)
    5.25                                    (* Get simpset rules *)
    5.26                                    (*********************)
    5.27 -                                  val (simpset_name_rules) =simpset_rules_of_thy Main.thy;
    5.28 +                                  val (simpset_name_rules) =simpset_rules_of_thy (the_context());
    5.29                                    val named_simps = List.filter has_name_pair simpset_name_rules;
    5.30  
    5.31                                    val simp_names = map fst named_simps;
    5.32                                    val simp_rules = map snd named_simps;
    5.33                                
    5.34 -                                  val (simpset_cls,badthms) = clausify_simpset_rules simp_rules [];
    5.35 +                                  val (simpset_cls,badthms) = ResAxioms.clausify_simpset_rules simp_rules [];
    5.36                                   (* 1137 clausif simps *)
    5.37                                    val clausifiable_simps = remove_all_simps badthms named_simps;
    5.38                                     
    5.39 @@ -179,7 +179,7 @@
    5.40                                      (* need to get names of claset_cluases so we can make sure we've*)
    5.41                                      (* got the same ones (ie. the named ones ) as the claset rules *)
    5.42                                      (* length 1374*)
    5.43 -                                    val new_simps = fst(clausify_simpset_rules simp_rules []);
    5.44 +                                    val new_simps = fst(ResAxioms.clausify_simpset_rules simp_rules []);
    5.45                                      val simpset_tptp_strs = map (map ResClause.tptp_clause) new_simps;
    5.46  
    5.47                                      val stick_strs = map stick simpset_tptp_strs;
     6.1 --- a/src/HOL/Tools/meson.ML	Tue Apr 12 11:07:42 2005 +0200
     6.2 +++ b/src/HOL/Tools/meson.ML	Tue Apr 12 11:08:25 2005 +0200
     6.3 @@ -67,8 +67,6 @@
     6.4  fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls))
     6.5    | tryres (th, []) = raise THM("tryres", 0, [th]);
     6.6  
     6.7 -val prop_of = #prop o rep_thm;
     6.8 -
     6.9  (*Permits forward proof from rules that discharge assumptions*)
    6.10  fun forward_res nf st =
    6.11    case Seq.pull (ALLGOALS (METAHYPS (fn [prem] => rtac (nf prem) 1)) st)
     7.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Apr 12 11:07:42 2005 +0200
     7.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Apr 12 11:08:25 2005 +0200
     7.3 @@ -29,7 +29,6 @@
     7.4  
     7.5  structure CodegenData = TheoryDataFun(CodegenArgs);
     7.6  
     7.7 -val prop_of = #prop o rep_thm;
     7.8  val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop;
     7.9  val lhs_of = fst o dest_eqn o prop_of;
    7.10  val const_of = dest_Const o head_of o fst o dest_eqn;
     8.1 --- a/src/HOL/Tools/res_atp.ML	Tue Apr 12 11:07:42 2005 +0200
     8.2 +++ b/src/HOL/Tools/res_atp.ML	Tue Apr 12 11:08:25 2005 +0200
     8.3 @@ -309,7 +309,7 @@
     8.4          val thmstring = string_of_thm thm
     8.5          val prems_string = concat_with_and (map (Sign.string_of_term sign) prems) ""
     8.6          (* set up variables for writing out the clasimps to a tptp file *)
     8.7 -        (* val _ = write_out_clasimp (File.sysify_path axiom_file)*)
     8.8 +        val _ = write_out_clasimp (File.sysify_path axiom_file)
     8.9          (* cq: add write out clasimps to file *)
    8.10          (* cq:create watcher and pass to isar_atp_aux *)                    
    8.11          val (childin,childout,pid) = Watcher.createWatcher()