isabelle: src/Tools/Metis/src/Portable.sig@e8552cba702d (annotated)

39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	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 cffceed8e7fa fix license blanchet parents: 39501 diff changeset	3	(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *)
39348 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	4	(* ========================================================================= *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	5
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	6	signature Portable =
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	7	sig
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	8
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	9	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	10	(* The ML implementation. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	11	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	12
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	13	val ml : string
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	14
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	15	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	16	(* Pointer equality using the run-time system. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	17	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	18
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	19	val pointerEqual : 'a * 'a -> bool
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	20
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	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 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	23	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	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 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	28	(* Generating random values. *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	29	(* ------------------------------------------------------------------------- *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	30
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	31	val randomBool : unit -> bool
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	32
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	33	val randomInt : int -> int (* n \|-> [0,n) *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	34
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	35	val randomReal : unit -> real (* () \|-> [0,1] *)
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	36
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	37	val randomWord : unit -> Word.word
6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	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 6f9c9899f99f new version of the Metis files blanchet parents: diff changeset	45	end

author	wenzelm
	Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389	e8552cba702d
parent 39502	cffceed8e7fa
child 72004	913162a47d9f
permissions	-rw-r--r--