isabelle: src/Tools/Metis/src/PortableIsabelle.sml@a51430528fe0 (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
25717 7f0647c6362f using RandomWord from Isabelle/Pure gains factor 10-20 speedup; wenzelm parents: 25430 diff changeset	36	val randomWord = RandomWord.next;
7f0647c6362f using RandomWord from Isabelle/Pure gains factor 10-20 speedup; wenzelm parents: 25430 diff changeset	37	val randomBool = RandomWord.next_bit;
7f0647c6362f using RandomWord from Isabelle/Pure gains factor 10-20 speedup; wenzelm parents: 25430 diff changeset	38	fun randomInt n = Word.toInt (Word.mod (randomWord (), Word.fromInt n));
25430 372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	39
25719 a51430528fe0 tuned RandomWord signature; wenzelm parents: 25717 diff changeset	40	val normalizer = 1.0 / real RandomWord.range;
a51430528fe0 tuned RandomWord signature; wenzelm parents: 25717 diff changeset	41	fun randomReal () = real (Word.toInt (RandomWord.next ())) * normalizer;
25430 372d6749f00e patching in the latest changes from Hurd paulson parents: 24324 diff changeset	42
23442 028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	43	end
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	44
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	(* Quotations a la Moscow ML. *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	47	(* ------------------------------------------------------------------------- *)
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	48
028e39e5e8f3 The Metis prover (slightly modified version from Larry); wenzelm parents: diff changeset	49	datatype 'a frag = QUOTE of string \| ANTIQUOTE of 'a;

author	wenzelm
	Wed, 19 Dec 2007 23:42:20 +0100
changeset 25719	a51430528fe0
parent 25717	7f0647c6362f
child 25721	5ae1dc2bb5ea
permissions	-rw-r--r--