src/Pure/ML-Systems/mosml.ML
author berghofe
Mon Jan 21 14:18:49 2008 +0100 (2008-01-21)
changeset 25939 ddea202704b4
parent 25732 308315ee2b6d
child 26084 a7475459c740
permissions -rw-r--r--
Removed Logic.auto_rename.
     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 load "Obj";
    28 load "Bool";
    29 load "Int";
    30 load "Real";
    31 load "ListPair";
    32 load "OS";
    33 load "Process";
    34 load "FileSys";
    35 load "IO";
    36 
    37 use "ML-Systems/exn.ML";
    38 use "ML-Systems/universal.ML";
    39 use "ML-Systems/multithreading.ML";
    40 use "ML-Systems/time_limit.ML";
    41 
    42 
    43 (*low-level pointer equality*)
    44 local val cast : 'a -> int = Obj.magic
    45 in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
    46 
    47 (*proper implementation available?*)
    48 structure IntInf =
    49 struct
    50   fun divMod (x, y) = (x div y, x mod y);
    51   open Int;
    52 end;
    53 
    54 structure Real =
    55 struct
    56   open Real;
    57   val realFloor = real o floor;
    58 end;
    59 
    60 structure String =
    61 struct
    62   fun isSuffix s1 s2 =
    63     let val n1 = size s1 and n2 = size s2
    64     in if n1 = n2 then s1 = s2 else n1 <= n2 andalso String.substring (s2, n2 - n1, n1) = s1 end;
    65   open String;
    66 end;
    67 
    68 structure Time =
    69 struct
    70   open Time;
    71   fun toString t = Time.toString t
    72     handle Overflow => Real.toString (Time.toReal t);   (*workaround Y2004 bug*)
    73 end;
    74 
    75 structure OS =
    76 struct
    77   open OS
    78   structure Process = Process
    79   structure FileSys = FileSys
    80 end;
    81 
    82 exception Option = Option.Option;
    83 
    84 
    85 (*limit the printing depth*)
    86 local
    87   val depth = ref 10;
    88 in
    89   fun get_print_depth () = ! depth;
    90   fun print_depth n =
    91    (depth := n;
    92     Meta.printDepth := n div 2;
    93     Meta.printLength := n);
    94 end;
    95 
    96 (*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
    97 (*the documentation refers to an installPP but I couldn't fine it!*)
    98 fun make_pp path pprint = ();
    99 fun install_pp _ = ();
   100 
   101 (*dummy implementation*)
   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 (** Compiler-independent timing functions **)
   115 
   116 load "Timer";
   117 
   118 fun start_timing () =
   119   let val CPUtimer = Timer.startCPUTimer();
   120       val time = Timer.checkCPUTimer(CPUtimer)
   121   in  (CPUtimer,time)  end;
   122 
   123 fun end_timing (CPUtimer, {gc,sys,usr}) =
   124   let open Time  (*...for Time.toString, Time.+ and Time.- *)
   125       val {gc=gc2,sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
   126   in  "User " ^ toString (usr2-usr) ^
   127       "  GC " ^ toString (gc2-gc) ^
   128       "  All "^ toString (sys2-sys + usr2-usr + gc2-gc) ^
   129       " secs"
   130       handle Time => ""
   131   end;
   132 
   133 fun check_timer timer =
   134   let val {sys, usr, gc} = Timer.checkCPUTimer timer
   135   in (sys, usr, gc) end;
   136 
   137 
   138 (* SML basis library fixes *)
   139 
   140 structure TextIO =
   141 struct
   142   fun canInput _ = raise IO.Io {cause = Fail "undefined", function = "canInput", name = ""};
   143   open TextIO;
   144   fun inputLine is =
   145     let val s = TextIO.inputLine is
   146     in if s = "" then NONE else SOME s end;
   147 end;
   148 
   149 
   150 (* ML command execution *)
   151 
   152 (*Can one redirect 'use' directly to an instream?*)
   153 fun use_text (tune: string -> string) _ _ _ txt =
   154   let
   155     val tmp_name = FileSys.tmpName ();
   156     val tmp_file = TextIO.openOut tmp_name;
   157   in
   158     TextIO.output (tmp_file, tune txt);
   159     TextIO.closeOut tmp_file;
   160     use tmp_name;
   161     FileSys.remove tmp_name
   162   end;
   163 
   164 fun use_file _ _ _ name = use name;
   165 
   166 
   167 
   168 (** interrupts **)      (*Note: may get into race conditions*)
   169 
   170 (* FIXME proper implementation available? *)
   171 
   172 exception Interrupt;
   173 
   174 fun ignore_interrupt f x = f x;
   175 fun raise_interrupt f x = f x;
   176 
   177 
   178 
   179 (** OS related **)
   180 
   181 (* current directory *)
   182 
   183 val cd = OS.FileSys.chDir;
   184 val pwd = OS.FileSys.getDir;
   185 
   186 
   187 (* system command execution *)
   188 
   189 (*execute Unix command which doesn't take any input from stdin and
   190   sends its output to stdout; could be done more easily by Unix.execute,
   191   but that function doesn't use the PATH*)
   192 fun execute command =
   193   let
   194     val tmp_name = FileSys.tmpName ();
   195     val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   196     val result = TextIO.inputAll is;
   197   in
   198     TextIO.closeIn is;
   199     FileSys.remove tmp_name;
   200     result
   201   end;
   202 
   203 (*plain version; with return code*)
   204 fun system cmd =
   205   if Process.system cmd = Process.success then 0 else 1;
   206 
   207 
   208 val string_of_pid = Int.toString;
   209 
   210 
   211 (* getenv *)
   212 
   213 fun getenv var =
   214   (case Process.getEnv var of
   215     NONE => ""
   216   | SOME txt => txt);