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