src/Pure/ML-Systems/mosml.ML
author wenzelm
Tue Sep 29 11:48:32 2009 +0200 (2009-09-29)
changeset 32737 76fa673eee8b
parent 31686 e54ae15335a1
child 32776 1504f9c2d060
permissions -rw-r--r--
Raw ML references as unsynchronized state variables.
     1 (*  Title:      Pure/ML-Systems/mosml.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Compatibility file for Moscow ML 2.01
     6 
     7 NOTE: saving images does not work; may run it interactively as follows:
     8 
     9 $ cd Isabelle/src/Pure
    10 $ isabelle-process RAW_ML_SYSTEM
    11 > val ml_system = "mosml";
    12 > use "ML-Systems/mosml.ML";
    13 > use "ROOT.ML";
    14 > Session.finish ();
    15 > cd "../FOL";
    16 > use "ROOT.ML";
    17 > Session.finish ();
    18 > cd "../ZF";
    19 > use "ROOT.ML";
    20 *)
    21 
    22 (** ML system related **)
    23 
    24 val ml_system_fix_ints = false;
    25 
    26 fun forget_structure _ = ();
    27 
    28 load "Obj";
    29 load "Word";
    30 load "Bool";
    31 load "Int";
    32 load "Real";
    33 load "ListPair";
    34 load "OS";
    35 load "Process";
    36 load "FileSys";
    37 load "IO";
    38 load "CharVector";
    39 
    40 exception Interrupt;
    41 fun reraise exn = raise exn;
    42 
    43 use "ML-Systems/exn.ML";
    44 use "ML-Systems/unsynchronized.ML";
    45 use "ML-Systems/universal.ML";
    46 use "ML-Systems/thread_dummy.ML";
    47 use "ML-Systems/multithreading.ML";
    48 use "ML-Systems/time_limit.ML";
    49 use "ML-Systems/ml_name_space.ML";
    50 use "ML-Systems/ml_pretty.ML";
    51 use "ML-Systems/use_context.ML";
    52 
    53 
    54 (*low-level pointer equality*)
    55 local val cast : 'a -> int = Obj.magic
    56 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
    57 
    58 (*proper implementation available?*)
    59 structure IntInf =
    60 struct
    61   fun divMod (x, y) = (x div y, x mod y);
    62 
    63   local
    64     fun log 1 a = a
    65       | log n a = log (n div 2) (a + 1);
    66   in
    67     fun log2 n = if n > 0 then log n 0 else raise Domain;
    68   end;
    69 
    70   open Int;
    71 end;
    72 
    73 structure Substring =
    74 struct
    75   open Substring;
    76   val full = all;
    77 end;
    78 
    79 structure Real =
    80 struct
    81   open Real;
    82   val realFloor = real o floor;
    83 end;
    84 
    85 structure String =
    86 struct
    87   fun isSuffix s1 s2 =
    88     let val n1 = size s1 and n2 = size s2
    89     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
    90   open String;
    91 end;
    92 
    93 structure Time =
    94 struct
    95   open Time;
    96   fun toString t = Time.toString t
    97     handle Overflow => Real.toString (Time.toReal t);   (*workaround Y2004 bug*)
    98 end;
    99 
   100 structure OS =
   101 struct
   102   open OS
   103   structure Process =
   104   struct
   105     open Process
   106     fun sleep _ = raise Fail "OS.Process.sleep undefined"
   107   end;
   108   structure FileSys = FileSys
   109 end;
   110 
   111 exception Option = Option.Option;
   112 
   113 
   114 (*limit the printing depth*)
   115 local
   116   val depth = ref 10;
   117 in
   118   fun get_print_depth () = ! depth;
   119   fun print_depth n =
   120    (depth := n;
   121     Meta.printDepth := n div 2;
   122     Meta.printLength := n);
   123 end;
   124 
   125 (*dummy implementation*)
   126 fun toplevel_pp _ _ _ = ();
   127 
   128 (*dummy implementation*)
   129 fun ml_prompts p1 p2 = ();
   130 
   131 (*dummy implementation*)
   132 fun profile (n: int) f x = f x;
   133 
   134 (*dummy implementation*)
   135 fun exception_trace f = f ();
   136 
   137 
   138 
   139 (** Compiler-independent timing functions **)
   140 
   141 load "Timer";
   142 
   143 fun start_timing () =
   144   let
   145     val timer = Timer.startCPUTimer ();
   146     val time = Timer.checkCPUTimer timer;
   147   in (timer, time) end;
   148 
   149 fun end_timing (timer, {gc, sys, usr}) =
   150   let
   151     open Time;  (*...for Time.toString, Time.+ and Time.- *)
   152     val {gc = gc2, sys = sys2, usr = usr2} = Timer.checkCPUTimer timer;
   153     val user = usr2 - usr + gc2 - gc;
   154     val all = user + sys2 - sys;
   155     val message = "User " ^ toString user ^ "  All "^ toString all ^ " secs" handle Time => "";
   156   in {message = message, user = user, all = all} end;
   157 
   158 
   159 (* SML basis library fixes *)
   160 
   161 structure TextIO =
   162 struct
   163   fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
   164   open TextIO;
   165   fun inputLine is =
   166     let val s = TextIO.inputLine is
   167     in if s = "" then NONE else SOME s end;
   168   fun getOutstream _ = ();
   169   structure StreamIO =
   170   struct
   171     fun setBufferMode _ = ();
   172   end
   173 end;
   174 
   175 structure IO =
   176 struct
   177   open IO;
   178   val BLOCK_BUF = ();
   179 end;
   180 
   181 
   182 (* ML command execution *)
   183 
   184 (*Can one redirect 'use' directly to an instream?*)
   185 fun use_text ({tune_source, ...}: use_context) _ _ txt =
   186   let
   187     val tmp_name = FileSys.tmpName ();
   188     val tmp_file = TextIO.openOut tmp_name;
   189   in
   190     TextIO.output (tmp_file, tune_source txt);
   191     TextIO.closeOut tmp_file;
   192     use tmp_name;
   193     FileSys.remove tmp_name
   194   end;
   195 
   196 fun use_file _ _ name = use name;
   197 
   198 
   199 
   200 (** interrupts **)      (*Note: may get into race conditions*)
   201 
   202 (* FIXME proper implementation available? *)
   203 
   204 fun interruptible f x = f x;
   205 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
   206 
   207 
   208 
   209 (** OS related **)
   210 
   211 (*dummy implementation*)
   212 structure Posix =
   213 struct
   214   structure ProcEnv =
   215   struct
   216     fun getpid () = 0;
   217   end;  
   218 end;
   219 
   220 local
   221 
   222 fun read_file name =
   223   let val is = TextIO.openIn name
   224   in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   225 
   226 fun write_file name txt =
   227   let val os = TextIO.openOut name
   228   in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   229 
   230 in
   231 
   232 fun system_out script =
   233   let
   234     val script_name = OS.FileSys.tmpName ();
   235     val _ = write_file script_name script;
   236 
   237     val output_name = OS.FileSys.tmpName ();
   238 
   239     val status =
   240       OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   241         script_name ^ " /dev/null " ^ output_name);
   242     val rc = if status = OS.Process.success then 0 else 1;
   243 
   244     val output = read_file output_name handle IO.Io _ => "";
   245     val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   246     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   247   in (output, rc) end;
   248 
   249 end;
   250 
   251 val cd = OS.FileSys.chDir;
   252 val pwd = OS.FileSys.getDir;
   253 
   254 val process_id = Int.toString o Posix.ProcEnv.getpid;
   255 
   256 fun getenv var =
   257   (case Process.getEnv var of
   258     NONE => ""
   259   | SOME txt => txt);