String.compare: slow version -- performance test;
authorwenzelm
Sat, 04 Nov 2006 19:25:43 +0100
changeset 21176 5ec545dbad6f
parent 21175 98c0405f5493
child 21177 e8228486aa03
String.compare: slow version -- performance test;
src/Pure/ML-Systems/polyml-4.9.1.ML
--- a/src/Pure/ML-Systems/polyml-4.9.1.ML	Sat Nov 04 19:25:41 2006 +0100
+++ b/src/Pure/ML-Systems/polyml-4.9.1.ML	Sat Nov 04 19:25:43 2006 +0100
@@ -9,3 +9,14 @@
 use "ML-Systems/polyml.ML";
 
 val pointer_eq = PolyML.pointerEq;
+
+(* FIXME slow version -- performance test *)
+structure String =
+struct
+  open String;
+
+  fun compare (s1: string, s2) =
+    if s1 = s2 then General.EQUAL
+    else if s1 < s2 then General.LESS
+    else General.GREATER;
+end;