src/Tools/Metis/src/PortableMosml.sml
author wenzelm
Sun, 18 Sep 2011 13:39:33 +0200
changeset 44962 5554ed48b13f
parent 42102 fcfd07f122d4
child 45778 df6e210fb44c
permissions -rw-r--r--
finite sequences as useful as introductory example;
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                                              *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2002 Joe Hurd, distributed under the BSD License            *)
39348
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
(* ------------------------------------------------------------------------- *)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    26
(* Marking critical sections of code.                                        *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    27
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    28
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    29
fun critical f () = f ();
39429
126b879df319 move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents: 39353
diff changeset
    30
126b879df319 move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents: 39353
diff changeset
    31
(* ------------------------------------------------------------------------- *)
39348
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
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    53
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    54
(* Timing function applications.                                             *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    55
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    56
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    57
val time = Mosml.time;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    58
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
(* Ensuring that interruptions (SIGINTs) are actually seen by the            *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
(* linked executable as Interrupt exceptions.                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
prim_val catch_interrupt : bool -> unit = 1 "sys_catch_break";
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
val _ = catch_interrupt true;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
(* ------------------------------------------------------------------------- *)
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    70
(* Forcing fully qualified names of functions with generic names.            *)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    71
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    72
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    73
(*BasicDebug
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    74
val explode = ()
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    75
and foldl = ()
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    76
and foldr = ()
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    77
and implode = ()
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    78
and map = ()
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
    79
and null = ()
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    80
and print = ();
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    81
*)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    82
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    83
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
(* Ad-hoc upgrading of the Moscow ML basis library.                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    87
fun Array_copy {src,dst,di} =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    88
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
      copy {src = src, si = 0, len = NONE, dst = dst, di = di}
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    93
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    94
fun Array_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    95
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
fun Array_foldri f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
      foldri f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
fun Array_modifyi f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
      modifyi f (a,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
fun OS_Process_isSuccess s = s = OS.Process.success;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   117
fun String_concatWith s =
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   118
    let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   119
      fun add (x,l) = s :: x :: l
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   120
    in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   121
      fn [] => ""
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   122
       | x :: xs =>
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   123
         let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   124
           val xs = List.foldl add [] (rev xs)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   125
         in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   126
           String.concat (x :: xs)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   127
         end
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   128
    end;
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   129
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   130
fun String_isSubstring p s =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   131
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   132
      val sizeP = size p
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   133
      and sizeS = size s
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   134
    in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   135
      if sizeP > sizeS then false
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   136
      else if sizeP = sizeS then p = s
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   137
      else
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   138
        let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   139
          fun check i = String.substring (s,i,sizeP) = p
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   140
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   141
          fun checkn i = check i orelse (i > 0 andalso checkn (i - 1))
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   142
        in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   143
          checkn (sizeS - sizeP)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   144
        end
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   145
    end;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   146
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   147
fun String_isSuffix p s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
      and sizeS = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
      sizeP <= sizeS andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
      String.extract (s, sizeS - sizeP, NONE) = p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
fun Substring_full s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
      open Substring
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
      all s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
fun TextIO_inputLine h =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
      open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
      case inputLine h of "" => NONE | s => SOME s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
fun Vector_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
fun Vector_mapi f v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
      mapi f (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
    end;