minor code tidyig
authorpaulson
Fri Oct 07 17:57:21 2005 +0200 (2005-10-07 ago)
changeset 177752679ba74411f
parent 17774 0ecfb66ea072
child 17776 4a518eec4a20
minor code tidyig
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_clause.ML
src/HOL/Tools/res_lib.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Oct 07 15:08:28 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Oct 07 17:57:21 2005 +0200
     1.3 @@ -156,27 +156,9 @@
     1.4  	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
     1.5      end
     1.6  
     1.7 -
     1.8 -(*****************************************************)
     1.9 -(* get names of clasimp axioms used                  *)
    1.10 -(*****************************************************)
    1.11 -
    1.12 +(* get names of clasimp axioms used*)
    1.13   fun get_axiom_names step_nums clause_arr =
    1.14 -   let 
    1.15 -     (* not sure why this is necessary again, but seems to be *)
    1.16 -      val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.17 -  
    1.18 -     (***********************************************)
    1.19 -     (* here need to add the clauses from clause_arr*)
    1.20 -     (***********************************************)
    1.21 -  
    1.22 -      val clasimp_names_cls = get_clasimp_cls clause_arr step_nums 
    1.23 -      val clasimp_names = map (ResClause.get_axiomName o #1) clasimp_names_cls
    1.24 -      val _ = (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    1.25 -   in
    1.26 -      clasimp_names
    1.27 -   end
    1.28 -   
    1.29 +   map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums);   
    1.30  
    1.31  fun get_axiom_names_spass proofstr clause_arr =
    1.32    let (* parse spass proof into datatype *)
    1.33 @@ -227,9 +209,7 @@
    1.34  fun addvars c (a,b)  = (a,b,c)
    1.35  
    1.36  fun get_axioms_used proof_steps thms clause_arr  =
    1.37 -  let 
    1.38 -     val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.39 -     val axioms = (List.filter is_axiom) proof_steps
    1.40 + let val axioms = (List.filter is_axiom) proof_steps
    1.41       val step_nums = get_step_nums axioms []
    1.42  
    1.43       val clauses = make_clauses thms    (*FIXME: must this be repeated??*)
    1.44 @@ -266,9 +246,9 @@
    1.45       val extra_with_vars = if (not (extra_metas = []) ) 
    1.46  			   then ListPair.zip (extra_metas,extra_vars)
    1.47  			   else []
    1.48 -  in
    1.49 -     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
    1.50 -  end;
    1.51 + in
    1.52 +    (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
    1.53 + end;
    1.54                                              
    1.55  
    1.56  (*********************************************************************)
    1.57 @@ -277,7 +257,7 @@
    1.58  (*********************************************************************)
    1.59  
    1.60  fun rules_to_string [] = "NONE"
    1.61 -  | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
    1.62 +  | rules_to_string xs = space_implode "  " xs
    1.63  
    1.64  
    1.65  (*The signal handler in watcher.ML must be able to read the output of this.*)
     2.1 --- a/src/HOL/Tools/res_atp.ML	Fri Oct 07 15:08:28 2005 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Oct 07 17:57:21 2005 +0200
     2.3 @@ -55,18 +55,18 @@
     2.4  
     2.5  (* write out a subgoal as tptp clauses to the file "xxxx_N"*)
     2.6  fun tptp_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) =
     2.7 -    let
     2.8 -      val clss = map (ResClause.make_conjecture_clause_thm) thms
     2.9 -      val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    2.10 -      val tfree_clss = map ResClause.tfree_clause (ResLib.flat_noDup tfree_litss)
    2.11 -      val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    2.12 -      val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    2.13 -      val out = TextIO.openOut(pf n)
    2.14 -    in
    2.15 -      writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    2.16 -      writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    2.17 -      TextIO.closeOut out
    2.18 -    end;
    2.19 +  let
    2.20 +    val clss = map (ResClause.make_conjecture_clause_thm) thms
    2.21 +    val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    2.22 +    val tfree_clss = map ResClause.tfree_clause (foldl (op union_string) [] tfree_litss)
    2.23 +    val classrel_cls = map ResClause.tptp_classrelClause classrel_clauses
    2.24 +    val arity_cls = map ResClause.tptp_arity_clause arity_clauses
    2.25 +    val out = TextIO.openOut(pf n)
    2.26 +  in
    2.27 +    writeln_strs out (List.concat (map ResClause.tptp_clause axclauses));
    2.28 +    writeln_strs out (tfree_clss @ tptp_clss @ classrel_cls @ arity_cls);
    2.29 +    TextIO.closeOut out
    2.30 +  end;
    2.31  
    2.32  (* write out a subgoal in DFG format to the file "xxxx_N"*)
    2.33  fun dfg_inputs_tfrees thms pf n (axclauses,classrel_clauses,arity_clauses) = 
    2.34 @@ -165,9 +165,17 @@
    2.35  	    pf n :: writenext (n-1))
    2.36        in (writenext (length prems), clause_arr) end;
    2.37  
    2.38 -val last_watcher_pid =
    2.39 -  ref (NONE : (TextIO.instream * TextIO.outstream * 
    2.40 -               Posix.Process.pid * string list) option);
    2.41 +val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    2.42 +                                    Posix.Process.pid * string list) option);
    2.43 +
    2.44 +fun kill_last_watcher () =
    2.45 +    (case !last_watcher_pid of 
    2.46 +         NONE => ()
    2.47 +       | SOME (_, childout, pid, files) => 
    2.48 +	  (debug ("Killing old watcher, pid = " ^ Int.toString (ResLib.intOfPid pid));
    2.49 +	   Watcher.killWatcher pid;  
    2.50 +	   ignore (map (try OS.FileSys.remove) files)))
    2.51 +     handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    2.52  
    2.53  (*writes out the current clasimpset to a tptp file;
    2.54    turns off xsymbol at start of function, restoring it at end    *)
    2.55 @@ -176,13 +184,7 @@
    2.56    if Thm.no_prems th then ()
    2.57    else
    2.58      let
    2.59 -      val _ = (case !last_watcher_pid of NONE => ()
    2.60 -               | SOME (_, childout, pid, files) => 
    2.61 -                  (debug ("Killing old watcher, pid = " ^ 
    2.62 -                          Int.toString (ResLib.intOfPid pid));
    2.63 -                   Watcher.killWatcher pid;  
    2.64 -                   ignore (map (try OS.FileSys.remove) files)))
    2.65 -              handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    2.66 +      val _ = kill_last_watcher()
    2.67        val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
    2.68        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    2.69      in
     3.1 --- a/src/HOL/Tools/res_clause.ML	Fri Oct 07 15:08:28 2005 +0200
     3.2 +++ b/src/HOL/Tools/res_clause.ML	Fri Oct 07 17:57:21 2005 +0200
     3.3 @@ -77,8 +77,10 @@
     3.4  val class_prefix = "class_"; 
     3.5  
     3.6  
     3.7 -(**** some useful functions ****)
     3.8 +fun union_all xss = foldl (op union) [] xss;
     3.9 +
    3.10   
    3.11 +(*Provide readable names for the more common symbolic functions*)
    3.12  val const_trans_table =
    3.13        Symtab.make [("op =", "equal"),
    3.14  	  	   ("op <=", "lessequals"),
    3.15 @@ -287,8 +289,8 @@
    3.16        let val foltyps_ts = map type_of Ts 
    3.17  	  val (folTyps,ts_funcs) = ListPair.unzip foltyps_ts
    3.18  	  val (ts, funcslist) = ListPair.unzip ts_funcs
    3.19 -	  val ts' = ResLib.flat_noDup ts
    3.20 -	  val funcs' = ResLib.flat_noDup funcslist
    3.21 +	  val ts' = union_all ts
    3.22 +	  val funcs' = union_all funcslist
    3.23  	  val t = make_fixed_type_const a
    3.24        in    
    3.25  	  ((t ^ paren_pack folTyps), (ts', (t, length Ts)::funcs'))
    3.26 @@ -366,8 +368,8 @@
    3.27  	      let val (funName,(funType,ts1),funcs) = fun_name_type f args
    3.28  		  val (args',ts_funcs) = ListPair.unzip (map term_of args)
    3.29  		  val (ts2,funcs') = ListPair.unzip ts_funcs
    3.30 -		  val ts3 = ResLib.flat_noDup (ts1::ts2)
    3.31 -		  val funcs'' = ResLib.flat_noDup((funcs::funcs'))
    3.32 +		  val ts3 = union_all (ts1::ts2)
    3.33 +		  val funcs'' = union_all(funcs::funcs')
    3.34  	      in
    3.35  		  (Fun(funName,funType,args'), (ts3,funcs''))
    3.36  	      end
    3.37 @@ -378,8 +380,8 @@
    3.38  		  val equal_name = make_fixed_const ("op =")
    3.39  	      in
    3.40  		  (Fun(equal_name,arg_typ,args'),
    3.41 -		   (ResLib.flat_noDup ts, 
    3.42 -		    (make_fixed_var equal_name, 2):: ResLib.flat_noDup funcs))
    3.43 +		   (union_all ts, 
    3.44 +		    (make_fixed_var equal_name, 2):: union_all funcs))
    3.45  	      end
    3.46        in
    3.47  	 case f of Const ("op =", typ) => term_of_eq (f,args)
    3.48 @@ -400,16 +402,16 @@
    3.49  	  val equal_name = make_fixed_const "op ="
    3.50        in
    3.51  	  (Predicate(equal_name,arg_typ,args'),
    3.52 -	   ResLib.flat_noDup ts, 
    3.53 +	   union_all ts, 
    3.54  	   [((make_fixed_var equal_name), 2)], 
    3.55 -	   (ResLib.flat_noDup funcs))
    3.56 +	   union_all funcs)
    3.57        end
    3.58    | pred_of (pred,args) = 
    3.59        let val (predName,(predType,ts1), pfuncs) = pred_name_type pred
    3.60  	  val (args',ts_funcs) = ListPair.unzip (map term_of args)
    3.61  	  val (ts2,ffuncs) = ListPair.unzip ts_funcs
    3.62 -	  val ts3 = ResLib.flat_noDup (ts1::ts2)
    3.63 -	  val ffuncs' = (ResLib.flat_noDup ffuncs)
    3.64 +	  val ts3 = union_all (ts1::ts2)
    3.65 +	  val ffuncs' = union_all ffuncs
    3.66  	  val newfuncs = distinct (pfuncs@ffuncs')
    3.67  	  val arity = 
    3.68  	    case pred of
    3.69 @@ -445,9 +447,8 @@
    3.70        let val ((pred,ts', preds', funcs'), pol, tag) = 
    3.71                predicate_of (P,true,false)
    3.72  	  val lits' = Literal(pol,pred,tag) :: lits
    3.73 -	  val ts'' = ResLib.no_rep_app ts ts' 
    3.74        in
    3.75 -	  (lits',ts'', distinct(preds'@preds), distinct(funcs'@funcs))
    3.76 +	  (lits', ts union ts', distinct(preds'@preds), distinct(funcs'@funcs))
    3.77        end;
    3.78  
    3.79  
    3.80 @@ -487,14 +488,14 @@
    3.81            val preds' = (map pred_of_sort vs)@preds
    3.82  	  val (vss,fss, preds'') = add_typs_aux tss preds'
    3.83        in
    3.84 -	  (ResLib.no_rep_app vs vss, fss, preds'')
    3.85 +	  (vs union vss, fss, preds'')
    3.86        end
    3.87    | add_typs_aux ((FOLTFree x,s)::tss) preds  =
    3.88        let val fs = sorts_on_typs (FOLTFree x, s)
    3.89            val preds' = (map pred_of_sort fs)@preds
    3.90  	  val (vss,fss, preds'') = add_typs_aux tss preds'
    3.91        in
    3.92 -	  (vss, ResLib.no_rep_app fs fss,preds'')
    3.93 +	  (vss, fs union fss, preds'')
    3.94        end;
    3.95  
    3.96  fun add_typs (Clause cls) preds  = add_typs_aux (#types_sorts cls) preds 
    3.97 @@ -614,7 +615,7 @@
    3.98  	 val tvars = get_TVars nargs
    3.99  	 val conclLit = make_TConsLit(true,(res,tcons,tvars))
   3.100           val tvars_srts = ListPair.zip (tvars,args)
   3.101 -	 val tvars_srts' = ResLib.flat_noDup(map pack_sort tvars_srts)
   3.102 +	 val tvars_srts' = union_all(map pack_sort tvars_srts)
   3.103           val false_tvars_srts' = map (pair false) tvars_srts'
   3.104  	 val premLits = map make_TVarLit false_tvars_srts'
   3.105       in
   3.106 @@ -761,7 +762,7 @@
   3.107  
   3.108   
   3.109  fun get_uvars (UVar(a,typ)) = [a] 
   3.110 -|   get_uvars (Fun (_,typ,tlist)) = ResLib.flat_noDup(map get_uvars tlist)
   3.111 +|   get_uvars (Fun (_,typ,tlist)) = union_all(map get_uvars tlist)
   3.112  
   3.113  
   3.114  fun is_uvar (UVar _) = true
   3.115 @@ -777,7 +778,7 @@
   3.116      let val lits = #literals cls
   3.117          val folterms = mergelist(map dfg_folterms lits)
   3.118      in 
   3.119 -        ResLib.flat_noDup(map get_uvars folterms)
   3.120 +        union_all(map get_uvars folterms)
   3.121      end
   3.122  
   3.123  
   3.124 @@ -888,7 +889,7 @@
   3.125          val axstr = (space_implode "\n" axstrs) ^ "\n\n"
   3.126          val conjstrs_tfrees = (map clause2dfg conjectures)
   3.127  	val (conjstrs, atfrees) = ListPair.unzip conjstrs_tfrees
   3.128 -        val tfree_clss = map tfree_dfg_clause (ResLib.flat_noDup atfrees) 
   3.129 +        val tfree_clss = map tfree_dfg_clause (union_all atfrees) 
   3.130          val conjstr = (space_implode "\n" (tfree_clss@conjstrs)) ^ "\n\n"
   3.131          val funcstr = string_of_funcs funcs
   3.132          val predstr = string_of_preds preds
   3.133 @@ -900,8 +901,8 @@
   3.134      end;
   3.135     
   3.136  fun clauses2dfg [] probname axioms conjectures funcs preds = 
   3.137 -      let val funcs' = (ResLib.flat_noDup(map funcs_of_cls axioms)) @ funcs
   3.138 -	  val preds' = (ResLib.flat_noDup(map preds_of_cls axioms)) @ preds
   3.139 +      let val funcs' = (union_all(map funcs_of_cls axioms)) @ funcs
   3.140 +	  val preds' = (union_all(map preds_of_cls axioms)) @ preds
   3.141        in
   3.142  	 gen_dfg_file probname axioms conjectures funcs' preds' 
   3.143        end
     4.1 --- a/src/HOL/Tools/res_lib.ML	Fri Oct 07 15:08:28 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_lib.ML	Fri Oct 07 17:57:21 2005 +0200
     4.3 @@ -8,10 +8,7 @@
     4.4  
     4.5  signature RES_LIB =
     4.6  sig
     4.7 -val flat_noDup : ''a list list -> ''a list
     4.8  val helper_path : string -> string -> string
     4.9 -val no_rep_add : ''a -> ''a list -> ''a list
    4.10 -val no_rep_app : ''a list -> ''a list -> ''a list
    4.11  val intOfPid : Posix.Process.pid -> Int.int
    4.12  val pidOfInt : Int.int -> Posix.Process.pid
    4.13  end;
    4.14 @@ -20,16 +17,6 @@
    4.15  structure ResLib : RES_LIB =
    4.16  struct
    4.17  
    4.18 -fun no_rep_add x []     = [x]
    4.19 -  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
    4.20 -
    4.21 -fun no_rep_app l1 []     = l1
    4.22 -  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
    4.23 -
    4.24 -fun flat_noDup []     = []
    4.25 -  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    4.26 -
    4.27 - 
    4.28  (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    4.29    it exists. --lcp *)  
    4.30  fun helper_path evar base =