author | desharna |
Thu, 09 Jul 2020 11:39:16 +0200 | |
changeset 72004 | 913162a47d9f |
parent 39502 | cffceed8e7fa |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* MLTON SPECIFIC FUNCTIONS *) |
|
72004 | 3 |
(* Copyright (c) 2002 Joe Leslie-Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
structure Portable :> Portable = |
|
7 |
struct |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
10 |
(* The ML implementation. *) |
|
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
||
13 |
val ml = "mlton"; |
|
14 |
||
15 |
(* ------------------------------------------------------------------------- *) |
|
16 |
(* Pointer equality using the run-time system. *) |
|
17 |
(* ------------------------------------------------------------------------- *) |
|
18 |
||
19 |
val pointerEqual = MLton.eq; |
|
20 |
||
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 | 49 |
(* Timing function applications. *) |
50 |
(* ------------------------------------------------------------------------- *) |
|
51 |
||
52 |
fun time f x = |
|
53 |
let |
|
54 |
fun p t = |
|
55 |
let |
|
56 |
val s = Time.fmt 3 t |
|
57 |
in |
|
58 |
case size (List.last (String.fields (fn x => x = #".") s)) of |
|
59 |
3 => s |
|
60 |
| 2 => s ^ "0" |
|
61 |
| 1 => s ^ "00" |
|
62 |
| _ => raise Fail "Portable.time" |
|
63 |
end |
|
64 |
||
65 |
val c = Timer.startCPUTimer () |
|
66 |
||
67 |
val r = Timer.startRealTimer () |
|
68 |
||
69 |
fun pt () = |
|
70 |
let |
|
71 |
val {usr,sys} = Timer.checkCPUTimer c |
|
72 |
val real = Timer.checkRealTimer r |
|
73 |
in |
|
74 |
||
75 |
("User: " ^ p usr ^ " System: " ^ p sys ^ |
|
76 |
" Real: " ^ p real ^ "\n") |
|
77 |
end |
|
78 |
||
79 |
val y = f x handle e => (pt (); raise e) |
|
80 |
||
81 |
val () = pt () |
|
82 |
in |
|
83 |
y |
|
84 |
end; |
|
85 |
||
86 |
end |
|
87 |
||
88 |
(* ------------------------------------------------------------------------- *) |
|
89 |
(* Quotations a la Moscow ML. *) |
|
90 |
(* ------------------------------------------------------------------------- *) |
|
91 |
||
92 |
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a; |