
   0 | module Data.Container.Base.Properties.Instances
   1 | 
   2 | import Data.Fin
   3 | import Data.Vect
   4 | import Decidable.Equality
   5 | import Data.Fin.Split
   6 | import Data.Finite
   7 | 
   8 | import Data.Container.Base.Object.Definition
   9 | import Data.Container.Base.Morphism.Definition
  10 | import Data.Container.Base.Extension.Definition
  11 | import Data.Container.Base.Properties.Definition
  12 | import Data.Container.Base.Product.Definition
  13 | 
  14 | import Data.Container.Base.Object.Instances
  15 | import Data.Container.Base.Extension.Instances
  16 | import Data.Container.Base.Morphism.Instances
  17 | 
  18 | import Data.Trees
  19 | import Data.Functor.Products
  20 | import Data.Functor.Algebra
  21 | import Data.Container.Base.TreeUtils
  22 | 
  23 | import Misc
  24 | 
  25 | %hide Data.Vect.fromList
  26 | %hide Prelude.toList
  27 | 
  28 | public export
  29 | IsConcrete Scalar where
  30 |   func = id
  31 |   functorInstance = MkFunctor id
  32 |   fromConcreteTy = pure
  33 |   toConcreteTy (() <| f) = f ()
  34 | 
  35 | public export
  36 | IsConcrete Maybe where
  37 |   func = Maybe
  38 |   functorInstance = %search
  39 | 
  40 |   fromConcreteTy Nothing = False <| absurd
  41 |   fromConcreteTy (Just x) = True <| \() => x
  42 | 
  43 |   toConcreteTy (False <| _) = Nothing
  44 |   toConcreteTy (True <| f) = Just (f ())
  45 | 
  46 | public export
  47 | IsConcrete Pair where
  48 |   func = \a => Pair a a
  49 |   functorInstance = MkFunctor $ \f, (x, y) => (f x, f y)
  50 |   fromConcreteTy (x, y) = () <| \case False => x; True => y
  51 |   toConcreteTy (() <| f) = (f False, f True)
  52 | 
  53 | ||| This is a concrete instance for Naperian containers
  54 | ||| It applies also to `s=Fin n` which is covered by Vect
  55 | ||| We therefore want this to only be applied if Vect isn't
  56 | %defaulthint
  57 | public export
  58 | lambdaNap : {s : Type} -> IsConcrete (Nap s)
  59 | lambdaNap = MkIsConcrete
  60 |   (\a => s -> a)
  61 |   (MkFunctor (.))
  62 |   (\content => () <| content)
  63 |   (\(() <| content) => content)
  64 | 
  65 | public export
  66 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >< d) where
  67 |   func = func @{icc} >< func @{icd}
  68 |   functorInstance = ?functorInstanceHancockProduct
  69 |   fromConcreteTy = ?fromConcreteTyHancockProduct
  70 |   toConcreteTy = ?toConcreteTyHancockProduct
  71 | 
  72 | public export
  73 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >@ d) where
  74 |   func = func @{icc} . func @{icd}
  75 |   functorInstance = MkFunctor $ \f => ?functorInstanceCompositionProduct
  76 |   fromConcreteTy = ?fromConcreteTyCompositionProduct
  77 |   toConcreteTy = ?toConcreteTyCompositionProduct
  78 | 
  79 | 
  80 | ||| For recursive types we need to extract out the conversion functions
  81 | namespace List
  82 |   public export
  83 |   fromList : List a -> List' a
  84 |   fromList [] = (0 <| absurd)
  85 |   fromList (x :: xs) = let (l <| c) = fromList xs
  86 |                        in (S l <| cons x c)
  87 | 
  88 |   public export
  89 |   toList : List' a -> List a
  90 |   toList (0 <| _) = []
  91 |   toList l@((S k) <| ind) = head ind :: toList
  92 |     (assert_smaller l (k <| tail ind))
  93 | 
  94 |   public export
  95 |   IsConcrete List where
  96 |     func = List
  97 |     functorInstance = %search
  98 |     fromConcreteTy = fromList
  99 |     toConcreteTy = toList
 100 | 
 101 | namespace Vect
 102 |   public export
 103 |   fromVect : Vect n a -> Vect' n a
 104 |   fromVect v = () <| \i => index i v
 105 |   
 106 |   public export
 107 |   toVect : {n : Nat} -> Vect' n a -> Vect n a
 108 |   toVect (_ <| index) = Vect.Fin.tabulate index
 109 | 
 110 |   -- public export
 111 |   -- test : {n : Nat} -> IsConcrete (Vect n)
 112 |   -- test = MkIsConcrete
 113 |   --   (Vect n)
 114 |   --   (%search)
 115 |   --   (fromVect)
 116 |   --   (toVect)
 117 | 
 118 |   public export
 119 |   {n : Nat} -> IsConcrete (Vect n) where
 120 |     func = Vect n
 121 |     functorInstance = %search
 122 |     fromConcreteTy = fromVect
 123 |     toConcreteTy = toVect
 124 | 
 125 | namespace Grid
 126 |   public export
 127 |   {h, w : Nat} -> IsConcrete (Grid (h, w)) where
 128 |     func a = (Fin h, Fin w) -> a
 129 |     functorInstance = MkFunctor (.)
 130 |     fromConcreteTy content = ((), ()) <| content
 131 |     toConcreteTy (((), ()) <| content) = content
 132 | 
 133 | namespace BinTreeSame
 134 |   public export
 135 |   fromBinTreeSame : BinTreeSame a -> BinTree' a
 136 |   fromBinTreeSame (Leaf x) = LeafS <| \_ => x
 137 |   fromBinTreeSame (Node x lt rt) =
 138 |     let (fblt, fbrt) = (fromBinTreeSame lt, fromBinTreeSame rt)
 139 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 140 |         AtNode => x
 141 |         GoLeft posL => index fblt posL
 142 |         GoRight posR => index fbrt posR
 143 | 
 144 |   public export
 145 |   toBinTreeSame : BinTree' a -> BinTreeSame a
 146 |   toBinTreeSame (LeafS <| index) = Leaf (index AtLeaf)
 147 |   toBinTreeSame n@(NodeS lt rt <| index) =
 148 |     Node (index AtNode)
 149 |          (toBinTreeSame $ assert_smaller n (lt <| index . GoLeft))
 150 |          (toBinTreeSame $ assert_smaller n (rt <| index . GoRight))
 151 | 
 152 |   public export
 153 |   IsConcrete BinTree where
 154 |     func = BinTreeSame
 155 |     functorInstance = %search
 156 |     fromConcreteTy = fromBinTreeSame
 157 |     toConcreteTy = toBinTreeSame
 158 | 
 159 | namespace BinTreeNode
 160 |   public export
 161 |   fromTreeHelper : BinTreePosNode LeafS -> a
 162 |   fromTreeHelper AtNode impossible
 163 |   fromTreeHelper (GoLeft x) impossible
 164 |   fromTreeHelper (GoRight x) impossible
 165 |   
 166 |   public export
 167 |   fromBinTreeNode : BinTreeNode a -> BinTreeNode' a
 168 |   fromBinTreeNode (Leaf ()) = LeafS <| fromTreeHelper
 169 |   fromBinTreeNode (Node node leftTree rightTree)
 170 |     = let (fblt, fbrt) = (fromBinTreeNode leftTree, fromBinTreeNode rightTree)
 171 |       in (NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 172 |             AtNode => node
 173 |             GoLeft posL => index fblt posL
 174 |             GoRight posR => index fbrt posR)
 175 | 
 176 |   public export
 177 |   toBinTreeNode : BinTreeNode' a -> BinTreeNode a
 178 |   toBinTreeNode (LeafS <| index) = Leaf ()
 179 |   toBinTreeNode n@(NodeS lt rt <| index) = 
 180 |     Node (index AtNode)
 181 |          (toBinTreeNode $ assert_smaller n (lt <| index . GoLeft))
 182 |          (toBinTreeNode $ assert_smaller n (rt <| index . GoRight))
 183 | 
 184 |   public export
 185 |   IsConcrete BinTreeNode where
 186 |     func = BinTreeNode
 187 |     functorInstance = %search
 188 |     fromConcreteTy = fromBinTreeNode
 189 |     toConcreteTy = toBinTreeNode
 190 | 
 191 | namespace BinTreeLeaf
 192 |   public export
 193 |   fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a
 194 |   fromBinTreeLeaf (Leaf leaf) = LeafS <| \_ => leaf
 195 |   fromBinTreeLeaf (Node node lt rt) =
 196 |     let (fblt, fbrt) = (fromBinTreeLeaf lt, fromBinTreeLeaf rt)
 197 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 198 |           GoLeft posL => index fblt posL
 199 |           GoRight posR => index fbrt posR
 200 | 
 201 |   public export
 202 |   toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a
 203 |   toBinTreeLeaf (LeafS <| content) = Leaf (content AtLeaf)
 204 |   toBinTreeLeaf n@(NodeS l r <| content) =
 205 |     Node' (toBinTreeLeaf $ assert_smaller n (l <| content . GoLeft))
 206 |           (toBinTreeLeaf $ assert_smaller n (r <| content . GoRight))
 207 | 
 208 |   public export
 209 |   IsConcrete BinTreeLeaf where
 210 |     func = BinTreeLeaf
 211 |     functorInstance = %search
 212 |     fromConcreteTy = fromBinTreeLeaf
 213 |     toConcreteTy = toBinTreeLeaf
 214 | 
 215 | 
 216 | public export
 217 | foldList : (a -> b -> b) -> b -> List' a -> b
 218 | foldList f z (0 <| _) = z
 219 | foldList f z l@((S k) <| content)
 220 |   = f (head content) $ foldList f z
 221 |     (assert_smaller l (k <| tail content))
 222 | 
 223 | public export
 224 | IsFoldable c => Foldable (Ext c) where
 225 |   foldr @{(MkIsFoldable toL)} f z = foldList f z . extMap toL 
 226 | 
 227 | public export
 228 | IsFoldable List where
 229 |   mapToList = id
 230 | 
 231 | public export
 232 | {n : Nat} -> IsFoldable (Vect n) where
 233 |   mapToList = vectToList
 234 | 
 235 | ||| Requires making a choice of traversal order
 236 | ||| Is there a good reason to prefer a particular order?
 237 | public export
 238 | IsFoldable BinTreeLeaf where
 239 |   mapToList = inorder
 240 | 
 241 | public export
 242 | IsFoldable BinTreeNode where
 243 |   mapToList = inorder
 244 | 
 245 | public export
 246 | IsFoldable BinTree where
 247 |   mapToList = inorder
 248 | 
 249 | -- old
 250 | -- ||| Indexing an element of `xs` and then applying `f` to it is the same as
 251 | -- ||| mapping `f` over xs, and then indexing the result
 252 | -- public export
 253 | -- mapIndexPreserve : {0 f : a -> b} ->
 254 | --   (xs : List a) ->
 255 | --   (i : Fin (length (f <$> xs))) ->
 256 | --   f (index' xs (rewrite sym (lengthMap {f=f} xs) in i))
 257 | --     = index' (f <$> xs) i
 258 | -- mapIndexPreserve (x :: xs) FZ = Refl
 259 | -- mapIndexPreserve (x :: xs) (FS j) = mapIndexPreserve xs j
 260 | 
 261 | 
 262 | -- the idea is that the bottom part of this file will slowly be made obsolete 
 263 | -- as more and more things are implemented in terms of containers
 264 | 
 265 | 
 266 | ||| Any finite container (i.e. whose each set of positions is finite) can be
 267 | ||| given an algebra instance simply by summing up all the concrete values
 268 | public export
 269 | algebraFinite : 
 270 |   (0 c : Cont) -> (isFinite : IsFinite c) =>
 271 |   (0 a : Type) -> Num a =>
 272 |   Algebra (Ext c) a
 273 | algebraFinite c {isFinite = MkI p} _
 274 |   = MkAlgebra $ \(shp <| content) => reduce $ values @{p shp} <&> content
 275 | 
 276 | 
 277 | namespace VectInstances
 278 |   public export
 279 |   {n : Nat} -> Eq x => Eq (Vect' n x) where
 280 |     v == v' = (toVect v) == (toVect v')
 281 |  
 282 |   -- public export
 283 |   -- {n : Nat} -> Show x => Show (Vect' n x) where
 284 |   --   show v = show (toVect v)
 285 | 
 286 |   public export
 287 |   {n : Nat} -> Num a => Algebra (Vect' n) a where
 288 |     reduce v = reduce (toVect v)
 289 | 
 290 |   public export
 291 |   {n : Nat} -> Traversable (Vect' n) where
 292 |     traverse f v = fromVect <$> traverse f (toVect v)
 293 | 
 294 |   -- Applicative and Naperian instance follow because the set of shapes is ()
 295 | 
 296 |   -- analogus to Misc.takeFin, but for Vect'
 297 |   public export 
 298 |   take : {n : Nat} ->
 299 |     (s : Fin (S n)) -> Vect' n a -> Vect' (finToNat s) a
 300 |   take s = fromVect . takeFin s . toVect
 301 | 
 302 |   public export
 303 |   (++) : {n : Nat} -> Vect' n a -> Vect' m a -> Vect' (n + m) a
 304 |   (++) v1 v2 = () <| \i => case splitSum i of
 305 |     Left i1 => index v1 i1
 306 |     Right i2 => index v2 i2
 307 | 
 308 | {---
 309 | Ideally, all instances would be defined in terms of ConcreteTypes,
 310 | but there are totality checking issues with types whose size isn't known
 311 | at compile time
 312 | ---}
 313 | namespace ListInstances
 314 |   ||| Is there a different way to convince Idris' totality checker?
 315 |   public export
 316 |   Eq a => Eq (List' a) where
 317 |     l == l' = assert_total ((toList l) == (toList l'))
 318 | 
 319 |   -- ||| Is there a different way to convince Idris' totality checker?
 320 |   -- public export
 321 |   -- Show a => Show (List' a) where
 322 |   --   show x = assert_total (show (toList x))
 323 | 
 324 |   public export
 325 |   Num a => Algebra List' a where
 326 |     reduce = reduce {f=List} . toList
 327 | 
 328 | 
 329 |   -- some attempts at fixing partiality below
 330 |   -- public export
 331 |   -- showListHelper : Show a => List' a -> String
 332 |   -- showListHelper (0 <| _) = ""
 333 |   -- showListHelper (1 <| index) = show $ index FZ
 334 |   -- showListHelper ((S k) <| index)
 335 |   --   = let (s, rest) = headTail index
 336 |   --     in show s ++ ", " ++ showListHelper (k <| rest)
 337 | 
 338 |   -- public export
 339 |   -- showListHelper : Show a => List' a -> String
 340 |   -- showListHelper x = show (toList x)
 341 | 
 342 | 
 343 | namespace BinTreeInstances
 344 |   ||| Is there a different way to convince Idris' totality checker?
 345 |   public export
 346 |   Eq a => Eq (BinTree' a) where
 347 |     t == t' = assert_total (toBinTreeSame t == toBinTreeSame t')
 348 | 
 349 |   -- ||| Is there a different way to convince Idris' totality checker?
 350 |   -- public export
 351 |   -- Show a => Show (BinTree' a) where
 352 |   --   show = assert_total (show . toBinTreeSame)
 353 | 
 354 |   ||| Summing up nodes and leaves of the tree given by the Num a structure
 355 |   public export
 356 |   Num a => Algebra BinTree' a where
 357 |     reduce = reduce {f=BinTreeSame} . toBinTreeSame
 358 | 
 359 |   -- public export
 360 |   -- binTreePosInterface : InterfaceOnPositions BinTree DecEq
 361 |   -- binTreePosInterface = MkI
 362 | 
 363 | 
 364 | namespace BinTreeLeafInstances
 365 |   ||| Is there a different way to convince Idris' totality checker?
 366 |   public export
 367 |   Eq a => Eq (BinTreeLeaf' a) where
 368 |     t == t' = assert_total (toBinTreeLeaf t == toBinTreeLeaf t')
 369 | 
 370 |   -- ||| Is there a different way to convince Idris' totality checker?
 371 |   -- public export
 372 |   -- Show a => Show (BinTreeLeaf' a) where
 373 |   --   show = assert_total (show . toBinTreeLeaf)
 374 | 
 375 |   ||| Summing up leaves of the tree given by the Num a structure
 376 |   public export
 377 |   Num a => Algebra BinTreeLeaf' a where
 378 |     reduce = reduce {f=BinTreeLeaf} . toBinTreeLeaf
 379 | 
 380 | 
 381 | namespace BinTreeNodeInstances
 382 |   ||| Is there a different way to convince Idris' totality checker?
 383 |   public export
 384 |   Eq a => Eq (BinTreeNode' a) where
 385 |     t == t' = assert_total (toBinTreeNode t == toBinTreeNode t')
 386 | 
 387 |   -- ||| Is there a different way to convince Idris' totality checker?
 388 |   -- public export
 389 |   -- Show a => Show (BinTreeNode' a) where
 390 |   --   show = assert_total (show . toBinTreeNode)
 391 | 
 392 |   ||| Summing up nodes of the tree given by the Num a structure
 393 |   public export
 394 |   Num a => Algebra BinTreeNode' a where
 395 |     reduce = reduce {f=BinTreeNode} . toBinTreeNode