Compatibility file for Alice 1.3 -- experimental!
authorwenzelm
Tue Apr 03 12:12:42 2007 +0200 (2007-04-03)
changeset 2256378fb2af1a5c3
parent 22562 80b814fe284b
child 22564 98a290c4b0b4
Compatibility file for Alice 1.3 -- experimental!
src/Pure/ML-Systems/alice.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Tue Apr 03 12:12:42 2007 +0200
     1.3 @@ -0,0 +1,168 @@
     1.4 +(*  Title:      Pure/ML-Systems/alice.ML
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Compatibility file for Alice 1.3.
     1.8 +val ml_system = "alice";
     1.9 +use "ML-Systems/alice.ML";
    1.10 +
    1.11 +*)
    1.12 +
    1.13 +fun exit 0 = (OS.Process.exit OS.Process.success): unit
    1.14 +  | exit _ = OS.Process.exit OS.Process.failure;
    1.15 +
    1.16 +
    1.17 +(** ML system related **)
    1.18 +
    1.19 +(*low-level pointer equality*)
    1.20 +fun pointer_eq (_: 'a, _: 'a) = false;
    1.21 +
    1.22 +
    1.23 +(* restore old-style character / string functions *)
    1.24 +
    1.25 +exception Ord;
    1.26 +fun ord "" = raise Ord
    1.27 +  | ord s = Char.ord (String.sub (s, 0));
    1.28 +
    1.29 +val chr = Char.toString o chr;
    1.30 +val explode = map Char.toString o String.explode;
    1.31 +val implode = String.concat;
    1.32 +
    1.33 +
    1.34 +(* Poly/ML emulation *)
    1.35 +
    1.36 +fun quit () = exit 0;
    1.37 +
    1.38 +fun print_depth n = Print.depth := n;
    1.39 +
    1.40 +
    1.41 +(* compiler-independent timing functions *)
    1.42 +
    1.43 +structure Timer =
    1.44 +struct
    1.45 +  open Timer;
    1.46 +  type cpu_timer = unit;
    1.47 +  fun startCPUTimer () = ();
    1.48 +  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
    1.49 +  fun checkGCTime () = Time.zeroTime;
    1.50 +end;
    1.51 +
    1.52 +fun start_timing () =
    1.53 +  let val CPUtimer = Timer.startCPUTimer();
    1.54 +      val time = Timer.checkCPUTimer(CPUtimer)
    1.55 +  in  (CPUtimer,time)  end;
    1.56 +
    1.57 +fun end_timing (CPUtimer, {sys,usr}) =
    1.58 +  let open Time  (*...for Time.toString, Time.+ and Time.- *)
    1.59 +      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
    1.60 +  in  "User " ^ toString (usr2-usr) ^
    1.61 +      "  All "^ toString (sys2-sys + usr2-usr) ^
    1.62 +      " secs"
    1.63 +      handle Time => ""
    1.64 +  end;
    1.65 +
    1.66 +fun check_timer timer =
    1.67 +  let
    1.68 +    val {sys, usr} = Timer.checkCPUTimer timer;
    1.69 +    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
    1.70 +  in (sys, usr, gc) end;
    1.71 +
    1.72 +
    1.73 +(*prompts*)
    1.74 +fun ml_prompts p1 p2 = ();
    1.75 +
    1.76 +(*dummy implementation*)
    1.77 +fun profile (n: int) f x = f x;
    1.78 +
    1.79 +(*dummy implementation*)
    1.80 +fun exception_trace f = f ();
    1.81 +
    1.82 +(*dummy implementation*)
    1.83 +fun print x = x;
    1.84 +
    1.85 +
    1.86 +(* toplevel pretty printing (see also Pure/install_pp.ML) *)
    1.87 +
    1.88 +fun make_pp path pprint = (path, pprint);
    1.89 +fun install_pp (path, pp) = ();
    1.90 +
    1.91 +
    1.92 +(* ML command execution *)
    1.93 +
    1.94 +fun use_text name (print, err) verbose txt = (Compiler.eval txt; ());
    1.95 +
    1.96 +fun use_file _ _ name = use name;
    1.97 +
    1.98 +
    1.99 +
   1.100 +(** interrupts **)
   1.101 +
   1.102 +exception Interrupt;
   1.103 +
   1.104 +fun ignore_interrupt f x = f x;
   1.105 +fun raise_interrupt f x = f x;
   1.106 +
   1.107 +
   1.108 +(* basis library fixes *)
   1.109 +
   1.110 +structure TextIO =
   1.111 +struct
   1.112 +  open TextIO;
   1.113 +
   1.114 +  fun inputLine is =
   1.115 +    (case TextIO.inputLine is of
   1.116 +      SOME str => str
   1.117 +    | NONE => "")
   1.118 +    handle IO.Io _ => raise Interrupt;
   1.119 +end;
   1.120 +
   1.121 +
   1.122 +(* bounded time execution *)
   1.123 +
   1.124 +(*dummy implementation*)
   1.125 +fun interrupt_timeout time f x =
   1.126 +  f x;
   1.127 +
   1.128 +
   1.129 +
   1.130 +(** OS related **)
   1.131 +
   1.132 +(* system command execution *)
   1.133 +
   1.134 +(*execute Unix command which doesn't take any input from stdin and
   1.135 +  sends its output to stdout; could be done more easily by Unix.execute,
   1.136 +  but that function doesn't use the PATH*)
   1.137 +fun execute command =
   1.138 +  let
   1.139 +    val tmp_name = OS.FileSys.tmpName ();
   1.140 +    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
   1.141 +    val result = TextIO.inputAll is;
   1.142 +  in
   1.143 +    TextIO.closeIn is;
   1.144 +    OS.FileSys.remove tmp_name;
   1.145 +    result
   1.146 +  end;
   1.147 +
   1.148 +(*plain version; with return code*)
   1.149 +val system = OS.Process.system: string -> int;
   1.150 +
   1.151 +structure OS =
   1.152 +struct
   1.153 +  open OS;
   1.154 +  structure FileSys =
   1.155 +  struct
   1.156 +    fun fileId name =
   1.157 +      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
   1.158 +        "" => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
   1.159 +      | s => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
   1.160 +    val compare = Int.compare;
   1.161 +    open FileSys;
   1.162 +  end;
   1.163 +end;
   1.164 +
   1.165 +
   1.166 +(* getenv *)
   1.167 +
   1.168 +fun getenv var =
   1.169 +  (case OS.Process.getEnv var of
   1.170 +    NONE => ""
   1.171 +  | SOME txt => txt);