0 | module Data.Maybe.Upper
 1 |
 2 | import Control.Function
 3 | import Data.Maybe
 4 | import Control.Relation
 5 | import Control.Relation.Trichotomy
 6 |
 7 | %default total
 8 |
 9 | ||| A total order for `Maybe a` where `a` has a total order
10 | ||| and `Nothing` is the maximal value.
11 | |||
12 | ||| This is useful, for instance, when implementing provably
13 | ||| sorted (assoc-) lists, indexed by a `Maybe key`, where
14 | ||| the empty list has a `Nothing` index:
15 | |||
16 | ||| ```idris example
17 | ||| data AssocList : (ix : Maybe Bits8) -> (a : Type) -> Type where
18 | |||   Nil  : AssocList Nothing a
19 | |||   (::) :  (p : (Bits8, a))
20 | |||        -> (ps : AssocList ix a)
21 | |||        -> (0 prf : Upper (<) (Just $ fst p) ix)
22 | |||        => AssocList (Just $ fst p) a
23 | ||| ```
24 | public export
25 | data Upper : (lt : a -> a -> Type) -> (m1,m2 : Maybe a) -> Type where
26 |   UNothing : Upper lt (Just v) Nothing
27 |   UJust    :  {0 lt : a -> a -> Type}
28 |            -> {0 v, w : a}
29 |            -> lt v w -> Upper lt (Just v) (Just w)
30 |
31 | public export
32 | Uninhabited (Upper lt Nothing m) where
33 |   uninhabited UNothing impossible
34 |   uninhabited (UJust _) impossible
35 |
36 | public export
37 | Strict a lt => Uninhabited (Upper lt (Just k) (Just k)) where
38 |   uninhabited UNothing impossible
39 |   uninhabited (UJust refl) = void (irreflexive refl)
40 |
41 | public export
42 | fromLT : Upper lt (Just a) (Just b) -> lt a b
43 | fromLT (UJust x) = x
44 |
45 | ||| Implementation and alias for `trichotomy`.
46 | export
47 | comp : Trichotomous a lt => (m1,m2 : Maybe a) -> Trichotomy (Upper lt) m1 m2
48 | comp (Just x) (Just y) = case trichotomy {rel = lt} x y of
49 |   LT p c1 c2 => LT (UJust p) (\r => c1 (injective r)) (\x => c2 (fromLT x))
50 |   EQ c1 p c2 => EQ (\x => c1 (fromLT x)) (cong Just p) (\x => c2 (fromLT x))
51 |   GT c1 c2 p => GT (\x => c1 (fromLT x)) (\r => c2 (injective r)) (UJust p)
52 | comp (Just x) Nothing  = LT UNothing absurd absurd
53 | comp Nothing  (Just y) = GT absurd absurd UNothing
54 | comp Nothing  Nothing  = EQ absurd Refl absurd
55 |
56 | ||| If `lt` is a total order of `a`, then `Upper lt` is a
57 | ||| total order of `Maybe a`.
58 | export %inline
59 | Trichotomous a lt => Trichotomous (Maybe a) (Upper lt) where
60 |   trichotomy = comp
61 |
62 | export %inline
63 | Transitive a lt => Transitive (Maybe a) (Upper lt) where
64 |   transitive (UJust x) UNothing  = UNothing
65 |   transitive (UJust x) (UJust y) = UJust $ transitive x y
66 |   transitive UNothing  y         = absurd y
67 |