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