0 | module Data.Container.Additive.Quantifiers
  1 |
  2 | import Data.Vect
  3 | import Data.List.Quantifiers
  4 | import Data.Vect.Quantifiers
  5 |
  6 | import Data.Container.Base
  7 |
  8 | import Data.Container.Additive.Object.Definition
  9 | import Data.ComMonoid
 10 |
 11 | -- Follows the structure of `Data.Container.Base.Quantifiers`
 12 |
 13 |
 14 | ||| Quantifiers for lists
 15 | ||| We can have All/Any on shapes, and All/Any on positions
 16 | ||| Because additivity is required, there are only two valid combinations
 17 | ||| AllAll and AnyShpPos
 18 | namespace List
 19 |   namespace AllShp
 20 |     public export
 21 |     data AllPos : {cs : List AddCont} -> All (.Shp) cs -> Type where
 22 |       Nil : AllPos []
 23 |       (::) : c.Pos s -> AllPos ss -> AllPos {cs=(c::cs)} (s :: ss)
 24 |
 25 |     public export
 26 |     head : {0 cs : List AddCont} -> {0 ss : All (.Shp) cs} ->
 27 |       AllPos {cs=c::cs} (s :: ss) -> c.Pos s
 28 |     head (p :: ps) = p
 29 |
 30 |     public export
 31 |     tail : {0 cs : List AddCont} -> {0 ss : All (.Shp) cs} ->
 32 |       AllPos {cs=c::cs} (s :: ss) -> AllPos {cs=cs} ss
 33 |     tail (p :: ps) = ps
 34 |
 35 |     public export
 36 |     allPosPlus : {cs : List AddCont} ->
 37 |       (s : All (.Shp) cs) ->
 38 |       AllPos s -> AllPos s -> AllPos s
 39 |     allPosPlus [] [] [] = []
 40 |     allPosPlus {cs=c::_} (s :: ss) (l :: ls) (r :: rs)
 41 |       = plus (UMon c s) l r :: allPosPlus ss ls rs
 42 |
 43 |     public export
 44 |     allPosNeutral : {cs : List AddCont} ->
 45 |       (s : All (.Shp) cs) ->
 46 |       AllPos s
 47 |     allPosNeutral {cs = []} [] = []
 48 |     allPosNeutral {cs = (c :: cs)} (s :: ss)
 49 |       = neutral (UMon c s) :: allPosNeutral ss
 50 |
 51 |     public export
 52 |     allPosComMonoid : {cs : List AddCont} ->
 53 |       (s : All (.Shp) cs) -> ComMonoid (AllPos s)
 54 |     allPosComMonoid s = MkComMonoid (allPosPlus s) (allPosNeutral s)
 55 |
 56 |   public export
 57 |   data AnyShpPos : {cs : List AddCont} -> Any (.Shp) cs -> Type where
 58 |     Here : c.Pos s -> AnyShpPos (Here {x=c} {xs=cs} s)
 59 |     There : AnyShpPos ss -> AnyShpPos (There ss)
 60 |
 61 |   public export
 62 |   anyShpPosPlus : {cs : List AddCont} ->
 63 |     (s : Any (.Shp) cs) -> AnyShpPos s -> AnyShpPos s -> AnyShpPos s
 64 |   anyShpPosPlus {cs = (c :: _)} (Here s) (Here l) (Here r)
 65 |     = Here (c.Plus s l r)
 66 |   anyShpPosPlus {cs = (c :: cs)} (There ss) (There l) (There r)
 67 |     = There (anyShpPosPlus ss l r)
 68 |
 69 |   public export
 70 |   anyShpPosNeutral : {cs : List AddCont} ->
 71 |     (s : Any (.Shp) cs) -> AnyShpPos s
 72 |   anyShpPosNeutral {cs = (c :: _)} (Here s) = Here (c.Zero s)
 73 |   anyShpPosNeutral {cs = (_ :: _)} (There ss) = There (anyShpPosNeutral ss)
 74 |
 75 |   public export
 76 |   anyShpPosComMonoid : {cs : List AddCont} ->
 77 |     (s : Any (.Shp) cs) -> ComMonoid (AnyShpPos s)
 78 |   anyShpPosComMonoid s = MkComMonoid (anyShpPosPlus s) (anyShpPosNeutral s)
 79 |
 80 |
 81 |
 82 | namespace Vect
 83 |   namespace AllShp
 84 |     public export
 85 |     data AllPos : {cs : Vect n AddCont} -> All (.Shp) cs -> Type where
 86 |       Nil : AllPos []
 87 |       (::) : c.Pos s -> AllPos {cs=cs} ss -> AllPos {cs=(c::cs)} (s :: ss)
 88 |
 89 |     public export
 90 |     head : {0 cs : Vect n AddCont} -> {0 ss : All (.Shp) cs} ->
 91 |       AllPos {cs=c::cs} (s :: ss) -> c.Pos s
 92 |     head (p :: ps) = p
 93 |
 94 |     public export
 95 |     tail : {0 cs : Vect n AddCont} -> {0 ss : All (.Shp) cs} ->
 96 |       AllPos {cs=c::cs} (s :: ss) -> AllPos {cs=cs} ss
 97 |     tail (p :: ps) = ps
 98 |
 99 |     public export
100 |     allPosPlus : {cs : Vect n AddCont} ->
101 |       (s : All (.Shp) cs) ->
102 |       AllPos s -> AllPos s -> AllPos s
103 |     allPosPlus [] [] [] = []
104 |     allPosPlus {cs=c::_} (s :: ss) (l :: ls) (r :: rs)
105 |       = plus (UMon c s) l r :: allPosPlus ss ls rs
106 |
107 |     public export
108 |     allPosNeutral : {cs : Vect n AddCont} ->
109 |       (s : All (.Shp) cs) ->
110 |       AllPos s
111 |     allPosNeutral {cs = []} [] = []
112 |     allPosNeutral {cs = (c :: cs)} (s :: ss)
113 |       = neutral (UMon c s) :: allPosNeutral ss
114 |
115 |     public export
116 |     allPosComMonoid : {cs : Vect n AddCont} ->
117 |       (s : All (.Shp) cs) -> ComMonoid (AllPos s)
118 |     allPosComMonoid s = MkComMonoid (allPosPlus s) (allPosNeutral s)
119 |
120 |
121 |   public export
122 |   data AnyShpPos : {cs : Vect n AddCont} -> Any (.Shp) cs -> Type where
123 |     Here : c.Pos s -> AnyShpPos (Here {x=c} {xs=cs} s)
124 |     There : AnyShpPos ss -> AnyShpPos (There ss)
125 |
126 |   public export
127 |   anyShpPosPlus : {cs : Vect n AddCont} ->
128 |     (s : Any (.Shp) cs) -> AnyShpPos s -> AnyShpPos s -> AnyShpPos s
129 |   anyShpPosPlus {cs = (c :: _)} (Here s) (Here l) (Here r)
130 |     = Here (c.Plus s l r)
131 |   anyShpPosPlus {cs = (c :: cs)} (There ss) (There l) (There r)
132 |     = There (anyShpPosPlus ss l r)
133 |
134 |   public export
135 |   anyShpPosNeutral : {cs : Vect n AddCont} ->
136 |     (s : Any (.Shp) cs) -> AnyShpPos s
137 |   anyShpPosNeutral {cs = (c :: _)} (Here s) = Here (c.Zero s)
138 |   anyShpPosNeutral {cs = (_ :: _)} (There ss) = There (anyShpPosNeutral ss)
139 |
140 |   public export
141 |   anyShpPosComMonoid : {cs : Vect n AddCont} ->
142 |     (s : Any (.Shp) cs) -> ComMonoid (AnyShpPos s)
143 |   anyShpPosComMonoid s = MkComMonoid (anyShpPosPlus s) (anyShpPosNeutral s)