src/Tools/Metis/src/PortableMosml.sml
author wenzelm
Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861 105f40051387
parent 25430 372d6749f00e
child 39353 7f11d833d65b
permissions -rw-r--r--
eliminated dead code;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     1
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     2
(* MOSCOW ML SPECIFIC FUNCTIONS                                              *)
23510
4521fead5609 GPL -> BSD
paulson
parents: 23442
diff changeset
     3
(* Copyright (c) 2002-2004 Joe Hurd, distributed under the BSD License *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     4
(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     5
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     6
structure Portable :> Portable =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     7
struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     8
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    10
(* The ML implementation.                                                    *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    12
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    13
val ml = "mosml";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    14
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    16
(* Pointer equality using the run-time system.                               *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    18
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    19
local
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    20
  val address : 'a -> int = Obj.magic
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    21
in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    22
  fun pointerEqual (x : 'a, y : 'a) = address x = address y
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    23
end;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    24
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    26
(* Timing function applications.                                             *)
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    27
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    28
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    29
val time = Mosml.time;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    30
24316
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    31
(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    32
(* Critical section markup (multiprocessing)                                 *)
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    33
(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    34
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    35
fun CRITICAL e = e ();     (*dummy*)
3880d21d6013 added CRITICAL section markup;
wenzelm
parents: 23510
diff changeset
    36
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    37
(* ------------------------------------------------------------------------- *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    38
(* Generating random values.                                                 *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    39
(* ------------------------------------------------------------------------- *)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    40
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    41
local
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    42
  val gen = Random.newgenseed 1.0;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    43
in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    44
  fun randomInt max = Random.range (0,max) gen;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    45
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    46
  fun randomReal () = Random.random gen;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    47
end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    48
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    49
fun randomBool () = randomInt 2 = 0;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    50
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    51
fun randomWord () =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    52
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    53
      val h = Word.fromInt (randomInt 65536)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    54
      and l = Word.fromInt (randomInt 65536)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    55
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    56
      Word.orb (Word.<< (h,0w16), l)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    57
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    58
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    59
end
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    60
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    61
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    62
(* Ensuring that interruptions (SIGINTs) are actually seen by the            *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    63
(* linked executable as Interrupt exceptions.                                *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    64
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    65
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    66
prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break";
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    67
val _ = catch_interrupt true;
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    68
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    69
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    70
(* Ad-hoc upgrading of the Moscow ML basis library.                          *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    71
(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
    72
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    73
fun Array_copy {src,dst,di} =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    74
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    75
      open Array
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    76
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    77
      copy {src = src, si = 0, len = NONE, dst = dst, di = di}
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    78
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    79
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    80
fun Array_foldli f b v =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    81
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    82
      open Array
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    83
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    84
      foldli f b (v,0,NONE)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    85
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    86
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    87
fun Array_foldri f b v =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    88
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    89
      open Array
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    90
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    91
      foldri f b (v,0,NONE)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    92
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    93
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    94
fun Array_modifyi f a =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    95
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    96
      open Array
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    97
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    98
      modifyi f (a,0,NONE)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
    99
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   100
23442
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   101
fun TextIO_inputLine h =
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   102
    let
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   103
      open TextIO
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   104
    in
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   105
      case inputLine h of "" => NONE | s => SOME s
028e39e5e8f3 The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff changeset
   106
    end;
25430
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   107
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   108
fun Vector_foldli f b v =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   109
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   110
      open Vector
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   111
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   112
      foldli f b (v,0,NONE)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   113
    end;
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   114
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   115
fun Vector_mapi f v =
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   116
    let
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   117
      open Vector
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   118
    in
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   119
      mapi f (v,0,NONE)
372d6749f00e patching in the latest changes from Hurd
paulson
parents: 24316
diff changeset
   120
    end;