
   0 | module Data.Container.Base.Extension.Instances
   1 | 
   2 | import Data.DPair
   3 | import Data.Vect
   4 | 
   5 | import Data.Container.Base.Object.Definition
   6 | import Data.Container.Base.Morphism.Definition
   7 | import Data.Container.Base.Extension.Definition
   8 | import Data.Container.Base.Product.Definition
   9 | 
  10 | import Data.Container.Base.Object.Instances
  11 | import Data.Container.Base.TreeUtils
  12 | 
  13 | import Data.Trees
  14 | import Data.Fin.Split
  15 | 
  16 | -- import Data.Functor.Naperian
  17 | import Misc
  18 | 
  19 | %hide Data.Vect.fromList
  20 | %hide Prelude.toList
  21 | %hide Prelude.(<|)
  22 | 
  23 | -- todo are these necessary still?
  24 | namespace ExtensionsOfMainExamples
  25 |   ||| Isomorphic to the Identity
  26 |   public export
  27 |   Scalar' : Type -> Type
  28 |   Scalar' = Ext Scalar
  29 | 
  30 |   ||| Isomorphic to Pair
  31 |   public export
  32 |   Pair' : Type -> Type
  33 |   Pair' = Ext Pair
  34 |   
  35 |   ||| Isomorphic to Either
  36 |   public export
  37 |   Either' : Type -> Type
  38 |   Either' = Ext Either
  39 | 
  40 |   ||| Isomorphic to Maybe
  41 |   public export
  42 |   Maybe' : Type -> Type
  43 |   Maybe' = Ext Maybe
  44 |   
  45 |   ||| Isomorphic to List
  46 |   public export
  47 |   List' : Type -> Type
  48 |   List' = Ext List
  49 | 
  50 |   ||| Isomorphic to Vect
  51 |   public export
  52 |   Vect' : (n : Nat) -> Type -> Type
  53 |   Vect' n = Ext (Vect n)
  54 | 
  55 |   ||| Isomorphic to Stream
  56 |   public export
  57 |   Stream' : Type -> Type
  58 |   Stream' = Ext Stream
  59 | 
  60 |   ||| Isomorphic to Data.Tree.BinTreeSame
  61 |   public export
  62 |   BinTree' : Type -> Type
  63 |   BinTree' = Ext BinTree
  64 | 
  65 |   ||| Isomorphic to Data.Tree.BinTreeNode
  66 |   public export
  67 |   BinTreeNode' : Type -> Type
  68 |   BinTreeNode' = Ext BinTreeNode
  69 |   
  70 |   ||| Isomorphic to Data.Tree.BinTreeLeaf
  71 |   public export
  72 |   BinTreeLeaf' : Type -> Type
  73 |   BinTreeLeaf' = Ext BinTreeLeaf
  74 | 
  75 |   {-
  76 |   Technically it is possible to a) use the alias that is below, and b) define Tensor' here, but a decision was made not to do any of these.
  77 |   Rather, Tensor' was defined as a record, and this was done in Data.Tensor as
  78 |   in most linear algebra operations explicit and cumbersome shape annotations 
  79 |   would have been otherwise necessary. Likewise, the definition of usual 
  80 |   interfaces the datatype Tensor' are often involved, making it much simpler
  81 |   to create a separate file for it.
  82 |   -}
  83 |   -- public export
  84 |   -- Tensor' : List Cont -> Type -> Type
  85 |   -- Tensor' cs = Ext (Tensor cs)
  86 | 
  87 | public export
  88 | composeExtensions : List Cont -> Type -> Type
  89 | composeExtensions = foldr (\c, f => (Ext c) . f) (Ext Scalar)
  90 | 
  91 | public export
  92 | fixShape : {c : Cont} ->
  93 |   Ext c a -> Cont
  94 | fixShape e = At c (shapeExt e)
  95 | 
  96 | ||| Continer describing how from an extension of another we can get a value out
  97 | public export
  98 | Pick : Cont -> Type -> Cont
  99 | Pick c a = Const2 (Ext c a) a
 100 | 
 101 | namespace ComposeExtensionsVect
 102 |   public export
 103 |   composeExtensions : Vect n Cont -> Type -> Type
 104 |   composeExtensions = foldr @{straightforward} (\c, f => (Ext c) . f) (Ext Scalar)
 105 | 
 106 | public export
 107 | [fe] {shape : List Cont} -> Functor (composeExtensions shape) where
 108 |   map {shape = []} f = map f
 109 |   map {shape = (s :: ss)} f = (map @{fe} f <$>)
 110 | 
 111 | ||| Generalisation of 'positions' from Data.Functor.Naperian
 112 | ||| Works for an arbitrary container, as long as we supply its shape
 113 | ||| The definition in Data.Functor.Naperian.positions is for Naperian containers
 114 | ||| i.e. containers with a unit shape
 115 | public export
 116 | positionsCont : {0 c : Cont} -> {sh : c.Shp} -> Ext c (c.Pos sh)
 117 | positionsCont = sh <| id
 118 | 
 119 | {-------------------------------------------------------------------------------
 120 | Conversions witnessing the isomorphisms of `ExtensionsOfMainExamples`
 121 | -------------------------------------------------------------------------------}
 122 | 
 123 | namespace List
 124 |   public export
 125 |   fromList : List a -> List' a
 126 |   fromList [] = (0 <| absurd)
 127 |   fromList (x :: xs) = let (l <| c) = fromList xs
 128 |                        in (S l <| cons x c)
 129 | 
 130 |   public export
 131 |   toList : List' a -> List a
 132 |   toList (0 <| _) = []
 133 |   toList l@((S k) <| ind) = head ind :: toList
 134 |     (assert_smaller l (k <| tail ind))
 135 | 
 136 | namespace Vect
 137 |   public export
 138 |   fromVect : Vect n a -> Vect' n a
 139 |   fromVect v = () <| \i => index i v
 140 | 
 141 |   public export
 142 |   toVect : {n : Nat} -> Vect' n a -> Vect n a
 143 |   toVect (_ <| index) = Vect.Fin.tabulate index
 144 | 
 145 | namespace BinTreeSame
 146 |   public export
 147 |   fromBinTreeSame : BinTreeSame a -> BinTree' a
 148 |   fromBinTreeSame (Leaf x) = LeafS <| \_ => x
 149 |   fromBinTreeSame (Node x lt rt) =
 150 |     let (fblt, fbrt) = (fromBinTreeSame lt, fromBinTreeSame rt)
 151 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 152 |         AtNode => x
 153 |         GoLeft posL => index fblt posL
 154 |         GoRight posR => index fbrt posR
 155 | 
 156 |   public export
 157 |   toBinTreeSame : BinTree' a -> BinTreeSame a
 158 |   toBinTreeSame (LeafS <| index) = Leaf (index AtLeaf)
 159 |   toBinTreeSame n@(NodeS lt rt <| index) =
 160 |     Node (index AtNode)
 161 |          (toBinTreeSame $ assert_smaller n (lt <| index . GoLeft))
 162 |          (toBinTreeSame $ assert_smaller n (rt <| index . GoRight))
 163 | 
 164 | namespace BinTreeNode
 165 |   public export
 166 |   fromTreeHelper : BinTreePosNode LeafS -> a
 167 |   fromTreeHelper AtNode impossible
 168 |   fromTreeHelper (GoLeft x) impossible
 169 |   fromTreeHelper (GoRight x) impossible
 170 | 
 171 |   public export
 172 |   fromBinTreeNode : BinTreeNode a -> BinTreeNode' a
 173 |   fromBinTreeNode (Leaf ()) = LeafS <| fromTreeHelper
 174 |   fromBinTreeNode (Node node leftTree rightTree)
 175 |     = let (fblt, fbrt) = (fromBinTreeNode leftTree, fromBinTreeNode rightTree)
 176 |       in (NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 177 |             AtNode => node
 178 |             GoLeft posL => index fblt posL
 179 |             GoRight posR => index fbrt posR)
 180 | 
 181 |   public export
 182 |   toBinTreeNode : BinTreeNode' a -> BinTreeNode a
 183 |   toBinTreeNode (LeafS <| index) = Leaf ()
 184 |   toBinTreeNode n@(NodeS lt rt <| index) = 
 185 |     Node (index AtNode)
 186 |          (toBinTreeNode $ assert_smaller n (lt <| index . GoLeft))
 187 |          (toBinTreeNode $ assert_smaller n (rt <| index . GoRight))
 188 | 
 189 | namespace BinTreeLeaf
 190 |   public export
 191 |   fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a
 192 |   fromBinTreeLeaf (Leaf leaf) = LeafS <| \_ => leaf
 193 |   fromBinTreeLeaf (Node node lt rt) =
 194 |     let (fblt, fbrt) = (fromBinTreeLeaf lt, fromBinTreeLeaf rt)
 195 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
 196 |           GoLeft posL => index fblt posL
 197 |           GoRight posR => index fbrt posR
 198 | 
 199 |   public export
 200 |   toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a
 201 |   toBinTreeLeaf (LeafS <| content) = Leaf (content AtLeaf)
 202 |   toBinTreeLeaf n@(NodeS l r <| content) =
 203 |     Node' (toBinTreeLeaf $ assert_smaller n (l <| content . GoLeft))
 204 |           (toBinTreeLeaf $ assert_smaller n (r <| content . GoRight))
 205 | 
 206 | -- the idea is that the bottom part of this file will slowly be made obsolete 
 207 | -- as more and more things are implemented in terms of containers
 208 | 
 209 | 
 210 | namespace VectInstances
 211 |   public export
 212 |   {n : Nat} -> Eq x => Eq (Vect' n x) where
 213 |     v == v' = (toVect v) == (toVect v')
 214 |  
 215 |   -- public export
 216 |   -- {n : Nat} -> Show x => Show (Vect' n x) where
 217 |   --   show v = show (toVect v)
 218 | 
 219 |   -- Applicative and Naperian instance follow because the set of shapes is ()
 220 | 
 221 |   -- analogus to Misc.takeFin, but for Vect'
 222 |   public export 
 223 |   take : {n : Nat} ->
 224 |     (s : Fin (S n)) -> Vect' n a -> Vect' (finToNat s) a
 225 |   take s = fromVect . takeFin s . toVect
 226 | 
 227 |   public export
 228 |   (++) : {n : Nat} -> Vect' n a -> Vect' m a -> Vect' (n + m) a
 229 |   (++) v1 v2 = () <| \i => case splitSum i of
 230 |     Left i1 => index v1 i1
 231 |     Right i2 => index v2 i2
 232 | 
 233 | {---
 234 | Ideally, all instances would be defined in terms of ConcreteTypes,
 235 | but there are totality checking issues with types whose size isn't known
 236 | at compile time
 237 | ---}
 238 | namespace ListInstances
 239 |   ||| Is there a different way to convince Idris' totality checker?
 240 |   public export
 241 |   Eq a => Eq (List' a) where
 242 |     l == l' = assert_total ((toList l) == (toList l'))
 243 | 
 244 |   -- ||| Is there a different way to convince Idris' totality checker?
 245 |   -- public export
 246 |   -- Show a => Show (List' a) where
 247 |   --   show x = assert_total (show (toList x))
 248 | 
 249 | 
 250 |   -- some attempts at fixing partiality below
 251 |   -- public export
 252 |   -- showListHelper : Show a => List' a -> String
 253 |   -- showListHelper (0 <| _) = ""
 254 |   -- showListHelper (1 <| index) = show $ index FZ
 255 |   -- showListHelper ((S k) <| index)
 256 |   --   = let (s, rest) = headTail index
 257 |   --     in show s ++ ", " ++ showListHelper (k <| rest)
 258 | 
 259 |   -- public export
 260 |   -- showListHelper : Show a => List' a -> String
 261 |   -- showListHelper x = show (toList x)
 262 | 
 263 | 
 264 | namespace BinTreeInstances
 265 |   ||| Is there a different way to convince Idris' totality checker?
 266 |   public export
 267 |   Eq a => Eq (BinTree' a) where
 268 |     t == t' = assert_total (toBinTreeSame t == toBinTreeSame t')
 269 | 
 270 |   -- ||| Is there a different way to convince Idris' totality checker?
 271 |   -- public export
 272 |   -- Show a => Show (BinTree' a) where
 273 |   --   show = assert_total (show . toBinTreeSame)
 274 | 
 275 | 
 276 | namespace BinTreeLeafInstances
 277 |   ||| Is there a different way to convince Idris' totality checker?
 278 |   public export
 279 |   Eq a => Eq (BinTreeLeaf' a) where
 280 |     t == t' = assert_total (toBinTreeLeaf t == toBinTreeLeaf t')
 281 | 
 282 |   -- ||| Is there a different way to convince Idris' totality checker?
 283 |   -- public export
 284 |   -- Show a => Show (BinTreeLeaf' a) where
 285 |   --   show = assert_total (show . toBinTreeLeaf)
 286 | 
 287 | 
 288 | namespace BinTreeNodeInstances
 289 |   ||| Is there a different way to convince Idris' totality checker?
 290 |   public export
 291 |   Eq a => Eq (BinTreeNode' a) where
 292 |     t == t' = assert_total (toBinTreeNode t == toBinTreeNode t')
 293 | 
 294 |   -- ||| Is there a different way to convince Idris' totality checker?
 295 |   -- public export
 296 |   -- Show a => Show (BinTreeNode' a) where
 297 |   --   show = assert_total (show . toBinTreeNode)
 298 |