author | paulson |
Fri, 01 Nov 1996 15:15:39 +0100 | |
changeset 2143 | 093bbe6d333b |
parent 2141 | c2aedd8169cd |
child 2242 | fa8c6c695a97 |
permissions | -rw-r--r-- |
0 | 1 |
(* Title: Pure/POLY |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1991 University of Cambridge |
|
5 |
||
6 |
Compatibility file for Poly/ML (AHL release 1.88) |
|
7 |
*) |
|
8 |
||
9 |
open PolyML ExtendedIO; |
|
10 |
||
11 |
||
2141 | 12 |
structure Int = |
13 |
struct |
|
14 |
fun max (x, y) = if x < y then y else x : int; |
|
15 |
fun min (x, y) = if x < y then x else y : int; |
|
16 |
end; |
|
17 |
||
18 |
||
0 | 19 |
(*A conditional timing function: applies f to () and, if the flag is true, |
20 |
prints its runtime.*) |
|
21 |
||
22 |
fun cond_timeit flag f = |
|
23 |
if flag then |
|
24 |
let val before = System.processtime() |
|
25 |
val result = f() |
|
26 |
val both = real(System.processtime() - before) / 10.0 |
|
27 |
in output(std_out, "Process time (incl GC): "^ |
|
28 |
makestring both ^ " secs\n"); |
|
29 |
result |
|
30 |
end |
|
31 |
else f(); |
|
32 |
||
33 |
||
34 |
(*Save function: in Poly/ML, ignores filename and commits to present file*) |
|
35 |
||
36 |
fun xML filename banner = commit(); |
|
37 |
||
38 |
||
39 |
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*) |
|
40 |
||
41 |
fun make_pp _ pprint (str, blk, brk, en) obj = |
|
19 | 42 |
pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0), |
43 |
fn () => brk (99999, 0), en); |
|
0 | 44 |
|
45 |
||
66 | 46 |
(*** File handling ***) |
0 | 47 |
|
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
48 |
local |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
49 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
50 |
(*These are functions from library.ML *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
51 |
fun take_suffix _ [] = ([], []) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
52 |
| take_suffix pred (x :: xs) = |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
53 |
(case take_suffix pred xs of |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
54 |
([], sffx) => if pred x then ([], x :: sffx) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
55 |
else ([x], sffx) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
56 |
| (prfx, sffx) => (x :: prfx, sffx)); |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
57 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
58 |
fun apr (f,y) x = f(x,y); |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
59 |
|
396
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
60 |
fun seq (proc: 'a -> unit) : 'a list -> unit = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
61 |
let fun seqf [] = () |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
62 |
| seqf (x :: xs) = (proc x; seqf xs) |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
63 |
in seqf end; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
64 |
|
1437 | 65 |
fun radixpand num : int list = |
66 |
let fun radix (n, tail) = |
|
67 |
if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail) |
|
68 |
in radix (num, []) end; |
|
69 |
||
70 |
fun radixstring num = |
|
71 |
let fun chrof n = chr (ord "0" + n); |
|
72 |
in implode (map chrof (radixpand num)) end; |
|
73 |
||
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
74 |
in |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
75 |
|
1480 | 76 |
(*Get time of last modification; if file doesn't exist return an empty string*) |
0 | 77 |
fun file_info "" = "" |
1480 | 78 |
| file_info name = radixstring (System.filedate name) handle _ => ""; |
66 | 79 |
|
73
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
80 |
(*Delete a file *) |
075db6ac7f2f
delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents:
66
diff
changeset
|
81 |
fun delete_file name = |
100
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
82 |
let val (is, os) = ExtendedIO.execute ("rm " ^ name) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
83 |
in close_in is; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
84 |
close_out os |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
85 |
end; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
86 |
|
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
87 |
(*Get pathname of current working directory *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
88 |
fun pwd () = |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
89 |
let val (is, os) = ExtendedIO.execute ("pwd") |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
90 |
val (path, _) = take_suffix (apr(op=,"\n")) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
91 |
(explode (ExtendedIO.input_line is)) (*remove newline *) |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
92 |
in close_in is; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
93 |
close_out os; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
94 |
implode path |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
95 |
end; |
e95b98536b3d
fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents:
73
diff
changeset
|
96 |
|
378
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
97 |
|
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
98 |
(*** ML command execution ***) |
85ff48546a05
added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents:
100
diff
changeset
|
99 |
|
396
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
100 |
val use_string = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
101 |
let fun exec command = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
102 |
let val firstLine = ref true; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
103 |
|
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
104 |
fun getLine () = |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
105 |
if !firstLine |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
106 |
then (firstLine := false; command) |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
107 |
else raise Io "use_string: buffer exhausted" |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
108 |
in PolyML.compiler (getLine, fn s => output (std_out, s)) () end |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
109 |
in seq exec end; |
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
110 |
|
18c9c28d0f7e
changed use_string's type to string list -> unit because POLY can only
clasohm
parents:
378
diff
changeset
|
111 |
end; |
1289 | 112 |
|
113 |
||
114 |
(*** System command execution ***) |
|
115 |
||
116 |
(*Execute an Unix command which doesn't take any input from stdin and |
|
117 |
sends its output to stdout.*) |
|
118 |
fun execute command = |
|
119 |
let val (is, os) = ExtendedIO.execute command; |
|
120 |
val result = input (is, 999999); |
|
121 |
in close_out os; |
|
122 |
close_in is; |
|
123 |
result |
|
124 |
end; |