
   0 | module Data.Container.Base.Morphism.Instances
   1 | 
   2 | import Data.Fin
   3 | import Data.Fin.Split
   4 | import Data.Vect
   5 | import Data.List.Elem
   6 | import Data.List.Quantifiers
   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 | import Data.Container.Base.Endofunctor.Definition
  14 | 
  15 | import Data.Container.Base.Object.Instances
  16 | 
  17 | import Data.Container.Base.Quantifiers
  18 | import Data.Container.Base.TreeUtils
  19 | 
  20 | 
  21 | import Data.Num
  22 | import Data.Layout
  23 | import Misc
  24 | 
  25 | ||| If we model the idea of a container (S !> P) as a box
  26 | |||  ┌──────┐
  27 | |||  │ s:S  │
  28 | |||  ├──────┤
  29 | |||  │  Ps  │
  30 | |||  └──────┘
  31 | ||| then `pushDown` is interpreted as pushing down the container,
  32 | ||| pruning anything that goes out of the box, and using `Unit` for
  33 | ||| anything new that appears:
  34 | |||  ┌──────┐
  35 | |||  │ Unit │
  36 | |||  ├──────┤
  37 | |||  │ s:S  │
  38 | |||  └──────┘
  39 | |||     Ps
  40 | public export
  41 | pushDown : Cont -> Cont
  42 | pushDown c = Const2 Unit c.Shp
  43 | 
  44 | public export
  45 | pushIntoContinuation : {0 d, p, l : Cont} ->
  46 |   d >< p =%> l ->
  47 |   p =%> (pushDown d) >@ l
  48 | pushIntoContinuation f = !% \p => (() <| \d => f.fwd (d, p) **
  49 |   \(d ** l') => snd $ f.bwd (d, p) l')
  50 | 
  51 | 
  52 | namespace CategoricalProduct
  53 |   public export
  54 |   terminal : c =%> UnitCont
  55 |   terminal = !% \_ => (() ** absurd)
  56 | 
  57 | 
  58 | namespace HancockTensorProduct
  59 |   public export
  60 |   leftUnit : Scalar >< c =%> c
  61 |   leftUnit = !% \((), s) => (s ** \p => ((), p))
  62 |   
  63 |   public export
  64 |   rightUnit : c >< Scalar =%> c
  65 |   rightUnit = !% \(x, ()) => (x ** \x' => (x', ()))
  66 | 
  67 |   public export
  68 |   leftUnitInv : c =%> Scalar >< c
  69 |   leftUnitInv = !% \x => (((), x) ** \((), x') => x')
  70 | 
  71 |   public export
  72 |   rightUnitInv : c =%> c >< Scalar
  73 |   rightUnitInv = !% \x => ((x, ()) ** \(x', ()) => x')
  74 | 
  75 |   public export
  76 |   assocL : (a >< b) >< c =%> a >< (b >< c)
  77 |   assocL = !% \((a, b), c) => ((a, (b, c)) ** \(a', (b', c')) => ((a', b'), c'))
  78 | 
  79 |   public export
  80 |   assocR : a >< (b >< c) =%> (a >< b) >< c
  81 |   assocR = !% \(a, (b, c)) => (((a, b), c) ** \((a', b'), c') => (a', (b', c')))
  82 | 
  83 |   public export
  84 |   swap : a >< b =%> b >< a
  85 |   swap = !% \(a, b) => ((b, a) ** \(b', a') => (a', b'))
  86 | 
  87 |   public export
  88 |   swapMiddle : (c1 >< c2) >< (c3 >< c4) =%> (c1 >< c3) >< (c2 >< c4)
  89 |   swapMiddle = assocL {c=_ >< _}
  90 |            %>> (id >< assocR)
  91 |            %>> (id >< swap >< id)
  92 |            %>> (id >< assocL)
  93 |            %>> assocR {c=_ >< _}
  94 | 
  95 | namespace CompositionProduct
  96 |   public export
  97 |   leftUnit : Scalar >@ c =%> c
  98 |   leftUnit = !% \ex => (index ex () ** \c' => (() ** c'))
  99 | 
 100 |   public export
 101 |   rightUnit : c >@ Scalar =%> c
 102 |   rightUnit = !% \ex => (shapeExt ex ** \cp => (cp ** ()))
 103 | 
 104 |   public export
 105 |   leftUnitInv : c =%> Scalar >@ c
 106 |   leftUnitInv = !% \s => (() <| (\_ => s) ** \(() ** c') => c')
 107 |   
 108 |   public export
 109 |   rightUnitInv : c =%> c >@ Scalar
 110 |   rightUnitInv = !% \s => (s <| \_ => () ** fst)
 111 | 
 112 |   public export
 113 |   assocL : (a >@ b) >@ c =%> a >@ (b >@ c)
 114 |   assocL = !% \((aShp <| f) <| g) =>
 115 |     (aShp <| \aPos => f aPos <| \bPos => g (aPos  ** bPos) **
 116 |       \(aPos ** bPos ** cPos) => ((aPos ** bPos) ** cPos))
 117 | 
 118 |   public export
 119 |   assocR : a >@ (b >@ c) =%> (a >@ b) >@ c
 120 |   assocR = !% \(aShp <| f) =>
 121 |     ((aShp <| shapeExt . f) <| \(aPos ** bPos) => index (f aPos) bPos **
 122 |       \((aPos ** bPos) ** cPos) => (aPos ** (bPos ** cPos)))
 123 | 
 124 | namespace Coproduct
 125 |   public export
 126 |   elim : c >+< c =%> c
 127 |   elim = !% \case
 128 |     Left x => (x ** id)
 129 |     Right y => (y ** id)
 130 | 
 131 |   public export
 132 |   initial : Empty =%> c
 133 |   initial = !% absurd
 134 | 
 135 |   public export
 136 |   cojoin : c =%> z ->
 137 |     d =%> z ->
 138 |     c >+< d =%> z
 139 |   cojoin f g = (f >+< g) %>> elim
 140 | 
 141 |   public export
 142 |   direct : (a.Shp -> Bool) ->
 143 |     a =%> a >+< a
 144 |   direct p = !% \x => case p x of
 145 |     False => (Left x ** id)
 146 |     True => (Right x ** id)
 147 | 
 148 | 
 149 | 
 150 | namespace CartesianClosure
 151 |   ||| The following is the proof that for any container `c` there is an
 152 |   ||| isomorphism in `Cont` between `c` and `CartesianClosure UnitCont c`
 153 |   ||| This holds in any monoidal closed category: `X ≅ [I, X]`
 154 |   namespace StateIsomorphismProof
 155 |     stateToCartClosureFw : c =%> (CartesianClosure UnitCont c)
 156 |     stateToCartClosureFw = !% \cShp => (!% \() => (cShp ** \_ => Nothing)
 157 |                                        ** \(() ** cPos ** ItIsNothing) => cPos)
 158 | 
 159 |     stateToCartClosureBw : CartesianClosure UnitCont c =%> c
 160 |     stateToCartClosureBw = !% \l => (l.fwd () ** \cPos =>
 161 |       (() ** cPos ** maybeVoidIsNothing (l.bwd () cPos)))
 162 | 
 163 | 
 164 | ||| For a overview of this interaction from the categorical perspective, see
 165 | ||| the Poly book (https://arxiv.org/abs/2312.00990) (Section 6.3.4)
 166 | namespace CompositionTensorInteraction
 167 |   ||| Interaction between composition and tensor product
 168 |   ||| Swaps the operations, and middle two containers
 169 |   ||| Not an isomorphism!
 170 |   public export
 171 |   duoidal : (c >@ d) >< (e >@ f) =%> (c >< e) >@ (d >< f)
 172 |   duoidal = !% \((sc <| idxC), (se <| idxE)) =>
 173 |     ((sc, se) <| \(cp, ep) => (idxC cp, idxE ep) **
 174 |       \((cp, ep) ** (dp, fp)) => ((cp ** dp), (ep ** fp)))
 175 |   
 176 |   ||| Tensor product embeds into composition
 177 |   ||| A special case of `duoidal`
 178 |   public export
 179 |   tensorToComp : c >< f =%> c >@ f
 180 |   tensorToComp =   (rightUnitInv >< leftUnitInv)
 181 |                %>> duoidal {d=Scalar,e=Scalar}
 182 |                %>> (rightUnit >@ leftUnit)
 183 | 
 184 |   ||| Going the other way is impossible without any constraints 
 185 |   ||| Two possibilities on constraints (this, and `compToTensor2`)
 186 |   public export 
 187 |   compToTensor : IsNaperian d =>
 188 |     c >@ d =%> c >< d
 189 |   compToTensor @{(MkIsNaperian dPos)} = !% \(cShp <| content) =>
 190 |     ((cShp,()) ** \(cPos, dPos) => (cPos ** dPos))
 191 |   
 192 |   public export
 193 |   compToTensor2 : IsFlat c =>
 194 |     c >@ d =%> c >< d
 195 |   compToTensor2 @{(ItIsFlat cShp)} = !% \(cShp <| dShp) =>
 196 |     ((cShp, dShp ()) ** \((), dPos') => (() ** dPos'))
 197 |   
 198 |   ||| Specific distributive law we need
 199 |   public export
 200 |   distribute : c >< e =%> s ->
 201 |     c >< (e >@ g) =%> s >@ g
 202 |   distribute f = (rightUnitInv >< id {c=e >@ g})
 203 |                %>> duoidal {d = Scalar}
 204 |                %>> (f >@ leftUnit)
 205 | 
 206 | 
 207 | namespace State
 208 |   ||| "State" as defined in https://arxiv.org/abs/2403.13001 and open games 
 209 |   |||
 210 |   |||       ┌─────────────┐
 211 |   |||       │             ├──► (x : c.Shp)
 212 |   |||       │    State    │
 213 |   |||       │             ├◄── c.Pos x
 214 |   |||       └─────────────┘
 215 |   public export
 216 |   State : Cont -> Type
 217 |   State c = Scalar =%> c
 218 | 
 219 |   ||| Given a shape of any container, state can be defined
 220 |   public export
 221 |   toState : (x : c.Shp) -> State c
 222 |   toState x = !% \() => (x ** \_ => ())
 223 | 
 224 |   public export
 225 |   fromState : State c -> c.Shp
 226 |   fromState f = f.fwd ()
 227 | 
 228 |   public export
 229 |   mapState : State c ->
 230 |     c =%> d ->
 231 |     State d
 232 |   mapState s f = s %>> f
 233 | 
 234 | namespace Costate
 235 |   ||| "Costate" as defined in https://arxiv.org/abs/2403.13001 and open games 
 236 |   |||
 237 |   |||                  ┌─────────────┐
 238 |   |||  (x : c.Shp)  ──►┤             │
 239 |   |||                  │   Costate   │
 240 |   |||     c.Pos x   ◄──┤             │
 241 |   |||                  └─────────────┘
 242 |   public export
 243 |   Costate : Cont -> Type
 244 |   Costate c = c =%> Scalar
 245 | 
 246 |   public export
 247 |   toCostate : ((x : c.Shp) -> c.Pos x) -> Costate c
 248 |   toCostate s = !% \x => (() ** \() => s x)
 249 | 
 250 |   public export
 251 |   fromCostate : Costate c -> (x : c.Shp) -> c.Pos x
 252 |   fromCostate f x = f.bwd x ()
 253 | 
 254 |   public export
 255 |   mapCostate : Costate d ->
 256 |     c =%> d ->
 257 |     Costate c
 258 |   mapCostate s f = f %>> s
 259 | 
 260 |   public export
 261 |   pairCostate : Costate c -> Costate d -> Costate (c >< d)
 262 |   pairCostate f g = (f >< g) %>> leftUnit {c=Scalar} %>> id
 263 |   
 264 | public export
 265 | fromNapCostateToState : Costate (Nap c.Shp) -> State c
 266 | fromNapCostateToState f = toState (f.bwd () ())
 267 | 
 268 | public export
 269 | fromStateToNapCostate : State c -> Costate (Nap c.Shp)
 270 | fromStateToNapCostate f = toCostate f.fwd
 271 | 
 272 | 
 273 | 
 274 | ||| Wraps a dependent lens `c =%> d`
 275 | ||| into one of type `c >@ Scalar =%> d >@ Scalar`
 276 | ||| Needed because `c >@ Scalar` isn't automatically reduced to `c`
 277 | public export
 278 | wrapIntoVector : c =%> d ->
 279 |   Tensor [c] =%> Tensor [d]
 280 | wrapIntoVector f = rightUnit %>> f %>> rightUnitInv
 281 | 
 282 | public export
 283 | wrapIntoMatrix : c >@ c' =%> d >@ d' ->
 284 |   Tensor [c, c'] =%> Tensor [d, d']
 285 | wrapIntoMatrix f =   (id >@ rightUnit)
 286 |                  %>> f
 287 |                  %>> (id >@ rightUnitInv)
 288 | 
 289 | ||| Wraps a dependent lens `c =%> d`
 290 | ||| into one of type `c >< Scalar =%> d >< Scalar`
 291 | ||| Needed because `c >< Scalar` isn't automatically reduced to `c`
 292 | public export
 293 | wrapIntoVectorHancock : c =%> d ->
 294 |   HancockTensor [c] =%> HancockTensor [d]
 295 | wrapIntoVectorHancock f = rightUnit %>> f %>> rightUnitInv
 296 | 
 297 | namespace CubicalHelpers
 298 |   ||| Helper function allowing `shape` in `cubicalShape` to have zero annotation
 299 |   public export
 300 |   cubicalShapeHelper : All IsCubical shape -> List Nat
 301 |   cubicalShapeHelper [] = []
 302 |   cubicalShapeHelper (ic :: ics) = dimHelper ic :: cubicalShapeHelper ics
 303 |     
 304 |   ||| Given a list of cubical containers, return the list of their dimensions
 305 |   public export
 306 |   cubicalShape : (0 shape : List Cont) -> All IsCubical shape => List Nat
 307 |   cubicalShape _ @{ac} = cubicalShapeHelper ac
 308 |     
 309 |   ||| Size of a list of cubical containers is the product of their dimensions
 310 |   public export
 311 |   size : (0 shape : List Cont) -> All IsCubical shape => Nat
 312 |   size shape = prod (cubicalShape shape)
 313 | 
 314 | ||| Layout-aware dependent lens flattening a cubical tensor
 315 | public export
 316 | flattenCubical : {shape : List Cont} ->
 317 |   (ac : All IsCubical shape) =>
 318 |   LayoutOrder ->
 319 |   Tensor shape =%> Vect (size shape)
 320 | flattenCubical {shape = [], ac=[]} _ = !% \() => (() ** \FZ => ())
 321 | flattenCubical {shape = (_ :: ss), ac=(MkIsCubical n :: as)} lo
 322 |   = !% \(() <| t) => (() ** \idx =>
 323 |       let (!% recBackward) = flattenCubical {shape = ss} lo
 324 |           (i, rest) = splitFinProd lo idx
 325 |           (_ ** backRec) = recBackward (t i)
 326 |       in (i ** backRec rest))
 327 | 
 328 | ||| Layout-aware dependent lens unflattening a tensor
 329 | public export
 330 | unflattenCubical : {shape : List Cont} ->
 331 |   (ac : All IsCubical shape) =>
 332 |   LayoutOrder ->
 333 |   Vect (size shape) =%> Tensor shape
 334 | unflattenCubical {shape = [], ac=[]} lo = !% \() => (() ** \() => FZ)
 335 | unflattenCubical {shape = (_ :: ss), ac=((MkIsCubical n) :: as)} lo =
 336 |   let (!% f) = unflattenCubical {shape = ss} lo
 337 |       (innerShape ** innerBack) = f ()
 338 |   in !% \() => ((() <| \_ => innerShape) ** (\(cp ** restPos) =>
 339 |     indexFinProd lo cp (innerBack restPos)))
 340 | 
 341 | ||| This is simply a rewrite!
 342 | public export
 343 | recastFlattenedTensor : {oldShape, newShape : List Cont} ->
 344 |   (oldAc : All IsCubical oldShape) => (newAc : All IsCubical newShape) =>
 345 |   {auto prf : size oldShape = size newShape} ->
 346 |   Vect (size oldShape) =%> Vect (size newShape)
 347 | recastFlattenedTensor = !% \() => (() ** \i => rewrite prf in i)
 348 | 
 349 | ||| Reshapes a cubical tensor by first flattening it to a linear representation,
 350 | ||| casting the type to the new shape, and then unflattening it back
 351 | ||| Is generic over layout order
 352 | public export
 353 | reshape : {oldShape, newShape : List Cont} ->
 354 |   (oldAc : All IsCubical oldShape) => (newAc : All IsCubical newShape) =>
 355 |   LayoutOrder ->
 356 |   {auto prf : size oldShape = size newShape} ->
 357 |   Tensor oldShape =%> Tensor newShape
 358 | reshape lo = flattenCubical lo
 359 |          %>> recastFlattenedTensor
 360 |          %>> unflattenCubical lo
 361 | 
 362 | 
 363 | namespace Transpose
 364 |   public export
 365 |   transposeLens : IsNaperian c => IsNaperian d => c >@ d =%> d >@ c
 366 |   transposeLens @{MkIsNaperian _} @{MkIsNaperian _} = !% \(() <| _) =>
 367 |     (() <| (\_ => ()) ** \(dInd ** cInd) => (cInd ** dInd))
 368 | 
 369 |   public export
 370 |   transpose : IsNaperian c => IsNaperian d =>
 371 |     Tensor [c, d] =%> Tensor [d, c]
 372 |   transpose @{MkIsNaperian _} @{MkIsNaperian _} = wrapIntoMatrix transposeLens
 373 | 
 374 |   -- ||| experiment, does this work?
 375 |   -- public export
 376 |   -- transposeMiddle : IsNaperian c => IsNaperian e =>
 377 |   --   Tensor [c, e, d] =%> 
 378 |   
 379 | 
 380 |   --||| Transpose a given element to the front of the shape
 381 |   --public export
 382 |   --transposeToFront : (shape : List Cont) ->
 383 |   --  (c : Cont) ->
 384 |   --  (elem : Elem c shape) =>
 385 |   --  All IsNaperian (dropAfterElem shape elem) =>
 386 |   --  Tensor shape =%> Tensor (c :: dropElem shape elem)
 387 |   --transposeToFront (_ :: xs) c @{Here} @{allNap} = ?transposeToFront_rhs_0
 388 |   --transposeToFront (y :: xs) c @{(There x)} @{allNap} = ?transposeToFront_rhs_1
 389 |   
 390 | ||| Functionality for transforming a tensor into a hancock tensor
 391 | namespace TransformIntoHancockTensor
 392 |   public export
 393 |   hancockTensorNaperianShape : {shape : List Cont} ->
 394 |     (allNap : All IsNaperian shape) =>
 395 |     (HancockTensor shape).Shp
 396 |   hancockTensorNaperianShape {shape = []} = ()
 397 |   hancockTensorNaperianShape {allNap = ((MkIsNaperian _) :: _)}
 398 |     = ((), hancockTensorNaperianShape)
 399 |   
 400 |   ||| Helper to compute the unique shape of Tensor when all containers are Naperian
 401 |   public export
 402 |   tensorNaperianShape : {shape : List Cont} ->
 403 |     (allNap : All IsNaperian shape) =>
 404 |     (Tensor shape).Shp
 405 |   tensorNaperianShape {shape = []} = ()
 406 |   tensorNaperianShape {shape = (_ :: ss), allNap = ((MkIsNaperian _) :: ns)}
 407 |     = () <| \_ => tensorNaperianShape {shape = ss} @{ns}
 408 |   
 409 |   ||| Analogous to `naperianPosEq` but for the HancockTensor structure
 410 |   ||| We can't use `naperianPosEq` directly because the shape of the resulting
 411 |   ||| container is not Unit, it is only isomorphic to it
 412 |   public export
 413 |   hancockTensorPosEq : {shape : List Cont} ->
 414 |     (allNap : All IsNaperian shape) =>
 415 |     {0 x, y : (HancockTensor shape).Shp} ->
 416 |     (HancockTensor shape).Pos x = (HancockTensor shape).Pos y
 417 |   hancockTensorPosEq {allNap = []} = Refl
 418 |   hancockTensorPosEq {allNap = ((MkIsNaperian _) :: _)} = cong2 Pair
 419 |     (naperianPosEq @{MkIsNaperian _} {x=()} {y=()})
 420 |     hancockTensorPosEq
 421 |   
 422 |   ||| Tensor shape is isomorphic to HancockTensor shape when all containers in
 423 |   ||| the shape are Naperian. This is one arrow of that isomorphism
 424 |   public export
 425 |   transformToHancock : {shape : List Cont} ->
 426 |     All IsNaperian shape =>
 427 |     Tensor shape =%> HancockTensor shape
 428 |   transformToHancock {shape = []} = id
 429 |   transformToHancock {shape = (_ :: _)} @{((MkIsNaperian _) :: _)}
 430 |     = !% \(() <| content) => (((), hancockTensorNaperianShape) **
 431 |        \(p, restPos) =>
 432 |          let (_ ** recBack) = (%!) transformToHancock (content p)
 433 |          in (p ** recBack $ replace {p = id} hancockTensorPosEq restPos))
 434 | 
 435 |   public export
 436 |   transformFromHancock : {shape : List Cont} ->
 437 |     All IsNaperian shape =>
 438 |     HancockTensor shape =%> Tensor shape
 439 |   transformFromHancock {shape = []} = id
 440 |   transformFromHancock {shape = (Nap s :: ss)} @{((MkIsNaperian s) :: _)}
 441 |     = !% \((), hShp) =>
 442 |         let (tShp ** recBack) = (%!) transformFromHancock hShp
 443 |         in (() <| (\_ => tShp) ** \(p ** restPos) => (p, recBack restPos))
 444 | 
 445 |     
 446 | 
 447 |   -- ||| Technically this is Unit, but hard to prove
 448 |   -- public export
 449 |   -- foldOverNaperianShapeComp : {shape : List Cont} ->
 450 |   --   (allNap : All IsNaperian shape) =>
 451 |   --   (Tensor shape).Shp
 452 |   -- foldOverNaperianShapeComp {shape = []} = ()
 453 |   -- foldOverNaperianShapeComp {allNap = ((MkIsNaperian pos) :: ns)}
 454 |   --   = () <| \_ => foldOverNaperianShapeComp
 455 |   -- 
 456 |   -- public export
 457 |   -- naperianHancockShape : {shape : List Cont} ->
 458 |   --   (allNap : All IsNaperian shape) =>
 459 |   --   (HancockTensor shape).Shp = Unit
 460 |   -- naperianHancockShape = believe_me ()
 461 |   -- 
 462 |   -- public export
 463 |   -- foldOverNaperianShapeHancock : {shape : List Cont} ->
 464 |   --   (allNap : All IsNaperian shape) =>
 465 |   --   (HancockTensor shape).Shp
 466 |   -- foldOverNaperianShapeHancock {shape = []} = ()
 467 |   -- foldOverNaperianShapeHancock {allNap = ((MkIsNaperian _) :: _)}
 468 |   --   = ((), foldOverNaperianShapeHancock)
 469 | 
 470 | 
 471 | -- public export
 472 | -- tensorIsNaperianShape : {shape : List Cont} ->
 473 | --   (allNap : All IsNaperian shape) =>
 474 | --   IsNaperian (Tensor shape)
 475 | -- tensorIsNaperianShape {shape = []} = MkIsNaperian ()
 476 | -- tensorIsNaperianShape {shape = (_ :: ss), allNap = ((MkIsNaperian pos) :: ns)}
 477 | --   = let tg = tensorIsNaperianShape {shape = ss} 
 478 | --     in ?tensorIsNaperianShape_rhs_1
 479 | --     --in rewrite naperianShpEq @{tg}
 480 | --     --in (rewrite (EmptyExtEq {c=(Nap pos)})
 481 | --     --in let tg = MkIsNaperian in ?tensorIsNaperianShape_rhs_2)
 482 | 
 483 | -- public export
 484 | -- transformToHancock : {shape : List Cont} ->
 485 | --   All IsNaperian shape =>
 486 | --   Tensor shape =%> HancockTensor shape
 487 | -- transformToHancock {shape = []} = id
 488 | -- transformToHancock {shape = (_ :: ss)} @{((MkIsNaperian pos) :: ns)}
 489 | --   = let f = (%!) (transformToHancock {shape = ss} @{ns})
 490 | --         (_ ** h) = f (foldOverNaperianShapeComp {shape=ss})
 491 | --     in !% \(() <| content) => (((), foldOverNaperianShapeHancock) **
 492 | --       \(p, fld) => (p ** ?hhh))
 493 | --       -- (((), rewrite -- foldOverNaperianShapeHancock {shape=ss} @{ns} in ()) **
 494 | --     --   \(p, fld) => (p ** ?bnn))
 495 | 
 496 | -- need to organise this
 497 | namespace BinTree
 498 |   public export
 499 |   inorderBackward : (b : BinTreeShape) ->
 500 |     Fin (numNodesAndLeaves b) ->
 501 |     BinTreePos b
 502 |   inorderBackward LeafS FZ = AtLeaf
 503 |   inorderBackward (NodeS lt rt) n with (strengthenN {m=numNodesAndLeaves lt} n)
 504 |      _ | Left p = GoLeft (inorderBackward lt p)
 505 |      _ | Right FZ = AtNode
 506 |      _ | Right (FS g) = GoRight (inorderBackward rt g)
 507 | 
 508 | 
 509 |   public export
 510 |   inorder : BinTree =%> List
 511 |   inorder = !% \b => (numNodesAndLeaves b ** inorderBackward b)
 512 | 
 513 | namespace BinTreeNode
 514 |   public export
 515 |   inorderBackward : (b : BinTreeShape) ->
 516 |     Fin (numNodes b) ->
 517 |     BinTreePosNode b
 518 |   inorderBackward (NodeS lt rt) n with (strengthenN {m=numNodes lt} n)
 519 |     _ | Left p = GoLeft (inorderBackward lt p)
 520 |     _ | Right FZ = AtNode
 521 |     _ | Right (FS g) = GoRight (inorderBackward rt g)
 522 | 
 523 |   ||| Traverses a binary tree container in order, producing a list container
 524 |   public export
 525 |   inorder : BinTreeNode =%> List
 526 |   inorder = !% \b => (numNodes b ** inorderBackward b)
 527 | 
 528 |   -- Need to do some rewriting for preorder
 529 |   public export
 530 |   preorderBinTreeNode : (b : BinTreeShape) ->
 531 |     Fin (numNodes b) -> BinTreePosNode b
 532 |   preorderBinTreeNode (NodeS lt rt) x = ?preorderBinTreeNode_rhs_1
 533 |   --preorderBinTreeNode (NodeS lt rt) n with (strengthenN {m=numNodes lt} n)
 534 |   --  _ | Left p = ?whl
 535 |   --  _ | Right FZ = ?whn
 536 |   --  _ | Right (FS g) = ?whr
 537 | 
 538 | namespace BinTreeLeaf
 539 |   public export
 540 |   inorderBackward : (b : BinTreeShape) ->
 541 |     Fin (numLeaves b) ->
 542 |     BinTreePosLeaf b
 543 |   inorderBackward LeafS 0 = AtLeaf
 544 |   inorderBackward (NodeS lt rt) i with (strengthenN {m=numLeaves lt} i)
 545 |     _ | (Left indLeft) = GoLeft (inorderBackward lt indLeft)
 546 |     _ | (Right indRight) = GoRight (inorderBackward rt indRight)
 547 | 
 548 |   public export
 549 |   inorder : BinTreeLeaf =%> List
 550 |   inorder = !% \b => (numLeaves b ** inorderBackward b)
 551 | 
 552 | -- public export
 553 | -- traverseLeaf : (x : BinTreeShape) -> FinBinTreeLeaf x -> Fin (numLeaves x)
 554 | -- traverseLeaf LeafS Done = FZ
 555 | -- traverseLeaf (NodeS lt rt) (GoLeft x) = weakenN (numLeaves rt) (traverseLeaf lt x)
 556 | -- traverseLeaf (NodeS lt rt) (GoRight x) = shift (numLeaves lt) (traverseLeaf rt x)
 557 | -- 
 558 | 
 559 | public export
 560 | vectToList : {n : Nat} -> Vect n =%> List
 561 | vectToList = !% \() => (n ** id)
 562 | 
 563 | public export
 564 | maybeToList : Maybe =%> List
 565 | maybeToList = !% \b => case b of 
 566 |   False => (0 ** absurd)
 567 |   True => (1 ** \_ => ())
 568 | 
 569 | -- TODO here maybe need to uncomment during merge?
 570 | -- public export
 571 | -- selectShape : {cs : Vect k Cont} ->
 572 | --   (shapes : All Shp cs) -> (i : Fin k) -> Any Shp cs
 573 | -- selectShape (s :: _) FZ = Here s
 574 | -- selectShape (_ :: ss) (FS j) = There (selectShape ss j)
 575 | -- 
 576 | -- ||| Extract the position from an AnyPos at a given index
 577 | -- public export
 578 | -- extractPos : {n : Nat} -> {xs : Vect n Cont} ->
 579 | --   {shapes : All Shp xs} ->
 580 | --   (i : Fin n) ->
 581 | --   AnyShpPos (selectShape shapes i) ->
 582 | --   AnyPos shapes
 583 | -- extractPos {shapes = (_ :: _)} FZ (Here x) = Here x
 584 | -- extractPos {shapes = (_ :: _)} (FS j) (There rest)
 585 | --   = There $ extractPos j rest
 586 | -- 
 587 | -- public export
 588 | -- SampleAndChoose : {n : Nat} -> {xs : Vect n Cont} ->
 589 | --   ConvexComb xs =%> (Sample n >@ Any xs)
 590 | -- SampleAndChoose = !% \(d, shapes) =>
 591 | --   (d <| selectShape shapes ** \(i ** grad) => (0, [extractPos i grad]))
 592 | 
 593 | -- SampleAndChooseWithDist = !% \(d, shapes) =>
 594 | --   (d <| electShape shapes ** \(i ** grad) => (0, [(i ** extractPos i grad)]))
 595 | 
 596 | -- public export
 597 | -- GetDist : {n : Nat} -> {xs : Vect n Cont} ->
 598 | --   ConvexComb xs =%> Simplex n
 599 | -- GetDist = !% \(d, shapes) => (d ** \d' => (d', ?GetDist_rhs))
 600 | 
 601 | public export
 602 | handleEffect : Monad m =>
 603 |   (handler : (m <!> effect) =%> Scalar) ->
 604 |   (program : a =%> effect) ->
 605 |   m <!> a =%> Scalar
 606 | handleEffect handler program = !% \x =>
 607 |   let (ef ** nn) = (%! program) x
 608 |       (() ** rest) = (%! handler) ef
 609 |   in (() ** \() => do 
 610 |     e <- rest ()
 611 |     pure (nn e))