src/Pure/ML-Systems/alice.ML
author wenzelm
Thu Sep 04 16:03:47 2008 +0200 (2008-09-04)
changeset 28124 10a1f1f4c6ae
parent 27004 616c553c7cf1
child 28488 18fea7e88ea1
permissions -rw-r--r--
moved Multithreading.task/schedule to Concurrent/schedule.ML;
wenzelm@22563
     1
(*  Title:      Pure/ML-Systems/alice.ML
wenzelm@22563
     2
    ID:         $Id$
wenzelm@22563
     3
wenzelm@22837
     4
Compatibility file for Alice 1.4.
wenzelm@23826
     5
wenzelm@23826
     6
NOTE: there is no wrapper script; may run it interactively as follows:
wenzelm@23826
     7
wenzelm@23826
     8
$ cd Isabelle/src/Pure
wenzelm@27004
     9
$ env ALICE_JIT_MODE=0 ISABELLE_HOME=$(cd ../..; pwd) alice
wenzelm@23835
    10
- val ml_system = "alice";
wenzelm@24807
    11
- use "ML-Systems/exn.ML";
wenzelm@26226
    12
- use "ML-Systems/universal.ML";
wenzelm@24807
    13
- use "ML-Systems/multithreading.ML";
wenzelm@24807
    14
- use "ML-Systems/time_limit.ML";
wenzelm@23826
    15
- use "ML-Systems/alice.ML";
wenzelm@23826
    16
- use "ROOT.ML";
wenzelm@23826
    17
- Session.finish ();
wenzelm@22563
    18
*)
wenzelm@22563
    19
wenzelm@24597
    20
val ml_system_fix_ints = false;
wenzelm@24597
    21
wenzelm@26474
    22
fun forget_structure _ = ();
wenzelm@26474
    23
wenzelm@22563
    24
fun exit 0 = (OS.Process.exit OS.Process.success): unit
wenzelm@22563
    25
  | exit _ = OS.Process.exit OS.Process.failure;
wenzelm@22563
    26
wenzelm@22563
    27
wenzelm@22563
    28
(** ML system related **)
wenzelm@22563
    29
wenzelm@22563
    30
(*low-level pointer equality*)
wenzelm@22563
    31
fun pointer_eq (_: 'a, _: 'a) = false;
wenzelm@22563
    32
wenzelm@24809
    33
wenzelm@24809
    34
(* integer compatibility -- downgraded IntInf *)
wenzelm@24809
    35
wenzelm@24809
    36
structure Time =
wenzelm@24809
    37
struct
wenzelm@24809
    38
  open Time;
wenzelm@24809
    39
  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
wenzelm@24809
    40
  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
wenzelm@24809
    41
end;
wenzelm@24809
    42
wenzelm@24807
    43
structure IntInf =
wenzelm@24807
    44
struct
wenzelm@24807
    45
  fun divMod (x, y) = (x div y, x mod y);
wenzelm@24807
    46
  open Int;
wenzelm@24807
    47
end;
wenzelm@24807
    48
wenzelm@22563
    49
wenzelm@22563
    50
(* restore old-style character / string functions *)
wenzelm@22563
    51
wenzelm@22563
    52
exception Ord;
wenzelm@22563
    53
fun ord "" = raise Ord
wenzelm@22563
    54
  | ord s = Char.ord (String.sub (s, 0));
wenzelm@22563
    55
wenzelm@22575
    56
val chr = String.str o chr;
wenzelm@22575
    57
val explode = map String.str o String.explode;
wenzelm@22563
    58
val implode = String.concat;
wenzelm@22563
    59
wenzelm@22563
    60
wenzelm@22563
    61
(* Poly/ML emulation *)
wenzelm@22563
    62
wenzelm@22563
    63
fun quit () = exit 0;
wenzelm@22563
    64
wenzelm@24329
    65
fun get_print_depth () = ! Print.depth;
wenzelm@22563
    66
fun print_depth n = Print.depth := n;
wenzelm@22563
    67
wenzelm@22563
    68
wenzelm@22563
    69
(* compiler-independent timing functions *)
wenzelm@22563
    70
wenzelm@22563
    71
structure Timer =
wenzelm@22563
    72
struct
wenzelm@22563
    73
  open Timer;
wenzelm@22563
    74
  type cpu_timer = unit;
wenzelm@22563
    75
  fun startCPUTimer () = ();
wenzelm@22563
    76
  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
wenzelm@22563
    77
  fun checkGCTime () = Time.zeroTime;
wenzelm@22563
    78
end;
wenzelm@22563
    79
wenzelm@22563
    80
fun start_timing () =
wenzelm@22563
    81
  let val CPUtimer = Timer.startCPUTimer();
wenzelm@22563
    82
      val time = Timer.checkCPUTimer(CPUtimer)
wenzelm@22563
    83
  in  (CPUtimer,time)  end;
wenzelm@22563
    84
wenzelm@22563
    85
fun end_timing (CPUtimer, {sys,usr}) =
wenzelm@22563
    86
  let open Time  (*...for Time.toString, Time.+ and Time.- *)
wenzelm@22563
    87
      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
wenzelm@22563
    88
  in  "User " ^ toString (usr2-usr) ^
wenzelm@22563
    89
      "  All "^ toString (sys2-sys + usr2-usr) ^
wenzelm@22563
    90
      " secs"
wenzelm@22563
    91
      handle Time => ""
wenzelm@22563
    92
  end;
wenzelm@22563
    93
wenzelm@22563
    94
fun check_timer timer =
wenzelm@22563
    95
  let
wenzelm@22563
    96
    val {sys, usr} = Timer.checkCPUTimer timer;
wenzelm@22563
    97
    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
wenzelm@22563
    98
  in (sys, usr, gc) end;
wenzelm@22563
    99
wenzelm@22563
   100
wenzelm@22563
   101
(*prompts*)
wenzelm@22563
   102
fun ml_prompts p1 p2 = ();
wenzelm@22563
   103
wenzelm@22563
   104
(*dummy implementation*)
wenzelm@22563
   105
fun profile (n: int) f x = f x;
wenzelm@22563
   106
wenzelm@22563
   107
(*dummy implementation*)
wenzelm@22563
   108
fun exception_trace f = f ();
wenzelm@22563
   109
wenzelm@22563
   110
(*dummy implementation*)
wenzelm@22563
   111
fun print x = x;
wenzelm@22563
   112
wenzelm@22563
   113
wenzelm@24290
   114
(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
wenzelm@22563
   115
wenzelm@22563
   116
fun make_pp path pprint = (path, pprint);
wenzelm@22563
   117
fun install_pp (path, pp) = ();
wenzelm@22563
   118
wenzelm@22563
   119
wenzelm@22563
   120
(* ML command execution *)
wenzelm@22563
   121
wenzelm@26884
   122
fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ());
wenzelm@26884
   123
fun use_file _ _ _ _ name = use name;
wenzelm@22563
   124
wenzelm@22563
   125
wenzelm@22563
   126
wenzelm@22563
   127
(** interrupts **)
wenzelm@22563
   128
wenzelm@22563
   129
exception Interrupt;
wenzelm@22563
   130
wenzelm@26084
   131
fun interruptible f x = f x;
wenzelm@26084
   132
fun uninterruptible f x = f (fn (g: 'c -> 'd) => g) x;
wenzelm@22563
   133
wenzelm@22563
   134
wenzelm@22563
   135
(* basis library fixes *)
wenzelm@22563
   136
wenzelm@22563
   137
structure TextIO =
wenzelm@22563
   138
struct
wenzelm@22563
   139
  open TextIO;
wenzelm@23139
   140
  fun inputLine is = TextIO.inputLine is
wenzelm@22563
   141
    handle IO.Io _ => raise Interrupt;
wenzelm@22563
   142
end;
wenzelm@22563
   143
wenzelm@22563
   144
wenzelm@22563
   145
wenzelm@22563
   146
(** OS related **)
wenzelm@22563
   147
wenzelm@27004
   148
structure OS =
wenzelm@27004
   149
struct
wenzelm@27004
   150
  open OS;
wenzelm@27004
   151
  structure FileSys =
wenzelm@27004
   152
  struct
wenzelm@27004
   153
    open FileSys;
wenzelm@27004
   154
    fun tmpName () =
wenzelm@27004
   155
      let val name = FileSys.tmpName () in
wenzelm@27004
   156
        if String.isSuffix "\000" name
wenzelm@27004
   157
        then String.substring (name, 0, size name - 1)
wenzelm@27004
   158
        else name
wenzelm@27004
   159
      end;
wenzelm@27004
   160
  end;
wenzelm@27004
   161
end;
wenzelm@27004
   162
wenzelm@23826
   163
val cd = OS.FileSys.chDir;
wenzelm@23826
   164
val pwd = OS.FileSys.getDir;
wenzelm@23826
   165
wenzelm@26226
   166
local
wenzelm@26226
   167
wenzelm@26226
   168
fun read_file name =
wenzelm@26226
   169
  let val is = TextIO.openIn name
wenzelm@26504
   170
  in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end;
wenzelm@26226
   171
wenzelm@26226
   172
fun write_file name txt =
wenzelm@26226
   173
  let val os = TextIO.openOut name
wenzelm@26504
   174
  in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end;
wenzelm@26226
   175
wenzelm@26226
   176
in
wenzelm@26226
   177
wenzelm@26226
   178
fun system_out script =
wenzelm@26226
   179
  let
wenzelm@26226
   180
    val script_name = OS.FileSys.tmpName ();
wenzelm@26226
   181
    val _ = write_file script_name script;
wenzelm@26226
   182
wenzelm@26226
   183
    val output_name = OS.FileSys.tmpName ();
wenzelm@26226
   184
wenzelm@26226
   185
    val status =
wenzelm@26226
   186
      OS.Process.system ("perl -w \"$ISABELLE_HOME/lib/scripts/system.pl\" nogroup " ^
wenzelm@26226
   187
        script_name ^ " /dev/null " ^ output_name);
wenzelm@26226
   188
    val rc = if OS.Process.isSuccess status then 0 else 1;
wenzelm@26226
   189
wenzelm@26226
   190
    val output = read_file output_name handle IO.Io _ => "";
wenzelm@26226
   191
    val _ = OS.FileSys.remove script_name handle OS.SysErr _ => ();
wenzelm@26226
   192
    val _ = OS.FileSys.remove output_name handle OS.SysErr _ => ();
wenzelm@26226
   193
  in (output, rc) end;
wenzelm@26226
   194
wenzelm@26226
   195
end;
wenzelm@22563
   196
wenzelm@22563
   197
structure OS =
wenzelm@22563
   198
struct
wenzelm@22563
   199
  open OS;
wenzelm@22563
   200
  structure FileSys =
wenzelm@22563
   201
  struct
wenzelm@22563
   202
    fun fileId name =
wenzelm@26226
   203
      (case system_out ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
wenzelm@26226
   204
        ("", _) => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
wenzelm@26226
   205
      | (s, _) => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
wenzelm@22563
   206
    val compare = Int.compare;
wenzelm@27004
   207
    fun fullPath name =
wenzelm@27004
   208
      (case system_out ("FILE='" ^ name ^
wenzelm@27004
   209
        "' && cd \"$(dirname \"$FILE\")\" && echo -n \"$(pwd -P)/$(basename \"$FILE\")\"") of
wenzelm@27004
   210
        ("", _) => raise SysErr ("Bad file", NONE)
wenzelm@27004
   211
      | (s, _) => s);
wenzelm@22563
   212
    open FileSys;
wenzelm@22563
   213
  end;
wenzelm@22563
   214
end;
wenzelm@22563
   215
wenzelm@27004
   216
structure Posix =
wenzelm@27004
   217
struct
wenzelm@27004
   218
  structure ProcEnv =
wenzelm@27004
   219
  struct
wenzelm@27004
   220
    fun getpid () = raise Fail "Posix.ProcEnv.getpoid undefined";
wenzelm@27004
   221
  end;
wenzelm@27004
   222
end;
wenzelm@27004
   223
wenzelm@26227
   224
fun string_of_pid _ = raise Fail "string_of_pid undefined";
wenzelm@26227
   225
wenzelm@22563
   226
fun getenv var =
wenzelm@22563
   227
  (case OS.Process.getEnv var of
wenzelm@22563
   228
    NONE => ""
wenzelm@22563
   229
  | SOME txt => txt);