Eta-expanded some declarations that are illegal under value polymorphism
authorpaulson
Wed Nov 27 10:52:31 1996 +0100 (1996-11-27)
changeset 22433ebeaaacfbd1
parent 2242 fa8c6c695a97
child 2244 dacee519738a
Eta-expanded some declarations that are illegal under value polymorphism

Converted I/O operatios for Basis Library compatibility
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Nov 27 10:45:58 1996 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Nov 27 10:52:31 1996 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  
     1.5  Basic library: functions, options, pairs, booleans, lists, integers,
     1.6  strings, lists as sets, association lists, generic tables, balanced trees,
     1.7 -input / output, timing, filenames, misc functions.
     1.8 +input / TextIO.output, timing, filenames, misc functions.
     1.9  *)
    1.10  
    1.11  infix |> ~~ \ \\ orelf ins ins_string ins_int orf andf prefix upto downto
    1.12 @@ -506,12 +506,12 @@
    1.13  fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)
    1.14    | [] \ x = [];
    1.15  
    1.16 -val op \\ = foldl (op \);
    1.17 +fun ys \\ xs = foldl (op \) (ys,xs);
    1.18  
    1.19  (*removing an element from a list -- possibly WITH duplicates*)
    1.20  fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
    1.21  
    1.22 -val gen_rems = foldl o gen_rem;
    1.23 +fun gen_rems eq = foldl (gen_rem eq);
    1.24  
    1.25  
    1.26  (*makes a list of the distinct members of the input; preserves order, takes
    1.27 @@ -528,7 +528,7 @@
    1.28      dist ([], lst)
    1.29    end;
    1.30  
    1.31 -val distinct = gen_distinct (op =);
    1.32 +fun distinct l = gen_distinct (op =) l;
    1.33  
    1.34  
    1.35  (*returns the tail beginning with the first repeated element, or []*)
    1.36 @@ -551,7 +551,7 @@
    1.37      dups ([], lst)
    1.38    end;
    1.39  
    1.40 -val duplicates = gen_duplicates (op =);
    1.41 +fun duplicates l = gen_duplicates (op =) l;
    1.42  
    1.43  
    1.44  
    1.45 @@ -633,8 +633,8 @@
    1.46  
    1.47  
    1.48  (*lists as tables*)
    1.49 -val extend_list = generic_extend (op =) I I;
    1.50 -val merge_lists = generic_merge (op =) I I;
    1.51 +fun extend_list tab = generic_extend (op =) I I tab;
    1.52 +fun merge_lists tab = generic_merge (op =) I I tab;
    1.53  
    1.54  fun merge_rev_lists xs [] = xs
    1.55    | merge_rev_lists [] ys = ys
    1.56 @@ -680,23 +680,25 @@
    1.57  
    1.58  (** input / output **)
    1.59  
    1.60 -val prs_fn = ref(fn s => output (std_out, s));
    1.61 +val cd = OS.FileSys.chDir;
    1.62 +
    1.63 +val prs_fn = ref(fn s => TextIO.output (TextIO.stdOut, s));
    1.64  
    1.65  fun prs s = !prs_fn s;
    1.66  fun writeln s = prs (s ^ "\n");
    1.67  
    1.68 -(* output to LaTeX / xdvi *)
    1.69 +(* TextIO.output to LaTeX / xdvi *)
    1.70  fun latex s = 
    1.71 -	execute ( "( cd /tmp ; echo \"" ^ s ^
    1.72 -	"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
    1.73 +        execute ( "( cd /tmp ; echo \"" ^ s ^
    1.74 +        "\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &" ) ;
    1.75  
    1.76  (*print warning*)
    1.77 -val warning_fn = ref(fn s => output (std_out, s ^ "\n"));
    1.78 +val warning_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
    1.79  fun warning s = !warning_fn ("Warning: " ^ s);
    1.80  
    1.81  (*print error message and abort to top level*)
    1.82  
    1.83 -val error_fn = ref(fn s => output (std_out, s ^ "\n"));
    1.84 +val error_fn = ref(fn s => TextIO.output (TextIO.stdOut, s ^ "\n"));
    1.85  
    1.86  exception ERROR;
    1.87  fun error msg = (!error_fn msg; raise ERROR);
    1.88 @@ -708,16 +710,16 @@
    1.89  (*Assert pred for every member of l, generating a message if pred fails*)
    1.90  fun assert_all pred l msg_fn = 
    1.91    let fun asl [] = ()
    1.92 -	| asl (x::xs) = if pred x then asl xs
    1.93 -	                else error (msg_fn x)
    1.94 +        | asl (x::xs) = if pred x then asl xs
    1.95 +                        else error (msg_fn x)
    1.96    in  asl l  end;
    1.97  
    1.98  (*for the "test" target in Makefiles -- signifies successful termination*)
    1.99  fun maketest msg =
   1.100    (writeln msg; 
   1.101 -   let val os = open_out "test" 
   1.102 -   in  output (os, "Test examples ran successfully\n");
   1.103 -       close_out os
   1.104 +   let val os = TextIO.openOut "test" 
   1.105 +   in  TextIO.output (os, "Test examples ran successfully\n");
   1.106 +       TextIO.closeOut os
   1.107     end);
   1.108  
   1.109  
   1.110 @@ -743,7 +745,7 @@
   1.111  (** timing **)
   1.112  
   1.113  (*unconditional timing function*)
   1.114 -val timeit = cond_timeit true;
   1.115 +fun timeit x = cond_timeit true x;
   1.116  
   1.117  (*timed application function*)
   1.118  fun timeap f x = timeit (fn () => f x);
   1.119 @@ -879,7 +881,7 @@
   1.120        let val qs = transitive_closure ps
   1.121            val zs = foldl (fn (zs, y) => assocs qs y union_string zs) (ys, ys)
   1.122            fun step(u, us) = (u, if x mem_string us then zs union_string us 
   1.123 -				else us)
   1.124 +                                else us)
   1.125        in (x, zs) :: map step qs end;
   1.126  
   1.127  
   1.128 @@ -917,7 +919,7 @@
   1.129      [division by two avoids overflow for ML systems whose maxint is 2^30 - 1 *)
   1.130  fun gensym pre = pre ^ 
   1.131                   (#1(newid (floor (!seedr/2.0)), 
   1.132 -		     seedr := nextrandom (!seedr)))
   1.133 +                     seedr := nextrandom (!seedr)))
   1.134  
   1.135  (*Increment a list of letters like a reversed base 26 number.
   1.136    If head is "z", bumps chars in tail.