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