1 (* ========================================================================= *) |
|
2 (* Isabelle ML SPECIFIC FUNCTIONS *) |
|
3 (* ========================================================================= *) |
|
4 |
|
5 structure Portable :> Portable = |
|
6 struct |
|
7 |
|
8 (* ------------------------------------------------------------------------- *) |
|
9 (* The ML implementation. *) |
|
10 (* ------------------------------------------------------------------------- *) |
|
11 |
|
12 val ml = ml_system; |
|
13 |
|
14 (* ------------------------------------------------------------------------- *) |
|
15 (* Pointer equality using the run-time system. *) |
|
16 (* ------------------------------------------------------------------------- *) |
|
17 |
|
18 val pointerEqual = pointer_eq; |
|
19 |
|
20 (* ------------------------------------------------------------------------- *) |
|
21 (* Timing function applications a la Mosml.time. *) |
|
22 (* ------------------------------------------------------------------------- *) |
|
23 |
|
24 val time = timeap; |
|
25 |
|
26 (* ------------------------------------------------------------------------- *) |
|
27 (* Critical section markup (multiprocessing) *) |
|
28 (* ------------------------------------------------------------------------- *) |
|
29 |
|
30 fun CRITICAL e = NAMED_CRITICAL "metis" e; |
|
31 |
|
32 (* ------------------------------------------------------------------------- *) |
|
33 (* Generating random values. *) |
|
34 (* ------------------------------------------------------------------------- *) |
|
35 |
|
36 val randomWord = Random_Word.next_word; |
|
37 val randomBool = Random_Word.next_bool; |
|
38 fun randomInt n = Random_Word.next_int 0 (n - 1); |
|
39 val randomReal = Random_Word.next_real; |
|
40 |
|
41 end; |
|
42 |
|
43 (* ------------------------------------------------------------------------- *) |
|
44 (* Quotations a la Moscow ML. *) |
|
45 (* ------------------------------------------------------------------------- *) |
|
46 |
|
47 datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a; |
|