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 |   concreteType = id
 26 |   concreteFunctor = MkFunctor id
 27 |   fromConcreteTy = pure
 28 |   toConcreteTy (() <| f) = f ()
 29 |
 30 | public export
 31 | IsConcrete Maybe where
 32 |   concreteType = Maybe
 33 |   concreteFunctor = %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 |   concreteType = \a => Pair a a
 44 |   concreteFunctor = 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 | public export
 49 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >< d) where
 50 |   concreteType = concreteType @{icc} >< concreteType @{icd}
 51 |   concreteFunctor = ?concreteFunctorHancockProduct
 52 |   fromConcreteTy = ?fromConcreteTyHancockProduct
 53 |   toConcreteTy = ?toConcreteTyHancockProduct
 54 |
 55 | public export
 56 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >@ d) where
 57 |   concreteType = concreteType @{icc} . concreteType @{icd}
 58 |   concreteFunctor = MkFunctor $ \f => ?concreteFunctorCompositionProduct
 59 |   fromConcreteTy = ?fromConcreteTyCompositionProduct
 60 |   toConcreteTy = ?toConcreteTyCompositionProduct
 61 |
 62 |
 63 | ||| For recursive types we need to extract out the conversion functions
 64 | namespace List
 65 |   public export
 66 |   fromList : List a -> List' a
 67 |   fromList [] = (0 <| absurd)
 68 |   fromList (x :: xs) = let (l <| c) = fromList xs
 69 |                        in (S l <| cons x c)
 70 |
 71 |   public export
 72 |   toList : List' a -> List a
 73 |   toList (0 <| _) = []
 74 |   toList ((S k) <| ind) = head ind :: toList (k <| tail ind)
 75 |
 76 |   public export
 77 |   IsConcrete List where
 78 |     concreteType = List
 79 |     concreteFunctor = %search
 80 |     fromConcreteTy = fromList
 81 |     toConcreteTy = toList
 82 |
 83 | namespace Vect
 84 |   public export
 85 |   fromVect : Vect n a -> Vect' n a
 86 |   fromVect v = () <| \i => index i v
 87 |   
 88 |   public export
 89 |   toVect : {n : Nat} -> Vect' n a -> Vect n a
 90 |   toVect (_ <| index) = Vect.Fin.tabulate index
 91 |
 92 |   public export
 93 |   {n : Nat} -> IsConcrete (Vect n) where
 94 |     concreteType = Vect n
 95 |     concreteFunctor = %search
 96 |     fromConcreteTy = fromVect
 97 |     toConcreteTy = toVect
 98 |
 99 | namespace BinTreeSame
100 |   public export
101 |   fromBinTreeSame : BinTreeSame a -> BinTree' a
102 |   fromBinTreeSame (Leaf x) = LeafS <| \_ => x
103 |   fromBinTreeSame (Node x lt rt) =
104 |     let (fblt, fbrt) = (fromBinTreeSame lt, fromBinTreeSame rt)
105 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
106 |         AtNode => x
107 |         GoLeft posL => index fblt posL
108 |         GoRight posR => index fbrt posR
109 |
110 |   public export
111 |   toBinTreeSame : BinTree' a -> BinTreeSame a
112 |   toBinTreeSame (LeafS <| index) = Leaf (index AtLeaf)
113 |   toBinTreeSame (NodeS lt rt <| index) =
114 |     Node (index AtNode)
115 |          (toBinTreeSame (lt <| index . GoLeft))
116 |          (toBinTreeSame (rt <| index . GoRight))
117 |
118 |   public export
119 |   IsConcrete BinTree where
120 |     concreteType = BinTreeSame
121 |     concreteFunctor = %search
122 |     fromConcreteTy = fromBinTreeSame
123 |     toConcreteTy = toBinTreeSame
124 |
125 | namespace BinTreeNode
126 |   public export
127 |   fromTreeHelper : BinTreePosNode LeafS -> a
128 |   fromTreeHelper AtNode impossible
129 |   fromTreeHelper (GoLeft x) impossible
130 |   fromTreeHelper (GoRight x) impossible
131 |   
132 |   public export
133 |   fromBinTreeNode : BinTreeNode a -> BinTreeNode' a
134 |   fromBinTreeNode (Leaf ()) = LeafS <| fromTreeHelper
135 |   fromBinTreeNode (Node node leftTree rightTree)
136 |     = let (fblt, fbrt) = (fromBinTreeNode leftTree, fromBinTreeNode rightTree)
137 |       in (NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
138 |             AtNode => node
139 |             GoLeft posL => index fblt posL
140 |             GoRight posR => index fbrt posR)
141 |
142 |   public export
143 |   toBinTreeNode : BinTreeNode' a -> BinTreeNode a
144 |   toBinTreeNode (LeafS <| index) = Leaf ()
145 |   toBinTreeNode (NodeS lt rt <| index) = 
146 |     Node (index AtNode)
147 |          (toBinTreeNode (lt <| index . GoLeft))
148 |          (toBinTreeNode (rt <| index . GoRight))
149 |
150 |   public export
151 |   IsConcrete BinTreeNode where
152 |     concreteType = BinTreeNode
153 |     concreteFunctor = %search
154 |     fromConcreteTy = fromBinTreeNode
155 |     toConcreteTy = toBinTreeNode
156 |
157 | namespace BinTreeLeaf
158 |   public export
159 |   fromBinTreeLeaf : BinTreeLeaf a -> BinTreeLeaf' a
160 |   fromBinTreeLeaf (Leaf leaf) = LeafS <| \_ => leaf
161 |   fromBinTreeLeaf (Node node lt rt) =
162 |     let (fblt, fbrt) = (fromBinTreeLeaf lt, fromBinTreeLeaf rt)
163 |     in NodeS (shapeExt fblt) (shapeExt fbrt) <| \case
164 |           GoLeft posL => index fblt posL
165 |           GoRight posR => index fbrt posR
166 |
167 |   public export
168 |   toBinTreeLeaf : BinTreeLeaf' a -> BinTreeLeaf a
169 |   toBinTreeLeaf (LeafS <| content) = Leaf (content AtLeaf)
170 |   toBinTreeLeaf (NodeS l r <| content) =
171 |     Node' (toBinTreeLeaf (l <| content . GoLeft))
172 |           (toBinTreeLeaf (r <| content . GoRight))
173 |
174 |   public export
175 |   IsConcrete BinTreeLeaf where
176 |     concreteType = BinTreeLeaf
177 |     concreteFunctor = %search
178 |     fromConcreteTy = fromBinTreeLeaf
179 |     toConcreteTy = toBinTreeLeaf
180 |
181 |
182 | public export
183 | foldList : (a -> b -> b) -> b -> List' a -> b
184 | foldList f z (0 <| _) = z
185 | foldList f z ((S k) <| content)
186 |   = f (head content) $ foldList f z (k <| tail content)
187 |
188 | public export
189 | IsFoldable c => Foldable (Ext c) where
190 |   foldr @{(MkIsFoldable toL)} f z = foldList f z . extMap toL 
191 |
192 | public export
193 | IsFoldable List where
194 |   mapToList = id
195 |
196 | public export
197 | {n : Nat} -> IsFoldable (Vect n) where
198 |   mapToList = vectToList
199 |
200 | ||| Requires making a choice of traversal order
201 | ||| Is there a good reason to prefer a particular order?
202 | public export
203 | IsFoldable BinTreeLeaf where
204 |   mapToList = inorder
205 |
206 | public export
207 | IsFoldable BinTreeNode where
208 |   mapToList = inorder
209 |
210 | public export
211 | IsFoldable BinTree where
212 |   mapToList = inorder
213 |
214 | -- old
215 | -- ||| Indexing an element of `xs` and then applying `f` to it is the same as
216 | -- ||| mapping `f` over xs, and then indexing the result
217 | -- public export
218 | -- mapIndexPreserve : {0 f : a -> b} ->
219 | --   (xs : List a) ->
220 | --   (i : Fin (length (f <$> xs))) ->
221 | --   f (index' xs (rewrite sym (lengthMap {f=f} xs) in i))
222 | --     = index' (f <$> xs) i
223 | -- mapIndexPreserve (x :: xs) FZ = Refl
224 | -- mapIndexPreserve (x :: xs) (FS j) = mapIndexPreserve xs j