zipper 0.1 → 0.2
raw patch · 4 files changed
+150/−167 lines, 4 filesdep ~basedep ~multirec
Dependency ranges changed: base, multirec
Files
- examples/ASTEditor.hs +6/−5
- src/Generics/MultiRec/Zipper.hs +136/−125
- src/Generics/MultiRec/Zipper/TEq.hs +0/−28
- zipper.cabal +8/−9
examples/ASTEditor.hs view
@@ -33,13 +33,13 @@ -- | Show the current location, with the focus being highlighted in red. showZipper :: Loc AST I0 Expr -> String-showZipper l = (spaces $ map ($ 0) $ unK0 (foldZipper focus hShowsPrecAlg l)) ""- where focus :: (Ix AST ix) => AST ix -> ix -> K0 ([Int -> ShowS]) ix+showZipper l = (spaces $ map ($ 0) $ unK0 (foldZipper focus (\ p x -> K0 (hShowsPrecAlg p x)) l)) ""+ where focus :: AST ix -> ix -> K0 ([Int -> ShowS]) ix focus ix x = K0 [\ n -> ("\ESC[01;31m" ++) . GS.showsPrec ix n x . ("\ESC[00m" ++)] typeOfFocus :: Loc AST I0 Expr -> String typeOfFocus = on focus- where focus :: (Ix AST ix) => AST ix -> I0 ix -> String+ where focus :: AST ix -> I0 ix -> String focus Expr _ = "expression" focus Decl _ = "declaration" focus Var _ = "variable"@@ -60,7 +60,8 @@ 'h' -> left 'k' -> up ' ' -> dfnext- '\b' -> dfprev+ 'n' -> dfnext+ 'b' -> dfprev _ -> return case op l of Nothing -> loop l@@ -69,4 +70,4 @@ -- | Introductory help message. intro :: IO () intro =- putStrLn "h: left, j: down, k: up, l: right, q: quit, [space]: df lr traversal, [backsp]: df rl traversal"+ putStrLn "h: left, j: down, k: up, l: right, q: quit, n,[space]: df lr traversal, b: df rl traversal"
src/Generics/MultiRec/Zipper.hs view
@@ -39,47 +39,59 @@ import Prelude hiding (last) import Control.Monad+import Control.Applicative import Data.Maybe import Generics.MultiRec.Base import Generics.MultiRec.Fold import Generics.MultiRec.HFunctor-import Generics.MultiRec.Zipper.TEq -- * Locations and context stacks -- | Abstract type of locations. A location contains the current focus--- and its context. A location is parameterized over the system of+-- and its context. A location is parameterized over the family of -- datatypes and over the type of the complete value. data Loc :: (* -> *) -> (* -> *) -> * -> * where- Loc :: (Ix s ix, Zipper (PF s)) => r ix -> Ctxs s r a ix -> Loc s r a+ Loc :: (Fam phi, Zipper phi (PF phi)) => phi ix -> r ix -> Ctxs phi ix r a -> Loc phi r a -data Ctxs :: (* -> *) -> (* -> *) -> * -> * -> * where- Empty :: Ctxs s r a a- Push :: Ix s ix => Ctx (PF s) s r ix b -> Ctxs s r a ix -> Ctxs s r a b+data Ctxs :: (* -> *) -> * -> (* -> *) -> * -> * where+ Empty :: Ctxs phi a r a+ Push :: phi ix -> Ctx (PF phi) b r ix -> Ctxs phi ix r a -> Ctxs phi b r a -- * Context frames -- | Abstract type of context frames. Not required for the high-level -- navigation functions. -data family Ctx f :: (* -> *) -> (* -> *) -> * -> * -> *+data family Ctx f :: * -> (* -> *) -> * -> * -data instance Ctx (K a) s r ix b-data instance Ctx U s r ix b-data instance Ctx (f :+: g) s r ix b = CL (Ctx f s r ix b)- | CR (Ctx g s r ix b)-data instance Ctx (f :*: g) s r ix b = C1 (Ctx f s r ix b) (g s r ix)- | C2 (f s r ix) (Ctx g s r ix b)+data instance Ctx (K a) b r ix+data instance Ctx U b r ix+data instance Ctx (f :+: g) b r ix = CL (Ctx f b r ix)+ | CR (Ctx g b r ix)+data instance Ctx (f :*: g) b r ix = C1 (Ctx f b r ix) (g r ix)+ | C2 (f r ix) (Ctx g b r ix) -- The equality constraints simulate GADTs. GHC currently -- does not allow us to use GADTs as data family instances. -data instance Ctx (I xi) s r ix b = CId (b :=: xi)-data instance Ctx (f :>: xi) s r ix b = CTag (ix :=: xi) (Ctx f s r ix b)-data instance Ctx (C c f) s r ix b = CC (Ctx f s r ix b)+data instance Ctx (I xi) b r ix = CId (b :=: xi)+data instance Ctx (f :>: xi) b r ix = CTag (ix :=: xi) (Ctx f b r ix)+data instance Ctx (C c f) b r ix = CC (Ctx f b r ix) +-- * Contexts and locations are functors++instance Zipper phi f => HFunctor phi (Ctx f b) where+ hmapA = cmapA++instance Zipper phi (PF phi) => HFunctor phi (Ctxs phi b) where+ hmapA f Empty = pure Empty+ hmapA f (Push p c s) = liftA2 (Push p) (hmapA f c) (hmapA f s)++instance HFunctor phi (Loc phi) where+ hmapA f (Loc p x s) = liftA2 (Loc p) (f p x) (hmapA f s)+ -- * Generic navigation functions -- | It is in general not necessary to use the generic navigation@@ -87,91 +99,90 @@ -- below are more user-friendly. -- -class HFunctor f => Zipper f where- cmap :: (forall b. Ix s b => s b -> r b -> r' b) ->- Ctx f s r ix b -> Ctx f s r' ix b- fill :: Ix s b => Ctx f s r ix b -> r b -> f s r ix- first, last :: (forall b. Ix s b => r b -> Ctx f s r ix b -> a)- -> f s r ix -> Maybe a- next, prev :: (forall b. Ix s b => r b -> Ctx f s r ix b -> a)- -> Ix s b => Ctx f s r ix b -> r b -> Maybe a+class HFunctor phi f => Zipper phi f where+ cmapA :: Applicative a => (forall ix. phi ix -> r ix -> a (r' ix)) ->+ Ctx f b r ix -> a (Ctx f b r' ix)+ fill :: phi b -> Ctx f b r ix -> r b -> f r ix+ first, last :: (forall b. phi b -> r b -> Ctx f b r ix -> a)+ -> f r ix -> Maybe a+ next, prev :: (forall b. phi b -> r b -> Ctx f b r ix -> a)+ -> phi b -> Ctx f b r ix -> r b -> Maybe a -instance Zipper (I xi) where- cmap f (CId prf) = CId prf- fill (CId prf) x = castId prf I x- first f (I x) = return (f x (CId Refl))- last f (I x) = return (f x (CId Refl))- next f (CId prf) x = Nothing - prev f (CId prf) x = Nothing +instance El phi xi => Zipper phi (I xi) where+ cmapA f (CId prf) = pure (CId prf)+ fill p (CId prf) x = castId prf I x+ first f (I x) = return (f proof x (CId Refl))+ last f (I x) = return (f proof x (CId Refl))+ next f p (CId prf) x = Nothing+ prev f p (CId prf) x = Nothing -instance Zipper (K a) where- cmap f void = impossible void- fill void x = impossible void- first f (K a) = Nothing- last f (K a) = Nothing- next f void x = impossible void- prev f void x = impossible void+instance Zipper phi (K a) where+ cmapA f void = impossible void+ fill p void x = impossible void+ first f (K a) = Nothing+ last f (K a) = Nothing+ next f p void x = impossible void+ prev f p void x = impossible void -instance Zipper U where- cmap f void = impossible void- fill void x = impossible void- first f U = Nothing- last f U = Nothing- next f void x = impossible void- prev f void x = impossible void+instance Zipper phi U where+ cmapA f void = impossible void+ fill p void x = impossible void+ first f U = Nothing+ last f U = Nothing+ next f p void x = impossible void+ prev f p void x = impossible void -instance (Zipper f, Zipper g) => Zipper (f :+: g) where- cmap f (CL c) = CL (cmap f c)- cmap f (CR c) = CR (cmap f c)- fill (CL c) x = L (fill c x)- fill (CR c) y = R (fill c y)- first f (L x) = first (\z -> f z . CL) x- first f (R y) = first (\z -> f z . CR) y- last f (L x) = last (\z -> f z . CL) x- last f (R y) = last (\z -> f z . CR) y- next f (CL c) x = next (\z -> f z . CL) c x- next f (CR c) y = next (\z -> f z . CR) c y- prev f (CL c) x = prev (\z -> f z . CL) c x- prev f (CR c) y = prev (\z -> f z . CR) c y+instance (Zipper phi f, Zipper phi g) => Zipper phi (f :+: g) where+ cmapA f (CL c) = liftA CL (cmapA f c)+ cmapA f (CR c) = liftA CR (cmapA f c)+ fill p (CL c) x = L (fill p c x)+ fill p (CR c) y = R (fill p c y)+ first f (L x) = first (\p z -> f p z . CL) x+ first f (R y) = first (\p z -> f p z . CR) y+ last f (L x) = last (\p z -> f p z . CL) x+ last f (R y) = last (\p z -> f p z . CR) y+ next f p (CL c) x = next (\p z -> f p z . CL) p c x+ next f p (CR c) y = next (\p z -> f p z . CR) p c y+ prev f p (CL c) x = prev (\p z -> f p z . CL) p c x+ prev f p (CR c) y = prev (\p z -> f p z . CR) p c y -instance (Zipper f, Zipper g) => Zipper (f :*: g) where- cmap f (C1 c y) = C1 (cmap f c) (hmap f y)- cmap f (C2 x c) = C2 (hmap f x) (cmap f c)- fill (C1 c y) x = fill c x :*: y- fill (C2 x c) y = x :*: fill c y+instance (Zipper phi f, Zipper phi g) => Zipper phi (f :*: g) where+ cmapA f (C1 c y) = liftA2 C1 (cmapA f c) (hmapA f y)+ cmapA f (C2 x c) = liftA2 C2 (hmapA f x) (cmapA f c)+ fill p (C1 c y) x = fill p c x :*: y+ fill p (C2 x c) y = x :*: fill p c y first f (x :*: y) =- first (\z c -> f z (C1 c y )) x `mplus`- first (\z c -> f z (C2 x c )) y+ first (\p z c -> f p z (C1 c y )) x `mplus`+ first (\p z c -> f p z (C2 x c )) y last f (x :*: y) =- last (\z c -> f z (C2 x c )) y `mplus`- last (\z c -> f z (C1 c y )) x- next f (C1 c y) x =- next (\z c' -> f z (C1 c' y )) c x `mplus`- first (\z c' -> f z (C2 (fill c x) c')) y- next f (C2 x c) y =- next (\z c' -> f z (C2 x c')) c y- prev f (C1 c y) x =- prev (\z c' -> f z (C1 c' y )) c x-- prev f (C2 x c) y =- prev (\z c' -> f z (C2 x c')) c y `mplus`- last (\z c' -> f z (C1 c' (fill c y))) x+ last (\p z c -> f p z (C2 x c )) y `mplus`+ last (\p z c -> f p z (C1 c y )) x+ next f p (C1 c y) x =+ next (\p' z c' -> f p' z (C1 c' y )) p c x `mplus`+ first (\p' z c' -> f p' z (C2 (fill p c x) c')) y+ next f p (C2 x c) y =+ next (\p' z c' -> f p' z (C2 x c')) p c y+ prev f p (C1 c y) x =+ prev (\p' z c' -> f p' z (C1 c' y )) p c x+ prev f p (C2 x c) y =+ prev (\p' z c' -> f p' z (C2 x c')) p c y `mplus`+ last (\p' z c' -> f p' z (C1 c' (fill p c y))) x -instance Zipper f => Zipper (f :>: xi) where- cmap f (CTag prf c) = CTag prf (cmap f c)- fill (CTag prf c) x = castTag prf Tag (fill c x)- first f (Tag x) = first (\z -> f z . CTag Refl) x- last f (Tag x) = last (\z -> f z . CTag Refl) x- next f (CTag prf c) x = next (\z -> f z . CTag prf) c x- prev f (CTag prf c) x = prev (\z -> f z . CTag prf) c x+instance Zipper phi f => Zipper phi (f :>: xi) where+ cmapA f (CTag prf c) = liftA (CTag prf) (cmapA f c)+ fill p (CTag prf c) x = castTag prf Tag (fill p c x)+ first f (Tag x) = first (\p z -> f p z . CTag Refl) x+ last f (Tag x) = last (\p z -> f p z . CTag Refl) x+ next f p (CTag prf c) x = next (\p z -> f p z . CTag prf) p c x+ prev f p (CTag prf c) x = prev (\p z -> f p z . CTag prf) p c x -instance (Constructor c, Zipper f) => Zipper (C c f) where- cmap f (CC c) = CC (cmap f c)- fill (CC c) x = C (fill c x)- first f (C x) = first (\z -> f z . CC) x- last f (C x) = last (\z -> f z . CC) x- next f (CC c) x = next (\z -> f z . CC) c x- prev f (CC c) x = prev (\z -> f z . CC) c x+instance (Constructor c, Zipper phi f) => Zipper phi (C c f) where+ cmapA f (CC c) = liftA CC (cmapA f c)+ fill p (CC c) x = C (fill p c x)+ first f (C x) = first (\p z -> f p z . CC) x+ last f (C x) = last (\p z -> f p z . CC) x+ next f p (CC c) x = next (\p z -> f p z . CC) p c x+ prev f p (CC c) x = prev (\p z -> f p z . CC) p c x -- * Interface @@ -179,39 +190,39 @@ -- | Start navigating a datastructure. Returns a location that -- focuses the entire value and has an empty context.-enter :: (Ix s ix, Zipper (PF s)) => s ix -> ix -> Loc s I0 ix-enter _ x = Loc (I0 x) Empty+enter :: (Fam phi, Zipper phi (PF phi)) => phi ix -> ix -> Loc phi I0 ix+enter p x = Loc p (I0 x) Empty -- ** Navigation -- | Move down to the leftmost child. Returns 'Nothing' if the -- current focus is a leaf.-down :: Loc s I0 ix -> Maybe (Loc s I0 ix)+down :: Loc phi I0 ix -> Maybe (Loc phi I0 ix) -- | Move down to the rightmost child. Returns 'Nothing' if the -- current focus is a leaf.-down' :: Loc s I0 ix -> Maybe (Loc s I0 ix)+down' :: Loc phi I0 ix -> Maybe (Loc phi I0 ix) -- | Move up to the parent. Returns 'Nothing' if the current -- focus is the root.-up :: Loc s I0 ix -> Maybe (Loc s I0 ix)+up :: Loc phi I0 ix -> Maybe (Loc phi I0 ix) -- | Move to the right sibling. Returns 'Nothing' if the current -- focus is the rightmost sibling.-right :: Loc s r ix -> Maybe (Loc s r ix)+right :: Loc phi r ix -> Maybe (Loc phi r ix) -- | Move to the left sibling. Returns 'Nothing' if the current -- focus is the leftmost sibling.-left :: Loc s r ix -> Maybe (Loc s r ix)+left :: Loc phi r ix -> Maybe (Loc phi r ix) -down (Loc (I0 x) s ) = first (\z c -> Loc z (Push c s)) (from x)-down' (Loc (I0 x) s ) = last (\z c -> Loc z (Push c s)) (from x)-up (Loc x Empty ) = Nothing-up (Loc x (Push c s)) = return (Loc (I0 $ to (fill c x)) s)-right (Loc x Empty ) = Nothing-right (Loc x (Push c s)) = next (\z c' -> Loc z (Push c' s)) c x-left (Loc x Empty ) = Nothing-left (Loc x (Push c s)) = prev (\z c' -> Loc z (Push c' s)) c x+down (Loc p (I0 x) s ) = first (\p' z c -> Loc p' z (Push p c s)) (from p x)+down' (Loc p (I0 x) s ) = last (\p' z c -> Loc p' z (Push p c s)) (from p x)+up (Loc p x Empty ) = Nothing+up (Loc p x (Push p' c s)) = return (Loc p' (I0 $ to p' (fill p c x)) s)+right (Loc p x Empty ) = Nothing+right (Loc p x (Push p' c s)) = next (\p z c' -> Loc p z (Push p' c' s)) p c x+left (Loc p x Empty ) = Nothing+left (Loc p x (Push p' c s)) = prev (\p z c' -> Loc p z (Push p' c' s)) p c x -- ** Derived navigation. @@ -229,37 +240,37 @@ r -> r -- | Move through all positions in depth-first left-to-right order.-dfnext :: Loc s I0 ix -> Maybe (Loc s I0 ix)+dfnext :: Loc phi I0 ix -> Maybe (Loc phi I0 ix) dfnext = df down up right -- | Move through all positions in depth-first right-to-left order.-dfprev :: Loc s I0 ix -> Maybe (Loc s I0 ix)+dfprev :: Loc phi I0 ix -> Maybe (Loc phi I0 ix) dfprev = df down' up left -- ** Elimination -- | Return the entire value, independent of the current focus.-leave :: Loc s I0 ix -> ix-leave (Loc (I0 x) Empty) = x-leave loc = leave (fromJust (up loc))+leave :: Loc phi I0 ix -> ix+leave (Loc p (I0 x) Empty) = x+leave loc = leave (fromJust (up loc)) -- | Operate on the current focus. This function can be used to -- extract the current point of focus.-on :: (forall xi. Ix s xi => s xi -> r xi -> a) -> Loc s r ix -> a-on f (Loc x _) = f index x+on :: (forall xi. phi xi -> r xi -> a) -> Loc phi r ix -> a+on f (Loc p x _) = f p x -- | Update the current focus without changing its type.-update :: (forall xi. Ix s xi => s xi -> xi -> xi) -> Loc s I0 ix -> Loc s I0 ix-update f (Loc (I0 x) s) = Loc (I0 $ f index x) s+update :: (forall xi. phi xi -> xi -> xi) -> Loc phi I0 ix -> Loc phi I0 ix+update f (Loc p (I0 x) s) = Loc p (I0 $ f p x) s -- | Most general eliminator. Both 'on' and 'update' can be defined -- in terms of 'foldZipper'.-foldZipper :: (forall xi. Ix s xi => s xi -> xi -> r xi) -> Algebra s r -> Loc s I0 ix -> r ix-foldZipper f alg (Loc (I0 x) c) = cfold alg c (f index x)+foldZipper :: (forall xi. phi xi -> xi -> r xi) -> Algebra phi r -> Loc phi I0 ix -> r ix+foldZipper f alg (Loc p (I0 x) c) = cfold alg p c (f p x) where- cfold :: (Ix s b, Zipper (PF s)) => Algebra s r -> Ctxs s I0 a b -> r b -> r a- cfold alg Empty x = x- cfold alg (Push c s) x = cfold alg s (alg index (fill (cmap (\ _ (I0 x) -> fold alg x) c) x))+ cfold :: (Fam phi, Zipper phi (PF phi)) => Algebra phi r -> phi b -> Ctxs phi b I0 a -> r b -> r a+ cfold alg p' Empty x = x+ cfold alg p' (Push p c s) x = cfold alg p s (alg p (fill p' (hmap (\ p (I0 x) -> fold alg p x) c) x)) -- * Internal functions @@ -269,12 +280,12 @@ -- Helping the typechecker to apply equality proofs correctly ... castId :: (b :=: xi)- -> (Ix s xi => r xi -> I xi s r ix)- -> (Ix s b => r b -> I xi s r ix)+ -> (r xi -> I xi r ix)+ -> (r b -> I xi r ix) castTag :: (ix :=: xi)- -> (f s r ix -> (f :>: ix) s r ix)- -> (f s r ix -> (f :>: xi) s r ix)+ -> (f r ix -> (f :>: ix) r ix)+ -> (f r ix -> (f :>: xi) r ix) castId Refl f = f castTag Refl f = f
− src/Generics/MultiRec/Zipper/TEq.hs
@@ -1,28 +0,0 @@-{-# LANGUAGE GADTs #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TypeOperators #-}---------------------------------------------------------------------------------- |--- Module : Generics.MultiRec.Zipper.TEq--- Copyright : (c) 2008--2009 Universiteit Utrecht--- License : BSD3------ Maintainer : generics@haskell.org--- Stability : experimental--- Portability : non-portable------ Type-level equality. This is an internal module used by the--- zipper. The zipper cannot currently use GADTs combined with--- data families because GHC does not yet support this combination.----------------------------------------------------------------------------------module Generics.MultiRec.Zipper.TEq where--infix 4 :=:--data (:=:) :: * -> * -> * where- Refl :: a :=: a--cast :: a :=: b -> a -> b-cast Refl x = x
zipper.cabal view
@@ -1,5 +1,5 @@ name: zipper-version: 0.1+version: 0.2 license: BSD3 license-file: LICENSE author: Alexey Rodriguez,@@ -8,7 +8,7 @@ Johan Jeuring maintainer: generics@haskell.org category: Generics-synopsis: Generic zipper for systems of recursive datatypes+synopsis: Generic zipper for families of recursive datatypes homepage: http://www.cs.uu.nl/wiki/GenericProgramming/Multirec description: The Zipper is a data structure that allows typed navigation on a value.@@ -17,23 +17,22 @@ up, down, left or right in the value. The term that is in focus can also be modified. .- This library offers a generic Zipper for systems of datatypes. In particular,+ This library offers a generic Zipper for families of datatypes. In particular, it is possible to move the focus between subterms of different types, in an entirely type-safe way. This library is built on top of the multirec library,- so all that is required to get a Zipper for a datatype system is to instantiate- the multirec library for that system.+ so all that is required to get a Zipper for a datatype family is to instantiate+ the multirec library for that family. stability: experimental build-type: Simple cabal-version: >= 1.2.1-tested-with: GHC == 6.8.3, GHC == 6.10.1+tested-with: GHC == 6.8.3, GHC == 6.10.3 hs-source-dirs: src exposed-modules: Generics.MultiRec.Zipper-other-modules: Generics.MultiRec.Zipper.TEq extra-source-files: examples/AST.hs examples/ASTZipper.hs examples/ASTEditor.hs CREDITS-build-depends: base >= 3 && < 4,- multirec >= 0.1.5 && < 0.3+build-depends: base >= 3 && < 5,+ multirec >= 0.3 && < 0.4