src/Pure/NJ093.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 2408 acddf41dbbf7
child 3319 0206e7507737
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     1 (*  Title:      Pure/NJ093.ML
     2     ID:         $Id$
     3     Author:     Carsten Clasohm, TU Muenchen
     4     Copyright   1996  TU Muenchen
     5 
     6 Compatibility file for Standard ML of New Jersey version 0.93.
     7 *)
     8 
     9 
    10 use"basis.ML";
    11 
    12 (*** Poly/ML emulation ***)
    13 
    14 (*To exit the system with an exit code -- an alternative to ^D *)
    15 val exit = System.Unsafe.CInterface.exit;
    16 fun quit () = exit 0;
    17 
    18 (*To limit the printing depth [divided by 2 for comparibility with Poly/ML]*)
    19 fun print_depth n = (System.Control.Print.printDepth := n div 2;
    20                      System.Control.Print.printLength := n);
    21 
    22 (*Interface for toplevel pretty printers, see also Pure/install_pp.ML*)
    23 
    24 fun make_pp path pprint =
    25   let
    26     open System.PrettyPrint;
    27 
    28     fun pp pps obj =
    29       pprint obj
    30         (add_string pps, begin_block pps INCONSISTENT,
    31           fn wd => add_break pps (wd, 0), fn () => add_newline pps,
    32           fn () => end_block pps);
    33   in
    34     (path, pp)
    35   end;
    36 
    37 fun install_pp (path, pp) = System.PrettyPrint.install_pp path pp;
    38 
    39 
    40 (*** New Jersey ML parameters ***)
    41 
    42 (* Suppresses Garbage Collection messages;  default was 2 *)
    43 System.Control.Runtime.gcmessages := 0;
    44 
    45 
    46 (*** Timing functions ***)
    47 
    48 (*Print microseconds, suppressing trailing zeroes*)
    49 fun umakestring 0 = ""
    50   | umakestring n = chr(ord "0" + n div 100000) ^
    51                     umakestring(10 * (n mod 100000));
    52 
    53 (*A conditional timing function: applies f to () and, if the flag is true,
    54   prints its runtime. *)
    55 fun cond_timeit flag f =
    56   if flag then
    57     let fun string_of_time (System.Timer.TIME {sec, usec}) =
    58             makestring sec ^ "." ^ (if usec=0 then "0" else umakestring usec)
    59         open System.Timer;
    60         val start = start_timer()
    61         val result = f();
    62         val nongc = check_timer(start)
    63         and gc = check_timer_gc(start);
    64         val both = add_time(nongc, gc)
    65     in  print("Non GC " ^ string_of_time nongc ^
    66                "   GC " ^ string_of_time gc ^
    67                "  both "^ string_of_time both ^ " secs\n");
    68         result
    69     end
    70   else f();
    71 
    72 
    73 (*** File handling ***)
    74 
    75 (*Get time of last modification; if file doesn't exist return an empty string*)
    76 local
    77     open System.Timer;
    78     open System.Unsafe.SysIO;
    79 in
    80   fun file_info "" = ""
    81     | file_info name = makestring (mtime (PATH name))  handle _ => "";
    82 end;
    83 
    84 structure OS =
    85   struct
    86   structure FileSys =
    87     struct
    88     val OS.FileSys.chDir = System.Directory.cd
    89     val remove = System.Unsafe.SysIO.unlink       (*Delete a file *)
    90     val getDir = System.Directory.getWD           (*path of working directory*)
    91     end
    92   end;
    93 
    94 
    95 (*** ML command execution ***)
    96 
    97 fun use_string commands = 
    98   System.Compile.use_stream (open_string (implode commands));
    99 
   100 
   101 (*** System command execution ***)
   102 
   103 (*Execute an Unix command which doesn't take any input from stdin and
   104   sends its output to stdout.
   105   This could be done more easily by IO.execute, but that function
   106   seems to be buggy in SML/NJ 0.93.*)
   107 fun execute command =
   108   let val tmp_name = "isa_converted.tmp"
   109       val is = (System.system (command ^ " > " ^ tmp_name);
   110                 open_in tmp_name);
   111       val result = input (is, 999999);
   112   in close_in is;
   113      delete_file tmp_name;
   114      result
   115   end;
   116 
   117 (*redefine to flush its output immediately -- temporary patch suggested
   118   by Kim Dam Petersen*)
   119 val output = fn(s, t) => (output(s, t); flush_out s);
   120 
   121 (*For use in Makefiles -- saves space*)
   122 fun xML filename banner = (exportML filename;  print(banner^"\n"));
   123 
   124 
   125 val needs_filtered_use = false;