Sharing control is working; seems pretty straight forward actually

src/Data/Digems/Patch/Diff.hs

@@ -221,17 +221,25 @@ close utx = case closure utx of
 --         both the source and deletion context
 --    v)   Extract the spine and compute the closure.
 --
-diff :: (EqHO ki , DigestibleHO ki , IsNat ix)
-     => MinHeight
-     -> Fix ki codes ix
-     -> Fix ki codes ix
-     -> Patch ki codes ix
-diff mh x y
-  = let dx      = preprocess x
-        dy      = preprocess y
+diff' :: (EqHO ki , DigestibleHO ki , IsNat ix)
+      => MinHeight
+      -> SharingControl ki codes
+      -> Fix ki codes ix
+      -> Fix ki codes ix
+      -> Patch ki codes ix
+diff' mh ctl x y
+  = let dx      = preprocess ctl x
+        dy      = preprocess ctl y
         (i, sh) = buildSharingTrie mh dx dy
         dx'     = tagProperShare sh dx
         dy'     = tagProperShare sh dy
         del     = extractUTx mh sh dx'
         ins     = extractUTx mh sh dy'
      in close (extractSpine metavarI2IK i del ins)
+
+diff :: (EqHO ki , DigestibleHO ki , IsNat ix)
+     => MinHeight
+     -> Fix ki codes ix
+     -> Fix ki codes ix
+     -> Patch ki codes ix
+diff mh x y = diff' mh noSharingControl x y

src/Data/Digems/Patch/Preprocess.hs

@@ -14,7 +14,7 @@ import Data.Proxy
 import Data.Functor.Const
 
 import Generics.MRSOP.Base
-import Generics.MRSOP.AG (AnnFix(..) , synthesize)
+import Generics.MRSOP.AG (AnnFix(..) , synthesize, getAnn)
 
 import Generics.MRSOP.Digems.Digest
 
@@ -45,22 +45,24 @@ heightAlgebra proj = Const . (1+) . elimRep (const 0) proj safeMax
 --  'synthesize' an annotated fixpoint quite easily:
 preprocess :: forall ki codes ix
             . (IsNat ix , DigestibleHO ki)
-           => Fix ki codes ix
+           => SharingControl ki codes
+           -> Fix ki codes ix
            -> PrepFix () ki codes ix
-preprocess = synthesize alg
+preprocess sharing = runSharingM . synthesizeM' (decideSharing sharing) alg
   where
     cast :: (IsNat iy) => Proxy iy -> Const ann iy -> Const ann iy
     cast _ = id
 
     alg :: forall iy sum
          . (IsNat iy)
         => Rep ki (Const (PrepData ())) sum
-        -> Const (PrepData ()) iy
+        -> SharingM (Const (PrepData ()) iy)
     alg rep
       = let f         = cast (Proxy :: Proxy iy)
             -- we need to help the type-checker infer that we
             -- we want the SAME index from both algebras. We do
             -- that by the means of our f function above.
-            Const dig = f $ authAlgebra   (treeDigest . getConst) rep
-            Const h   = f $ heightAlgebra (treeHeight . getConst) rep
-         in Const (PrepData dig h ())
+            digM    = f <$> authAlgebra   (treeDigest . getConst) rep
+            Const h = f $ heightAlgebra (treeHeight . getConst) rep
+         in digM >>= \(Const dig) -> return (Const (PrepData dig h ()))
+

src/Generics/MRSOP/Digems/Digest.hs

@@ -18,8 +18,71 @@ import qualified Data.ByteArray.Mapping as BA
 import qualified Crypto.Hash            as Hash
 import qualified Crypto.Hash.Algorithms as Hash (Blake2s_256)
 
+import Control.Monad.Reader
+
 import Generics.MRSOP.Base
-import Generics.MRSOP.AG (AnnFix(..) , synthesize)
+import Generics.MRSOP.AG (AnnFix(..) , synthesize, getAnn)
+
+-------------------------
+-- To be sent to mrsop
+
+cataM' :: (Monad m , IsNat ix)
+       => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a)
+       -> (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy))
+       -> Fix ki codes ix
+       -> m (phi ix)
+cataM' p f xo@(Fix x) = mapRepM (p xo . cataM' p f) x >>= f
+
+synthesizeM' :: forall ki phi codes ix m a
+              . (Monad m , IsNat ix)
+             => (forall iy a. IsNat iy => Fix ki codes iy -> m a -> m a)
+             -> (forall iy  . IsNat iy => Rep ki phi (Lkup iy codes) -> m (phi iy))
+             -> Fix ki codes ix
+             -> m (AnnFix ki codes phi ix)
+synthesizeM' p f = cataM' p alg
+  where
+    alg :: forall iy
+         . (IsNat iy)
+        => Rep ki (AnnFix ki codes phi) (Lkup iy codes)
+        -> m (AnnFix ki codes phi iy)
+    alg xs = flip AnnFix xs <$> f (mapRep getAnn xs)
+
+-- End of 'to be sent to mrsop'
+----------------------------
+
+---------------------------
+-- Sharing info
+
+type SharingControl ki codes
+  = forall ix . (IsNat ix) => (Fix ki codes ix -> Maybe String)
+
+noSharingControl :: SharingControl ki codes
+noSharingControl = const Nothing
+
+newtype SharingBarrier = SharingBarrier { sharingStack :: [String] }
+  deriving (Eq , Show)
+
+pushName :: String -> SharingBarrier -> SharingBarrier
+pushName name (SharingBarrier xs) = SharingBarrier $ name : xs
+
+type SharingM = Reader SharingBarrier
+
+runSharingM = flip runReader (SharingBarrier [])
+
+decideSharing :: (IsNat iy)
+              => SharingControl ki codes
+              -> Fix ki codes iy
+              -> SharingM a -> SharingM a
+decideSharing sh f = case sh f of
+                    Nothing      -> id
+                    Just scopeId -> local (pushName scopeId)
+
+hashSharingBarrier :: SharingBarrier -> Digest
+hashSharingBarrier = hashStr . concat . sharingStack
+
+-------------------------
+
+
 
 -- |Our digests come from Blake2s_256 
 newtype Digest
@@ -68,15 +131,17 @@ class DigestibleHO (f :: k -> *) where
   digestHO :: forall ki . f ki -> Digest
 
 -- |Type synonym for fixpoints annotated with their digest.
-type DigFix ki codes = AnnFix ki codes (Const Digest)
+type DigFix ki cOdes = AnnFix ki codes (Const Digest)
 
 -- |Given a generic fixpoint, annotate every recursive position
 --  with its cryptographic digests.
 auth :: forall ki codes ix
       . (IsNat ix , DigestibleHO ki)
-     => Fix ki codes ix
+     => SharingControl ki codes
+     -> Fix ki codes ix
      -> DigFix ki codes ix
-auth = synthesize (authAlgebra getConst)
+auth sh = flip runReader (SharingBarrier [])
+        . synthesizeM' (decideSharing sh) (authAlgebra getConst)
 
 -- |And a more general form of the algebra used
 --  to compute a merkelized fixpoint.
@@ -85,13 +150,15 @@ authAlgebra :: forall ki sum ann iy
              . (DigestibleHO ki , IsNat iy)
             => (forall ix . ann ix -> Digest)
             -> Rep ki ann sum
-            -> Const Digest iy
+            -> SharingM (Const Digest iy)
 authAlgebra proj rep
   = let siy = snat2W64 $ getSNat (Proxy :: Proxy iy)
-     in case sop rep of
-       Tag c p -> Const . digestConcat
-                $ ([digest (constr2W64 c) , digest siy] ++)
-                $ elimNP (elimNA digestHO proj) p
+     in do
+       scope <- ask
+       case sop rep of
+         Tag c p -> return . Const . digestConcat
+                  $ ([hashSharingBarrier scope , digest (constr2W64 c) , digest siy] ++)
+                  $ elimNP (elimNA digestHO proj) p
   where
     -- We are mapping Constr and SNat's to
     -- Word64 because these are better handled by the 'memory'

src/Languages/RTree/Diff.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE DataKinds             #-}
+{-# LANGUAGE GADTs                 #-}
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE TypeApplications      #-}
 module Languages.RTree.Diff where
@@ -18,16 +19,32 @@ type PatchRTree = Patch W CodesRTree Z
 rbin :: RTree -> RTree -> RTree
 rbin l r = "bin" :>: [l , r]
 
+rblock :: RTree -> RTree -> RTree
+rblock l r = "ZZZ" :>: [l , r]
+
 rlf :: String -> RTree
 rlf = (:>: [])
 
-x1 = rbin (rbin (rlf "t") (rbin (rlf "u") (rlf "u"))) (rlf "k")
-y1 = rbin (rbin (rlf "t") (rbin (rlf "u") (rlf "u"))) (rlf "t")
+x1 = rbin (rblock (rlf "t") (rbin (rlf "u") (rlf "l"))) (rlf "k")
+y1 = rbin (rblock (rlf "t") (rbin (rlf "u") (rlf "l"))) (rlf "t")
 
 digemRTree :: RTree -> RTree -> PatchRTree
 digemRTree a b = diff 1 (dfrom $ into @FamRTree a)
                         (dfrom $ into @FamRTree b)
 
+block :: (IsNat ix) => Fix W CodesRTree ix -> Maybe String
+block xo@(Fix x) = case getFixSNat xo of
+  IdxRTree -> case sop x of
+                Tag CZ (NA_K (W_String str) :* _)
+                  -> if str == "ZZZ" then Just str else Nothing
+  _        -> Nothing
+
+digemRTree' :: RTree -> RTree -> PatchRTree
+digemRTree' a b = diff' 1 block
+                          (dfrom $ into @FamRTree a)
+                          (dfrom $ into @FamRTree b)
+
+
 applyRTree :: PatchRTree -> RTree -> Either String RTree
 applyRTree p x = either Left (Right . unEl . dto @Z . unFix)
                $ apply p (dfrom $ into @FamRTree x)