proper implementation of pointer_eq;
authorwenzelm
Tue, 21 Jun 2005 18:55:57 +0200
changeset 16517 4699288139f4
parent 16516 0842635545c3
child 16518 086c6a97f340
proper implementation of pointer_eq;
src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Tue Jun 21 18:55:44 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Tue Jun 21 18:55:57 2005 +0200
@@ -19,12 +19,7 @@
 
 (** ML system related **)
 
-(*proper implementation available?*)
-fun pointer_eq (x:''a, y) = false;
-
-
-(* Poly/ML emulation *)
-
+load "Obj";
 load "Bool";
 load "Int";
 load "Real";
@@ -33,6 +28,10 @@
 load "Process";
 load "FileSys";
 
+(*low-level pointer equality*)
+local val cast : 'a -> int = Obj.magic
+in fun pointer_eq (x:'a, y:'a) = (cast x = cast y) end;
+
 (*proper implementation available?*)
 structure IntInf =
 struct
@@ -93,6 +92,7 @@
       f x;
 end;
 
+
 (* ML command execution *)
 
 (*Can one redirect 'use' directly to an instream?*)