src/Pure/POLY.ML
author lcp
Tue, 21 Jun 1994 17:20:34 +0200
changeset 435 ca5356bd315a
parent 396 18c9c28d0f7e
child 1289 2edd7a39d92a
permissions -rw-r--r--
Addition of cardinals and order types, various tidying
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     1
(*  Title:      Pure/POLY
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     2
    ID:         $Id$
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     4
    Copyright   1991  University of Cambridge
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     5
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     6
Compatibility file for Poly/ML (AHL release 1.88)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     7
*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     8
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
     9
open PolyML ExtendedIO;
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    10
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    11
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    12
(*A conditional timing function: applies f to () and, if the flag is true,
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    13
  prints its runtime.*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    14
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    15
fun cond_timeit flag f =
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    16
  if flag then
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    17
    let val before = System.processtime()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    18
        val result = f()
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    19
        val both = real(System.processtime() - before) / 10.0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    20
    in  output(std_out, "Process time (incl GC): "^
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    21
                         makestring both ^ " secs\n");
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    22
        result
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    23
    end
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    24
  else f();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    25
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    26
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    27
(*Save function: in Poly/ML, ignores filename and commits to present file*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    28
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    29
fun xML filename banner = commit();
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    30
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    31
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    32
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    33
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    34
fun make_pp _ pprint (str, blk, brk, en) obj =
19
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    35
  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
929ad32d63fc Pure/ROOT.ML
wenzelm
parents: 0
diff changeset
    36
    fn () => brk (99999, 0), en);
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    37
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    38
66
1b14cd923772 /NJ,POLY/delete_file: new
lcp
parents: 58
diff changeset
    39
(*** File handling ***)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    40
100
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    41
local
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    42
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    43
(*These are functions from library.ML *)
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    44
fun take_suffix _ [] = ([], [])
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    45
  | take_suffix pred (x :: xs) =
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    46
      (case take_suffix pred xs of
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    47
         ([], 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
    48
                                 else ([x], sffx)
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    49
       | (prfx, sffx) => (x :: prfx, sffx));
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    50
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    51
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
    52
396
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    53
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
    54
  let fun seqf [] = ()
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    55
        | 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
    56
  in seqf end;
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    57
100
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    58
in
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    59
58
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    60
(*Get a string containing the time of last modification, attributes, owner
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    61
  and size of file (but not the path) *)
0
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    62
fun file_info "" = ""
a5a9c433f639 Initial revision
clasohm
parents:
diff changeset
    63
  | file_info name =
58
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    64
      let
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    65
          val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    66
          val (result, _) = take_suffix (apr(op<>," ")) 
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    67
                              (explode (ExtendedIO.input_line is))
66
1b14cd923772 /NJ,POLY/delete_file: new
lcp
parents: 58
diff changeset
    68
             (*Remove the part after the last " " (i.e. the path/filename) *)
58
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    69
        in close_in is;
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    70
           close_out os;
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    71
           implode result
b30802dfbe80 file_info now returns a string that does not contain the path/filename
clasohm
parents: 19
diff changeset
    72
        end;
66
1b14cd923772 /NJ,POLY/delete_file: new
lcp
parents: 58
diff changeset
    73
73
075db6ac7f2f delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents: 66
diff changeset
    74
(*Delete a file *)
075db6ac7f2f delete_file now has type string -> unit in both NJ and POLY,
clasohm
parents: 66
diff changeset
    75
fun delete_file name =
100
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    76
  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
    77
  in close_in is;
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    78
     close_out os
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    79
  end;
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    80
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    81
(*Get pathname of current working directory *)
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    82
fun pwd () =
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    83
  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
    84
      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
    85
                       (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
    86
  in close_in is;
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    87
     close_out os;
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    88
     implode path
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    89
  end;
e95b98536b3d fixed a bug in POLY.ML: delete_file didn't close streams;
clasohm
parents: 73
diff changeset
    90
378
85ff48546a05 added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents: 100
diff changeset
    91
85ff48546a05 added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents: 100
diff changeset
    92
(*** ML command execution ***)
85ff48546a05 added use_string: string -> unit to execute ML commands passed in a string
clasohm
parents: 100
diff changeset
    93
396
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    94
val use_string =
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    95
  let fun exec command =
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    96
    let val firstLine = ref true;
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    97
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    98
        fun getLine () =
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
    99
          if !firstLine
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
   100
          then (firstLine := false; command)
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
   101
          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
   102
    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
   103
  in seq exec end;
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
   104
18c9c28d0f7e changed use_string's type to string list -> unit because POLY can only
clasohm
parents: 378
diff changeset
   105
end;