src/Pure/ML-Systems/mosml.ML
author wenzelm
Sat, 11 Jun 2005 23:17:28 +0200
changeset 16374 f4b7cf8975af
parent 16266 7a6616be8712
child 16469 7e27422c603e
permissions -rw-r--r--
some cygwin support;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/mosml.ML
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     4
    Copyright   1999  University of Cambridge
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     5
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     6
Compatibility file for Moscow ML 2.00
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     7
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     8
NOTE: saving images does not work (yet!?), may run it interactively as follows:
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
     9
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    10
$ cd .../Pure
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    11
$ isabelle RAW_ML_SYSTEM
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    12
> val ml_system = "mosml";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    13
> use "ML-Systems/mosml.ML";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    14
> use "ROOT.ML";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    15
*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    16
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    17
(** ML system related **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    18
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    19
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    20
(* Poly/ML emulation *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    21
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    22
load "Bool";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    23
load "Int";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    24
load "Real";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    25
load "ListPair";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    26
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    27
load "OS";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    28
load "Process";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    29
load "FileSys";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    30
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    31
structure OS =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    32
  struct
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    33
  open OS
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    34
  structure Process = Process
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    35
  structure FileSys = FileSys
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    36
  end;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    37
 
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    38
(*To exit the system with an exit code -- an alternative to ^D *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    39
fun exit 0 = Process.exit Process.success
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    40
  | exit _ = Process.exit Process.failure;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    41
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    42
(*limit the printing depth*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    43
fun print_depth n =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    44
 (Meta.printDepth := n div 2;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    45
  Meta.printLength := n);
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    46
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    47
(*interface for toplevel pretty printers, see also Pure/install_pp.ML*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    48
(*the documentation refers to an installPP but I couldn't fine it!*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    49
fun make_pp path pprint = ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    50
fun install_pp _ = ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    51
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    52
(*prompts*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    53
(*n.a.??*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    54
fun ml_prompts p1 p2 = ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    55
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    56
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    57
(** Compiler-independent timing functions **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    58
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    59
load "Timer";
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    60
14519
4ca3608fdf4f Added support for the newer versions of SML/NJ, which break several of the
skalberg
parents: 12988
diff changeset
    61
use "ML-Systems/cpu-timer-gc.ML";
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    62
14851
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    63
(* bounded time execution *)
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    64
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    65
(* FIXME proper implementation available? *)
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    66
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    67
structure TimeLimit : sig
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    68
   exception TimeOut
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    69
   val timeLimit : Time.time -> ('a -> 'b) -> 'a -> 'b
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    70
end = struct
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    71
   exception TimeOut
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    72
   fun timeLimit t f x =
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    73
      f x;
0fc75361e0c7 TimeLimit structure added (no proper implementation yet)
webertj
parents: 14519
diff changeset
    74
end;
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    75
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    76
(* ML command execution *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    77
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    78
(*Can one redirect 'use' directly to an instream?*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    79
fun use_text _ _ txt =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    80
  let
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    81
    val tmp_name = FileSys.tmpName ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    82
    val tmp_file = TextIO.openOut tmp_name;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    83
  in
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    84
    TextIO.output (tmp_file, txt);
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    85
    TextIO.closeOut tmp_file;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    86
    use tmp_name;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    87
    FileSys.remove tmp_name
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    88
  end;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    89
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    90
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    91
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    92
(** interrupts **)	(*Note: may get into race conditions*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    93
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    94
(* FIXME proper implementation available? *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    95
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    96
exception Interrupt;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
    97
12988
2112f9e337bb renamed mask_interrupt to ignore_interrupt;
wenzelm
parents: 12896
diff changeset
    98
fun ignore_interrupt f x = f x;           
2112f9e337bb renamed mask_interrupt to ignore_interrupt;
wenzelm
parents: 12896
diff changeset
    99
fun raise_interrupt f x = f x;
9254
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   100
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   101
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   102
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   103
(** OS related **)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   104
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   105
(* system command execution *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   106
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   107
(*execute Unix command which doesn't take any input from stdin and
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   108
  sends its output to stdout; could be done more easily by Unix.execute,
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   109
  but that function doesn't use the PATH*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   110
fun execute command =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   111
  let
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   112
    val tmp_name = FileSys.tmpName ();
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   113
    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn 
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   114
tmp_name);
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   115
    val result = TextIO.inputAll is;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   116
  in
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   117
    TextIO.closeIn is;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   118
    FileSys.remove tmp_name;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   119
    result
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   120
  end;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   121
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   122
(*plain version; with return code*)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   123
fun system cmd =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   124
  if Process.system cmd = Process.success then 0 else 1;
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   125
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   126
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   127
(* getenv *)
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   128
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   129
fun getenv var =
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   130
  (case Process.getEnv var of
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   131
    NONE => ""
f8a0e8b9bcd8 Compatibility file for Moscow ML 2.00;
wenzelm
parents:
diff changeset
   132
  | SOME txt => txt);