--- /dev/null
+implementation module GenLexOrd\r
+\r
+import StdEnv\r
+import StdGeneric, GenEq\r
+\r
+:: LexOrd = LT |EQ | GT\r
+derive gEq LexOrd\r
+\r
+generic gLexOrd a b :: a b -> LexOrd\r
+gLexOrd{|Int|} x y\r
+ | x == y = EQ\r
+ | x < y = LT\r
+ = GT\r
+gLexOrd{|Bool|} True True = EQ\r
+gLexOrd{|Bool|} False True = LT\r
+gLexOrd{|Bool|} True False = GT\r
+gLexOrd{|Bool|} False False = EQ\r
+gLexOrd{|Real|} x y\r
+ | x == y = EQ\r
+ | x < y = LT\r
+ = GT\r
+gLexOrd{|Char|} x y\r
+ | x == y = EQ\r
+ | x < y = LT\r
+ = GT\r
+gLexOrd{|String|} x y\r
+ | x == y = EQ\r
+ | x < y = LT\r
+ = GT \r
+gLexOrd{|UNIT|} UNIT UNIT = EQ\r
+gLexOrd{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = case fx x1 x2 of\r
+ EQ -> fy y1 y2\r
+ LT -> LT\r
+ GT -> GT\r
+ \r
+gLexOrd{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y \r
+gLexOrd{|EITHER|} fl fr (LEFT x) (RIGHT y) = LT\r
+gLexOrd{|EITHER|} fl fr (RIGHT x) (LEFT y) = GT\r
+gLexOrd{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y\r
+gLexOrd{|CONS|} f (CONS x) (CONS y) = f x y\r
+gLexOrd{|FIELD|} f (FIELD x) (FIELD y) = f x y\r
+gLexOrd{|OBJECT|} f (OBJECT x) (OBJECT y) = f x y\r
+\r
+// Instance on standard lists is needed because\r
+// standard lists have unnatural internal ordering of constructors: Cons < Nil,\r
+// i.e Cons is LEFT and Nil is RIGHT in the generic representation.\r
+// We want ordering Nil < Cons\r
+gLexOrd{|[]|} f [] [] = EQ\r
+gLexOrd{|[]|} f [] _ = LT\r
+gLexOrd{|[]|} f _ [] = GT\r
+gLexOrd{|[]|} f [x:xs] [y:ys] = gLexOrd{|*->*->*|} f (gLexOrd{|*->*|} f) (PAIR x xs) (PAIR y ys)\r
+\r
+gLexOrd{|{}|} f xs ys = lexOrdArray f xs ys \r
+gLexOrd{|{!}|} f xs ys = lexOrdArray f xs ys \r
+\r
+\r
+// standard types\r
+derive gLexOrd (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,)\r
+\r
+ \r
+(=?=) infix 4 :: a a -> LexOrd | gLexOrd{|*|} a\r
+(=?=) x y = gLexOrd{|*|} x y \r
+\r
+\r
+lexOrdArray f xs ys\r
+ #! size_xs = size xs\r
+ #! size_ys = size ys\r
+ | size_xs < size_ys = LT\r
+ | size_xs > size_ys = GT\r
+ | otherwise = lexord 0 size_xs xs ys\r
+where\r
+ lexord i n xs ys\r
+ | i == n = EQ\r
+ | otherwise = case f xs.[i] ys.[i] of\r
+ LT -> LT\r
+ GT -> GT \r
+ EQ -> lexord (inc i) n xs ys\r