src/Tools/Metis/src/PortableMosml.sml
author blanchet
Mon, 13 Sep 2010 21:09:43 +0200
changeset 39348 6f9c9899f99f
child 39349 2d0a4361c3ef
permissions -rw-r--r--
new version of the Metis files
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* MOSCOW ML SPECIFIC FUNCTIONS                                              *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     3
(* Copyright (c) 2002 Joe Hurd, distributed under the GNU GPL version 2      *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
structure Portable :> Portable =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
struct
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
(* The ML implementation.                                                    *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
val ml = "mosml";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
(* Pointer equality using the run-time system.                               *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
  val address : 'a -> int = Obj.magic
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    22
  fun pointerEqual (x : 'a, y : 'a) = address x = address y
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    23
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    24
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    25
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    26
(* Timing function applications.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    29
val time = Mosml.time;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    30
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    31
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    32
(* Generating random values.                                                 *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    33
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    34
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    35
local
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    36
  val gen = Random.newgenseed 1.0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    37
in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    38
  fun randomInt max = Random.range (0,max) gen;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    39
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    40
  fun randomReal () = Random.random gen;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    41
end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    42
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    43
fun randomBool () = randomInt 2 = 0;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    44
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    45
fun randomWord () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    46
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    47
      val h = Word.fromInt (randomInt 65536)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    48
      and l = Word.fromInt (randomInt 65536)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
      Word.orb (Word.<< (h,0w16), l)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
(* Ensuring that interruptions (SIGINTs) are actually seen by the            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
(* linked executable as Interrupt exceptions.                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
val _ = catch_interrupt true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
(* Ad-hoc upgrading of the Moscow ML basis library.                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
fun Array_copy {src,dst,di} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
      copy {src = src, si = 0, len = NONE, dst = dst, di = di}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
fun Array_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
fun Array_foldri f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
      foldri f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
fun Array_modifyi f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
      modifyi f (a,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
fun OS_Process_isSuccess s = s = OS.Process.success;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
fun String_isSuffix p s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
      and sizeS = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
      sizeP <= sizeS andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
      String.extract (s, sizeS - sizeP, NONE) = p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
fun Substring_full s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
      open Substring
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
      all s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
fun TextIO_inputLine h =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
      open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
      case inputLine h of "" => NONE | s => SOME s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   118
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   119
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   120
fun Vector_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   121
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   122
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   123
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   124
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   125
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   126
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   127
fun Vector_mapi f v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   128
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   129
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   130
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   131
      mapi f (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   132
    end;