0 | module Data.Container.Base.Properties.Instances

  2 | import Data.Fin

  3 | import Data.Vect

  4 | import Data.List.Quantifiers

  5 | import Decidable.Equality

  6 | import Data.Fin.Split

  7 | import Data.Finite

  9 | import Data.Container.Base.Object.Definition

 10 | import Data.Container.Base.Morphism.Definition

 11 | import Data.Container.Base.Extension.Definition

 12 | import Data.Container.Base.Properties.Definition

 13 | import Data.Container.Base.Endofunctor.Definition

 14 | import Data.Container.Base.Product.Definition

 16 | import Data.Container.Base.Object.Instances

 17 | import Data.Container.Base.Extension.Instances

 18 | import Data.Container.Base.Morphism.Instances

 20 | import Data.Trees

 21 | import Data.Functor.Products

 22 | import Data.Functor.Algebra

 23 | import Data.Layout

 24 | import Data.Container.Base.TreeUtils

 26 | import Misc

 28 | %hide Data.Vect.fromList

 29 | %hide Prelude.toList

 30 | %hide Prelude.(<|)

 37 | public export

 38 | EmptyExt : {0 c : Cont} -> IsNaperian c => Ext c Unit

 39 | EmptyExt @{Via _} = () <| \_ => ()

 41 | public export

 42 | liftA2ConstCont : IsNaperian c => Ext c a -> Ext c b -> Ext c (a, b)

 43 | liftA2ConstCont @{Via _} ea eb = () <| (\x => (index ea x, index eb x))

 48 | public export

 49 | IsNaperian c => Applicative (Ext c) where

 50 |   pure @{Via _} a = () <| \_ => a

 51 |   (<*>) fs xs @{Via _} = uncurry ($) <$> liftA2ConstCont fs xs

 53 | namespace CompositionTensorInteraction

 54 |   ||| Going the other way is impossible without any constraints

 56 |   public export

 57 |   compToTensor : IsNaperian d =>

 58 |     c >@ d =%> c >< d

 59 |   compToTensor @{(Via dPos)} = !% \(cShp <| content) =>

 60 |     ((cShp,()) ** \(cPos, dPos) => (cPos ** dPos))

 62 |   public export

 63 |   compToTensor2 : IsFlat c =>

 64 |     c >@ d =%> c >< d

 65 |   compToTensor2 @{(Via cShp)} = !% \(cShp <| dShp) =>

 66 |     ((cShp, dShp ()) ** \((), dPos') => (() ** dPos'))

 68 | namespace Transpose

 69 |   public export

 70 |   transposeLens : IsNaperian c => IsNaperian d => c >@ d =%> d >@ c

 71 |   transposeLens @{Via _} @{Via _} = !% \(() <| _) =>

 72 |     (() <| (\_ => ()) ** \(dInd ** cInd) => (cInd ** dInd))

 74 |   public export

 75 |   transpose : IsNaperian c => IsNaperian d =>

 76 |     Tensor [c, d] =%> Tensor [d, c]

 77 |   transpose @{Via _} @{Via _} = wrapIntoMatrix transposeLens

 79 |   -- ||| experiment, does this work?

 80 |   -- public export

 81 |   -- transposeMiddle : IsNaperian c => IsNaperian e =>

 82 |   --   Tensor [c, e, d] =%>

 85 |   --||| Transpose a given element to the front of the shape

 86 |   --public export

 87 |   --transposeToFront : (shape : List Cont) ->

 88 |   --  (c : Cont) ->

 89 |   --  (elem : Elem c shape) =>

 90 |   --  All IsNaperian (dropAfterElem shape elem) =>

 91 |   --  Tensor shape =%> Tensor (c :: dropElem shape elem)

 92 |   --transposeToFront (_ :: xs) c @{Here} @{allNap} = ?transposeToFront_rhs_0

 93 |   --transposeToFront (y :: xs) c @{(There x)} @{allNap} = ?transposeToFront_rhs_1

 95 | namespace CubicalHelpers

 96 |   ||| Helper function allowing `shape` in `cubicalShape` to have zero annotation

 97 |   public export

 98 |   cubicalShapeHelper : All IsCubical shape -> List Nat

 99 |   cubicalShapeHelper [] = []

100 |   cubicalShapeHelper (ic :: ics) = dimHelper ic :: cubicalShapeHelper ics

101 |     

102 |   ||| Given a list of cubical containers, return the list of their dimensions

103 |   public export

104 |   cubicalShape : (0 shape : List Cont) -> All IsCubical shape => List Nat

105 |   cubicalShape _ @{ac} = cubicalShapeHelper ac

106 |     

107 |   ||| Size of a list of cubical containers is the product of their dimensions

108 |   public export

109 |   size : (0 shape : List Cont) -> All IsCubical shape => Nat

110 |   size shape = prod (cubicalShape shape)

113 | public export

114 | flattenCubical : {shape : List Cont} ->

115 |   (ac : All IsCubical shape) =>

116 |   LayoutOrder ->

117 |   Tensor shape =%> Vect (size shape)

118 | flattenCubical {shape = [], ac=[]} _ = !% \() => (() ** \FZ => ())

119 | flattenCubical {shape = (_ :: ss), ac=(Via n :: as)} lo

120 |   = !% \(() <| t) => (() ** \idx =>

121 |       let (!% recBackward) = flattenCubical {shape = ss} lo

122 |           (i, rest) = splitFinProd lo idx

123 |           (_ ** backRec) = recBackward (t i)

124 |       in (i ** backRec rest))

127 | public export

128 | unflattenCubical : {shape : List Cont} ->

129 |   (ac : All IsCubical shape) =>

130 |   LayoutOrder ->

131 |   Vect (size shape) =%> Tensor shape

132 | unflattenCubical {shape = [], ac=[]} lo = !% \() => (() ** \() => FZ)

133 | unflattenCubical {shape = (_ :: ss), ac=((Via n) :: as)} lo =

134 |   let (!% f) = unflattenCubical {shape = ss} lo

135 |       (innerShape ** innerBack) = f ()

136 |   in !% \() => ((() <| \_ => innerShape) ** (\(cp ** restPos) =>

137 |     indexFinProd lo cp (innerBack restPos)))

140 | public export

141 | recastFlattenedTensor : {oldShape, newShape : List Cont} ->

142 |   (oldAc : All IsCubical oldShape) => (newAc : All IsCubical newShape) =>

143 |   {auto prf : size oldShape = size newShape} ->

144 |   Vect (size oldShape) =%> Vect (size newShape)

145 | recastFlattenedTensor = !% \() => (() ** \i => rewrite prf in i)

150 | public export

151 | reshape : {oldShape, newShape : List Cont} ->

152 |   (oldAc : All IsCubical oldShape) => (newAc : All IsCubical newShape) =>

153 |   LayoutOrder ->

154 |   {auto prf : size oldShape = size newShape} ->

155 |   Tensor oldShape =%> Tensor newShape

156 | reshape lo = flattenCubical lo

157 |          %>> recastFlattenedTensor

158 |          %>> unflattenCubical lo

161 | namespace TransformIntoHancockTensor

162 |   public export

163 |   hancockTensorNaperianShape : {shape : List Cont} ->

164 |     (allNap : All IsNaperian shape) =>

165 |     (HancockTensor shape).Shp

166 |   hancockTensorNaperianShape {shape = []} = ()

167 |   hancockTensorNaperianShape {allNap = ((Via _) :: _)}

168 |     = ((), hancockTensorNaperianShape)

169 |   

170 |   ||| Helper to compute the unique shape of Tensor when all containers are Naperian

171 |   public export

172 |   tensorNaperianShape : {shape : List Cont} ->

173 |     (allNap : All IsNaperian shape) =>

174 |     (Tensor shape).Shp

175 |   tensorNaperianShape {shape = []} = ()

176 |   tensorNaperianShape {shape = (_ :: ss), allNap = ((Via _) :: ns)}

177 |     = () <| \_ => tensorNaperianShape {shape = ss} @{ns}

178 |   

179 |   ||| Analogous to `naperianPosEq` but for the HancockTensor structure

182 |   public export

183 |   hancockTensorPosEq : {shape : List Cont} ->

184 |     (allNap : All IsNaperian shape) =>

185 |     {0 x, y : (HancockTensor shape).Shp} ->

186 |     (HancockTensor shape).Pos x = (HancockTensor shape).Pos y

187 |   hancockTensorPosEq {allNap = []} = Refl

188 |   hancockTensorPosEq {allNap = ((Via _) :: _)} = cong2 Pair

189 |     (naperianPosEq @{Via _} {x=()} {y=()})

190 |     hancockTensorPosEq

191 |   

192 |   ||| Tensor shape is isomorphic to HancockTensor shape when all containers in

194 |   public export

195 |   transformToHancock : {shape : List Cont} ->

196 |     All IsNaperian shape =>

197 |     Tensor shape =%> HancockTensor shape

198 |   transformToHancock {shape = []} = id

199 |   transformToHancock {shape = (_ :: _)} @{((Via _) :: _)}

200 |     = !% \(() <| content) => (((), hancockTensorNaperianShape) **

201 |        \(p, restPos) =>

202 |          let (_ ** recBack) = (%!) transformToHancock (content p)

203 |          in (p ** recBack $ replace {p = id} hancockTensorPosEq restPos))

205 |   public export

206 |   transformFromHancock : {shape : List Cont} ->

207 |     All IsNaperian shape =>

208 |     HancockTensor shape =%> Tensor shape

209 |   transformFromHancock {shape = []} = id

210 |   transformFromHancock {shape = (Nap s :: ss)} @{((Via s) :: _)}

211 |     = !% \((), hShp) =>

212 |         let (tShp ** recBack) = (%!) transformFromHancock hShp

213 |         in (() <| (\_ => tShp) ** \(p ** restPos) => (p, recBack restPos))

215 | public export

216 | IsConcrete Scalar where

217 |   func = id

218 |   functorInstance = MkFunctor id

219 |   fromConcreteTy x = () <| \_ => x

220 |   toConcreteTy (() <| f) = f ()

222 | public export

223 | IsConcrete UnitCont where

224 |   func = const Unit

225 |   functorInstance = MkFunctor (\f, () => ())

226 |   fromConcreteTy () = () <| absurd

227 |   toConcreteTy _ = ()

229 | public export

230 | IsConcrete Maybe where

231 |   func = Maybe

232 |   functorInstance = %search

234 |   fromConcreteTy Nothing = False <| absurd

235 |   fromConcreteTy (Just x) = True <| \() => x

237 |   toConcreteTy (False <| _) = Nothing

238 |   toConcreteTy (True <| f) = Just (f ())

240 | public export

241 | IsConcrete Pair where

242 |   func = \a => Pair a a

243 |   functorInstance = MkFunctor $ \f, (x, y) => (f x, f y)

244 |   fromConcreteTy (x, y) = () <| \case False => x; True => y

245 |   toConcreteTy (() <| f) = (f False, f True)

251 | public export

252 | lambdaNap : {s : Type} -> IsConcrete (Nap s)

253 | lambdaNap = MkIsConcrete

254 |   (\a => s -> a)

255 |   (MkFunctor (.))

256 |   (\content => () <| content)

257 |   (\(() <| content) => content)

259 | public export

260 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >< d) where

261 |   func = func @{icc} >< func @{icd}

262 |   functorInstance = ?functorInstanceHancockProduct

263 |   fromConcreteTy = ?fromConcreteTyHancockProduct

264 |   toConcreteTy = ?toConcreteTyHancockProduct

266 | public export

267 | (icc : IsConcrete c) => (icd : IsConcrete d) => IsConcrete (c >@ d) where

268 |   func = func @{icc} . func @{icd}

269 |   functorInstance = MkFunctor $ \f => ?functorInstanceCompositionProduct

270 |   fromConcreteTy = ?fromConcreteTyCompositionProduct

271 |   toConcreteTy = ?toConcreteTyCompositionProduct

276 | namespace List

277 |   public export

278 |   IsConcrete List where

279 |     func = List

280 |     functorInstance = %search

281 |     fromConcreteTy = fromList

282 |     toConcreteTy = toList

284 | namespace Vect

285 |   -- public export

286 |   -- test : {n : Nat} -> IsConcrete (Vect n)

287 |   -- test = MkIsConcrete

288 |   --   (Vect n)

289 |   --   (%search)

290 |   --   (fromVect)

291 |   --   (toVect)

293 |   public export

294 |   {n : Nat} -> IsConcrete (Vect n) where

295 |     func = Vect n

296 |     functorInstance = %search

297 |     fromConcreteTy = fromVect

298 |     toConcreteTy = toVect

300 | namespace Grid

301 |   public export

302 |   {h, w : Nat} -> IsConcrete (Grid (h, w)) where

303 |     func a = (Fin h, Fin w) -> a

304 |     functorInstance = MkFunctor (.)

305 |     fromConcreteTy content = ((), ()) <| content

306 |     toConcreteTy (((), ()) <| content) = content

308 | namespace BinTreeSame

309 |   public export

310 |   IsConcrete BinTree where

311 |     func = BinTreeSame

312 |     functorInstance = %search

313 |     fromConcreteTy = fromBinTreeSame

314 |     toConcreteTy = toBinTreeSame

316 | namespace BinTreeNode

317 |   public export

318 |   IsConcrete BinTreeNode where

319 |     func = BinTreeNode

320 |     functorInstance = %search

321 |     fromConcreteTy = fromBinTreeNode

322 |     toConcreteTy = toBinTreeNode

324 | namespace BinTreeLeaf

325 |   public export

326 |   IsConcrete BinTreeLeaf where

327 |     func = BinTreeLeaf

328 |     functorInstance = %search

329 |     fromConcreteTy = fromBinTreeLeaf

330 |     toConcreteTy = toBinTreeLeaf

335 | public export

336 | maybeIsDecidable : IsDecidable Maybe

337 | maybeIsDecidable = MkI decPos

338 |   where decPos : (b : Bool) -> DecEq (if b then Unit else Void)

339 |         decPos False = %search

340 |         decPos True = %search

343 | public export

344 | maybeTwoIsDecidable : IsDecidable MaybeTwo

345 | maybeTwoIsDecidable = MkI decPos

346 |   where decPos : (b : Bool) -> DecEq (if b then Fin 2 else Void)

347 |         decPos False = %search

348 |         decPos True = %search

350 | public export

351 | compositionIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >@ d)

352 | compositionIsDecidable @{cd} @{dd} = MkI $ \ex => DecEqDPair

353 |   @{GetInterface cd (shapeExt ex)} @{\cp => GetInterface dd (index ex cp)}

356 | public export

357 | hancockIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >< d)

358 | hancockIsDecidable @{cd} @{dd} = MkI $ \ss =>

359 |   let decC = GetInterface cd (fst ss)

360 |       decD = GetInterface dd (snd ss)

361 |   in %search

364 | public export

365 | cartesianIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >*< d)

366 | cartesianIsDecidable @{cd} @{dd} = MkI $ \ss =>

367 |   let decC = GetInterface cd (fst ss)

368 |       decD = GetInterface dd (snd ss)

369 |   in %search

372 | public export

373 | coproductIsDecidable : IsDecidable c => IsDecidable d => IsDecidable (c >+< d)

374 | coproductIsDecidable @{cd} @{dd} = MkI decPos

375 |   where decPos : (es : Either c.Shp d.Shp) -> DecEq (either c.Pos d.Pos es)

376 |         decPos (Left s) = GetInterface cd s

377 |         decPos (Right s) = GetInterface dd s

381 | public export

382 | tensorIsDecidable : All IsDecidable cs => IsDecidable (Tensor cs)

383 | tensorIsDecidable @{[]} = %search

384 | tensorIsDecidable @{cd :: cds}

385 |   = compositionIsDecidable @{cd} @{tensorIsDecidable @{cds}}

406 | public export

407 | IsFoldable c => Foldable (Ext c) where

408 |   foldr @{Along toL} f z e = foldr

409 |     (\p, acc => f (index e p) acc)

410 |     z

411 |     (tabulate (toL.bwd (shapeExt e)))

415 | public export

416 | enumerableIsFoldable : IsEnumerable c => IsFoldable c

417 | enumerableIsFoldable @{MkIsEnum e} = Along (!% (%! ((:%) e)))

421 | public export

422 | listIsEnumerable : IsEnumerable List

423 | listIsEnumerable = MkIsEnum (!: \n => (n ** idIso))

426 | public export

427 | list1IsEnumerable : IsEnumerable List1

428 | list1IsEnumerable = MkIsEnum (!: \n => (S n ** idIso))

431 | public export

432 | vectIsEnumerable : {n : Nat} -> IsEnumerable (Vect n)

433 | vectIsEnumerable = MkIsEnum (!: \() => (n ** idIso))

436 | public export

437 | forgetOrder : List =%> Bag

438 | forgetOrder = !% \n => (n ** toFin)

442 | public export

443 | foldableIsSummable : IsFoldable c => IsSummable c

444 | foldableIsSummable @{Along toL} = Along (toL %>> forgetOrder)

447 | public export

448 | foldableAt : IsFoldable c => (s : c.Shp) -> IsFoldable (At c s)

449 | foldableAt s = Along (atShape s %>> mapToList)

452 | public export

453 | index : IsFoldable c => Pick c a =%> List

454 | index = pick %>> mapToList

460 | public export

461 | binTreeLeafIsEnumerable : IsEnumerable BinTreeLeaf

462 | binTreeLeafIsEnumerable = MkIsEnum (!: \b => (numLeaves b ** MkIso

463 |   ?inorderForward_binTreeLeaf (BinTreeLeaf.inorderBackward b)

464 |   ?inorderForwardBackward_binTreeLeaf ?inorderBackwardForward_binTreeLeaf))

467 | public export

468 | binTreeNodeIsEnumerable : IsEnumerable BinTreeNode

469 | binTreeNodeIsEnumerable = MkIsEnum (!: \b => (numNodes b ** MkIso

470 |   ?inorderForward_binTreeNode (BinTreeNode.inorderBackward b)

471 |   ?inorderForwardBackward_binTreeNode ?inorderBackwardForward_binTreeNode))

474 | public export

475 | binTreeIsEnumerable : IsEnumerable BinTree

476 | binTreeIsEnumerable = MkIsEnum (!: \b => (numNodesAndLeaves b ** MkIso

477 |   ?inorderForward_binTree (BinTree.inorderBackward b)

478 |   ?inorderForwardBackward_binTree ?inorderBackwardForward_binTree))

481 | public export

482 | algebraFoldable : {f : Type -> Type} ->

483 |   Foldable f => Num a => Algebra f a

484 | algebraFoldable = MkAlgebra sum

488 | public export

489 | IsFoldable c => Num a => Algebra (Ext c) a where

490 |   reduce = sum

492 | public export

493 | argmax : Ord a => (isF : IsFoldable c) => (ne : IsNonEmpty c) =>

494 |   (e : Ext c a) -> c.Pos (shapeExt e)

495 | argmax e = foldr

496 |   (\p, best => if index e p >= index e best then p else best)

497 |   (GetInterface ne (shapeExt e))

498 |   positionsCont

502 | public export

503 | IsEnumerable c => Traversable (Ext c) where

504 |   traverse f (sh <| ind) =

505 |     let (n ** iso) = (:!) enumerate sh

506 |     in (\v => sh <| index (fromVect v) . iso.forward)

507 |          <$> traverse f (toVect (() <| ind . iso.backward))