src/Pure/ML-Systems/alice.ML
author wenzelm
Mon Oct 01 22:52:20 2007 +0200 (2007-10-01)
changeset 24809 41a21f59f74d
parent 24807 f66ab1dfbae1
child 26084 a7475459c740
permissions -rw-r--r--
integer compatibility: added wrapper for structure Time;
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@23826
     9
$ env ALICE_JIT_MODE=0 alice
wenzelm@23835
    10
- val ml_system = "alice";
wenzelm@24807
    11
- use "ML-Systems/exn.ML";
wenzelm@24807
    12
- use "ML-Systems/multithreading.ML";
wenzelm@24807
    13
- use "ML-Systems/time_limit.ML";
wenzelm@23826
    14
- use "ML-Systems/alice.ML";
wenzelm@23826
    15
- use "ROOT.ML";
wenzelm@23826
    16
- Session.finish ();
wenzelm@22563
    17
*)
wenzelm@22563
    18
wenzelm@24597
    19
val ml_system_fix_ints = false;
wenzelm@24597
    20
wenzelm@22563
    21
fun exit 0 = (OS.Process.exit OS.Process.success): unit
wenzelm@22563
    22
  | exit _ = OS.Process.exit OS.Process.failure;
wenzelm@22563
    23
wenzelm@22563
    24
wenzelm@22563
    25
(** ML system related **)
wenzelm@22563
    26
wenzelm@22563
    27
(*low-level pointer equality*)
wenzelm@22563
    28
fun pointer_eq (_: 'a, _: 'a) = false;
wenzelm@22563
    29
wenzelm@24809
    30
wenzelm@24809
    31
(* integer compatibility -- downgraded IntInf *)
wenzelm@24809
    32
wenzelm@24809
    33
structure Time =
wenzelm@24809
    34
struct
wenzelm@24809
    35
  open Time;
wenzelm@24809
    36
  val fromMilliseconds = Time.fromMilliseconds o IntInf.fromInt;
wenzelm@24809
    37
  val fromSeconds = Time.fromSeconds o IntInf.fromInt;
wenzelm@24809
    38
end;
wenzelm@24809
    39
wenzelm@24807
    40
structure IntInf =
wenzelm@24807
    41
struct
wenzelm@24807
    42
  fun divMod (x, y) = (x div y, x mod y);
wenzelm@24807
    43
  open Int;
wenzelm@24807
    44
end;
wenzelm@24807
    45
wenzelm@22563
    46
wenzelm@22563
    47
(* restore old-style character / string functions *)
wenzelm@22563
    48
wenzelm@22563
    49
exception Ord;
wenzelm@22563
    50
fun ord "" = raise Ord
wenzelm@22563
    51
  | ord s = Char.ord (String.sub (s, 0));
wenzelm@22563
    52
wenzelm@22575
    53
val chr = String.str o chr;
wenzelm@22575
    54
val explode = map String.str o String.explode;
wenzelm@22563
    55
val implode = String.concat;
wenzelm@22563
    56
wenzelm@22563
    57
wenzelm@22563
    58
(* Poly/ML emulation *)
wenzelm@22563
    59
wenzelm@22563
    60
fun quit () = exit 0;
wenzelm@22563
    61
wenzelm@24329
    62
fun get_print_depth () = ! Print.depth;
wenzelm@22563
    63
fun print_depth n = Print.depth := n;
wenzelm@22563
    64
wenzelm@22563
    65
wenzelm@22563
    66
(* compiler-independent timing functions *)
wenzelm@22563
    67
wenzelm@22563
    68
structure Timer =
wenzelm@22563
    69
struct
wenzelm@22563
    70
  open Timer;
wenzelm@22563
    71
  type cpu_timer = unit;
wenzelm@22563
    72
  fun startCPUTimer () = ();
wenzelm@22563
    73
  fun checkCPUTimer () = {sys = Time.zeroTime, usr = Time.zeroTime};
wenzelm@22563
    74
  fun checkGCTime () = Time.zeroTime;
wenzelm@22563
    75
end;
wenzelm@22563
    76
wenzelm@22563
    77
fun start_timing () =
wenzelm@22563
    78
  let val CPUtimer = Timer.startCPUTimer();
wenzelm@22563
    79
      val time = Timer.checkCPUTimer(CPUtimer)
wenzelm@22563
    80
  in  (CPUtimer,time)  end;
wenzelm@22563
    81
wenzelm@22563
    82
fun end_timing (CPUtimer, {sys,usr}) =
wenzelm@22563
    83
  let open Time  (*...for Time.toString, Time.+ and Time.- *)
wenzelm@22563
    84
      val {sys=sys2,usr=usr2} = Timer.checkCPUTimer(CPUtimer)
wenzelm@22563
    85
  in  "User " ^ toString (usr2-usr) ^
wenzelm@22563
    86
      "  All "^ toString (sys2-sys + usr2-usr) ^
wenzelm@22563
    87
      " secs"
wenzelm@22563
    88
      handle Time => ""
wenzelm@22563
    89
  end;
wenzelm@22563
    90
wenzelm@22563
    91
fun check_timer timer =
wenzelm@22563
    92
  let
wenzelm@22563
    93
    val {sys, usr} = Timer.checkCPUTimer timer;
wenzelm@22563
    94
    val gc = Timer.checkGCTime timer;    (* FIXME already included in usr? *)
wenzelm@22563
    95
  in (sys, usr, gc) end;
wenzelm@22563
    96
wenzelm@22563
    97
wenzelm@22563
    98
(*prompts*)
wenzelm@22563
    99
fun ml_prompts p1 p2 = ();
wenzelm@22563
   100
wenzelm@22563
   101
(*dummy implementation*)
wenzelm@22563
   102
fun profile (n: int) f x = f x;
wenzelm@22563
   103
wenzelm@22563
   104
(*dummy implementation*)
wenzelm@22563
   105
fun exception_trace f = f ();
wenzelm@22563
   106
wenzelm@22563
   107
(*dummy implementation*)
wenzelm@22563
   108
fun print x = x;
wenzelm@22563
   109
wenzelm@22563
   110
wenzelm@24290
   111
(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
wenzelm@22563
   112
wenzelm@22563
   113
fun make_pp path pprint = (path, pprint);
wenzelm@22563
   114
fun install_pp (path, pp) = ();
wenzelm@22563
   115
wenzelm@22563
   116
wenzelm@22563
   117
(* ML command execution *)
wenzelm@22563
   118
wenzelm@24807
   119
fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ());
wenzelm@22563
   120
wenzelm@24807
   121
fun use_file tune output verbose name = use name;
wenzelm@22563
   122
wenzelm@22563
   123
wenzelm@22563
   124
wenzelm@22563
   125
(** interrupts **)
wenzelm@22563
   126
wenzelm@22563
   127
exception Interrupt;
wenzelm@22563
   128
wenzelm@22563
   129
fun ignore_interrupt f x = f x;
wenzelm@22563
   130
fun raise_interrupt f x = f x;
wenzelm@22563
   131
wenzelm@22563
   132
wenzelm@22563
   133
(* basis library fixes *)
wenzelm@22563
   134
wenzelm@22563
   135
structure TextIO =
wenzelm@22563
   136
struct
wenzelm@22563
   137
  open TextIO;
wenzelm@23139
   138
  fun inputLine is = TextIO.inputLine is
wenzelm@22563
   139
    handle IO.Io _ => raise Interrupt;
wenzelm@22563
   140
end;
wenzelm@22563
   141
wenzelm@22563
   142
wenzelm@22563
   143
wenzelm@22563
   144
(** OS related **)
wenzelm@22563
   145
wenzelm@23826
   146
(* current directory *)
wenzelm@23826
   147
wenzelm@23826
   148
val cd = OS.FileSys.chDir;
wenzelm@23826
   149
val pwd = OS.FileSys.getDir;
wenzelm@23826
   150
wenzelm@23826
   151
wenzelm@22563
   152
(* system command execution *)
wenzelm@22563
   153
wenzelm@22563
   154
(*execute Unix command which doesn't take any input from stdin and
wenzelm@22563
   155
  sends its output to stdout; could be done more easily by Unix.execute,
wenzelm@22563
   156
  but that function doesn't use the PATH*)
wenzelm@22563
   157
fun execute command =
wenzelm@22563
   158
  let
wenzelm@22563
   159
    val tmp_name = OS.FileSys.tmpName ();
wenzelm@22563
   160
    val is = (OS.Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
wenzelm@22563
   161
    val result = TextIO.inputAll is;
wenzelm@22563
   162
  in
wenzelm@22563
   163
    TextIO.closeIn is;
wenzelm@22563
   164
    OS.FileSys.remove tmp_name;
wenzelm@22563
   165
    result
wenzelm@22563
   166
  end;
wenzelm@22563
   167
wenzelm@22563
   168
(*plain version; with return code*)
wenzelm@22563
   169
val system = OS.Process.system: string -> int;
wenzelm@22563
   170
wenzelm@22563
   171
structure OS =
wenzelm@22563
   172
struct
wenzelm@22563
   173
  open OS;
wenzelm@22563
   174
  structure FileSys =
wenzelm@22563
   175
  struct
wenzelm@22563
   176
    fun fileId name =
wenzelm@22563
   177
      (case execute ("perl -e '@_ = stat(q:" ^ name ^ ":); print $_[1]'") of
wenzelm@22563
   178
        "" => raise Fail "OS.FileSys.fileId"   (* FIXME IO.Io!? *)
wenzelm@22563
   179
      | s => (case Int.fromString s of NONE => raise Fail "OS.FileSys.fileId" | SOME i => i));
wenzelm@22563
   180
    val compare = Int.compare;
wenzelm@22563
   181
    open FileSys;
wenzelm@22563
   182
  end;
wenzelm@22563
   183
end;
wenzelm@22563
   184
wenzelm@22563
   185
wenzelm@22563
   186
(* getenv *)
wenzelm@22563
   187
wenzelm@22563
   188
fun getenv var =
wenzelm@22563
   189
  (case OS.Process.getEnv var of
wenzelm@22563
   190
    NONE => ""
wenzelm@22563
   191
  | SOME txt => txt);