src/Pure/ML-Systems/alice.ML
author wenzelm
Tue Jul 17 13:19:21 2007 +0200 (2007-07-17)
changeset 23826 463903573934
parent 23139 aa899bce7c3b
child 23835 1990e9acc7d1
permissions -rw-r--r--
moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
     1 (*  Title:      Pure/ML-Systems/alice.ML
     2     ID:         $Id$
     3 
     4 Compatibility file for Alice 1.4.
     5 
     6 NOTE: there is no wrapper script; may run it interactively as follows:
     7 
     8 $ cd Isabelle/src/Pure
     9 $ env ALICE_JIT_MODE=0 alice
    10 - use "ML-Systems/alice.ML";
    11 - use "ROOT.ML";
    12 - Session.finish ();
    13 *)
    14 
    15 fun exit 0 = (OS.Process.exit OS.Process.success): unit
    16   | exit _ = OS.Process.exit OS.Process.failure;
    17 
    18 
    19 (** ML system related **)
    20 
    21 (*low-level pointer equality*)
    22 fun pointer_eq (_: 'a, _: 'a) = false;
    23 
    24 
    25 (* restore old-style character / string functions *)
    26 
    27 exception Ord;
    28 fun ord "" = raise Ord
    29   | ord s = Char.ord (String.sub (s, 0));
    30 
    31 val chr = String.str o chr;
    32 val explode = map String.str o String.explode;
    33 val implode = String.concat;
    34 
    35 
    36 (* Poly/ML emulation *)
    37 
    38 fun quit () = exit 0;
    39 
    40 fun print_depth n = Print.depth := n;
    41 
    42 
    43 (* compiler-independent timing functions *)
    44 
    45 structure Timer =
    46 struct
    47   open Timer;
    48   type cpu_timer = unit;
    49   fun startCPUTimer () = ();
    50   fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
    51   fun checkGCTime () = Time.zeroTime;
    52 end;
    53 
    54 fun start_timing () =
    55   let val CPUtimer = Timer.startCPUTimer();
    56       val time = Timer.checkCPUTimer(CPUtimer)
    57   in  (CPUtimer,time)  end;
    58 
    59 fun end_timing (CPUtimer, {sys,usr}) =
    60   let open Time  (*...for Time.toString, Time.+ and Time.- *)
    61       val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    62   in  "User " ^ toString (usr2-usr) ^
    63       "  All "^ toString (sys2-sys + usr2-usr) ^
    64       " secs"
    65       handle Time => ""
    66   end;
    67 
    68 fun check_timer timer =
    69   let
    70     val {sys, usr} = Timer.checkCPUTimer timer;
    71     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    72   in (sys, usr, gc) end;
    73 
    74 
    75 (*prompts*)
    76 fun ml_prompts p1 p2 = ();
    77 
    78 (*dummy implementation*)
    79 fun profile (n: int) f x = f x;
    80 
    81 (*dummy implementation*)
    82 fun exception_trace f = f ();
    83 
    84 (*dummy implementation*)
    85 fun print x = x;
    86 
    87 
    88 (* toplevel pretty printing (see also Pure/install_pp.ML) *)
    89 
    90 fun make_pp path pprint = (path, pprint);
    91 fun install_pp (path, pp) = ();
    92 
    93 
    94 (* ML command execution *)
    95 
    96 fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
    97 
    98 fun use_file _ _ name = use name;
    99 
   100 
   101 
   102 (** interrupts **)
   103 
   104 exception Interrupt;
   105 
   106 fun ignore_interrupt f x = f x;
   107 fun raise_interrupt f x = f x;
   108 
   109 
   110 (* basis library fixes *)
   111 
   112 structure TextIO =
   113 struct
   114   open TextIO;
   115   fun inputLine is = TextIO.inputLine is
   116     handle IO.Io _ => raise Interrupt;
   117 end;
   118 
   119 
   120 (* bounded time execution *)
   121 
   122 (*dummy implementation*)
   123 fun interrupt_timeout time f x =
   124   f x;
   125 
   126 
   127 
   128 (** OS related **)
   129 
   130 (* current directory *)
   131 
   132 val cd = OS.FileSys.chDir;
   133 val pwd = OS.FileSys.getDir;
   134 
   135 
   136 (* system command execution *)
   137 
   138 (*execute Unix command which doesn't take any input from stdin and
   139   sends its output to stdout; could be done more easily by Unix.execute,
   140   but that function doesn't use the PATH*)
   141 fun execute command =
   142   let
   143     val tmp_name = OS.FileSys.tmpName ();
   144     val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   145     val result = TextIO.inputAll is;
   146   in
   147     TextIO.closeIn is;
   148     OS.FileSys.remove tmp_name;
   149     result
   150   end;
   151 
   152 (*plain version; with return code*)
   153 val system = OS.Process.system: string -> int;
   154 
   155 structure OS =
   156 struct
   157   open OS;
   158   structure FileSys =
   159   struct
   160     fun fileId name =
   161       (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   162         "" => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
   163       | s => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
   164     val compare = Int.compare;
   165     open FileSys;
   166   end;
   167 end;
   168 
   169 
   170 (* getenv *)
   171 
   172 fun getenv var =
   173   (case OS.Process.getEnv var of
   174     NONE => ""
   175   | SOME txt => txt);