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