src/Tools/Metis/src/Portable.sig
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 39502 cffceed8e7fa
child 72004 913162a47d9f
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;

(* ========================================================================= *)
(* ML COMPILER SPECIFIC FUNCTIONS                                            *)
(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
(* ========================================================================= *)

signature Portable =
sig

(* ------------------------------------------------------------------------- *)
(* The ML implementation.                                                    *)
(* ------------------------------------------------------------------------- *)

val ml : string

(* ------------------------------------------------------------------------- *)
(* Pointer equality using the run-time system.                               *)
(* ------------------------------------------------------------------------- *)

val pointerEqual : 'a * 'a -> bool

(* ------------------------------------------------------------------------- *)
(* Marking critical sections of code.                                        *)
(* ------------------------------------------------------------------------- *)

val critical : (unit -> 'a) -> unit -> 'a

(* ------------------------------------------------------------------------- *)
(* Generating random values.                                                 *)
(* ------------------------------------------------------------------------- *)

val randomBool : unit -> bool

val randomInt : int -> int  (* n |-> [0,n) *)

val randomReal : unit -> real  (* () |-> [0,1] *)

val randomWord : unit -> Word.word

(* ------------------------------------------------------------------------- *)
(* Timing function applications.                                             *)
(* ------------------------------------------------------------------------- *)

val time : ('a -> 'b) -> 'a -> 'b

end