[fix] changed container record fields to start with uppercase

Author: bgavran

src/Architectures/Transformer/Attention.idr

@@ -81,6 +81,6 @@ causalMask : {a : Type} -> Num a =>
   AllApplicative [c] =>
   CTensor [c, c] a -> CTensor [c, c] a
 causalMask attentionMatrix = 
-  let contShape : c.shp
+  let contShape : c.Shp
       contShape = shapeExt (shapeExt (GetT attentionMatrix))
   in maskedFill attentionMatrix (not <$> cTriBool contShape) minusInfinity

src/Data/Container/Applicative/Definition.idr

@@ -24,12 +24,12 @@ public export prefix 0 #
 
 ||| Convenience functions so we dont have to keep writing GetC
 public export
-(.shp) : ContA -> Type
-(.shp) c = (GetC c) .shp
+(.Shp) : ContA -> Type
+(.Shp) c = (GetC c) .Shp
 
 public export
-(.pos) : (c : ContA) -> c.shp -> Type
-(.pos) c sh = (GetC c) .pos sh
+(.Pos) : (c : ContA) -> c.Shp -> Type
+(.Pos) c sh = (GetC c) .Pos sh
 
 -- alternative method of using applicative instances, not sure yet if this is better
 public export
@@ -55,9 +55,9 @@ oneToTwoAppl @{Cons} = Cons
 --   composeExtensionsA conts a -> Ext (composeContainersA conts) a
 -- ToContainerComp {conts = []} ce = ce
 -- ToContainerComp {conts = [c]} ce = ce
--- ToContainerComp {conts = (c :: d :: cs)} (shp <| idx) = 
+-- ToContainerComp {conts = (c :: d :: cs)} (Shp <| idx) = 
 --   let rst = (ToContainerComp {conts=(d :: cs)}) . idx
---   in (shp <| shapeExt . rst) <| (\(cp ** fsh) => index (rst cp) fsh)
+--   in (Shp <| shapeExt . rst) <| (\(cp ** fsh) => index (rst cp) fsh)
 
 -- public export
 -- FromContainerComp : {conts : List ContA} ->
@@ -128,13 +128,13 @@ oneToTwoAppl @{Cons} = Cons
 -- ||| Hence, just like with EmptyExt we provide convenience functions to create this unit shape easily
 -- public export
 -- emptyShapeCubicalTensor : {shape : List Nat} ->
---   (composeContainersA (Vect <$> shape)) .shp
+--   (composeContainersA (Vect <$> shape)) .Shp
 -- emptyShapeCubicalTensor {shape = []} = ()
 -- emptyShapeCubicalTensor {shape = (_ :: _)}
 --   = () <| (\_ => emptyShapeCubicalTensor)
 
 -- shapeOfCubicalTensorIsUnit : {shape : List Nat} ->
---   (composeContainersA (Vect <$> shape)) .shp = ()
+--   (composeContainersA (Vect <$> shape)) .Shp = ()
 -- shapeOfCubicalTensorIsUnit {shape = []} = Refl
 -- shapeOfCubicalTensorIsUnit {shape = (s :: ss)}
 --   = rewrite shapeOfCubicalTensorIsUnit {shape = ss} in ?afasdf

src/Data/Container/Extension/Definition.idr

@@ -11,8 +11,8 @@ import Misc
 public export
 record Ext (c : Cont) (x : Type) where
   constructor (<|)
-  shapeExt : c.shp
-  index : c.pos shapeExt -> x
+  shapeExt : c.Shp
+  index : c.Pos shapeExt -> x
 
 ||| Container c can be said to be "full off" a type x
 ||| `fullOf` is sometimes used as infix operator to aid readability
@@ -33,7 +33,7 @@ Functor ((Ext d) . (Ext c)) where
 ||| Container setter
 public export
 set : {c : Cont} -> InterfaceOnPositions c Eq =>
-  (e : Ext c x) -> c.pos (shapeExt e) -> x -> Ext c x
+  (e : Ext c x) -> c.Pos (shapeExt e) -> x -> Ext c x
 set {c=(s !> p)} @{MkI} (sh <| contentAt) i x
   = sh <| updateAt contentAt (i, x)
 
@@ -48,7 +48,7 @@ namespace ExtProofs
   public export
   mapIndexCont : {0 f : a -> b} -> {c : Cont} ->
     (l : c `fullOf` a) ->
-    (ps : c.pos (shapeExt (f <$> l))) ->
+    (ps : c.Pos (shapeExt (f <$> l))) ->
     f (index l (rewrite sym (mapShapeExt {f=f} l) in ps))
       = index (f <$> l) ps
   mapIndexCont {c=shp !> pos} (sh <| contentAt) ps = Refl
@@ -68,9 +68,9 @@ namespace EqExt
     shapesEqual : e1.shapeExt = e2.shapeExt
     ||| For each position in that shape, the values must be equal
     ||| Relying on rewrite to get the correct type for the position
-    valuesEqual : (p : c.pos (e1.shapeExt)) ->
+    valuesEqual : (p : c.Pos (e1.shapeExt)) ->
       e1.index p =
-      e2.index (rewrite__impl (c.pos) (sym shapesEqual) p)
+      e2.index (rewrite__impl (c.Pos) (sym shapesEqual) p)
     {-
     Another alternative is to use DecEq, and a different explicit rewrite
      -}

src/Data/Container/Extension/Instances.idr

@@ -113,5 +113,5 @@ public export
 ||| The definition in Data.Functor.positions is for Naperian containers
 ||| i.e. containers with a unit shape
 public export
-positionsCont : {sh : c.shp} -> Ext c (c.pos sh)
+positionsCont : {sh : c.Shp} -> Ext c (c.Pos sh)
 positionsCont = sh <| id

src/Data/Container/Morphism/Definition.idr

@@ -24,18 +24,24 @@ namespace DependentLenses
   public export
   record (=%>) (c1, c2 : Cont) where
     constructor (<%!)
-    fwd : c1.shp -> c2.shp
-    bwd : (x : c1.shp) -> c2.pos (fwd x) -> c1.pos x
+    fwd : c1.Shp -> c2.Shp
+    bwd : (x : c1.Shp) -> c2.Pos (fwd x) -> c1.Pos x
 
   %name (=%>) f, g, h
 
 
   ||| Constructor for closed dependent lens
   public export 
   (!%) : {0 c1, c2 : Cont} ->
-    ((x : c1.shp) -> (y : c2.shp ** (c2.pos y -> c1.pos x))) ->
+    ((x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))) ->
     c1 =%> c2
   (!%) f = (\x => fst (f x)) <%! (\x => snd (f x))
+
+  public export
+  (%!) : {0 c1, c2 : Cont} ->
+    (f : c1 =%> c2) ->
+    (x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))
+  (%!) f x = (f.fwd x ** f.bwd x)
 
   ||| Composition of dependent lenses
   public export
@@ -58,14 +64,14 @@ namespace DependentCharts
   public export
   record (=&>) (c1, c2 : Cont) where
     constructor (<&!)
-    fwd : c1.shp -> c2.shp
-    fwd' : (x : c1.shp) -> c1.pos x -> c2.pos (fwd x)
+    fwd : c1.Shp -> c2.Shp
+    fwd' : (x : c1.Shp) -> c1.Pos x -> c2.Pos (fwd x)
 
 
   ||| Constructor for closed dependent chart
   public export
   (!&) : {0 c1, c2 : Cont} ->
-    ((x : c1.shp) -> (y : c2.shp ** (c1.pos x -> c2.pos y))) ->
+    ((x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))) ->
     c1 =&> c2
   (!&) f = (\x => fst (f x)) <&! (\x => snd (f x))
 
@@ -102,7 +108,7 @@ valContMap {c1=(shp !> pos)} {c2=(shp' !> pos')} (fwd <&! fwd')
 -- public export
 -- record (~%>) (c1, c2 : ContF R) where
 --   constructor (<~!)
---   fwd' : c1.shp' -> c2.shp'
+--   fwd' : c1.Shp' -> c2.Shp'
 
 
 -- upd : c1 ~%> c2 -> 

src/Data/Container/Object/Definition.idr

@@ -2,15 +2,15 @@ module Data.Container.Object.Definition
 
 ||| Containers capture the idea that datatypes consist of memory locations where
 ||| data can be stored.  Each memory location is a one 'shape' of data, and 
-||| there are `shp : Type` many of them. These locations are usually referred 
+||| there are `Shp : Type` many of them. These locations are usually referred 
 ||| to as 'positions'
 public export
 record Cont where
   constructor (!>)
   ||| A type of shapes
-  shp : Type
+  Shp : Type
   ||| For each shape, a set of positions
-  pos : shp -> Type
+  Pos : Shp -> Type
 
 export typebind infixr 0 !>
 
@@ -20,6 +20,6 @@ export typebind infixr 0 !>
 ||| a container `c` has an interface `i` on its positions
 public export
 data InterfaceOnPositions : (c : Cont) -> (i : Type -> Type) -> Type where
-  ||| For every shape s the set of positions c.pos s has that interface
-  MkI : (p : (s : c.shp) -> i (c.pos s)) =>
+  ||| For every shape s the set of positions c.Pos s has that interface
+  MkI : (p : (s : c.Shp) -> i (c.Pos s)) =>
     InterfaceOnPositions c i

src/Data/Container/Object/Instances.idr

@@ -108,15 +108,15 @@ Tensor = foldr (>@) Scalar
 public export
 InternalLens : Cont -> Cont -> Cont
 InternalLens c d
-  = (f : ((x : c.shp) -> (y : d.shp ** d.pos y -> c.pos x)))
-    !> (xx : c.shp ** d.pos (fst (f xx)))
+  = (f : ((x : c.Shp) -> (y : d.Shp ** d.Pos y -> c.Pos x)))
+    !> (xx : c.Shp ** d.Pos (fst (f xx)))
 
 ||| From https://www.cs.ox.ac.uk/people/samuel.staton/papers/cie10.pdf
 public export
 CartesianClosure : Cont -> Cont -> Cont
 CartesianClosure c d
-  = (f : ((x : c.shp) -> (y : d.shp ** d.pos y -> Maybe (c.pos x))))
-    !> (xx : c.shp ** yy' : d.pos (fst (f xx)) ** ?cartesianClosureImpl)
+  = (f : ((x : c.Shp) -> (y : d.Shp ** d.Pos y -> Maybe (c.Pos x))))
+    !> (xx : c.Shp ** yy' : d.Pos (fst (f xx)) ** ?cartesianClosureImpl)
 
 ||| Constant container, positions do not depend on shapes
 ||| Some of the above containers can be refactored in terms of these

src/Data/Container/Products.idr

@@ -16,15 +16,14 @@ public export infixr 0 >@
 ||| Categorical product of containers
 public export
 (>*<) : Cont -> Cont -> Cont
-(shp !> pos) >*< (shp' !> pos')
-  = ((s, s') : (shp, shp')) !> Either (pos s) (pos' s')
+c1 >*< c2 = ((s, s') : (c1.Shp, c2.Shp)) !> (c1.Pos s, c2.Pos s')
 
 ||| Non-categorical product of containers, often also called
-||| 'Hancock' (Scotland), 'Dirichlet' (Spivak ), or 'Tensor product' (various)
+||| 'Hancock' (Scotland), 'Dirichlet' (Spivak), or 'Tensor product' (various)
 ||| Monoid with CUnit
 public export
 (><) : Cont -> Cont -> Cont
-(shp !> pos) >< (shp' !> pos') = ((s, s') : (shp, shp')) !> (pos s, pos' s')
+c1 >< c2 = ((s, s') : (c1.Shp, c2.Shp)) !> (c1.Pos s, c2.Pos s')
 
 
 ||| Coproduct of containers
@@ -39,19 +38,19 @@ public export
 ||| Monoid with Scalar
 public export
 (>@) : Cont -> Cont -> Cont
-c >@ d = (ex : Ext c d.shp) !> (cp : c.pos (shapeExt ex) ** d.pos (index ex cp))
+c >@ d = (ex : Ext c d.Shp) !> (cp : c.Pos (shapeExt ex) ** d.Pos (index ex cp))
 
 public export infixr 0 @>
 
 ||| Diagrammatic composition of containers
 public export
 (@>) : Cont -> Cont -> Cont
-c @> d = (ex : Ext d c.shp) !> (dp : d.pos (shapeExt ex) ** c.pos (index ex dp))
+c @> d = (ex : Ext d c.Shp) !> (dp : d.Pos (shapeExt ex) ** c.Pos (index ex dp))
 
 
 ||| Derivative of a container
-||| Given c=(shp !> pos) the derivative can be thought of as 
-||| a shape s : shp, a distinguished position p : pos s, and the set of *all other positions*
+||| Given c=(Shp !> pos) the derivative can be thought of as 
+||| a shape s : Shp, a distinguished position p : pos s, and the set of *all other positions*
 public export
 Deriv : (c : Cont) ->
   InterfaceOnPositions c DecEq =>

src/Data/Container/TreeUtils.idr

@@ -166,7 +166,7 @@ namespace ApplicativeRoseTree
       AtNode : {ts : (GetC c) `fullOf` (RoseTreeShape c)} ->
         RoseTreePos c (NodeS ts)
       SubTree : {ts : (GetC c) `fullOf` (RoseTreeShape c)} ->
-        (ps : c.pos (shapeExt ts)) -> -- position in a given list
+        (ps : c.Pos (shapeExt ts)) -> -- position in a given list
         RoseTreePos c (index ts ps) -> -- position in the shape of RoseTree at a location specified by ps
         RoseTreePos c (NodeS ts)
 
@@ -176,7 +176,7 @@ namespace ApplicativeRoseTree
       AtNode : {ts : (GetC c) `fullOf` (RoseTreeShape c)} ->
         RoseTreePosNode c (NodeS ts)
       SubTree : {ts : (GetC c) `fullOf` (RoseTreeShape c)} ->
-        (ps : c.pos (shapeExt ts)) -> -- position in a given list
+        (ps : c.Pos (shapeExt ts)) -> -- position in a given list
         RoseTreePosNode c (index ts ps) -> -- position in the sub-tree at the above defined position
         RoseTreePosNode c (NodeS ts)
 
@@ -185,7 +185,7 @@ namespace ApplicativeRoseTree
     data RoseTreePosLeaf : (c : ContA) -> (t : RoseTreeShape c) -> Type where
       AtLeaf : RoseTreePosLeaf c LeafS
       SubTree : {ts : (GetC c) `fullOf` (RoseTreeShape c)} ->
-        (ps : c.pos (shapeExt ts)) -> -- position in a given list
+        (ps : c.Pos (shapeExt ts)) -> -- position in a given list
         RoseTreePosLeaf c (index ts ps) -> -- position in the sub-tree at the above defined position
         RoseTreePosLeaf c (NodeS ts)
 

src/Data/Tensor/Tensor.idr

@@ -555,7 +555,7 @@ namespace TensorInstances
     ||| Naperian instance here
     public export
     positions : {c : Cont} ->
-      {sh : c.shp} -> CTensor [c] (c.pos sh)
+      {sh : c.Shp} -> CTensor [c] (c.Pos sh)
     positions = extToVector positionsCont
 
   namespace ShowInstance
@@ -771,7 +771,7 @@ namespace SetterGetter
   data Index : (shape : List Cont) -> (t : CTensor shape dtype) -> Type where
     Nil : {val : dtype} -> Index [] (embed val)
     (::) : {t : CTensor (c :: cs) dtype} ->
-      (p : c.pos (shapeExt (extractTopExt t))) ->
+      (p : c.Pos (shapeExt (extractTopExt t))) ->
       Index cs (index (extractTopExt t) p) ->
       Index (c :: cs) t