
  0 | ||| A module defining a dependent sum
  1 | module Data.DSum
  2 | 
  3 | import Data.String
  4 | 
  5 | import public Data.DEq
  6 | import public Data.DOrd
  7 | import public Data.DShow
  8 | import public Data.Some
  9 | 
 10 | export infixr 1 :=>
 11 | ||| A dependent sum
 12 | ||| This data type is supposed to mimic the `DSum` type from Haskells "dependent-sum" package
 13 | public export
 14 | data DSum : (tag : a -> Type) -> (f : a -> Type) -> Type where
 15 |   (:=>) : {0 x : a} -> tag x -> f x -> DSum tag f
 16 | 
 17 | ||| The first component of a dependent sum
 18 | export
 19 | fst : DSum tag f -> Some tag
 20 | fst (x :=> y) = MkSome x
 21 | 
 22 | ||| The sencond component of a dependent sum
 23 | export
 24 | snd : DSum tag f -> Some f
 25 | snd (x :=> y) = MkSome y
 26 | 
 27 | ||| Convert a dependent sum to `Some`
 28 | export
 29 | toSome : DSum tag f -> Some (\x => (tag x, f x))
 30 | toSome (x :=> y) = MkSome (x, y)
 31 | 
 32 | export
 33 | implementation (tagimpl : DEq tag) => (fimpl : DEq f) => Eq (DSum tag f) where
 34 |   (x :=> y) == (x' :=> y') = deq' @{tagimpl} x x' && deq' @{fimpl} y y'
 35 | 
 36 | export
 37 | implementation (tagimpl : DOrd tag) => (fimpl : DOrd f) => Ord (DSum tag f) where
 38 |   compare (x :=> y) (x' :=> y') = case dcompare @{tagimpl} x x' of
 39 |     DLT => LT
 40 |     DGT => GT
 41 |     DEQ => dcompare' @{fimpl} y y'
 42 | 
 43 | export
 44 | implementation (tagimpl : DShow tag) => (fimpl : DShow f) => Show (DSum tag f) where
 45 |   -- TODO use `showPrec` to only print parentheses when necessary
 46 |   show (x :=> y) = let
 47 |     noParens = unwords [dshow x @{tagimpl}, ":=>", dshow y @{fimpl}]
 48 |     in showParens True noParens
 49 |