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