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