
  0 | module Data.Trichotomy
  1 | 
  2 | %default total
  3 | 
  4 | ||| Trichotomy formalises the fact that three relations are mutually
  5 | ||| exclusive. A value of type `Trichotomy lt m n` proofs, that
  6 | ||| exactly one of the relations `lt m n`, `m === n`, or `lt n m` holds.
  7 | |||
  8 | ||| All proofs held by a value of type `Trichotomous` are erased, so
  9 | ||| at runtime such values get optimized to numbers 0, 1, or 2
 10 | ||| respectively.
 11 | public export
 12 | data Trichotomy : (lt : a -> a -> Type) -> (a -> a -> Type) where
 13 |   LT :  {0 lt : a -> a -> Type}
 14 |      -> (0 _ : lt v w)
 15 |      -> (0 _ : Not (v === w))
 16 |      -> (0 _ : Not (lt w v))
 17 |      -> Trichotomy lt v w
 18 | 
 19 |   EQ :  {0 lt : a -> a -> Type}
 20 |      -> (0 _ : Not (lt v w))
 21 |      -> (0 _ : v === w)
 22 |      -> (0 _ : Not (lt w v))
 23 |      -> Trichotomy lt v w
 24 | 
 25 |   GT :  {0 lt : a -> a -> Type}
 26 |      -> (0 _ : Not (lt v w))
 27 |      -> (0 _ : Not (v === w))
 28 |      -> (0 _ : lt w v)
 29 |      -> Trichotomy lt v w
 30 | 
 31 | public export
 32 | Eq (Trichotomy lt m n) where
 33 |   LT _ _ _ == LT _ _ _ = True
 34 |   EQ _ _ _ == EQ _ _ _ = True
 35 |   GT _ _ _ == GT _ _ _ = True
 36 |   _        == _        = False
 37 | 
 38 | public export
 39 | Ord (Trichotomy lt m n) where
 40 |   compare (LT _ _ _) (LT _ _ _) = EQ
 41 |   compare (LT _ _ _) _          = LT
 42 |   compare _          (LT _ _ _) = GT
 43 |   compare (EQ _ _ _) (EQ _ _ _) = EQ
 44 |   compare (EQ _ _ _) _          = LT
 45 |   compare _          (EQ _ _ _) = GT
 46 |   compare (GT _ _ _) (GT _ _ _) = EQ
 47 | 
 48 | public export
 49 | Show (Trichotomy lt m n) where
 50 |   show (LT _ _ _) = "LT"
 51 |   show (EQ _ _ _) = "EQ"
 52 |   show (GT _ _ _) = "GT"
 53 | 
 54 | public export
 55 | toOrdering : Trichotomy lt m n -> Ordering
 56 | toOrdering (LT _ _ _) = LT
 57 | toOrdering (EQ _ _ _) = EQ
 58 | toOrdering (GT _ _ _) = GT
 59 |