src/Pure/ML-Systems/mosml.ML
author wenzelm
Sun Mar 01 23:36:12 2009 +0100 (2009-03-01)
changeset 30190 479806475f3c
parent 30187 b92b3375e919
child 30619 0226c07352db
permissions -rw-r--r--
use long names for old-style fold combinators;
     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 
    42 use "ML-Systems/exn.ML";
    43 use "ML-Systems/universal.ML";
    44 use "ML-Systems/thread_dummy.ML";
    45 use "ML-Systems/multithreading.ML";
    46 use "ML-Systems/time_limit.ML";
    47 use "ML-Systems/ml_name_space.ML";
    48 
    49 
    50 (*low-level pointer equality*)
    51 local val cast : 'a -> int = Obj.magic
    52 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
    53 
    54 (*proper implementation available?*)
    55 structure IntInf =
    56 struct
    57   fun divMod (x, y) = (x div y, x mod y);
    58 
    59   local
    60     fun log 1 a = a
    61       | log n a = log (n div 2) (a + 1);
    62   in
    63     fun log2 n = if n > 0 then log n 0 else raise Domain;
    64   end;
    65 
    66   open Int;
    67 end;
    68 
    69 structure Substring =
    70 struct
    71   open Substring;
    72   val full = all;
    73 end;
    74 
    75 structure Real =
    76 struct
    77   open Real;
    78   val realFloor = real o floor;
    79 end;
    80 
    81 structure String =
    82 struct
    83   fun isSuffix s1 s2 =
    84     let val n1 = size s1 and n2 = size s2
    85     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
    86   open String;
    87 end;
    88 
    89 structure Time =
    90 struct
    91   open Time;
    92   fun toString t = Time.toString t
    93     handle Overflow => Real.toString (Time.toReal t);   (*workaround Y2004 bug*)
    94 end;
    95 
    96 structure OS =
    97 struct
    98   open OS
    99   structure Process =
   100   struct
   101     open Process
   102     fun sleep _ = raise Fail "OS.Process.sleep undefined"
   103   end;
   104   structure FileSys = FileSys
   105 end;
   106 
   107 exception Option = Option.Option;
   108 
   109 
   110 (*limit the printing depth*)
   111 local
   112   val depth = ref 10;
   113 in
   114   fun get_print_depth () = ! depth;
   115   fun print_depth n =
   116    (depth := n;
   117     Meta.printDepth := n div 2;
   118     Meta.printLength := n);
   119 end;
   120 
   121 (*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
   122 (*the documentation refers to an installPP but I couldn't fine it!*)
   123 fun make_pp path pprint = ();
   124 fun install_pp _ = ();
   125 
   126 (*dummy implementation*)
   127 fun ml_prompts p1 p2 = ();
   128 
   129 (*dummy implementation*)
   130 fun profile (n: int) f x = f x;
   131 
   132 (*dummy implementation*)
   133 fun exception_trace f = f ();
   134 
   135 (*dummy implementation*)
   136 fun print x = x;
   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 fun check_timer timer =
   159   let val {sys, usr, gc} = Timer.checkCPUTimer timer
   160   in (sys, usr, gc) end;
   161 
   162 
   163 (* SML basis library fixes *)
   164 
   165 structure TextIO =
   166 struct
   167   fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
   168   open TextIO;
   169   fun inputLine is =
   170     let val s = TextIO.inputLine is
   171     in if s = "" then NONE else SOME s end;
   172   fun getOutstream _ = ();
   173   structure StreamIO =
   174   struct
   175     fun setBufferMode _ = ();
   176   end
   177 end;
   178 
   179 structure IO =
   180 struct
   181   open IO;
   182   val BLOCK_BUF = ();
   183 end;
   184 
   185 
   186 (* ML command execution *)
   187 
   188 (*Can one redirect 'use' directly to an instream?*)
   189 fun use_text (tune: string -> string) _ _ _ _ _ txt =
   190   let
   191     val tmp_name = FileSys.tmpName ();
   192     val tmp_file = TextIO.openOut tmp_name;
   193   in
   194     TextIO.output (tmp_file, tune txt);
   195     TextIO.closeOut tmp_file;
   196     use tmp_name;
   197     FileSys.remove tmp_name
   198   end;
   199 
   200 fun use_file _ _ _ _ _ name = use name;
   201 
   202 
   203 
   204 (** interrupts **)      (*Note: may get into race conditions*)
   205 
   206 (* FIXME proper implementation available? *)
   207 
   208 fun interruptible f x = f x;
   209 fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
   210 
   211 
   212 
   213 (** OS related **)
   214 
   215 (*dummy implementation*)
   216 structure Posix =
   217 struct
   218   structure ProcEnv =
   219   struct
   220     fun getpid () = 0;
   221   end;  
   222 end;
   223 
   224 local
   225 
   226 fun read_file name =
   227   let val is = TextIO.openIn name
   228   in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
   229 
   230 fun write_file name txt =
   231   let val os = TextIO.openOut name
   232   in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
   233 
   234 in
   235 
   236 fun system_out script =
   237   let
   238     val script_name = OS.FileSys.tmpName ();
   239     val _ = write_file script_name script;
   240 
   241     val output_name = OS.FileSys.tmpName ();
   242 
   243     val status =
   244       OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
   245         script_name ^ " /dev/null " ^ output_name);
   246     val rc = if status = OS.Process.success then 0 else 1;
   247 
   248     val output = read_file output_name handle IO.Io _ => "";
   249     val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
   250     val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
   251   in (output, rc) end;
   252 
   253 end;
   254 
   255 val cd = OS.FileSys.chDir;
   256 val pwd = OS.FileSys.getDir;
   257 
   258 val process_id = Int.toString o Posix.ProcEnv.getpid;
   259 
   260 fun getenv var =
   261   (case Process.getEnv var of
   262     NONE => ""
   263   | SOME txt => txt);