
  0 | module Data.Container.Base.Quantifiers
  1 | 
  2 | import Data.Vect
  3 | import Data.List.Quantifiers
  4 | import Data.Vect.Quantifiers
  5 | 
  6 | import Data.Container.Base.Object.Definition
  7 | 
  8 | ||| Quantifiers for lists
  9 | ||| The predicate for each container's shape is considered its positions
 10 | ||| We can have All/Any on shapes, and All/Any on positions
 11 | ||| We get 3 valid combinations, since AnyAll=AnyAny.
 12 | ||| That overlap is called AnyShpPos below
 13 | namespace List
 14 |   namespace AllShp
 15 |     public export
 16 |     data AllPos : {cs : List Cont} -> All Shp cs -> Type where
 17 |       Nil : AllPos []
 18 |       (::) : Pos c s -> AllPos {cs=cs} ss -> AllPos {cs=(c::cs)} (s :: ss)
 19 | 
 20 |     public export
 21 |     head : AllPos {cs=c::cs} (s :: ss) -> c.Pos s
 22 |     head (p :: ps) = p
 23 | 
 24 |     public export
 25 |     tail : AllPos {cs=c::cs} (s :: ss) -> AllPos {cs=cs} ss
 26 |     tail (p :: ps) = ps
 27 | 
 28 |     public export
 29 |     data AnyPos : {cs : List Cont} -> All Shp cs -> Type where
 30 |       Here : c.Pos s -> AnyPos {cs=(c::cs)} (s :: ss)
 31 |       There : AnyPos ss -> AnyPos (s :: ss)
 32 |   
 33 |   ||| Once we pick a particular shape, we're forced to pick that position
 34 |   public export
 35 |   data AnyShpPos : {cs : List Cont} -> Any Shp cs -> Type where
 36 |     Here : c.Pos s -> AnyShpPos (Here {x=c} {xs=cs} s)
 37 |     There : AnyShpPos ss -> AnyShpPos (There ss)
 38 |     
 39 | 
 40 | ||| Same deal as above, but for Vects
 41 | namespace Vect
 42 |   namespace AllShp
 43 |     public export
 44 |     data AllPos : {cs : Vect n Cont} -> All Shp cs -> Type where
 45 |       Nil : AllPos []
 46 |       (::) : Pos c s -> AllPos {cs=cs} ss -> AllPos {cs=(c::cs)} (s :: ss)
 47 | 
 48 |     public export
 49 |     head : {0 cs : Vect n Cont} -> {0 ss : All Shp cs} ->
 50 |       AllPos {cs=c::cs} (s :: ss) -> c.Pos s
 51 |     head (p :: ps) = p
 52 | 
 53 |     public export
 54 |     tail : {0 cs : Vect n Cont} -> {0 ss : All Shp cs} ->
 55 |       AllPos {cs=c::cs} (s :: ss) -> AllPos {cs=cs} ss
 56 |     tail (p :: ps) = ps
 57 | 
 58 | 
 59 |     public export 
 60 |     data AnyPos : {cs : Vect n Cont} -> All Shp cs -> Type where
 61 |       Here : c.Pos s -> AnyPos {cs=(c::cs)} (s :: ss)
 62 |       There : AnyPos ss -> AnyPos {cs=(c::cs)} (s :: ss)
 63 | 
 64 | public export
 65 | data AnyShpPos : {cs : Vect n Cont} -> Any Shp cs -> Type where
 66 |   Here : c.Pos s -> AnyShpPos (Here {x=c} {xs=cs} s)
 67 |   There : AnyShpPos ss -> AnyShpPos (There ss)