
   0 | module Data.SnocVect
   1 | 
   2 | import Data.Vect
   3 | 
   4 | %hide Prelude.Types.elem
   5 | 
   6 | %default total
   7 | 
   8 | ||| A Backwards Vect
   9 | public export
  10 | data SnocVect : Nat -> Type -> Type where
  11 |   ||| Empty snoc-vect
  12 |   Lin : SnocVect 0 a
  13 | 
  14 |   ||| A non-empty snoc-vect, consisting of the rest of the snoc-vect and the final element.
  15 |   (:<) : (SnocVect n a) -> a -> SnocVect (S n) a
  16 | 
  17 | %name SnocVect sx, sy, sz
  18 | 
  19 | export infixl 7 <><
  20 | export infixr 6 <>>
  21 | 
  22 | ||| 'fish': Action of lists on snoc-lists
  23 | public export
  24 | (<><) : SnocVect n a -> Vect m a -> SnocVect (n + m) a
  25 | sx <>< [] = rewrite plusZeroRightNeutral n in sx
  26 | sx <>< ((::) x xs {len}) =
  27 |   rewrite sym $ plusSuccRightSucc n len in
  28 |           sx :< x <>< xs
  29 | 
  30 | ||| 'chips': Action of snoc-lists on lists
  31 | public export
  32 | (<>>) : SnocVect j a -> Vect k a -> Vect (j + k) a
  33 | Lin       <>> xs = xs
  34 | ((:<) sx x {n}) <>> xs =
  35 |   rewrite plusSuccRightSucc n k in
  36 |           sx <>> x :: xs
  37 | 
  38 | export
  39 | Cast (SnocVect n a) (Vect n a) where
  40 |   cast sx = rewrite sym $ plusZeroRightNeutral n in
  41 |                     sx <>> []
  42 | 
  43 | export
  44 | Cast (Vect n a) (SnocVect n a) where
  45 |   cast xs = Lin <>< xs
  46 | 
  47 | ||| Transform to a vect but keeping the contents in the spine order (term depth).
  48 | public export
  49 | asVect : SnocVect n type -> Vect n type
  50 | asVect = (reverse . cast)
  51 | 
  52 | public export
  53 | Eq a => Eq (SnocVect n a) where
  54 |   (==) Lin Lin = True
  55 |   (==) (sx :< x) (sy :< y) = x == y && sx == sy
  56 |   (==) _ _ = False
  57 | 
  58 | public export
  59 | Ord a => Ord (SnocVect n a) where
  60 |   compare Lin Lin = EQ
  61 |   compare (sx :< x) (sy :< y)
  62 |     = case compare sx sy of
  63 |         EQ => compare x y
  64 |         c  => c
  65 | 
  66 | ||| True iff input is Lin
  67 | public export
  68 | isLin : SnocVect n a -> Bool
  69 | isLin Lin = True
  70 | isLin (sx :< x) = False
  71 | 
  72 | ||| True iff input is (:<)
  73 | public export
  74 | isSnoc : SnocVect n a -> Bool
  75 | isSnoc Lin     = False
  76 | isSnoc (sx :< x) = True
  77 | 
  78 | public export
  79 | (++) : (sx : SnocVect j a) ->  (sy : SnocVect k a) -> SnocVect (j + k) a
  80 | (++) sx Lin = rewrite plusZeroRightNeutral j in sx
  81 | (++) sx ((:<) sy y {n}) =
  82 |   rewrite sym $ plusSuccRightSucc j n in
  83 |           (sx ++ sy) :< y
  84 | 
  85 | public export
  86 | length : SnocVect n a -> Nat
  87 | length Lin = Z
  88 | length (sx :< x) = S $ length sx
  89 | 
  90 | export
  91 | lengthCorrect : (sx : SnocVect n a) -> length sx = n
  92 | lengthCorrect [<]       = Refl
  93 | lengthCorrect (sx :< x) = cong S (lengthCorrect sx)
  94 | 
  95 | public export
  96 | replicate : (k : Nat) -> a -> SnocVect k a
  97 | replicate 0 x = [<]
  98 | replicate (S k) x = replicate k x :< x
  99 | 
 100 | ||| The "head" of the snoc-vect
 101 | public export
 102 | deah : SnocVect (S n) a -> a
 103 | deah (sx :< x) = x
 104 | 
 105 | ||| The "tail" of the snoc-vect
 106 | public export
 107 | liat : SnocVect (S n) a -> SnocVect n a
 108 | liat (sx :< x) = sx
 109 | 
 110 | export
 111 | Show a => Show (SnocVect n a) where
 112 |   show sx = concat ("[< " :: intersperse ", " (show' [] sx) ++ ["]"])
 113 |     where
 114 |       show' : Vect j String -> SnocVect k a -> Vect (j + k) String
 115 |       show' acc Lin       = rewrite plusZeroRightNeutral j in acc
 116 |       show' acc ((:<) xs x {n}) = 
 117 |         rewrite sym $ plusSuccRightSucc j n in
 118 |                 show' (show x :: acc) xs
 119 | 
 120 | public export
 121 | Functor (SnocVect n) where
 122 |   map f Lin = Lin
 123 |   map f (sx :< x) = (map f sx) :< (f x)
 124 | 
 125 | public export
 126 | Zippable (SnocVect k) where
 127 |   zipWith _ [<] [<] = [<]
 128 |   zipWith f (sx :< x) (sy :< y) = zipWith f sx sy :< f x y
 129 | 
 130 |   zipWith3 _ [<] [<] [<] = [<]
 131 |   zipWith3 f (sx :< x) (sy :< y) (sz :< z) = zipWith3 f sx sy sz :< f x y z 
 132 | 
 133 |   unzipWith f [<] = ([<], [<])
 134 |   unzipWith f (sx :< x) = let (b, c) = f x
 135 |                               (sb, sc) = unzipWith f sx in
 136 |                               (sb :< b, sc :< c)
 137 | 
 138 |   unzipWith3 f [<] = ([<], [<], [<])
 139 |   unzipWith3 f (sx :< x) = let (b, c, d) = f x
 140 |                                (sb, sc, sd) = unzipWith3 f sx in
 141 |                                (sb :< b, sc :< c, sd :< d)
 142 | 
 143 | public export
 144 | Semigroup a => Semigroup (SnocVect n a) where
 145 |   (<+>) = zipWith (<+>)
 146 | 
 147 | public export
 148 | {k : Nat} -> Monoid a => Monoid (SnocVect k a) where
 149 |   neutral = replicate k neutral
 150 | 
 151 | public export
 152 | Foldable (SnocVect n) where
 153 |   foldr f z = foldr f z . (<>> [])
 154 | 
 155 |   foldl f z xs = h xs where
 156 |     h : SnocVect k elem -> acc
 157 |     h Lin = z
 158 |     h (xs :< x) = f (h xs) x
 159 | 
 160 |   null Lin      = True
 161 |   null (_ :< _) = False
 162 | 
 163 |   toList = toList . (<>> [])
 164 | 
 165 |   foldMap f = foldl (\xs, x => xs <+> f x) neutral
 166 | 
 167 | public export
 168 | {k : Nat} -> Applicative (SnocVect k) where
 169 |   pure = replicate _
 170 |   fs <*> sx = zipWith apply fs sx
 171 | 
 172 | ||| Get diagonal elements
 173 | public export
 174 | diag : SnocVect len (SnocVect len elem) -> SnocVect len elem
 175 | diag [<]             = [<]
 176 | diag (ssx :< (sx :< x)) = diag (map liat ssx) :< x
 177 | 
 178 | ||| This monad is different from the List monad, (>>=)
 179 | ||| uses the diagonal.
 180 | public export
 181 | {k : Nat} -> Monad (SnocVect k) where
 182 |   sx >>= f = diag (map f sx)
 183 | 
 184 | public export
 185 | Traversable (SnocVect k) where
 186 |   traverse _ Lin = pure Lin
 187 |   traverse f (xs :< x) = [| traverse f xs :< f x |]
 188 | 
 189 | ||| Check if something is a member of a snoc-vect using the default Boolean equality.
 190 | public export
 191 | elem : Eq a => a -> SnocVect k a -> Bool
 192 | elem x Lin = False
 193 | elem x (sx :< y) = x == y || elem x sx
 194 | 
 195 | ||| Find the first element of the snoc-vect that satisfies the predicate.
 196 | public export
 197 | find : (a -> Bool) -> SnocVect k a -> Maybe a
 198 | find p Lin = Nothing
 199 | find p (xs :< x) = if p x then Just x else find p xs
 200 | 
 201 | ||| Satisfiable if `k` is a valid index into `xs`.
 202 | |||
 203 | ||| @ k  the potential index
 204 | ||| @ xs the snoc-list into which k may be an index
 205 | public export
 206 | data InBounds : (k : Nat) -> (xs : SnocVect j a) -> Type where
 207 |     ||| Z is a valid index into any cons cell
 208 |     InFirst : InBounds Z (xs :< x)
 209 |     ||| Valid indices can be extended
 210 |     InLater : InBounds k xs -> InBounds (S k) (xs :< x)
 211 | 
 212 | ||| Find the index and proof of InBounds of the first element (if exists) of a
 213 | ||| snoc-list that satisfies the given test, else `Nothing`.
 214 | public export
 215 | findIndex : (a -> Bool) -> (sx : SnocVect k a) -> Maybe $ Fin (length sx)
 216 | findIndex _ Lin = Nothing
 217 | findIndex p (xs :< x) = if p x
 218 |   then Just FZ
 219 |   else FS <$> findIndex p xs
 220 |