[refactor] all lenses are now closed

Author: bgavran

src/Data/Container/Morphism/Definition.idr

@@ -10,86 +10,66 @@ Two different types of morphisms:
 dependent lenses, and dependent charts
 -------------------------------------------------------------------------------}
 
-export infixr 1 =%> -- dependent lens
-export infixr 1 =&> -- dependent chart
-export infix 1 <%! -- constructor for dependent lens
-export infix 1 <&! -- constructor for dependent chart
-export prefix 0 !% -- constructor for closed dependent lens
-export prefix 0 !& -- constructor for closed dependent chart
+export infixr 1 =%> -- (closed) dependent lens
+export infixr 1 =&> -- (closed) dependent chart
+export prefix 0 !% -- constructor the (closed) dependent lens
+export prefix 0 !& -- constructor the (closed) dependent chart
 export infixl 5 %>> -- composition of dependent lenses
+export infixl 5 &>> -- composition of dependent charts
 
 namespace DependentLenses
   ||| Dependent lenses
   ||| Forward-backward container morphisms
   public export
-  record (=%>) (c1, c2 : Cont) where
-    constructor (<%!)
-    fwd : c1.Shp -> c2.Shp
-    bwd : (x : c1.Shp) -> c2.Pos (fwd x) -> c1.Pos x
+  data (=%>) : (c1, c2 : Cont) -> Type where
+    (!%) : ((x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))) -> c1 =%> c2
 
   %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))) ->
-    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)
+  (%!) : c1 =%> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c2.Pos y -> c1.Pos x))
+  (%!) (!% f) x = f x
 
   ||| Composition of dependent lenses
   public export
   compDepLens : a =%> b -> b =%> c -> a =%> c
-  compDepLens f g =
-      (g.fwd . f.fwd) <%!
-      (\x => f.bwd x . g.bwd (f.fwd x))
-  
+  compDepLens (!% f) (!% g) = !% \x => let (b ** kb) = f x 
+                                           (c ** kc) = g b
+                                       in (c ** kb . kc)
   public export
   (%>>) : a =%> b -> b =%> c -> a =%> c
   (%>>) = compDepLens
 
   public export
   id : a =%> a
-  id = !% \x => (x ** \y => y)
+  id = !% \x => (x ** id)
 
 namespace DependentCharts
   ||| Dependent charts
   ||| Forward-forward container morphisms
   public export
-  record (=&>) (c1, c2 : Cont) where
-    constructor (<&!)
-    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))) ->
-    c1 =&> c2
-  (!&) f = (\x => fst (f x)) <&! (\x => snd (f x))
+  data (=&>) : (c1, c2 : Cont) -> Type where
+    (!&) : ((x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))) -> c1 =&> c2
 
+  %name (=&>) f, g, h
 
+  public export
+  (%!) : c1 =&> c2 -> (x : c1.Shp) -> (y : c2.Shp ** (c1.Pos x -> c2.Pos y))
+  (%!) (!& f) x = f x
+  
   public export
   compDepChart : a =&> b -> b =&> c -> a =&> c
-  compDepChart f g =
-      (g.fwd . f.fwd) <&!
-      (\x => g.fwd' (f.fwd x) . f.fwd' x)
+  compDepChart (!& f) (!& g) = !& \x => let (b ** kb) = f x 
+                                            (c ** kc) = g b
+                                        in (c ** kc . kb)
 
   public export
   (&>>) : a =&> b -> b =&> c -> a =&> c
   (&>>) = compDepChart
 
   public export
   id : a =&> a
-  id = !& \x => (x ** \y => y)
-
+  id = !& \x => (x ** id)
 
 -- experimental stuff below
 ||| TODO is this the extension of a container?
@@ -101,16 +81,5 @@ val (shp !> pos) r = (s : shp) !> (pos s -> r)
 valContMap : {c1, c2 : Cont} -> {r : Type}
   ->  (f : c1 =&> c2)
   ->  (c1 `val` r) =%> (c2 `val` r)
-valContMap {c1=(shp !> pos)} {c2=(shp' !> pos')} (fwd <&! fwd')
-  = fwd <%! (\x, k, x' => k (fwd' x x'))
-
--- ||| A container morphism
--- public export
--- record (~%>) (c1, c2 : ContF R) where
---   constructor (<~!)
---   fwd' : c1.Shp' -> c2.Shp'
-
-
--- upd : c1 ~%> c2 -> 
--- %pair (=%>) fwd bwd
-
+valContMap {c1=(shp !> pos)} {c2=(shp' !> pos')} (!& f)
+  = !% \x => let (y ** ky) = f x in (y ** (. ky))

src/Data/Container/Morphism/Instances.idr

@@ -1,6 +1,7 @@
 module Data.Container.Morphism.Instances
 
 import Data.Fin
+import Data.Fin.Split
 
 import Data.Container.Object.Instances
 import Data.Container.Morphism.Definition
@@ -15,7 +16,13 @@ public export
 extMap : {c, d : Cont} ->
   c =%> d ->
   Ext c a -> Ext d a
-extMap (fwd <%! bwd) (sh <| index) = fwd sh <| index . bwd sh
+extMap (!% f) (sh <| index) = let (y ** ky) = f sh
+                              in y <| (index . ky)
+
+
+||| Reshape is an isomorphism!
+reshapeVectIndexes : {n, m : Nat} -> (Vect n >< Vect m) =%> Vect (n * m)
+reshapeVectIndexes = !% \((), ()) => (() ** splitProd) 
 
 
 -- need to organise this
@@ -51,17 +58,13 @@ namespace BinTreeNode
   inorder = !% \b => (numNodes b ** inorderBackward b)
 
 
-
   -- TODO reshape commented out for the same reason as reshapeTensorA is
   -- public export
   -- reshape : {oldShape, newShape : List Nat} ->
   --   Tensor oldShape a ->
   --   {auto prf : prod oldShape = prod newShape} ->
   --   Tensor newShape a
 
-
-
-
 -- Need to do some rewriting for preorder
 public export
 preorderBinTreeNode : (b : BinTreeShape) -> Fin (numNodes b) -> BinTreePosNode b
@@ -71,29 +74,16 @@ preorderBinTreeNode (NodeS lt rt) x = ?preorderBinTreeNode_rhs_1
 --  _ | Right FZ = ?whn
 --  _ | Right (FS g) = ?whr
 
-
 public export
 maybeToList : Maybe =%> List
 maybeToList = !% \b => case b of 
   False => (0 ** absurd)
   True => (1 ** \_ => ())
 
-reshapeVectIndexes : (Vect n >< Vect m) =%> Vect (n * m)
-reshapeVectIndexes = (\_ => ()) <%! (\((), ()) => ?reshapeVects_rhs2)
-
-reshapeVects :
-  (Vect n >< Vect m) `fullOf` a -> 
-  Vect (n * m) `fullOf` a
-reshapeVects (((), ()) <| index)
-  = () <| ?reshapeVects_rhs_4
-
-
 
 -- public export
 -- traverseLeaf : (x : BinTreeShape) -> FinBinTreeLeaf x -> Fin (numLeaves x)
 -- traverseLeaf LeafS Done = FZ
 -- traverseLeaf (NodeS lt rt) (GoLeft x) = weakenN (numLeaves rt) (traverseLeaf lt x)
 -- traverseLeaf (NodeS lt rt) (GoRight x) = shift (numLeaves lt) (traverseLeaf rt x)
--- 
-
--- reshapings are isomorphisms
+-- 

src/Data/Tensor/Tensor.idr

@@ -699,8 +699,8 @@ namespace Reshape
   wrap : {c, d : Cont} ->
     c =%> d ->
     Cont.Tensor [c] =%> Cont.Tensor [d]
-  wrap (fwd <%! bwd) = (\e => fwd (shapeExt e) <| \_ => ()) <%!
-    (\e, (cp ** ()) => (bwd (shapeExt e) cp ** ()))
+  wrap (!% f) = !% \e => let (y ** ky) = f (shapeExt e)
+                         in (y <| \_ => () ** \(cp ** ()) => (ky cp ** ()))
 
   ||| Effectively a wrapper around `extMap`
   ||| Allows us to define views, traversals and general reshaping
@@ -745,7 +745,7 @@ namespace Reshape
   dLensReshape : {oldShape, newShape : List Nat} ->
     {auto prf : prod oldShape = prod newShape} ->
     Vect (prod oldShape) =%> Vect (prod newShape)
-  dLensReshape = id <%! \(), i => rewrite prf in i
+  dLensReshape = !% \() => (() ** \i => rewrite prf in i)
 
   ||| Restructuring for cubical tensors that leaves number of elements unchanged
   public export
@@ -893,4 +893,4 @@ namespace Concatenate
   public export
   concat : {shape : List Nat} -> {x : Nat} ->
     Tensor (x :: shape) a -> Tensor (y :: shape) a -> Tensor (x + y :: shape) a
-  concat t t' = embedTopExt $ extractTopExt t ++ extractTopExt t'
+  concat t t' = embedTopExt $ extractTopExt t ++ extractTopExt t'