isabelle: src/Tools/Metis/src/PortableIsabelle.sml@105f40051387 (annotated)

23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	1	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	2	(* Isabelle ML SPECIFIC FUNCTIONS *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	3	(* ========================================================================= *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	4
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	5	structure Portable :> Portable =
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	6	struct
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	7
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	8	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	9	(* The ML implementation. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	10	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	11
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	12	val ml = ml_system;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	13
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	14	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	15	(* Pointer equality using the run-time system. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	16	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	17
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	18	val pointerEqual = pointer_eq;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	19
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	20	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	21	(* Timing function applications a la Mosml.time. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	22	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	23
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	24	val time = timeap;
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	25
24316 3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	26	(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	27	(* Critical section markup (multiprocessing) *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	28	(* ------------------------------------------------------------------------- *)
3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	29
24324 9625e5bfa456 NAMED_CRITICAL; wenzelm parents: 24316 diff changeset	30	fun CRITICAL e = NAMED_CRITICAL "metis" e;
24316 3880d21d6013 added CRITICAL section markup; wenzelm parents: 23442 diff changeset	31
25430 372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	32	(* ------------------------------------------------------------------------- *)
372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	33	(* Generating random values. *)
372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	34	(* ------------------------------------------------------------------------- *)
372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	35
25743 6810d07f29de tuned RandomWord interface; wenzelm parents: 25721 diff changeset	36	val randomWord = RandomWord.next_word;
6810d07f29de tuned RandomWord interface; wenzelm parents: 25721 diff changeset	37	val randomBool = RandomWord.next_bool;
6810d07f29de tuned RandomWord interface; wenzelm parents: 25721 diff changeset	38	fun randomInt n = RandomWord.next_int 0 (n - 1);
6810d07f29de tuned RandomWord interface; wenzelm parents: 25721 diff changeset	39	val randomReal = RandomWord.next_real;
25430 372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	40
25743 6810d07f29de tuned RandomWord interface; wenzelm parents: 25721 diff changeset	41	end;
23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	42
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	43	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	44	(* Quotations a la Moscow ML. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	45	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	46
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	47	datatype 'a frag = QUOTE of string \| ANTIQUOTE of 'a;

author	wenzelm
	Fri, 02 Oct 2009 22:15:08 +0200
changeset 32861	105f40051387
parent 25743	6810d07f29de
child 33513	b2259183e282
permissions	-rw-r--r--