0 | ||| A module defining the `DOrd` interface
  1 | module Data.DOrd
  2 |
  3 | import public Data.DEq
  4 |
  5 | ||| An ordering of single-parameter dependent types
  6 | |||
  7 | ||| Modeled after the `GOrdering` type from Haskells "some" package
  8 | public export
  9 | data DOrdering : t -> t -> Type where
 10 |   DLT : DOrdering a b
 11 |   DEQ : DOrdering a a
 12 |   DGT : DOrdering a b
 13 |
 14 | export
 15 | ||| Like `ordcong` but the function is implicit
 16 | ordcong'
 17 |    : {0 f : a -> b}
 18 |   -> {0 x, y : a}
 19 |   -> DOrdering x y
 20 |   -> DOrdering (f x) (f y)
 21 | ordcong' DLT = DLT
 22 | ordcong' DGT = DGT
 23 | ordcong' DEQ = DEQ
 24 |
 25 | ||| Takes a function and an ordering of the two values and returns an ordering
 26 | ||| of the results of that function applied to these values.
 27 | |||
 28 | ||| @ f   the function
 29 | ||| @ x y the values
 30 | ||| @ ord the ordering
 31 | export
 32 | ordcong
 33 |    : (0 f : a -> b)
 34 |   -> {0 x, y : a}
 35 |   -> (ord : DOrdering x y)
 36 |   -> DOrdering (f x) (f y)
 37 | ordcong f = ordcong' {f}
 38 |
 39 | ||| ``ordL `precedes` ordR`` means that, in the resulting ordering, `ordL`
 40 | ||| precedes' `ordR`, that is, `ordR` is considered only if `ordL` is `DEQ`
 41 | export
 42 | precedes
 43 |    : {0 a, b   : t}
 44 |   -> {0 aa, bb : tt}
 45 |   -> {0 f        : t -> tt -> ttt}
 46 |   -> (lhs      : DOrdering a        b)
 47 |   -> (rhs      : DOrdering aa       bb)
 48 |   ->             DOrdering (f a aa) (f b bb)
 49 | precedes DLT _   = DLT
 50 | precedes DGT _   = DGT
 51 | precedes DEQ DLT = DLT
 52 | precedes DEQ DGT = DGT
 53 | precedes DEQ DEQ = DEQ
 54 |
 55 | ||| Like `precedes`, except the preceding ordering is a regular `Ordering`
 56 | export
 57 | precedes' : Ordering -> DOrdering a b -> DOrdering a b
 58 | precedes' LT dord = DLT
 59 | precedes' EQ dord = dord
 60 | precedes' GT dord = DGT
 61 |
 62 | ||| Similar to `Ord` but the operands can be equal only when they actually are,
 63 | ||| that is, when the statement `p = q` is true (there is a `Refl : (p = q)`),
 64 | ||| where `p` and `q` are the operands
 65 | |||
 66 | ||| The "P" in `POrd` stands for "proof"
 67 | ||| Note, this is not the same as `OrdP` from the "some" package from Hackage
 68 | public export
 69 | interface POrd a where
 70 |   ||| Compare two values
 71 |   pcompare : (x, y : a) -> DOrdering x y
 72 |
 73 | ||| Constructors of types that allow for comparing values of such types, even
 74 | ||| in the case when their types are constructed from different parameters
 75 | |||
 76 | ||| Modeled after the `GCompare` typeclass from Haskells "some" package
 77 | |||
 78 | ||| @ f the type constructor
 79 | ||| @ t the parameter type
 80 | public export
 81 | interface (impl : DEq f) => DOrd (0 f : t -> Type) where
 82 |   ||| Compare the operands
 83 |   dcompare : f a -> f b -> DOrdering a b
 84 |
 85 | ||| Compare the operands and ignore the equality proof (if the result is `DEQ`)
 86 | export
 87 | dcompare' : (impl : DOrd f) => f a -> f b -> Ordering
 88 | dcompare' fa fb = case dcompare fa fb @{impl} of
 89 |   DLT => LT
 90 |   DEQ => EQ
 91 |   DGT => GT
 92 |
 93 | ||| Use only when absolutely sure that `compare x y` returns `EQ` only when `x`
 94 | ||| and `y` are identical.
 95 | export
 96 | implementation [unsafeViaOrd] Ord a => POrd a where
 97 |   pcompare x y = case compare x y of
 98 |     LT => DLT
 99 |     GT => DGT
100 |     EQ => (believe_me $ the (DOrdering x x) DEQ)
101 |
102 | export
103 | implementation POrd Bool where
104 |   pcompare x y = pcompare x y @{unsafeViaOrd}
105 |
106 | export
107 | implementation POrd Nat where
108 |   pcompare x y = pcompare x y @{unsafeViaOrd}
109 |
110 |   -- A "kosher" definition:
111 |   -- pcompare Z     Z     = DEQ
112 |   -- pcompare (S n) (S m) = ordcong S (pcompare n m)
113 |   -- pcompare Z     (S m) = DLT
114 |   -- pcompare (S n) Z     = DGT
115 |
116 | export
117 | implementation POrd Int where
118 |   pcompare x y = pcompare x y @{unsafeViaOrd}
119 |
120 | export
121 | implementation POrd Integer where
122 |   pcompare x y = pcompare x y @{unsafeViaOrd}
123 |
124 | export
125 | implementation POrd Char where
126 |   pcompare x y = pcompare x y @{unsafeViaOrd}
127 |
128 | export
129 | implementation POrd String where
130 |   pcompare x y = pcompare x y @{unsafeViaOrd}
131 |
132 | export
133 | implementation POrd a => POrd (List a) where
134 |   pcompare Nil Nil = DEQ
135 |   pcompare (x :: xs) (y :: ys)
136 |     = (pcompare x y `precedes` pcompare xs ys) {f = (::)}
137 |   pcompare Nil (y :: ys) = DLT
138 |   pcompare (x :: xs) Nil = DGT
139 |
140 | export
141 | implementation POrd a => POrd b => POrd (a, b) where
142 |   pcompare (a1, b1) (a2, b2)
143 |     = (pcompare a1 a2 `precedes` pcompare b1 b2) {f = (,)}
144 |