0 | module Data.Container.Base.Properties.Instances
  1 |
  2 | import Data.Fin
  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.Properties.Definitions
  9 | import Data.Container.Base.Product.Definitions
 10 |
 11 | import Data.Container.Base.Object.Instances
 12 | import Data.Container.Base.Extension.Instances
 13 | import Data.Container.Base.Morphism.Instances
 14 |
 15 | import Data.Trees
 16 | import Data.Functor.Products
 17 | import Data.Container.Base.TreeUtils
 18 |
 19 | import Misc
 20 |
 21 | %hide Data.Vect.fromList
 22 |
 23 | public export
 24 | IsConcrete Scalar where
 25 |   func = id
 26 |   functorInstance = MkFunctor id
 27 |   fromConcreteTy = pure
 28 |   toConcreteTy (() <| f) = f ()
 29 |
 30 | public export
 31 | IsConcrete Maybe where
 32 |   func = Maybe
 33 |   functorInstance = %search
 34 |
 35 |   fromConcreteTy Nothing = False <| absurd
 36 |   fromConcreteTy (Just x) = True <| \() => x
 37 |
 38 |   toConcreteTy (False <| _) = Nothing
 39 |   toConcreteTy (True <| f) = Just (f ())
 40 |
 41 | public export
 42 | IsConcrete Pair where
 43 |   func = \a => Pair a a
 44 |   functorInstance = MkFunctor $ \f, (x, y) => (f x, f y)
 45 |   fromConcreteTy (x, y) = () <| \case False => x; True => y
 46 |   toConcreteTy (() <| f) = (f False, f True)
 47 |
 48 | ||| This is a concrete instance for Naperian containers
 49 | ||| It applies also to `s=Fin n` which is covered by Vect
 50 | ||| We therefore want this to only be applied if Vect isn't
 51 | %defaulthint
 52 | public export
 53 | lambdaNap : {s : Type} -> IsConcrete (Nap s)
 54 | lambdaNap = MkIsConcrete
 55 |   (\a => s -> a)
 56 |   (MkFunctor (.))
 57 |   (\content => () <| content)
 58 |   (\(() <| content) => content)
 59 |
 60 | public export
 61 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >< d) where
 62 |   func = func @{icc} >< func @{icd}
 63 |   functorInstance = ?functorInstanceHancockProduct
 64 |   fromConcreteTy = ?fromConcreteTyHancockProduct
 65 |   toConcreteTy = ?toConcreteTyHancockProduct
 66 |
 67 | public export
 68 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >@ d) where
 69 |   func = func @{icc} . func @{icd}
 70 |   functorInstance = MkFunctor $ \f => ?functorInstanceCompositionProduct
 71 |   fromConcreteTy = ?fromConcreteTyCompositionProduct
 72 |   toConcreteTy = ?toConcreteTyCompositionProduct
 73 |
 74 |
 75 | ||| For recursive types we need to extract out the conversion functions
 76 | namespace List
 77 |   public export
 78 |   fromList : List a -> List' a
 79 |   fromList [] = (0 <| absurd)
 80 |   fromList (x :: xs) = let (l <| c) = fromList xs
 81 |                        in (S l <| cons x c)
 82 |
 83 |   public export
 84 |   toList : List' a -> List a
 85 |   toList (0 <| _) = []
 86 |   toList l@((S k) <| ind) = head ind :: toList
 87 |     (assert_smaller l (k <| tail ind))
 88 |
 89 |   public export
 90 |   IsConcrete List where
 91 |     func = List
 92 |     functorInstance = %search
 93 |     fromConcreteTy = fromList
 94 |     toConcreteTy = toList
 95 |
 96 | namespace Vect
 97 |   public export
 98 |   fromVect : Vect n a -> Vect' n a
 99 |   fromVect v = () <| \i => index i v
100 |   
101 |   public export
102 |   toVect : {n : Nat} -> Vect' n a -> Vect n a
103 |   toVect (_ <| index) = Vect.Fin.tabulate index
104 |
105 |   public export prefix 0 >##, ##>
106 |
107 |   public export
108 |   (>##) : Vect n a -> Vect' n a
109 |   (>##) = fromVect
110 |
111 |   public export
112 |   (##>) : {n : Nat} -> Vect' n a -> Vect n a
113 |   (##>) = toVect
114 |
115 |   -- public export
116 |   -- test : {n : Nat} -> IsConcrete (Vect n)
117 |   -- test = MkIsConcrete
118 |   --   (Vect n)
119 |   --   (%search)
120 |   --   (fromVect)
121 |   --   (toVect)
122 |
123 |   public export
124 |   {n : Nat} -> IsConcrete (Vect n) where
125 |     func = Vect n
126 |     functorInstance = %search
127 |     fromConcreteTy = fromVect
128 |     toConcreteTy = toVect
129 |
130 | namespace Grid
131 |   public export
132 |   {h, w : Nat} -> IsConcrete (Grid (h, w)) where
133 |     func a = (Fin h, Fin w) -> a
134 |     functorInstance = MkFunctor (.)
135 |     fromConcreteTy content = ((), ()) <| content
136 |     toConcreteTy (((), ()) <| content) = content
137 |
138 | namespace BinTreeSame
139 |   public export
140 |   fromBinTreeSame : BinTreeSame a -> BinTree' a
141 |   fromBinTreeSame (Leaf x) = LeafS <| \_ => x
142 |   fromBinTreeSame (Node x lt rt) =
143 |     let (fblt, fbrt) = (fromBinTreeSame lt, fromBinTreeSame rt)
144 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
145 |         AtNode => x
146 |         GoLeft posL => index fblt posL
147 |         GoRight posR => index fbrt posR
148 |
149 |   public export
150 |   toBinTreeSame : BinTree' a -> BinTreeSame a
151 |   toBinTreeSame (LeafS <| index) = Leaf (index AtLeaf)
152 |   toBinTreeSame n@(NodeS lt rt <| index) =
153 |     Node (index AtNode)
154 |          (toBinTreeSame $ assert_smaller n (lt <| index . GoLeft))
155 |          (toBinTreeSame $ assert_smaller n (rt <| index . GoRight))
156 |
157 |   public export
158 |   IsConcrete BinTree where
159 |     func = BinTreeSame
160 |     functorInstance = %search
161 |     fromConcreteTy = fromBinTreeSame
162 |     toConcreteTy = toBinTreeSame
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 |   public export
190 |   IsConcrete BinTreeNode where
191 |     func = BinTreeNode
192 |     functorInstance = %search
193 |     fromConcreteTy = fromBinTreeNode
194 |     toConcreteTy = toBinTreeNode
195 |
196 | namespace BinTreeLeaf
197 |   public export
198 |   fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a
199 |   fromBinTreeLeaf (Leaf leaf) = LeafS <| \_ => leaf
200 |   fromBinTreeLeaf (Node node lt rt) =
201 |     let (fblt, fbrt) = (fromBinTreeLeaf lt, fromBinTreeLeaf rt)
202 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
203 |           GoLeft posL => index fblt posL
204 |           GoRight posR => index fbrt posR
205 |
206 |   public export
207 |   toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a
208 |   toBinTreeLeaf (LeafS <| content) = Leaf (content AtLeaf)
209 |   toBinTreeLeaf n@(NodeS l r <| content) =
210 |     Node' (toBinTreeLeaf $ assert_smaller n (l <| content . GoLeft))
211 |           (toBinTreeLeaf $ assert_smaller n (r <| content . GoRight))
212 |
213 |   public export
214 |   IsConcrete BinTreeLeaf where
215 |     func = BinTreeLeaf
216 |     functorInstance = %search
217 |     fromConcreteTy = fromBinTreeLeaf
218 |     toConcreteTy = toBinTreeLeaf
219 |
220 |
221 | public export
222 | foldList : (a -> b -> b) -> b -> List' a -> b
223 | foldList f z (0 <| _) = z
224 | foldList f z l@((S k) <| content)
225 |   = f (head content) $ foldList f z
226 |     (assert_smaller l (k <| tail content))
227 |
228 | public export
229 | IsFoldable c => Foldable (Ext c) where
230 |   foldr @{(MkIsFoldable toL)} f z = foldList f z . extMap toL 
231 |
232 | public export
233 | IsFoldable List where
234 |   mapToList = id
235 |
236 | public export
237 | {n : Nat} -> IsFoldable (Vect n) where
238 |   mapToList = vectToList
239 |
240 | ||| Requires making a choice of traversal order
241 | ||| Is there a good reason to prefer a particular order?
242 | public export
243 | IsFoldable BinTreeLeaf where
244 |   mapToList = inorder
245 |
246 | public export
247 | IsFoldable BinTreeNode where
248 |   mapToList = inorder
249 |
250 | public export
251 | IsFoldable BinTree where
252 |   mapToList = inorder
253 |
254 | -- old
255 | -- ||| Indexing an element of `xs` and then applying `f` to it is the same as
256 | -- ||| mapping `f` over xs, and then indexing the result
257 | -- public export
258 | -- mapIndexPreserve : {0 f : a -> b} ->
259 | --   (xs : List a) ->
260 | --   (i : Fin (length (f <$> xs))) ->
261 | --   f (index' xs (rewrite sym (lengthMap {f=f} xs) in i))
262 | --     = index' (f <$> xs) i
263 | -- mapIndexPreserve (x :: xs) FZ = Refl
264 | -- mapIndexPreserve (x :: xs) (FS j) = mapIndexPreserve xs j