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