0 | module Data.SOP.Utils
  1 |
  2 | import Data.List
  3 | import Data.String
  4 |
  5 | %default total
  6 |
  7 | ||| Type-level identity function.
  8 | public export
  9 | I : Type -> Type
 10 | I v = v
 11 |
 12 | ||| Type-level constant function.
 13 | public export
 14 | K : Type -> k -> Type
 15 | K t _ = t
 16 |
 17 | --------------------------------------------------------------------------------
 18 | --          Singleton Lists
 19 | --------------------------------------------------------------------------------
 20 |
 21 | ||| Witness that a list is actually a singleton list.
 22 | public export
 23 | data SingletonList : (vs : List a) -> Type where
 24 |   IsSingletonList : (v : a) -> SingletonList [v]
 25 |
 26 | public export
 27 | Uninhabited (SingletonList []) where
 28 |   uninhabited v impossible
 29 |
 30 | public export
 31 | Uninhabited (SingletonList $ a :: b :: t) where
 32 |   uninhabited v impossible
 33 |
 34 | ||| Covering function for singleton lists.
 35 | public export
 36 | singletonList : (vs : List a) -> Dec (SingletonList vs)
 37 | singletonList []              = No absurd
 38 | singletonList (v :: [])       = Yes (IsSingletonList v)
 39 | singletonList (_ :: (_ :: _)) = No absurd
 40 |
 41 | --------------------------------------------------------------------------------
 42 | --          Updating Lists
 43 | --------------------------------------------------------------------------------
 44 |
 45 | ||| View for updating a single occurence of a value
 46 | ||| in a list
 47 | public export
 48 | data UpdateOnce :
 49 |        (t   : k)
 50 |     -> (t'  : k)
 51 |     -> (ks  : List k)
 52 |     -> (ks' : List k)
 53 |     -> Type where
 54 |
 55 |   UpdateHere  : UpdateOnce t t' (t :: ks) (t' :: ks)
 56 |   UpdateThere : UpdateOnce t t' ks ks' -> UpdateOnce t t' (k :: ks) (k :: ks')
 57 |
 58 | ||| View for updating several occurences of a value
 59 | ||| in a list
 60 | public export
 61 | data UpdateMany :
 62 |        (t   : k)
 63 |     -> (t'  : k)
 64 |     -> (ks  : List k)
 65 |     -> (ks' : List k)
 66 |     -> Type where
 67 |   UMNil      : UpdateMany t t' [] []
 68 |   UMConsSame : UpdateMany t t' ks ks' -> UpdateMany t t' (t::ks) (t'::ks')
 69 |   UMConsDiff : UpdateMany t t' ks ks' -> UpdateMany t t' (k::ks) (k::ks')
 70 |
 71 | --------------------------------------------------------------------------------
 72 | --          Sublists
 73 | --------------------------------------------------------------------------------
 74 |
 75 | ||| View of the second List containing all values (in the same order)
 76 | ||| of the first List interleaved with arbitrary additional values.
 77 | public export
 78 | data Sublist : (ks : List k) -> (ks' : List k) -> Type where
 79 |   SLNil  : Sublist [] ks'
 80 |   SLSame : Sublist ks ks' -> Sublist (k::ks) (k::ks')
 81 |   SLDiff : Sublist ks ks' -> Sublist ks (k::ks')
 82 |
 83 | --------------------------------------------------------------------------------
 84 | --          Enumerations
 85 | --------------------------------------------------------------------------------
 86 |
 87 | ||| Witness that a list of list of types (representing the
 88 | ||| constructors and fields of an ADT) represents an enum type, i.e.
 89 | ||| that all constructors are nullary.
 90 | public export
 91 | data EnumType : (kss : List $ List k) -> Type where
 92 |   EZ : EnumType Nil
 93 |   ES : EnumType kss -> EnumType ([] :: kss)
 94 |
 95 | ||| If `ks :: kss` is an enum type, then so is `kss`
 96 | public export
 97 | 0 enumTail : EnumType (ks :: kss) -> EnumType kss
 98 | enumTail (ES x) = x
 99 |
100 | --------------------------------------------------------------------------------
101 | --          Show Utilities
102 | --------------------------------------------------------------------------------
103 |
104 | export
105 | dispStringList : List String -> String
106 | dispStringList ss = "[" ++ fastConcat (intersperse "," ss) ++ "]"
107 |