src/Tools/Metis/src/PortableMlton.sml
author desharna
Thu, 09 Jul 2020 11:39:16 +0200
changeset 72004 913162a47d9f
parent 39502 cffceed8e7fa
permissions -rw-r--r--
Update Metis to 2.4
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
(* MLTON SPECIFIC FUNCTIONS                                                  *)
72004
913162a47d9f Update Metis to 2.4
desharna
parents: 39502
diff changeset
     3
(* Copyright (c) 2002 Joe Leslie-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 = "mlton";
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
val pointerEqual = MLton.eq;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    20
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    21
(* ------------------------------------------------------------------------- *)
39443
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    22
(* Marking critical sections of code.                                        *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    23
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    24
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    25
fun critical f () = f ();
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    26
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    27
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    28
(* Generating random values.                                                 *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    29
(* ------------------------------------------------------------------------- *)
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    30
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    31
fun randomWord () = MLton.Random.rand ();
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    32
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    33
fun randomBool () = Word.andb (randomWord (),0w1) = 0w0;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    34
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    35
fun randomInt 1 = 0
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    36
  | randomInt 2 = Word.toInt (Word.andb (randomWord (), 0w1))
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    37
  | randomInt 4 = Word.toInt (Word.andb (randomWord (), 0w3))
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    38
  | randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    39
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    40
local
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    41
  fun wordToReal w = Real.fromInt (Word.toInt (Word.>> (w,0w1)))
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    42
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    43
  val normalizer = 1.0 / wordToReal (Word.notb 0w0);
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    44
in
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    45
  fun randomReal () = normalizer * wordToReal (randomWord ());
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    46
end;
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    47
e330437cd22a copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents: 39429
diff changeset
    48
(* ------------------------------------------------------------------------- *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    49
(* Timing function applications.                                             *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    50
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    51
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    52
fun time f x =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    53
    let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    54
      fun p t =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    55
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    56
            val s = Time.fmt 3 t
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    57
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    58
            case size (List.last (String.fields (fn x => x = #".") s)) of
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    59
              3 => s
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    60
            | 2 => s ^ "0"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    61
            | 1 => s ^ "00"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    62
            | _ => raise Fail "Portable.time"
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    63
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    64
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    65
      val c = Timer.startCPUTimer ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    66
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    67
      val r = Timer.startRealTimer ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    68
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    69
      fun pt () =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    70
          let
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    71
            val {usr,sys} = Timer.checkCPUTimer c
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    72
            val real = Timer.checkRealTimer r
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    73
          in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    74
            print
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    75
              ("User: " ^ p usr ^ "  System: " ^ p sys ^
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    76
               "  Real: " ^ p real ^ "\n")
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    77
          end
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    78
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    79
      val y = f x handle e => (pt (); raise e)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    80
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    81
      val () = pt ()
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    82
    in
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    83
      y
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    84
    end;
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    85
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
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    89
(* Quotations a la Moscow ML.                                                *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    90
(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    91
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    92
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;