(* ========================================================================= *)
(* Isabelle ML SPECIFIC FUNCTIONS *)
(* ========================================================================= *)
structure Portable :> Portable =
struct
(* ------------------------------------------------------------------------- *)
(* The ML implementation. *)
(* ------------------------------------------------------------------------- *)
val ml = ml_system;
(* ------------------------------------------------------------------------- *)
(* Pointer equality using the run-time system. *)
(* ------------------------------------------------------------------------- *)
val pointerEqual = pointer_eq;
(* ------------------------------------------------------------------------- *)
(* Timing function applications a la Mosml.time. *)
(* ------------------------------------------------------------------------- *)
val time = timeap;
(* ------------------------------------------------------------------------- *)
(* Critical section markup (multiprocessing) *)
(* ------------------------------------------------------------------------- *)
fun CRITICAL e = NAMED_CRITICAL "metis" e;
(* ------------------------------------------------------------------------- *)
(* Generating random values. *)
(* ------------------------------------------------------------------------- *)
val randomWord = Random_Word.next_word;
val randomBool = Random_Word.next_bool;
fun randomInt n = Random_Word.next_int 0 (n - 1);
val randomReal = Random_Word.next_real;
end;
(* ------------------------------------------------------------------------- *)
(* Quotations a la Moscow ML. *)
(* ------------------------------------------------------------------------- *)
datatype 'a frag = QUOTE of string | ANTIQUOTE of 'a;