spl / splonderzoek

{-#  OPTIONS_GHC -Wall -fno-warn-missing-signatures -fno-warn-incomplete-patterns  #-}
{-#  LANGUAGE CPP  #-}
{-#  LANGUAGE StandaloneDeriving  #-}
{-#  LANGUAGE MultiParamTypeClasses  #-}
{-#  LANGUAGE TypeFamilies  #-}
{-#  LANGUAGE FunctionalDependencies  #-}
{-#  LANGUAGE FlexibleContexts  #-}
{-#  LANGUAGE FlexibleInstances  #-}
{-#  LANGUAGE TypeSynonymInstances  #-}
{-#  LANGUAGE TypeOperators  #-}
{-#  LANGUAGE UndecidableInstances  #-} --  Show (Fix ff)
{-#  LANGUAGE GADTs  #-}
{-#  LANGUAGE KindSignatures  #-}
 
module Draft_IFL_2009 where
import Prelude hiding (lookup, zipWith, mod)
import Data.List (genericLength)
import Data.Maybe
import Control.Monad
import Control.Arrow (second)
 
type family Alg tt ss :: *
 
class Fold tt where
  fold :: Alg tt ss -> tt -> ss
 
data Tree aa = Tip | Bin aa (Tree aa) (Tree aa)
 
type instance Alg (Tree aa) ss = (ss, aa -> ss -> ss -> ss)
 
instance Fold (Tree aa) where
  fold       (t, _) Tip            = t
  fold alg@  (_, b) (Bin x tL tR)  = b x (fold alg tL) (fold alg tR)
 
repFold :: (Fold tt) => Alg tt ss -> (tt -> tt) -> tt -> (ss, ss)
repFold alg f x = let { s = fold alg x ; x' = f x ; s' = fold alg x' } in (s, s')
 
empty      :: Set aa
singleton  :: aa -> Set aa
size       :: Set aa -> Int
 
insert     :: (Ord aa) => aa -> Set aa -> Set aa
fromList   :: (Ord aa) => [aa] -> Set aa
fold_      :: (ss, aa -> ss -> ss -> ss) -> Set aa -> ss
 
type Set aa = Tree aa
 
fromList = foldl (flip insert) empty
 
insert x Tip            =  singleton x
insert x (Bin y tL tR)  =  case compare x y of
                             LT  -> balance  y  (insert x tL)  tR
                             GT  -> balance  y  tL             (insert x tR)
                             EQ  -> Bin      x  tL             tR
 
balance x tL tR  | sL + sR <= 1  = Bin x tL tR
                 | sR >= 4 * sL  = rotateL x tL tR
                 | sL >= 4 * sR  = rotateR x tL tR
                 | otherwise     = Bin x tL tR
  where  sL  = size tL
         sR  = size tR
 
sizeAlg  = (0, \ _ sL sR -> 1 + sL + sR)
size     = fold sizeAlg
 
data Tree1 aa = Tip1 Int | Bin1 Int aa (Tree1 aa) (Tree1 aa)
 
size1  (Tip1  s        ) = s
size1  (Bin1  s _ _ _  ) = s
 
class TreeLike tt aa | tt -> aa where
  tip       :: tt
  bin       :: aa -> tt -> tt -> tt
  caseTree  :: tt -> rr -> (aa -> tt -> tt -> rr) -> rr
 
instance TreeLike (Tree1 aa) aa where
  tip             = Tip1  (fst sizeAlg)
  bin x tL tR     = Bin1  (snd sizeAlg x (size1 tL) (size1 tR)) x tL tR
  caseTree n t b  = case n of { Tip1 _ -> t ; Bin1 _ x tL tR -> b x tL tR }
 
insert1 x t = caseTree t  (singleton1 x)
                          $ \ y tL tR ->  case compare x y of
                                            LT  -> balance1    y  (insert1 x tL)  tR
                                            GT  -> balance1    y  tL              (insert1 x tR)
                                            EQ  -> bin         x  tL              tR
 
newtype Fix ff = In { out :: ff (Fix ff) } 
 
data Extt1 ss ff rr = Ext1 ss (ff rr)
 
type Fix1 ss ff = Fix (Extt1 ss ff)
 
in1   :: ss -> ff (Fix1 ss ff) -> Fix1 ss ff
out1  :: Fix1 ss ff -> ff (Fix1 ss ff)
ann   :: Fix1 ss ff -> ss
 
data TreeF aa rr  =  TipF | BinF aa rr rr
 
type TreeU aa     =  Fix1 Int (TreeF aa)
 
type family AlgU (ff :: * -> *) ss :: *
 
class IncrementalU ff where
  pullUp :: AlgU ff ss -> ff ss -> ss
 
type instance AlgU (TreeF aa) ss = (ss, aa -> ss -> ss -> ss)
 
instance IncrementalU (TreeF aa) where
  pullUp (t, _) TipF            = t
  pullUp (_, b) (BinF x sL sR)  = b x sL sR
 
inU :: (IncrementalU ff, Functor ff) => AlgU ff ss -> ff (Fix1 ss ff) -> Fix1 ss ff
inU alg fx = in1 (pullUp alg (fmap ann fx)) fx
 
instance TreeLike (TreeU aa) aa where
  tip             = inU sizeAlg TipF
  bin x tL tR     = inU sizeAlg (BinF x tL tR)
  caseTree n t b  = case out1 n of { TipF -> t ; BinF x tL tR -> b x tL tR }
 
type family AlgD (ff :: * -> *) ii :: *
 
class IncrementalD ff where
  pushDown :: AlgD ff ii -> ff ss -> ii -> ff ii
 
type instance AlgD (TreeF3 aa) ii = (ii -> TreeF3 aa ii, aa -> ii -> TreeF3 aa ii)
 
instance IncrementalD (TreeF3 aa) where
  pushDown (t, _) TipF3          = t
  pushDown (_, b) (BinF3 x _ _)  = b x
 
class ZipWith ff where
  zipWith :: (aa -> bb -> cc) -> ff aa -> ff bb -> ff cc
 
inD_ :: (IncrementalD ff, ZipWith ff) => AlgD ff ii -> ii -> ff (Fix1 ii ff) -> Fix1 ii ff
inD_ alg ini fx = in1 ini (zipWith push (pushDown alg fx ini) fx)
  where  push i  = inD_ alg i . out1
 
depths :: Tree aa -> Tree Int
depths Tip            = Tip
depths (Bin _ tL tR)  = Bin 1 (fmap (+1) (depths tL)) (fmap (+1) (depths tR))
 
depthAlg  = (const TipF3, \ x i -> let i' = 1 + i in BinF3 x i' i')
depthIni  = 1
 
instance TreeLike (Fix1 Int (TreeF3 aa)) aa where
  tip             = inD depthAlg depthIni TipF3
  bin x tL tR     = inD depthAlg depthIni (BinF3 x tL tR)
  caseTree n t b  = case out1 n of { TipF3 -> t ; BinF3 x tL tR -> b x tL tR }
 
depthOf k t = caseTree t  Nothing
                          $ \ x tL tR ->  case compare k x of
                                            EQ  -> Just (ann t)
                                            LT  -> depthOf k tL
                                            GT  -> depthOf k tR
 
inD :: (IncrementalD ff, ZipWith ff, Eq ii) => AlgD ff ii -> ii -> ff (Fix1 ii ff) -> Fix1 ii ff
inD alg ini fx = in1 ini (zipWith push (pushDown alg fx ini) fx)
  where  push i x  | i == ann x  = x
                   | otherwise   = inD alg i (out1 x)
 
data Extt2  ii ss ff rr  = Ext2 ii ss (ff rr)
type Fix2   ii ss ff     = Fix (Extt2 ii ss ff)
 
in2   :: ii -> ss -> ff (Fix2 ii ss ff) -> Fix2 ii ss ff
out2  :: Fix2 ii ss ff -> ff (Fix2 ii ss ff)
syn   :: Fix2 ii ss ff -> ss
inh   :: Fix2 ii ss ff -> ii
 
type family AlgC (ff :: * -> *) ii ss :: *
 
class IncrementalC ff where
  passAround :: AlgC ff ii ss -> ff ss -> ii -> (ss, ff ii)
 
type instance AlgC (TreeF aa) ii ss = (ii -> (ss, TreeF aa ii), aa -> ss -> ss -> ii -> (ss, TreeF aa ii))
 
instance IncrementalC (TreeF aa) where
  passAround (t, _) TipF            = t
  passAround (_, b) (BinF x sL sR)  = b x sL sR
 
inC ::  (IncrementalC ff, Functor ff, ZipWith ff, Eq ii)
        => AlgC ff ii ss -> (ss -> ii) -> ff (Fix2 ii ss ff) -> Fix2 ii ss ff
inC alg top fx = in2 ini s (zipWith push fi fx)
  where  ini      = top s
         (s, fi)  = passAround alg (fmap syn fx) ini
         push i x  | i == inh x  = x
                   | otherwise   = inC alg (const i) (out2 x)
 
diff :: [Float] -> [Float]
diff xs = let avg ys = sum ys / genericLength ys in map (\ x -> x - avg xs) xs
 
data     DiffS  = DS  { sumS :: Float, sizeS :: Float, diffS :: Float }
newtype  DiffI  = DI  { avgI :: Float }
 
diffAlg = (t, b)
  where  t  _          = (DS { sumS = 0, sizeS = 0, diffS = 0 }  , TipF        )
         b  x sL sR i  = (s                                      , BinF x i i  )
           where s = DS  {  sumS   = x + sumS sL + sumS sR
                         ,  sizeS  = 1 + sizeS sL + sizeS sR
                         ,  diffS  = x - avgI i }
 
diffFun s = DI { avgI = sumS s / sizeS s }
 
instance TreeLike (Fix2 DiffI DiffS (TreeF Float)) Float where
  tip             = inC diffAlg diffFun TipF
  bin x tL tR     = inC diffAlg diffFun (BinF x tL tR)
  caseTree n t b  = case out2 n of { TipF -> t ; BinF x tL tR -> b x tL tR }
 
diffC :: (TreeLike (Fix2 ii DiffS ff) aa, TreeLike tt Float) => Fix2 ii DiffS ff -> tt
diffC n =  caseTree n tip (\ _ tL tR -> bin (diffOf n) (diffC tL) (diffC tR))
 
diffOf :: Fix2 ii DiffS ff -> Float
diffOf = diffS . syn
 
newtype  KK aa            rr = K aa
newtype  II               rr = I rr
data     UU               rr = U
data     (ff  ::*::  gg)  rr = ff rr :*: gg rr
data     (ff  :+:    gg)  rr = L (ff rr) | R (gg rr)
 
type TreePF aa = UU :+: KK aa ::*:: II ::*:: II
 
instance TreeLike (Fix (TreePF aa)) aa where
  tip             = In (L U)
  bin x tL tR     = In (R (K x :*: I tL :*: I tR))
  caseTree n t b  = case out n of { L U -> t ; R (K x :*: I tL :*: I tR) -> b x tL tR }
 
type instance AlgC II ii ss = ss -> ii -> (ss, ii)
 
instance IncrementalC II where
  passAround f (I x) = second I . f x
 
type instance AlgC (II ::*:: gg) ii ss = ss -> ii -> (AlgC gg ii ss, ii)
 
instance (IncrementalC gg) => IncrementalC (II ::*:: gg) where
  passAround f (I x :*: y) i =  let  (g, i')  = f x i
                                     (s, gi)  = passAround g y i
                                in   (s, I i' :*: gi)
 
diffAlgPF = (t, bL)
  where  bL x sL iL = (bR, iL)
           where  bR sR iR = (s, iR)
          
 
                    where s = DS  {  sumS   = x + sumS sL + sumS sR
                                  ,  sizeS  = 1 + sizeS sL + sizeS sR
                                  ,  diffS  = x - avgI iL
                                  }
         t _ = DS { sumS = 0, sizeS = 0, diffS = 0 }
 
class (Functor ff) => Zipper ff where
  fill    :: Ctx ff rr -> rr -> ff rr
  first   :: (rr -> Ctx ff rr -> aa) -> ff rr -> Maybe aa
  next    :: (rr -> Ctx ff rr -> aa) -> Ctx ff rr -> rr -> Maybe aa
 
  fillS   :: (Zipper gg) => Ctx ff (Fix2 ii ss gg) -> ss -> ff ss
  seekI   :: Ctx ff ss -> ff ii -> ii
 
data family Ctx (ff :: * -> *) :: * -> *
 
data Locc :: * -> * -> (* -> *) -> * where
  Loc ::  (Zipper ff, IncrementalC ff, ZipWith ff, Eq ii)
          =>  AlgC ff ii ss ->  (ss -> ii) ->  Fix2 ii ss ff ->  [Ctx ff (Fix2 ii ss ff)] ->  Locc ii ss ff
 
enter   ::  (Zipper ff, IncrementalC ff, ZipWith ff, Eq ii)
            => AlgC ff ii ss -> (ss -> ii) -> Fix2 ii ss ff -> Locc ii ss ff
leave   :: Locc ii ss ff -> Fix2 ii ss ff
up      :: Locc ii ss ff -> Maybe (Locc ii ss ff)
down    :: Locc ii ss ff -> Maybe (Locc ii ss ff)
right   :: Locc ii ss ff -> Maybe (Locc ii ss ff)
update  :: (Functor (Ctx ff)) => (Fix2 ii ss ff -> Fix2 ii ss ff) -> Locc ii ss ff -> Locc ii ss ff
 
digest ::  (Zipper ff, Zipper gg, IncrementalC ff) => AlgC ff ii ss -> Ctx ff (Fix2 ii ss gg) -> ss -> ii -> (ss, ii)
digest alg c s = second (seekI c) . passAround alg (fillS c s)
 
data family Thread (ff :: * -> *) aa :: *
 
class (Functor ff) => Paths ff where
  paths :: ff aa -> ff (Thread ff aa)
 
data instance Thread Tree aa = T aa | TL (Thread Tree aa) aa | TR (Thread Tree aa) aa
 
accumD :: (Fold (Thread ff aa), Paths ff) => Alg (Thread ff aa) ss -> ff aa -> ff ss
accumD alg = fmap (fold alg) . paths
 
empty        = Tip
singleton x  = Bin x empty empty
fold_        = fold
 
empty1      :: Tree1 aa
singleton1  :: aa -> Tree1 aa
insert1     :: (Ord aa) => aa -> Tree1 aa -> Tree1 aa
 
empty1 = tip
 
singleton1 x = bin x empty1 empty1
 
rotateL x tL tR@(Bin _ tRL tRR)
  | size tRL < 2 * size tRR  = singleL x tL tR
  | otherwise                = doubleL x tL tR
  where
    singleL x' tA (Bin y tB            tC) = Bin y (Bin x' tA tB) tC
    doubleL x' tA (Bin y (Bin z tB tC) tD) = Bin z (Bin x' tA tB) (Bin y tC tD)
 
rotateR x tL@(Bin _ tLL tLR) tR
  | size tLR < 2 * size tLL  = singleR x tL tR
  | otherwise                = doubleR x tL tR
  where
    singleR x' (Bin y tA tB           ) tC = Bin y tA            (Bin x' tB tC)
    doubleR x' (Bin y tA (Bin z tB tC)) tD = Bin z (Bin y tA tB) (Bin x' tC tD)
 
balance1 x tL tR
  | sL + sR <= 1  = bin x tL tR
  | sR >= 4 * sL  = rotateL1 x tL tR
  | sL >= 4 * sR  = rotateR1 x tL tR
  | otherwise     = bin x tL tR
  where
    sL   = size1 tL
    sR   = size1 tR
    rotateL1 x' tL' tR'@(Bin1 _ _ tRL tRR)
      | size1 tRL < 2 * size1 tRR  = singleL1 x' tL' tR'
      | otherwise                  = doubleL1 x' tL' tR'
      where
        singleL1 x'' tA (Bin1 _ y tB tC)               = bin y (bin x'' tA tB) tC
        doubleL1 x'' tA (Bin1 _ y (Bin1 _ z tB tC) tD) = bin z (bin x'' tA tB) (bin y tC tD)
    rotateR1 x' tL'@(Bin1 _ _ tLL tLR) tR'
      | size1 tLR < 2 * size1 tLL    = singleR1 x' tL' tR'
      | otherwise                    = doubleR1 x' tL' tR'
      where
        singleR1 x'' (Bin1 _ y tA tB) tC               = bin y tA (bin x'' tB tC)
        doubleR1 x'' (Bin1 _ y tA (Bin1 _ z tB tC)) tD = bin z (bin y tA tB) (bin x'' tC tD)
 
-- 
 
deriving instance (Show aa) => Show (Tree aa)
deriving instance (Eq aa) => Eq (Tree aa)
 
instance Functor Tree where
  fmap _ Tip            = Tip
  fmap f (Bin x tL tR)  = Bin (f x) (fmap f tL) (fmap f tR)
 
deriving instance (Show aa) => Show (Tree1 aa)
deriving instance (Eq aa) => Eq (Tree1 aa)
 
-- 
 
instance Functor (TreeF aa) where
  fmap _ TipF            = TipF
  fmap f (BinF a rL rR)  = BinF a (f rL) (f rR)
 
instance ZipWith (TreeF aa) where
  zipWith _  TipF               TipF              = TipF
  zipWith f  (BinF x1 sL1 sR1)  (BinF _ sL2 sR2)  = BinF x1 (f sL1 sL2) (f sR1 sR2)
  zipWith _  _                  _                 = error "zipWith: mismatch!"
 
deriving instance (Show aa, Show rr) => Show (TreeF aa rr)
deriving instance (Eq aa, Eq rr) => Eq (TreeF aa rr)
 
-- 
 
foldFix :: (Functor ff) => (ff ss -> ss) -> Fix ff -> ss
foldFix f = f . fmap (foldFix f) . out
 
deriving instance (Show (ff (Fix ff))) => Show (Fix ff)
deriving instance (Eq (ff (Fix ff))) => Eq (Fix ff)
 
-- 
 
deriving instance (Show ss, Show (ff rr)) => Show (Extt1 ss ff rr)
deriving instance (Eq ss, Eq (ff rr)) => Eq (Extt1 ss ff rr)
 
deriving instance (Show ii, Show ss, Show (ff rr)) => Show (Extt2 ii ss ff rr)
deriving instance (Eq ii, Eq ss, Eq (ff rr)) => Eq (Extt2 ii ss ff rr)
 
-- 
 
in1 s x = In (Ext1 s x)
out1 (In (Ext1 _ x)) = x
ann (In (Ext1 s _)) = s
 
size2 :: TreeU aa -> Int
size2 = ann
 
data TreeF3 aa rr  =  TipF3
                   |  BinF3 aa rr rr
  deriving (Show, Eq)
 
instance ZipWith (TreeF3 aa) where
  zipWith _  TipF3               TipF3              = TipF3
  zipWith f  (BinF3 x1 sL1 sR1)  (BinF3 _ sL2 sR2)  = BinF3 x1 (f sL1 sL2) (f sR1 sR2)
  zipWith _  _                   _                  = error "zipWith: mismatch!"
 
depthAlg :: (Int -> TreeF3 aa Int, aa -> Int -> TreeF3 aa Int)
depthIni :: Int
 
 
val3 :: Fix1 Int (TreeF3 Char)
val3 = bin 'b' (bin 'a' tip tip) (bin 'c' tip (bin 'd' tip tip))
 
val3_ :: Fix1 Int (TreeF3 Char)
val3_ = bin_ 'b' (bin_ 'a' tip_ tip_) (bin_ 'c' tip_ (bin_ 'd' tip_ tip_))
  where
    tip_          = inD_ depthAlg depthIni TipF3
    bin_ x tL tR  = inD_ depthAlg depthIni (BinF3 x tL tR)
 
test_inD3_1 = val3 == val3_
 
-- 
 
in2 i s x = In (Ext2 i s x)
out2 (In (Ext2 _ _ x)) = x
syn (In (Ext2 _ s _)) = s
inh (In (Ext2 i _ _)) = i
 
-- 
 
data     CountS = CS { sizeOf :: Int, countOf :: Int } deriving (Eq, Show)
newtype  CountI = CI' { startOf :: Int } deriving (Eq, Show)
 
countAlg :: (CountI -> (CountS, TreeF aa CountI), aa -> CountS -> CountS -> CountI -> (CountS, TreeF aa CountI))
countAlg = (t, b)
  where t _ = (CS 0 0, TipF)
        b x sL sR i = (CS (1 + sizeOf sL + sizeOf sR) (startOf i + sizeOf sL), BinF x i (CI' (1 + startOf i + sizeOf sL)))
 
countFun :: CountS -> CountI
countFun _ = CI' 1
 
instance TreeLike (Fix2 CountI CountS (TreeF aa)) aa where
  tip             = inC countAlg countFun TipF
  bin x tL tR     = inC countAlg countFun (BinF x tL tR)
  caseTree n t b  = case out2 n of { TipF -> t ; BinF x tL tR -> b x tL tR }
 
val4 :: Fix2 CountI CountS (TreeF Char)
val4 = bin 'b' (bin 'a' tip tip) (bin 'c' tip (bin 'd' tip tip))
 
toPairs n = go n []
  where go t = caseTree t id (\ x tL tR -> go tL . ((x, countOf (syn t)) :) . go tR)
 
-- 
 
deriving instance Show DiffI
deriving instance Eq DiffI
deriving instance Show DiffS
deriving instance Eq DiffS
 
val5 :: Fix2 DiffI DiffS (TreeF Float)
val5 = bin 2 (bin 1 tip tip) (bin 3 tip (bin 4 tip tip))
 
-- 
 
infixr 6 :+:
infixr 7 :*:, ::*::
 
deriving instance (Eq aa) => Eq (KK aa rr)
deriving instance (Show aa) => Show (KK aa rr)
deriving instance Show (UU rr)
deriving instance Eq (UU rr)
deriving instance (Eq rr) => Eq (II rr)
deriving instance (Show rr) => Show (II rr)
deriving instance (Eq (ff rr), Eq (gg rr)) => Eq ((ff :+: gg) rr)
deriving instance (Show (ff rr), Show (gg rr)) => Show ((ff :+: gg) rr)
deriving instance (Eq (ff rr), Eq (gg rr)) => Eq ((ff ::*:: gg) rr)
deriving instance (Show (ff rr), Show (gg rr)) => Show ((ff ::*:: gg) rr)
 
-- 
 
instance Functor (KK a) where
  fmap _ (K a) = K a
 
instance Functor UU where
  fmap _ U = U
 
instance Functor II where
  fmap f (I r) = I (f r)
 
instance (Functor f, Functor g) => Functor (f :+: g) where
  fmap f (L x) = L (fmap f x)
  fmap f (R y) = R (fmap f y)
 
instance (Functor f, Functor g) => Functor (f ::*:: g) where
  fmap f (x :*: y) = fmap f x :*: fmap f y
 
-- 
 
instance ZipWith (KK a) where
  zipWith _ (K x) (K _) = K x
 
instance ZipWith UU where
  zipWith _ U U = U
 
instance ZipWith II where
  zipWith f (I x) (I y) = I (f x y)
 
instance (ZipWith f, ZipWith g) => ZipWith (f :+: g) where
  zipWith f (L x) (L y) = L (zipWith f x y)
  zipWith f (R x) (R y) = R (zipWith f x y)
  zipWith _ _     _     = error "zipWith: mismatch!"
 
instance (ZipWith f, ZipWith g) => ZipWith (f ::*:: g) where
  zipWith f (x1 :*: y1) (x2 :*: y2) = zipWith f x1 x2 :*: zipWith f y1 y2
 
-- 
 
type family PF tt :: * -> *
 
class Regular tt where
  from  :: tt -> PF tt tt
  to    :: PF tt tt -> tt
 
-- 
 
impossible :: a
impossible = error "Impossible!"
 
-- 
 
type instance AlgU (KK aa) ss = aa -> ss
instance IncrementalU (KK a) where
  pullUp f (K x) = f x
 
type instance AlgU UU ss = ss
instance IncrementalU UU where
  pullUp f U = f
 
type instance AlgU II ss = ss -> ss
instance IncrementalU II where
  pullUp f (I x) = f x
 
type instance AlgU (ff :+: gg) ss = (AlgU ff ss, AlgU gg ss)
instance (IncrementalU f, IncrementalU g) => IncrementalU (f :+: g) where
  pullUp (f, _) (L x) = pullUp f x
  pullUp (_, g) (R x) = pullUp g x
 
type instance AlgU (KK aa ::*:: gg) ss = aa -> AlgU gg ss
instance (IncrementalU g) => IncrementalU (KK a ::*:: g) where
  pullUp f (K x :*: y) = pullUp (f x) y
 
type instance AlgU (II ::*:: gg) ss = ss -> AlgU gg ss
instance (IncrementalU g) => IncrementalU (II ::*:: g) where
  pullUp f (I x :*: y) = pullUp (f x) y
 
foldF :: (Regular a, IncrementalU (PF a), Functor (PF a)) => AlgU (PF a) r -> a -> r
foldF f = pullUp f . fmap (\ x -> foldF f x) . from
 
-- 
 
type instance AlgD (KK aa) ii = ()
instance IncrementalD (KK aa) where
  pushDown _ (K x) _ = K x
 
type instance AlgD UU ii = ()
instance IncrementalD UU where
  pushDown _ U _ = U
 
type instance AlgD II ii = ii -> ii
instance IncrementalD II where
  pushDown f (I _) i = I (f i)
 
type instance AlgD (ff :+: gg) ii = (AlgD ff ii, AlgD gg ii)
instance (IncrementalD ff, IncrementalD gg) => IncrementalD (ff :+: gg) where
  pushDown (f, _) (L x) = L . pushDown f x
  pushDown (_, g) (R y) = R . pushDown g y
 
type instance AlgD (KK aa ::*:: gg) ii = aa -> AlgD gg ii
instance (IncrementalD gg) => IncrementalD (KK aa ::*:: gg) where
  pushDown f (K x :*: y) = (:*:) (K x) . pushDown (f x) y
 
type instance AlgD (II ::*:: gg) ii = ii -> (ii, AlgD gg ii)
instance (IncrementalD gg) => IncrementalD (II ::*:: gg) where
  pushDown f (I _ :*: y) i1 = let (i2, g) = f i1 in I i2 :*: pushDown g y i1
 
-- 
 
type instance AlgC (KK aa) ii ss = aa -> ii -> ss
instance IncrementalC (KK aa) where
  passAround f (K x) i = (f x i, K x)
 
type instance AlgC UU ii ss = ii -> ss
instance IncrementalC UU where
  passAround f U i = (f i, U)
 
type instance AlgC (KK aa ::*:: gg) ii ss = aa -> AlgC gg ii ss
instance (IncrementalC gg) => IncrementalC (KK aa ::*:: gg) where
  passAround f (K x :*: y) = second (K x :*:) . passAround (f x) y
 
type instance AlgC (ff :+: gg) ii ss = (AlgC ff ii ss, AlgC gg ii ss)
instance (IncrementalC ff, IncrementalC gg) => IncrementalC (ff :+: gg) where
  passAround (f  , _  ) (L  x) = second L  . passAround f  x
  passAround (_  , g  ) (R  x) = second R  . passAround g  x
 
-- 
 
diffAlgPF :: AlgC (TreePF Float) DiffI DiffS
 
instance TreeLike (Fix2 DiffI DiffS (TreePF Float)) Float where
  tip             = inC diffAlgPF diffFun (L U)
  bin x tL tR     = inC diffAlgPF diffFun (R (K x :*: I tL :*: I tR))
  caseTree n t b  = case out2 n of { L U -> t ; R (K x :*: I tL :*: I tR) -> b x tL tR }
 
val6 :: Fix2 DiffI DiffS (TreePF Float)
val6 = bin 2 (bin 1 tip tip) (bin 3 tip (bin 4 tip tip))
 
tmap :: (TreeLike tt1 aa, TreeLike tt2 bb) => (aa -> bb) -> tt1 -> tt2
tmap f t = caseTree t tip (\ x tL tR -> bin (f x) (tmap f tL) (tmap f tR))
 
-- 
 
countAlg' :: AlgC (TreePF aa) CountI CountS
countAlg' = (t, bL)
  where  t _ = CS 0 0
         bL _ sL iL = (bR, iL)
           where bR sR iR = (s, iR')
                   where s = CS (1 + sizeOf sL + sizeOf sR) (startOf iL + sizeOf sL)
                         iR' = CI' (1 + startOf iR + sizeOf sL)
 
instance TreeLike (Fix2 CountI CountS (TreePF aa)) aa where
  tip             = inC countAlg' countFun (L U)
  bin x tL tR     = inC countAlg' countFun (R (K x :*: I tL :*: I tR))
  caseTree n t b  = case out2 n of { L U -> t ; R (K x :*: I tL :*: I tR) -> b x tL tR }
 
val6b :: Fix2 CountI CountS (TreePF Char)
val6b = bin 'x' (bin 'w' (bin 'v' tip tip) tip) (bin 'y' tip (bin 'z' tip tip))
 
-- 
 
data instance Ctx (KK a) rr
data instance Ctx UU rr
data instance Ctx II rr = CI
data instance Ctx (ff :+: gg) rr = CL (Ctx ff rr)
                                 | CR (Ctx gg rr)
data instance Ctx (ff ::*:: gg) rr = C1 (Ctx ff rr) (gg rr)
                                   | C2 (ff rr) (Ctx gg rr)
 
-- 
 
instance Functor (Ctx (KK a)) where
  fmap _ _ = impossible
 
instance Functor (Ctx UU) where
  fmap _ _ = impossible
 
instance Functor (Ctx II) where
  fmap _ CI = CI
 
instance (Functor (Ctx f), Functor (Ctx g)) => Functor (Ctx (f :+: g)) where
  fmap f (CL c) = CL (fmap f c)
  fmap f (CR c) = CR (fmap f c)
 
instance (Functor f, Functor g, Functor (Ctx f), Functor (Ctx g))
         => Functor (Ctx (f ::*:: g)) where
  fmap f (C1 c y) = C1 (fmap f c) (fmap f y)
  fmap f (C2 x c) = C2 (fmap f x) (fmap f c)
 
-- 
 
instance Show (Ctx (KK a) r) where show _ = impossible
instance Show (Ctx UU r) where show _ = impossible
deriving instance (Show r) => Show (Ctx II r)
deriving instance (Show (Ctx f r), Show (Ctx g r)) => Show (Ctx (f :+: g) r)
deriving instance (Show (f r), Show (g r), Show (Ctx f r), Show (Ctx g r)) => Show (Ctx (f ::*:: g) r)
 
-- 
 
instance Eq (Ctx (KK a) r) where _ == _ = True
instance Eq (Ctx UU r) where _ == _ = True
deriving instance Eq (Ctx II r)
deriving instance (Eq (Ctx f r), Eq (Ctx g r)) => Eq (Ctx (f :+: g) r)
deriving instance (Eq (f r), Eq (g r), Eq (Ctx f r), Eq (Ctx g r)) => Eq (Ctx (f ::*:: g) r)
 
-- 
 
instance IncrementalC (Ctx (KK aa)) where
  passAround _ _ _ = impossible
 
instance IncrementalC (Ctx UU) where
  passAround _ _ _ = impossible
 
type instance AlgC (Ctx II) ii ss = ii -> ss
instance IncrementalC (Ctx II) where
  passAround f CI i = (f i, CI)
 
type instance AlgC (Ctx (ff :+: gg)) ii ss = (AlgC (Ctx ff) ii ss, AlgC (Ctx gg) ii ss)
instance (IncrementalC (Ctx ff), IncrementalC (Ctx gg)) => IncrementalC (Ctx (ff :+: gg)) where
  passAround (f, _) (CL c) = second CL . passAround f c
  passAround (_, g) (CR c) = second CR . passAround g c
 
type instance AlgC (Ctx (ff ::*:: gg)) ii ss = (AlgC (Ctx ff) ii ss, ss -> AlgC gg ii ss, AlgC ff ii ss, ss -> AlgC (Ctx gg) ii ss)
instance (IncrementalC ff, IncrementalC gg, IncrementalC (Ctx ff), IncrementalC (Ctx gg)) => IncrementalC (Ctx (ff ::*:: gg)) where
  passAround (fc, g, _, _) (C1 c y) i =
    let  (sc, ci) = passAround fc c i
         (sy, yi) = passAround (g sc) y i
    in   (sy, C1 ci yi)
  passAround (_, _, f, gc) (C2 x c) i =
    let  (sx, xi) = passAround f x i
         (sc, ci) = passAround (gc sx) c i
    in   (sc, C2 xi ci)
 
-- 
 
instance Zipper (KK aa) where
  fill _ _ = impossible
  first _ _ = Nothing
  next _ _ _ = Nothing
  fillS _ _ = impossible
  seekI _ _ = impossible
 
instance Zipper UU where
  fill _ _ = impossible
  first _ _ = Nothing
  next _ _ _ = Nothing
  fillS _ _ = impossible
  seekI _ _ = impossible
 
instance Zipper II where
  fill _ x = I x
  first f (I r)  = Just (f r CI)
  next _ _ _ = Nothing
  fillS _ s = I s
  seekI _ (I i) = i
 
instance (Zipper ff, Zipper gg) => Zipper (ff :+: gg) where
  fill (CL c) x = L (fill c x)
  fill (CR c) y = R (fill c y)
  first f (L x) = first (\ foc -> f foc . CL) x
  first f (R y) = first (\ foc -> f foc . CR) y
  next f (CL c) x = next  (\ foc -> f foc . CL) c x
  next f (CR c) y = next  (\ foc -> f foc . CR) c y
  fillS (CL c) s = L (fillS c s)
  fillS (CR c) s = R (fillS c s)
  seekI (CL c) (L x) = seekI c x
  seekI (CR c) (R y) = seekI c y
 
instance (Zipper ff, Zipper gg, IncrementalC ff, IncrementalC gg) => Zipper (ff ::*:: gg) where
  fill (C1 c y) x = fill c x :*: y
  fill (C2 x c) y = x :*: fill c y
  first f (x :*: y) =
    first (\ foc c -> f foc (C1 c y)) x `mplus` first (\ foc c -> f foc (C2 x c)) y
  next f (C1 c y) x =
    next (\ foc c' -> f foc (C1 c' y )) c x `mplus` first (\ foc c' -> f foc (C2 (fill c x) c')) y
  next f (C2 x c) y =
    next (\ foc c' -> f foc (C2 x  c')) c y
  fillS (C1 c y) s = fillS c s :*: fmap syn y
  fillS (C2 x c) s = fmap syn x :*: fillS c s
  seekI (C1 c _) (x :*: _) = seekI c x
  seekI (C2 _ c) (_ :*: y) = seekI c y
 
-- 
 
focus :: Locc ii ss ff -> Fix2 ii ss ff
focus (Loc _ _ foc _) = foc
 
instance (Show ii, Show ss, Show (ff (Fix2 ii ss ff)), Show (Fix2 ii ss ff), Show (Ctx ff (Fix2 ii ss ff))) => Show (Locc ii ss ff) where
  show (Loc _ _ foc cs) = "(Loc (" ++ show foc ++ ") " ++ show cs ++ ")"
 
instance (Eq ii, Eq ss, Eq (ff (Fix2 ii ss ff)), Eq (Fix2 ii ss ff), Eq (Ctx ff (Fix2 ii ss ff))) => Eq (Locc ii ss ff) where
  Loc _ _ foc1 cs1 == Loc _ _ foc2 cs2 = foc1 == foc2 && cs1 == cs2
 
-- 
 
enter alg fun foc = Loc alg fun foc []
 
--  Works for Diff and Count algebras and all test cases
up (Loc _   _   _   []    )  = Nothing
up (Loc alg fun foc (c:cs))  = Just (Loc alg fun foc' cs)
  where
    fun' s | null cs    = fun s    --  top-level
           | otherwise  = inh foc  --  every other level
    foc' = inC alg fun' (fill c foc)
 
leave (Loc _ _ foc []) = foc
leave loc              = leave (fromJust (up loc))
 
leaveM :: (Eq ii, ZipWith ff, Monad m) => Locc ii ss ff -> m (Fix2 ii ss ff)
leaveM = return . leave
 
down (Loc alg fun foc cs) =
  first (\ foc' c -> Loc alg fun foc' (c:cs)) (out2 foc)
 
--  See note for 'update'.
pushCtxs ::  (Functor (Ctx ff), ZipWith ff, Eq ii, Zipper ff, IncrementalC ff)
             => AlgC ff ii ss -> ss -> ii -> [Ctx ff (Fix2 ii ss ff)] -> (ss, ii, [Ctx ff (Fix2 ii ss ff)])
pushCtxs _   s     i     []     = (s, i, [])
pushCtxs alg s_bot i_top (c:cs) = (s_top, i_bot, c':cs')
  where
    (s, i_bot) = digest alg c s_bot i
    c' = fmap (inC alg (const i) . out2) c
    (s_top, i, cs') = pushCtxs alg s i_top cs
 
right (Loc _   _   _   []    ) = Nothing
right (Loc alg fun foc (c:cs)) = next (\ foc' c' -> Loc alg fun foc' (c':cs)) c foc
 
--  Works for given Diff algebra, but may not work with algebras that pass
--  values between siblings. I fmap over each context, so there is only an 'i'
--  coming from the top of the context, not the siblings. This seems to work for
--  Count, so I'm not sure how to show that it doesn't work.
update mod (Loc alg fun foc cs) = Loc alg fun foc2 cs1
  where
    foc1 = mod foc
    (s, i, cs1) = pushCtxs alg (syn foc1) (fun s) cs
    foc2 = inC alg (const i) (out2 foc1)
 
updateM f = return . update f
 
on :: (Fix2 ii ss ff -> Fix2 ii ss ff) -> Locc ii ss ff -> Fix2 ii ss ff
on f (Loc _ _ foc _) = f foc
 
-- 
 
val7 = enter diffAlgPF diffFun val6
test_zipper_1 = val7 == fromJust (return val7 >>= down >>= up)
test_zipper_2 = val7 == fromJust (return val7 >>= down >>= down >>= up >>= up)
test_zipper_3 = val7 == fromJust (return val7 >>= down >>= right >>= up)
test_zipper_4 = focus val7 == fromJust (return val7 >>= down >>= right >>= down >>= leaveM)
test_zipper_5 = val7 == update id val7
val7b = enter diffAlgPF diffFun (bin 1 tip tip :: Fix2 DiffI DiffS (TreePF Float))
test_zipper_6 = Just val7b == (return val7b >>= down >>= updateM id >>= up)
test_zipper_7 = bin 2 (bin 1 tip tip) (bin 0 tip tip) == fromJust (return val7 >>= down >>= right >>= updateM (const (bin 0 tip tip)) >>= leaveM)
val7c = enter countAlg' countFun val6b
test_zipper_8 = val7c == fromJust (return val7c >>= down >>= up)
test_zipper_9 = val7c == fromJust (return val7c >>= down >>= right >>= up)
test_zipper_10 = val7c == fromJust (return val7c >>= down >>= down >>= right >>= up >>= up)
test_zipper_11 = bin 'x' (bin 'w' tip tip) (bin 'y' tip (bin 'z' tip tip)) == fromJust (return val7c >>= down >>= down >>= updateM (const tip) >>= leaveM)
 
--  The following should return True.
test_zipper
  =  test_zipper_1
  && test_zipper_2
  && test_zipper_3
  && test_zipper_4
  && test_zipper_5
  && test_zipper_6
  && test_zipper_7
  && test_zipper_8
  && test_zipper_9
  && test_zipper_10
  && test_zipper_11
 
-- 
 
type instance Alg (Thread Tree aa) ss = (aa -> ss, ss -> aa -> ss, ss -> aa -> ss)
 
instance Fold (Thread Tree aa) where
  fold       (t, _, _) (T x)     = t x
  fold alg@  (_, l, _) (TL t x)   = l (fold alg t) x
  fold alg@  (_, _, r) (TR t x)  = r (fold alg t) x
 
deriving instance (Show aa) => Show (Thread Tree aa)
deriving instance (Eq aa) => Eq (Thread Tree aa)
 
instance Paths Tree where
  paths Tip           = Tip
  paths (Bin x tL tR) = Bin (T x) (fmap (lt x) (paths tL)) (fmap (rt x) (paths tR))
    where
      lt y = fold (TL (T y), TL, TR)
      rt y = fold (TR (T y), TL, TR)