Prelude.EqOrd


   0 | module Prelude.EqOrd
   1 | 
   2 | import Builtin
   3 | import Prelude.Basics
   4 | 
   5 | %default total
   6 | 
   7 | ------------------------
   8 | -- EQUALITY, ORDERING --
   9 | ------------------------
  10 | 
  11 | ||| The Eq interface defines inequality and equality.
  12 | ||| A minimal definition includes either `(==)` or `(/=)`.
  13 | public export
  14 | interface Eq ty where
  15 |   constructor MkEq
  16 |   total
  17 |   (==) : ty -> ty -> Bool
  18 |   total
  19 |   (/=) : ty -> ty -> Bool
  20 | 
  21 |   x == y = not (x /= y)
  22 |   x /= y = not (x == y)
  23 | 
  24 | public export
  25 | Eq Void where
  26 |   _ == _ impossible
  27 | 
  28 | public export
  29 | Eq () where
  30 |   _ == _ = True
  31 | 
  32 | public export
  33 | Eq Bool where
  34 |   True == True = True
  35 |   False == False = True
  36 |   _ == _ = False
  37 | 
  38 | public export
  39 | Eq Int where
  40 |   x == y = intToBool (prim__eq_Int x y)
  41 | 
  42 | public export
  43 | Eq Integer where
  44 |   x == y = intToBool (prim__eq_Integer x y)
  45 | 
  46 | public export
  47 | Eq Bits8 where
  48 |   x == y = intToBool (prim__eq_Bits8 x y)
  49 | 
  50 | public export
  51 | Eq Bits16 where
  52 |   x == y = intToBool (prim__eq_Bits16 x y)
  53 | 
  54 | public export
  55 | Eq Bits32 where
  56 |   x == y = intToBool (prim__eq_Bits32 x y)
  57 | 
  58 | public export
  59 | Eq Bits64 where
  60 |   x == y = intToBool (prim__eq_Bits64 x y)
  61 | 
  62 | public export
  63 | Eq Int8 where
  64 |   x == y = intToBool (prim__eq_Int8 x y)
  65 | 
  66 | public export
  67 | Eq Int16 where
  68 |   x == y = intToBool (prim__eq_Int16 x y)
  69 | 
  70 | public export
  71 | Eq Int32 where
  72 |   x == y = intToBool (prim__eq_Int32 x y)
  73 | 
  74 | public export
  75 | Eq Int64 where
  76 |   x == y = intToBool (prim__eq_Int64 x y)
  77 | 
  78 | public export
  79 | Eq Double where
  80 |   x == y = intToBool (prim__eq_Double x y)
  81 | 
  82 | public export
  83 | Eq Char where
  84 |   x == y = intToBool (prim__eq_Char x y)
  85 | 
  86 | public export
  87 | Eq String where
  88 |   x == y = intToBool (prim__eq_String x y)
  89 | 
  90 | public export
  91 | Eq a => Eq b => Eq (a, b) where
  92 |   (x1, y1) == (x2, y2) = x1 == x2 && y1 == y2
  93 | 
  94 | public export
  95 | data Ordering = LT | EQ | GT
  96 | 
  97 | public export
  98 | contra : Ordering -> Ordering
  99 | contra LT = GT
 100 | contra EQ = EQ
 101 | contra GT = LT
 102 | 
 103 | public export
 104 | Eq Ordering where
 105 |   LT == LT = True
 106 |   EQ == EQ = True
 107 |   GT == GT = True
 108 |   _  == _  = False
 109 | 
 110 | ||| The Ord interface defines comparison operations on ordered data types.
 111 | ||| A minimal definition includes either `compare` or `(<)`.
 112 | public export
 113 | interface Eq ty => Ord ty where
 114 |   constructor MkOrd
 115 |   total
 116 |   compare : ty -> ty -> Ordering
 117 |   compare x y = if x < y then LT else if x == y then EQ else GT
 118 | 
 119 |   total
 120 |   (<) : ty -> ty -> Bool
 121 |   (<) x y = compare x y == LT
 122 | 
 123 |   total
 124 |   (>) : ty -> ty -> Bool
 125 |   (>) x y = compare x y == GT
 126 | 
 127 |   total
 128 |   (<=) : ty -> ty -> Bool
 129 |   (<=) x y = compare x y /= GT
 130 | 
 131 |   total
 132 |   (>=) : ty -> ty -> Bool
 133 |   (>=) x y = compare x y /= LT
 134 | 
 135 |   total
 136 |   max : ty -> ty -> ty
 137 |   max x y = if x > y then x else y
 138 | 
 139 |   total
 140 |   min : ty -> ty -> ty
 141 |   min x y = if (x < y) then x else y
 142 | 
 143 | export
 144 | comparing : Ord a => (b -> a) -> b -> b -> Ordering
 145 | comparing p x y = compare (p x) (p y)
 146 | 
 147 | public export
 148 | [Reverse] (fwd : Ord a) => Ord a where
 149 |   compare x y = contra $ compare @{fwd} x y
 150 | 
 151 | public export
 152 | Ord Void where
 153 |   compare _ _ impossible
 154 | 
 155 | public export
 156 | Ord () where
 157 |   compare _ _ = EQ
 158 | 
 159 | public export
 160 | Ord Bool where
 161 |   compare False False = EQ
 162 |   compare False True = LT
 163 |   compare True False = GT
 164 |   compare True True = EQ
 165 | 
 166 | public export
 167 | Ord Int where
 168 |   (<) x y = intToBool (prim__lt_Int x y)
 169 |   (<=) x y = intToBool (prim__lte_Int x y)
 170 |   (>) x y = intToBool (prim__gt_Int x y)
 171 |   (>=) x y = intToBool (prim__gte_Int x y)
 172 | 
 173 | public export
 174 | Ord Integer where
 175 |   (<) x y = intToBool (prim__lt_Integer x y)
 176 |   (<=) x y = intToBool (prim__lte_Integer x y)
 177 |   (>) x y = intToBool (prim__gt_Integer x y)
 178 |   (>=) x y = intToBool (prim__gte_Integer x y)
 179 | 
 180 | -- Used for the nat hack
 181 | public export
 182 | compareInteger : (x, y : Integer) -> Ordering
 183 | compareInteger = compare
 184 | 
 185 | public export
 186 | Ord Bits8 where
 187 |   (<) x y = intToBool (prim__lt_Bits8 x y)
 188 |   (<=) x y = intToBool (prim__lte_Bits8 x y)
 189 |   (>) x y = intToBool (prim__gt_Bits8 x y)
 190 |   (>=) x y = intToBool (prim__gte_Bits8 x y)
 191 | 
 192 | public export
 193 | Ord Bits16 where
 194 |   (<) x y = intToBool (prim__lt_Bits16 x y)
 195 |   (<=) x y = intToBool (prim__lte_Bits16 x y)
 196 |   (>) x y = intToBool (prim__gt_Bits16 x y)
 197 |   (>=) x y = intToBool (prim__gte_Bits16 x y)
 198 | 
 199 | public export
 200 | Ord Bits32 where
 201 |   (<) x y = intToBool (prim__lt_Bits32 x y)
 202 |   (<=) x y = intToBool (prim__lte_Bits32 x y)
 203 |   (>) x y = intToBool (prim__gt_Bits32 x y)
 204 |   (>=) x y = intToBool (prim__gte_Bits32 x y)
 205 | 
 206 | public export
 207 | Ord Bits64 where
 208 |   (<) x y = intToBool (prim__lt_Bits64 x y)
 209 |   (<=) x y = intToBool (prim__lte_Bits64 x y)
 210 |   (>) x y = intToBool (prim__gt_Bits64 x y)
 211 |   (>=) x y = intToBool (prim__gte_Bits64 x y)
 212 | 
 213 | public export
 214 | Ord Int8 where
 215 |   (<) x y = intToBool (prim__lt_Int8 x y)
 216 |   (<=) x y = intToBool (prim__lte_Int8 x y)
 217 |   (>) x y = intToBool (prim__gt_Int8 x y)
 218 |   (>=) x y = intToBool (prim__gte_Int8 x y)
 219 | 
 220 | public export
 221 | Ord Int16 where
 222 |   (<) x y = intToBool (prim__lt_Int16 x y)
 223 |   (<=) x y = intToBool (prim__lte_Int16 x y)
 224 |   (>) x y = intToBool (prim__gt_Int16 x y)
 225 |   (>=) x y = intToBool (prim__gte_Int16 x y)
 226 | 
 227 | public export
 228 | Ord Int32 where
 229 |   (<) x y = intToBool (prim__lt_Int32 x y)
 230 |   (<=) x y = intToBool (prim__lte_Int32 x y)
 231 |   (>) x y = intToBool (prim__gt_Int32 x y)
 232 |   (>=) x y = intToBool (prim__gte_Int32 x y)
 233 | 
 234 | public export
 235 | Ord Int64 where
 236 |   (<) x y = intToBool (prim__lt_Int64 x y)
 237 |   (<=) x y = intToBool (prim__lte_Int64 x y)
 238 |   (>) x y = intToBool (prim__gt_Int64 x y)
 239 |   (>=) x y = intToBool (prim__gte_Int64 x y)
 240 | 
 241 | public export
 242 | Ord Double where
 243 |   (<) x y = intToBool (prim__lt_Double x y)
 244 |   (<=) x y = intToBool (prim__lte_Double x y)
 245 |   (>) x y = intToBool (prim__gt_Double x y)
 246 |   (>=) x y = intToBool (prim__gte_Double x y)
 247 | 
 248 | public export
 249 | Ord String where
 250 |   (<) x y = intToBool (prim__lt_String x y)
 251 |   (<=) x y = intToBool (prim__lte_String x y)
 252 |   (>) x y = intToBool (prim__gt_String x y)
 253 |   (>=) x y = intToBool (prim__gte_String x y)
 254 | 
 255 | public export
 256 | Ord Char where
 257 |   (<) x y = intToBool (prim__lt_Char x y)
 258 |   (<=) x y = intToBool (prim__lte_Char x y)
 259 |   (>) x y = intToBool (prim__gt_Char x y)
 260 |   (>=) x y = intToBool (prim__gte_Char x y)
 261 | 
 262 | public export
 263 | Ord a => Ord b => Ord (a, b) where
 264 |   compare (x1, y1) (x2, y2)
 265 |       = if x1 /= x2 then compare x1 x2
 266 |                     else compare y1 y2
 267 |