author | wenzelm |
Tue, 26 Mar 2019 13:25:32 +0100 | |
changeset 69988 | 6fa51a36b7f7 |
parent 39502 | cffceed8e7fa |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
2 |
(* POLY/ML SPECIFIC FUNCTIONS *) |
|
39502 | 3 |
(* Copyright (c) 2008 Joe 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 = "polyml"; |
|
14 |
||
15 |
(* ------------------------------------------------------------------------- *) |
|
16 |
(* Pointer equality using the run-time system. *) |
|
17 |
(* ------------------------------------------------------------------------- *) |
|
18 |
||
19 |
fun pointerEqual (x : 'a, y : 'a) = PolyML.pointerEq(x,y); |
|
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 |
val randomWord = Random.nextWord; |
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 |
val randomBool = Random.nextBool; |
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 |
val randomInt = Random.nextInt; |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
36 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
37 |
val randomReal = Random.nextReal; |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
38 |
|
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
39 |
(* ------------------------------------------------------------------------- *) |
39348 | 40 |
(* Timing function applications. *) |
41 |
(* ------------------------------------------------------------------------- *) |
|
42 |
||
43 |
fun time f x = |
|
44 |
let |
|
45 |
fun p t = |
|
46 |
let |
|
47 |
val s = Time.fmt 3 t |
|
48 |
in |
|
49 |
case size (List.last (String.fields (fn x => x = #".") s)) of |
|
50 |
3 => s |
|
51 |
| 2 => s ^ "0" |
|
52 |
| 1 => s ^ "00" |
|
53 |
| _ => raise Fail "Portable.time" |
|
54 |
end |
|
55 |
||
56 |
val c = Timer.startCPUTimer () |
|
57 |
||
58 |
val r = Timer.startRealTimer () |
|
59 |
||
60 |
fun pt () = |
|
61 |
let |
|
62 |
val {usr,sys} = Timer.checkCPUTimer c |
|
63 |
val real = Timer.checkRealTimer r |
|
64 |
in |
|
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
65 |
|
39348 | 66 |
("User: " ^ p usr ^ " System: " ^ p sys ^ |
67 |
" Real: " ^ p real ^ "\n") |
|
68 |
end |
|
69 |
||
70 |
val y = f x handle e => (pt (); raise e) |
|
71 |
||
72 |
val () = pt () |
|
73 |
in |
|
74 |
y |
|
75 |
end; |
|
76 |
||
77 |
end |
|
78 |
||
79 |
(* ------------------------------------------------------------------------- *) |
|
80 |
(* Quotations a la Moscow ML. *) |
|
81 |
(* ------------------------------------------------------------------------- *) |
|
82 |
||
83 |
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a; |