renamed from POLY.ML;
authorwenzelm
Mon Dec 09 09:59:43 1996 +0100 (1996-12-09)
changeset 2336008ce88c9913
parent 2335 e965156e84e3
child 2337 5b18cc02adb7
renamed from POLY.ML;
src/Pure/ML-Systems/polyml-2.07.ML
src/Pure/ML-Systems/polyml-3.1.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml-2.07.ML	Mon Dec 09 09:59:43 1996 +0100
     1.3 @@ -0,0 +1,123 @@
     1.4 +(*  Title:      Pure/POLY
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1991  University of Cambridge
     1.8 +
     1.9 +Compatibility file for Poly/ML (AHL release 1.88)
    1.10 +*)
    1.11 +
    1.12 +open PolyML ExtendedIO;
    1.13 +
    1.14 +use"basis.ML";
    1.15 +
    1.16 +(*A conditional timing function: applies f to () and, if the flag is true,
    1.17 +  prints its runtime.*)
    1.18 +
    1.19 +fun cond_timeit flag f =
    1.20 +  if flag then
    1.21 +    let val before = System.processtime()
    1.22 +        val result = f()
    1.23 +        val both = real(System.processtime() - before) / 10.0
    1.24 +    in  output(std_out, "Process time (incl GC): "^
    1.25 +                         makestring both ^ " secs\n");
    1.26 +        result
    1.27 +    end
    1.28 +  else f();
    1.29 +
    1.30 +
    1.31 +(*Save function: in Poly/ML, ignores filename and commits to present file*)
    1.32 +
    1.33 +fun xML filename banner = commit();
    1.34 +
    1.35 +
    1.36 +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    1.37 +
    1.38 +fun make_pp _ pprint (str, blk, brk, en) obj =
    1.39 +  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    1.40 +    fn () => brk (99999, 0), en);
    1.41 +
    1.42 +
    1.43 +(*** File handling ***)
    1.44 +
    1.45 +local
    1.46 +
    1.47 +(*These are functions from library.ML *)
    1.48 +fun take_suffix _ [] = ([], [])
    1.49 +  | take_suffix pred (x :: xs) =
    1.50 +      (case take_suffix pred xs of
    1.51 +         ([], sffx) => if pred x then ([], x :: sffx)
    1.52 +                                 else ([x], sffx)
    1.53 +       | (prfx, sffx) => (x :: prfx, sffx));
    1.54 +
    1.55 +fun apr (f,y) x = f(x,y);
    1.56 +
    1.57 +fun seq (proc: 'a -> unit) : 'a list -> unit =
    1.58 +  let fun seqf [] = ()
    1.59 +        | seqf (x :: xs) = (proc x; seqf xs)
    1.60 +  in seqf end;
    1.61 +
    1.62 +fun radixpand num : int list =
    1.63 +  let fun radix (n, tail) =
    1.64 +    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    1.65 +  in radix (num, []) end;
    1.66 +
    1.67 +fun radixstring num =
    1.68 +  let fun chrof n = chr (ord "0" + n);
    1.69 +  in implode (map chrof (radixpand num)) end;
    1.70 +
    1.71 +in
    1.72 +
    1.73 +(*Get time of last modification; if file doesn't exist return an empty string*)
    1.74 +fun file_info "" = ""
    1.75 +  | file_info name = radixstring (System.filedate name)  handle _ => "";
    1.76 +
    1.77 +
    1.78 +structure OS =
    1.79 +  struct
    1.80 +  structure FileSys =
    1.81 +    struct
    1.82 +    val chDir = PolyML.cd
    1.83 +
    1.84 +    fun remove name =    (*Delete a file *)
    1.85 +      let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    1.86 +      in close_in is; close_out os end;
    1.87 +
    1.88 +    (*Get pathname of current working directory *)
    1.89 +    fun getDir () =
    1.90 +      let val (is, os) = ExtendedIO.execute ("pwd")
    1.91 +	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
    1.92 +			   (explode (ExtendedIO.input_line is)) 
    1.93 +      in close_in is; close_out os; implode path end;
    1.94 +
    1.95 +    end
    1.96 +  end;
    1.97 +
    1.98 +
    1.99 +
   1.100 +(*** ML command execution ***)
   1.101 +
   1.102 +val use_string =
   1.103 +  let fun exec command =
   1.104 +    let val firstLine = ref true;
   1.105 +
   1.106 +        fun getLine () =
   1.107 +          if !firstLine
   1.108 +          then (firstLine := false; command)
   1.109 +          else raise Io "use_string: buffer exhausted"
   1.110 +    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   1.111 +  in seq exec end;
   1.112 +
   1.113 +end;
   1.114 +
   1.115 +
   1.116 +(*** System command execution ***)
   1.117 +
   1.118 +(*Execute an Unix command which doesn't take any input from stdin and
   1.119 +  sends its output to stdout.*)
   1.120 +fun execute command =
   1.121 +  let val (is, os) =  ExtendedIO.execute command;
   1.122 +      val result = input (is, 999999);
   1.123 +  in close_out os;
   1.124 +     close_in is;
   1.125 +     result
   1.126 +  end;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/polyml-3.1.ML	Mon Dec 09 09:59:43 1996 +0100
     2.3 @@ -0,0 +1,123 @@
     2.4 +(*  Title:      Pure/POLY
     2.5 +    ID:         $Id$
     2.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     2.7 +    Copyright   1991  University of Cambridge
     2.8 +
     2.9 +Compatibility file for Poly/ML (AHL release 1.88)
    2.10 +*)
    2.11 +
    2.12 +open PolyML ExtendedIO;
    2.13 +
    2.14 +use"basis.ML";
    2.15 +
    2.16 +(*A conditional timing function: applies f to () and, if the flag is true,
    2.17 +  prints its runtime.*)
    2.18 +
    2.19 +fun cond_timeit flag f =
    2.20 +  if flag then
    2.21 +    let val before = System.processtime()
    2.22 +        val result = f()
    2.23 +        val both = real(System.processtime() - before) / 10.0
    2.24 +    in  output(std_out, "Process time (incl GC): "^
    2.25 +                         makestring both ^ " secs\n");
    2.26 +        result
    2.27 +    end
    2.28 +  else f();
    2.29 +
    2.30 +
    2.31 +(*Save function: in Poly/ML, ignores filename and commits to present file*)
    2.32 +
    2.33 +fun xML filename banner = commit();
    2.34 +
    2.35 +
    2.36 +(*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    2.37 +
    2.38 +fun make_pp _ pprint (str, blk, brk, en) obj =
    2.39 +  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
    2.40 +    fn () => brk (99999, 0), en);
    2.41 +
    2.42 +
    2.43 +(*** File handling ***)
    2.44 +
    2.45 +local
    2.46 +
    2.47 +(*These are functions from library.ML *)
    2.48 +fun take_suffix _ [] = ([], [])
    2.49 +  | take_suffix pred (x :: xs) =
    2.50 +      (case take_suffix pred xs of
    2.51 +         ([], sffx) => if pred x then ([], x :: sffx)
    2.52 +                                 else ([x], sffx)
    2.53 +       | (prfx, sffx) => (x :: prfx, sffx));
    2.54 +
    2.55 +fun apr (f,y) x = f(x,y);
    2.56 +
    2.57 +fun seq (proc: 'a -> unit) : 'a list -> unit =
    2.58 +  let fun seqf [] = ()
    2.59 +        | seqf (x :: xs) = (proc x; seqf xs)
    2.60 +  in seqf end;
    2.61 +
    2.62 +fun radixpand num : int list =
    2.63 +  let fun radix (n, tail) =
    2.64 +    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    2.65 +  in radix (num, []) end;
    2.66 +
    2.67 +fun radixstring num =
    2.68 +  let fun chrof n = chr (ord "0" + n);
    2.69 +  in implode (map chrof (radixpand num)) end;
    2.70 +
    2.71 +in
    2.72 +
    2.73 +(*Get time of last modification; if file doesn't exist return an empty string*)
    2.74 +fun file_info "" = ""
    2.75 +  | file_info name = radixstring (System.filedate name)  handle _ => "";
    2.76 +
    2.77 +
    2.78 +structure OS =
    2.79 +  struct
    2.80 +  structure FileSys =
    2.81 +    struct
    2.82 +    val chDir = PolyML.cd
    2.83 +
    2.84 +    fun remove name =    (*Delete a file *)
    2.85 +      let val (is, os) = ExtendedIO.execute ("rm " ^ name)
    2.86 +      in close_in is; close_out os end;
    2.87 +
    2.88 +    (*Get pathname of current working directory *)
    2.89 +    fun getDir () =
    2.90 +      let val (is, os) = ExtendedIO.execute ("pwd")
    2.91 +	  val (path, _) = take_suffix (apr(op=,"\n")) (*remove newline*)
    2.92 +			   (explode (ExtendedIO.input_line is)) 
    2.93 +      in close_in is; close_out os; implode path end;
    2.94 +
    2.95 +    end
    2.96 +  end;
    2.97 +
    2.98 +
    2.99 +
   2.100 +(*** ML command execution ***)
   2.101 +
   2.102 +val use_string =
   2.103 +  let fun exec command =
   2.104 +    let val firstLine = ref true;
   2.105 +
   2.106 +        fun getLine () =
   2.107 +          if !firstLine
   2.108 +          then (firstLine := false; command)
   2.109 +          else raise Io "use_string: buffer exhausted"
   2.110 +    in PolyML.compiler (getLine, fn s => output (std_out, s)) () end
   2.111 +  in seq exec end;
   2.112 +
   2.113 +end;
   2.114 +
   2.115 +
   2.116 +(*** System command execution ***)
   2.117 +
   2.118 +(*Execute an Unix command which doesn't take any input from stdin and
   2.119 +  sends its output to stdout.*)
   2.120 +fun execute command =
   2.121 +  let val (is, os) =  ExtendedIO.execute command;
   2.122 +      val result = input (is, 999999);
   2.123 +  in close_out os;
   2.124 +     close_in is;
   2.125 +     result
   2.126 +  end;