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