src/Pure/POLY.ML
author lcp
Tue Jul 25 17:03:16 1995 +0200 (1995-07-25 ago)
changeset 1194 563ecd14c1d8
parent 396 18c9c28d0f7e
child 1289 2edd7a39d92a
permissions -rw-r--r--
Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
clasohm@0
     1
(*  Title:      Pure/POLY
clasohm@0
     2
    ID:         $Id$
clasohm@0
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1991  University of Cambridge
clasohm@0
     5
clasohm@0
     6
Compatibility file for Poly/ML (AHL release 1.88)
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open PolyML ExtendedIO;
clasohm@0
    10
clasohm@0
    11
clasohm@0
    12
(*A conditional timing function: applies f to () and, if the flag is true,
clasohm@0
    13
  prints its runtime.*)
clasohm@0
    14
clasohm@0
    15
fun cond_timeit flag f =
clasohm@0
    16
  if flag then
clasohm@0
    17
    let val before = System.processtime()
clasohm@0
    18
        val result = f()
clasohm@0
    19
        val both = real(System.processtime() - before) / 10.0
clasohm@0
    20
    in  output(std_out, "Process time (incl GC): "^
clasohm@0
    21
                         makestring both ^ " secs\n");
clasohm@0
    22
        result
clasohm@0
    23
    end
clasohm@0
    24
  else f();
clasohm@0
    25
clasohm@0
    26
clasohm@0
    27
(*Save function: in Poly/ML, ignores filename and commits to present file*)
clasohm@0
    28
clasohm@0
    29
fun xML filename banner = commit();
clasohm@0
    30
clasohm@0
    31
clasohm@0
    32
(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
clasohm@0
    33
clasohm@0
    34
fun make_pp _ pprint (str, blk, brk, en) obj =
wenzelm@19
    35
  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
wenzelm@19
    36
    fn () => brk (99999, 0), en);
clasohm@0
    37
clasohm@0
    38
lcp@66
    39
(*** File handling ***)
clasohm@0
    40
clasohm@100
    41
local
clasohm@100
    42
clasohm@100
    43
(*These are functions from library.ML *)
clasohm@100
    44
fun take_suffix _ [] = ([], [])
clasohm@100
    45
  | take_suffix pred (x :: xs) =
clasohm@100
    46
      (case take_suffix pred xs of
clasohm@100
    47
         ([], sffx) => if pred x then ([], x :: sffx)
clasohm@100
    48
                                 else ([x], sffx)
clasohm@100
    49
       | (prfx, sffx) => (x :: prfx, sffx));
clasohm@100
    50
clasohm@100
    51
fun apr (f,y) x = f(x,y);
clasohm@100
    52
clasohm@396
    53
fun seq (proc: 'a -> unit) : 'a list -> unit =
clasohm@396
    54
  let fun seqf [] = ()
clasohm@396
    55
        | seqf (x :: xs) = (proc x; seqf xs)
clasohm@396
    56
  in seqf end;
clasohm@396
    57
clasohm@100
    58
in
clasohm@100
    59
clasohm@58
    60
(*Get a string containing the time of last modification, attributes, owner
clasohm@58
    61
  and size of file (but not the path) *)
clasohm@0
    62
fun file_info "" = ""
clasohm@0
    63
  | file_info name =
clasohm@58
    64
      let
clasohm@58
    65
          val (is, os) = ExtendedIO.execute ("ls -l " ^ name)
clasohm@58
    66
          val (result, _) = take_suffix (apr(op<>," ")) 
clasohm@58
    67
                              (explode (ExtendedIO.input_line is))
lcp@66
    68
             (*Remove the part after the last " " (i.e. the path/filename) *)
clasohm@58
    69
        in close_in is;
clasohm@58
    70
           close_out os;
clasohm@58
    71
           implode result
clasohm@58
    72
        end;
lcp@66
    73
clasohm@73
    74
(*Delete a file *)
clasohm@73
    75
fun delete_file name =
clasohm@100
    76
  let val (is, os) = ExtendedIO.execute ("rm " ^ name)
clasohm@100
    77
  in close_in is;
clasohm@100
    78
     close_out os
clasohm@100
    79
  end;
clasohm@100
    80
clasohm@100
    81
(*Get pathname of current working directory *)
clasohm@100
    82
fun pwd () =
clasohm@100
    83
  let val (is, os) = ExtendedIO.execute ("pwd")
clasohm@100
    84
      val (path, _) = take_suffix (apr(op=,"\n"))
clasohm@100
    85
                       (explode (ExtendedIO.input_line is)) (*remove newline *)
clasohm@100
    86
  in close_in is;
clasohm@100
    87
     close_out os;
clasohm@100
    88
     implode path
clasohm@100
    89
  end;
clasohm@100
    90
clasohm@378
    91
clasohm@378
    92
(*** ML command execution ***)
clasohm@378
    93
clasohm@396
    94
val use_string =
clasohm@396
    95
  let fun exec command =
clasohm@396
    96
    let val firstLine = ref true;
clasohm@396
    97
clasohm@396
    98
        fun getLine () =
clasohm@396
    99
          if !firstLine
clasohm@396
   100
          then (firstLine := false; command)
clasohm@396
   101
          else raise Io "use_string: buffer exhausted"
clasohm@396
   102
    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
clasohm@396
   103
  in seq exec end;
clasohm@396
   104
clasohm@396
   105
end;