[ base ] Implemented Ord for Name, Namespace and UserName (#2973)

CHANGELOG.md

@@ -156,6 +156,9 @@
 
 * Add `zipPropertyWith` to `Data.Vect.Quantifiers.All.All`.
 
+* Implemented `Ord` for `Language.Reflection.TT.Name`, `Language.Reflection.TT.Namespace`
+  and `Language.Reflection.TT.UserName`.
+
 #### System
 
 * Changes `getNProcessors` to return the number of online processors rather than

libs/base/Language/Reflection/TT.idr

@@ -382,6 +382,65 @@ Eq Constant where
   WorldVal    == WorldVal    = True
   _ == _ = False
 
+public export
+Ord Namespace where
+    compare (MkNS ms) (MkNS ns) = compare ms ns
+
+usernameTag : UserName -> Int
+usernameTag (Basic _)  = 0
+usernameTag (Field _)  = 1
+usernameTag Underscore = 2
+
+public export
+Ord UserName where
+  compare (Basic x) (Basic y)   = compare x y
+  compare (Field x) (Field y)   = compare x y
+  compare Underscore Underscore = EQ
+  compare x y                   = compare (usernameTag x) (usernameTag y)
+
+nameTag : Name -> Int
+nameTag (NS _ _)        = 0
+nameTag (UN _)          = 1
+nameTag (MN _ _)        = 2
+nameTag (DN _ _)        = 3
+nameTag (Nested _ _)    = 4
+nameTag (CaseBlock _ _) = 5
+nameTag (WithBlock _ _) = 6
+
+public export
+Ord Name where
+    compare (NS x y) (NS x' y')
+        = case compare y y' of -- Compare base name first (more likely to differ)
+               EQ => compare x x'
+               -- Because of the terrible way Idris 1 compiles 'case', this
+               -- is actually faster than just having 't => t'...
+               GT => GT
+               LT => LT
+    compare (UN x) (UN y) = compare x y
+    compare (MN x y) (MN x' y')
+        = case compare y y' of
+               EQ => compare x x'
+               GT => GT
+               LT => LT
+    compare (DN _ n) (DN _ n') = compare n n'
+    compare (Nested x y) (Nested x' y')
+        = case compare y y' of
+               EQ => compare x x'
+               GT => GT
+               LT => LT
+    compare (CaseBlock x y) (CaseBlock x' y')
+        = case compare y y' of
+               EQ => compare x x'
+               GT => GT
+               LT => LT
+    compare (WithBlock x y) (WithBlock x' y')
+        = case compare y y' of
+               EQ => compare x x'
+               GT => GT
+               LT => LT
+
+    compare x y = compare (nameTag x) (nameTag y)
+
 export Injective MkNS where injective Refl = Refl
 
 public export