author | blanchet |
Wed, 27 Aug 2014 08:41:12 +0200 | |
changeset 58043 | a90847f03ec8 |
parent 39502 | cffceed8e7fa |
child 72004 | 913162a47d9f |
permissions | -rw-r--r-- |
39348 | 1 |
(* ========================================================================= *) |
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
2 |
(* ML COMPILER SPECIFIC FUNCTIONS *) |
39502 | 3 |
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) |
39348 | 4 |
(* ========================================================================= *) |
5 |
||
6 |
signature Portable = |
|
7 |
sig |
|
8 |
||
9 |
(* ------------------------------------------------------------------------- *) |
|
10 |
(* The ML implementation. *) |
|
11 |
(* ------------------------------------------------------------------------- *) |
|
12 |
||
13 |
val ml : string |
|
14 |
||
15 |
(* ------------------------------------------------------------------------- *) |
|
16 |
(* Pointer equality using the run-time system. *) |
|
17 |
(* ------------------------------------------------------------------------- *) |
|
18 |
||
19 |
val pointerEqual : 'a * 'a -> bool |
|
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. *) |
39348 | 23 |
(* ------------------------------------------------------------------------- *) |
24 |
||
39443
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
25 |
val critical : (unit -> 'a) -> unit -> 'a |
39429
126b879df319
move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents:
39353
diff
changeset
|
26 |
|
126b879df319
move "CRITICAL" to "PortableXxx", where it belongs and used to be;
blanchet
parents:
39353
diff
changeset
|
27 |
(* ------------------------------------------------------------------------- *) |
39348 | 28 |
(* Generating random values. *) |
29 |
(* ------------------------------------------------------------------------- *) |
|
30 |
||
31 |
val randomBool : unit -> bool |
|
32 |
||
33 |
val randomInt : int -> int (* n |-> [0,n) *) |
|
34 |
||
35 |
val randomReal : unit -> real (* () |-> [0,1] *) |
|
36 |
||
37 |
val randomWord : unit -> Word.word |
|
38 |
||
39443
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 |
(* Timing function applications. *) |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
41 |
(* ------------------------------------------------------------------------- *) |
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 time : ('a -> 'b) -> 'a -> 'b |
e330437cd22a
copied the unmodified official Metis 2.3 (15 Sept. 2010) sources into Isabelle
blanchet
parents:
39429
diff
changeset
|
44 |
|
39348 | 45 |
end |