src/Tools/Metis/src/PortableMosml.sml
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45778 df6e210fb44c
child 72004 913162a47d9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
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 = ()
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
    80
and print = ()
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
    81
and rev = ();
39443
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
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    84
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
(* Ad-hoc upgrading of the Moscow ML basis library.                          *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    86
(* ------------------------------------------------------------------------- *)
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_copy {src,dst,di} =
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
      copy {src = src, si = 0, len = NONE, dst = dst, di = di}
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 Array_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    96
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    97
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    98
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    99
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   100
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   101
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   102
fun Array_foldri f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   103
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   104
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   105
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   106
      foldri f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   107
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   108
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   109
fun Array_modifyi f a =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   110
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   111
      open Array
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   112
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   113
      modifyi f (a,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   114
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   115
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   116
fun OS_Process_isSuccess s = s = OS.Process.success;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   117
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   118
fun String_concatWith s =
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   119
    let
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   120
      fun add (x,l) = s :: x :: l
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   121
    in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   122
      fn [] => ""
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   123
       | x :: xs =>
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   124
         let
45778
df6e210fb44c updated Metis to 20110926 version
blanchet
parents: 42102
diff changeset
   125
           val xs = List.foldl add [] (List.rev xs)
42102
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   126
         in
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   127
           String.concat (x :: xs)
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   128
         end
fcfd07f122d4 new version of Metis 2.3 (29 Dec. 2010)
blanchet
parents: 39502
diff changeset
   129
    end;
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   130
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   131
fun String_isSubstring p s =
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   132
    let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   133
      val sizeP = size p
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   134
      and sizeS = size s
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   135
    in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   136
      if sizeP > sizeS then false
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   137
      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
   138
      else
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   139
        let
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   140
          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
   141
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   142
          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
   143
        in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   144
          checkn (sizeS - sizeP)
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
    end;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
   147
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   148
fun String_isSuffix p s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   149
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   150
      val sizeP = size p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   151
      and sizeS = size s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   152
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   153
      sizeP <= sizeS andalso
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   154
      String.extract (s, sizeS - sizeP, NONE) = p
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   155
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   156
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   157
fun Substring_full s =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   158
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   159
      open Substring
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   160
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   161
      all s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   162
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   163
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   164
fun TextIO_inputLine h =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   165
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   166
      open TextIO
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   167
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   168
      case inputLine h of "" => NONE | s => SOME s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   169
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   170
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   171
fun Vector_foldli f b v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   172
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   173
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   174
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   175
      foldli f b (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   176
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   177
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   178
fun Vector_mapi f v =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   179
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   180
      open Vector
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   181
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   182
      mapi f (v,0,NONE)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
   183
    end;