src/Pure/ML-Systems/alice.ML
author wenzelm
Thu Sep 04 16:03:47 2008 +0200 (2008-09-04)
changeset 28124 10a1f1f4c6ae
parent 27004 616c553c7cf1
child 28488 18fea7e88ea1
permissions -rw-r--r--
moved Multithreading.task/schedule to Concurrent/schedule.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 ISABELLE_HOME=$(cd ../..; pwd) alice
    10 - val ml_system = "alice";
    11 - use "ML-Systems/exn.ML";
    12 - use "ML-Systems/universal.ML";
    13 - use "ML-Systems/multithreading.ML";
    14 - use "ML-Systems/time_limit.ML";
    15 - use "ML-Systems/alice.ML";
    16 - use "ROOT.ML";
    17 - Session.finish ();
    18 *)
    19 
    20 val ml_system_fix_ints = false;
    21 
    22 fun forget_structure _ = ();
    23 
    24 fun exit 0 = (OS.Process.exit OS.Process.success): unit
    25   | exit _ = OS.Process.exit OS.Process.failure;
    26 
    27 
    28 (** ML system related **)
    29 
    30 (*low-level pointer equality*)
    31 fun pointer_eq (_: 'a, _: 'a) = false;
    32 
    33 
    34 (* integer compatibility -- downgraded IntInf *)
    35 
    36 structure Time =
    37 struct
    38   open Time;
    39   val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
    40   val fromSeconds = Time.fromSeconds o IntInf.fromInt;
    41 end;
    42 
    43 structure IntInf =
    44 struct
    45   fun divMod (x, y) = (x div y, x mod y);
    46   open Int;
    47 end;
    48 
    49 
    50 (* restore old-style character / string functions *)
    51 
    52 exception Ord;
    53 fun ord "" = raise Ord
    54   | ord s = Char.ord (String.sub (s, 0));
    55 
    56 val chr = String.str o chr;
    57 val explode = map String.str o String.explode;
    58 val implode = String.concat;
    59 
    60 
    61 (* Poly/ML emulation *)
    62 
    63 fun quit () = exit 0;
    64 
    65 fun get_print_depth () = ! Print.depth;
    66 fun print_depth n = Print.depth := n;
    67 
    68 
    69 (* compiler-independent timing functions *)
    70 
    71 structure Timer =
    72 struct
    73   open Timer;
    74   type cpu_timer = unit;
    75   fun startCPUTimer () = ();
    76   fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
    77   fun checkGCTime () = Time.zeroTime;
    78 end;
    79 
    80 fun start_timing () =
    81   let val CPUtimer = Timer.startCPUTimer();
    82       val time = Timer.checkCPUTimer(CPUtimer)
    83   in  (CPUtimer,time)  end;
    84 
    85 fun end_timing (CPUtimer, {sys,usr}) =
    86   let open Time  (*...for Time.toString, Time.+ and Time.- *)
    87       val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    88   in  "User " ^ toString (usr2-usr) ^
    89       "  All "^ toString (sys2-sys + usr2-usr) ^
    90       " secs"
    91       handle Time => ""
    92   end;
    93 
    94 fun check_timer timer =
    95   let
    96     val {sys, usr} = Timer.checkCPUTimer timer;
    97     val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    98   in (sys, usr, gc) end;
    99 
   100 
   101 (*prompts*)
   102 fun ml_prompts p1 p2 = ();
   103 
   104 (*dummy implementation*)
   105 fun profile (n: int) f x = f x;
   106 
   107 (*dummy implementation*)
   108 fun exception_trace f = f ();
   109 
   110 (*dummy implementation*)
   111 fun print x = x;
   112 
   113 
   114 (* toplevel pretty printing (see also Pure/pure_setup.ML) *)
   115 
   116 fun make_pp path pprint = (path, pprint);
   117 fun install_pp (path, pp) = ();
   118 
   119 
   120 (* ML command execution *)
   121 
   122 fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
   123 fun use_file _ _ _ _ name = use name;
   124 
   125 
   126 
   127 (** interrupts **)
   128 
   129 exception Interrupt;
   130 
   131 fun interruptible f x = f x;
   132 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
   133 
   134 
   135 (* basis library fixes *)
   136 
   137 structure TextIO =
   138 struct
   139   open TextIO;
   140   fun inputLine is = TextIO.inputLine is
   141     handle IO.Io _ => raise Interrupt;
   142 end;
   143 
   144 
   145 
   146 (** OS related **)
   147 
   148 structure OS =
   149 struct
   150   open OS;
   151   structure FileSys =
   152   struct
   153     open FileSys;
   154     fun tmpName () =
   155       let val name = FileSys.tmpName () in
   156         if String.isSuffix "\000" name
   157         then String.substring (name, 0, size name - 1)
   158         else name
   159       end;
   160   end;
   161 end;
   162 
   163 val cd = OS.FileSys.chDir;
   164 val pwd = OS.FileSys.getDir;
   165 
   166 local
   167 
   168 fun read_file name =
   169   let val is = TextIO.openIn name
   170   in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   171 
   172 fun write_file name txt =
   173   let val os = TextIO.openOut name
   174   in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   175 
   176 in
   177 
   178 fun system_out script =
   179   let
   180     val script_name = OS.FileSys.tmpName ();
   181     val _ = write_file script_name script;
   182 
   183     val output_name = OS.FileSys.tmpName ();
   184 
   185     val status =
   186       OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   187         script_name ^ " /dev/null " ^ output_name);
   188     val rc = if OS.Process.isSuccess status then 0 else 1;
   189 
   190     val output = read_file output_name handle IO.Io _ => "";
   191     val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   192     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   193   in (output, rc) end;
   194 
   195 end;
   196 
   197 structure OS =
   198 struct
   199   open OS;
   200   structure FileSys =
   201   struct
   202     fun fileId name =
   203       (case system_out ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   204         ("", _) => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
   205       | (s, _) => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
   206     val compare = Int.compare;
   207     fun fullPath name =
   208       (case system_out ("FILE='" ^ name ^
   209         "' && cd \"$(dirname \"$FILE\")\" && echo -n \"$(pwd -P)/$(basename \"$FILE\")\"") of
   210         ("", _) => raise SysErr ("Bad file", NONE)
   211       | (s, _) => s);
   212     open FileSys;
   213   end;
   214 end;
   215 
   216 structure Posix =
   217 struct
   218   structure ProcEnv =
   219   struct
   220     fun getpid () = raise Fail "Posix.ProcEnv.getpoid undefined";
   221   end;
   222 end;
   223 
   224 fun string_of_pid _ = raise Fail "string_of_pid undefined";
   225 
   226 fun getenv var =
   227   (case OS.Process.getEnv var of
   228     NONE => ""
   229   | SOME txt => txt);