
   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 |     allPosNeutral : {cs : Vect n AddCont} ->
 108 |       (s : All (.Shp) cs) ->
 109 |       AllPos s
 110 |     allPosNeutral {cs = []} [] = []
 111 |     allPosNeutral {cs = (c :: cs)} (s :: ss)
 112 |       = neutral (UMon c s) :: allPosNeutral ss
 113 | 
 114 |     public export
 115 |     allPosComMonoid : {cs : Vect n AddCont} ->
 116 |       (s : All (.Shp) cs) -> ComMonoid (AllPos s)
 117 |     allPosComMonoid s = MkComMonoid (allPosPlus s) (allPosNeutral s)
 118 | 
 119 | 
 120 |   public export
 121 |   data AnyShpPos : {cs : Vect n AddCont} -> Any (.Shp) cs -> Type where
 122 |     Here : c.Pos s -> AnyShpPos (Here {x=c} {xs=cs} s)
 123 |     There : AnyShpPos ss -> AnyShpPos (There ss)
 124 | 
 125 |   public export
 126 |   anyShpPosPlus : {cs : Vect n AddCont} ->
 127 |     (s : Any (.Shp) cs) -> AnyShpPos s -> AnyShpPos s -> AnyShpPos s
 128 |   anyShpPosPlus {cs = (c :: _)} (Here s) (Here l) (Here r)
 129 |     = Here (c.Plus s l r)
 130 |   anyShpPosPlus {cs = (c :: cs)} (There ss) (There l) (There r)
 131 |     = There (anyShpPosPlus ss l r)
 132 | 
 133 |   public export
 134 |   anyShpPosNeutral : {cs : Vect n AddCont} ->
 135 |     (s : Any (.Shp) cs) -> AnyShpPos s
 136 |   anyShpPosNeutral {cs = (c :: _)} (Here s) = Here (c.Zero s)
 137 |   anyShpPosNeutral {cs = (_ :: _)} (There ss) = There (anyShpPosNeutral ss)
 138 | 
 139 |   public export
 140 |   anyShpPosComMonoid : {cs : Vect n AddCont} ->
 141 |     (s : Any (.Shp) cs) -> ComMonoid (AnyShpPos s)
 142 |   anyShpPosComMonoid s = MkComMonoid (anyShpPosPlus s) (anyShpPosNeutral s)