zipper (empty) → 0.1
raw patch · 9 files changed
+536/−0 lines, 9 filesdep +basedep +multirecsetup-changed
Dependencies added: base, multirec
Files
- CREDITS +21/−0
- LICENSE +27/−0
- Setup.hs +3/−0
- examples/AST.hs +30/−0
- examples/ASTEditor.hs +72/−0
- examples/ASTZipper.hs +36/−0
- src/Generics/MultiRec/Zipper.hs +280/−0
- src/Generics/MultiRec/Zipper/TEq.hs +28/−0
- zipper.cabal +39/−0
+ CREDITS view
@@ -0,0 +1,21 @@++Credits for zipper+==================++This is a list of those who have contributed to the research, concept, code,+and/or other issues of the zipper library.++Research and Code+-----------------++* Alexey Rodriguez+* Stefan Holdermans+* Andres Löh+* Johan Jeuring++Ideas and Support+-----------------++* Thomas van Noort+* Sean Leather+* José Pedro Magalhães
+ LICENSE view
@@ -0,0 +1,27 @@+Copyright (c) 2008--2009 Universiteit Utrecht++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. Neither the name of the author nor the names of his contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE+ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT+LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY+OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF+SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,3 @@+import Distribution.Simple++main = defaultMain
+ examples/AST.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE EmptyDataDecls #-}++module AST where++import Generics.MultiRec.Base++-- * The AST type from the paper++infix 1 :=++data Expr = Const Int+ | Add Expr Expr+ | Mul Expr Expr+ | EVar Var+ | Let Decl Expr+ deriving Show++data Decl = Var := Expr+ | Seq Decl Decl+ | None+ deriving Show++type Var = String+
+ examples/ASTEditor.hs view
@@ -0,0 +1,72 @@+{-# LANGUAGE FlexibleContexts #-}++module Main where++-- This is currently more a navigator than an editor, because+-- there is no way to update the value yet.+-- Also, the implementation uses ugly non-portable ANSI escape codes+-- at the moment.++import AST+import ASTUse++import Generics.MultiRec.Base+import Generics.MultiRec.Zipper+import Generics.MultiRec.Show as GS++import System.IO+import Control.Monad++main :: IO ()+main = startEditor++-- | Call this to start the navigation demo.+startEditor :: IO ()+startEditor = + do+ intro+ hSetBuffering stdin NoBuffering+ loop $ enter Expr example++example = Let (Seq (Seq ("x" := Mul (Const 6) (Const 9)) ("y" := Const (-12))) None)+ (Add (EVar "x") (EVar "y"))++-- | 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+ 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+ focus Expr _ = "expression"+ focus Decl _ = "declaration"+ focus Var _ = "variable"++-- | Main loop. Prints current location, asks for a command and executes+-- a navigation operation depending on that command.+loop :: Loc AST I0 Expr -> IO ()+loop l =+ do+ putStr $ (showZipper l) ++ " {" ++ typeOfFocus l ++ "}"+ cmd <- getChar+ putStr "\r\ESC[2K"+ when (cmd == 'q') $ putStrLn ""+ when (cmd /= 'q') $ do+ let op = case cmd of+ 'j' -> down+ 'l' -> right+ 'h' -> left+ 'k' -> up+ ' ' -> dfnext+ '\b' -> dfprev+ _ -> return+ case op l of+ Nothing -> loop l+ Just l' -> loop l'++-- | 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"
+ examples/ASTZipper.hs view
@@ -0,0 +1,36 @@+{-# LANGUAGE FlexibleContexts #-}++module ASTZipper where++import Data.Maybe (fromJust)+import Control.Arrow ((>>>))+import Control.Monad ((>=>))++import AST+import ASTUse++import Generics.MultiRec.Zipper++-- | Example expression++example = Let ("x" := Mul (Const 6) (Const 9))+ (Add (EVar "x") (EVar "y"))++-- | Test for the generic zipper++testZipper :: Maybe Expr+testZipper =+ enter Expr >>>+ down >=>+ down >=>+ right >=>+ update solve >>>+ leave >>>+ return $ example+ where+ solve :: AST ix -> ix -> ix+ solve Expr _ = Const 42+ solve _ x = x+++
+ src/Generics/MultiRec/Zipper.hs view
@@ -0,0 +1,280 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++-----------------------------------------------------------------------------+-- |+-- Module : Generics.MultiRec.Zipper+-- Copyright : (c) 2008--2009 Universiteit Utrecht+-- License : BSD3+--+-- Maintainer : generics@haskell.org+-- Stability : experimental+-- Portability : non-portable+--+--+-- The generic zipper.+--+-----------------------------------------------------------------------------++module Generics.MultiRec.Zipper+ (-- * Locations+ Loc(),+ -- * Context frames+ Ctx(),+ -- * Generic zipper class+ Zipper(..),+ -- * Interface+ enter,+ down, down', up, right, left,+ dfnext, dfprev,+ leave, on, update, foldZipper+ ) where++import Prelude hiding (last)++import Control.Monad+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+-- 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++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++-- * Context frames++-- | Abstract type of context frames. Not required for the high-level+-- navigation functions.++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)++-- 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)++-- * Generic navigation functions++-- | It is in general not necessary to use the generic navigation+-- functions directly. The functions listed in the ``Interface'' section+-- 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++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 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 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 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 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+ first f (x :*: y) =+ first (\z c -> f z (C1 c y )) x `mplus`+ first (\z c -> f 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++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 (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++-- * Interface++-- ** Introduction++-- | 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++-- ** 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)++-- | 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)++-- | Move up to the parent. Returns 'Nothing' if the current+-- focus is the root.+up :: Loc s I0 ix -> Maybe (Loc s 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)++-- | 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)++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++-- ** Derived navigation.++df :: (a -> Maybe a) -> (a -> Maybe a) -> (a -> Maybe a) -> a -> Maybe a+df d u lr l =+ case d l of+ Nothing -> df' l+ r -> r+ where+ df' l =+ case lr l of+ Nothing -> case u l of+ Nothing -> Nothing+ Just l' -> df' l'+ r -> r++-- | Move through all positions in depth-first left-to-right order.+dfnext :: Loc s I0 ix -> Maybe (Loc s 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 = 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))++-- | 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++-- | 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++-- | 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)+ 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))++-- * Internal functions++impossible :: a -> b+impossible x = error "impossible"++-- 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)++castTag :: (ix :=: xi)+ -> (f s r ix -> (f :>: ix) s r ix)+ -> (f s r ix -> (f :>: xi) s r ix)++castId Refl f = f+castTag Refl f = f
+ src/Generics/MultiRec/Zipper/TEq.hs view
@@ -0,0 +1,28 @@+{-# 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
@@ -0,0 +1,39 @@+name: zipper+version: 0.1+license: BSD3+license-file: LICENSE+author: Alexey Rodriguez,+ Stefan Holdermans,+ Andres Löh,+ Johan Jeuring+maintainer: generics@haskell.org+category: Generics+synopsis: Generic zipper for systems 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.+ It maintains a subterm as a current point of focus. The rest of the value+ is the context. Focus and context are automatically updated when navigating+ 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,+ 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.+ +stability: experimental+build-type: Simple+cabal-version: >= 1.2.1+tested-with: GHC == 6.8.3, GHC == 6.10.1+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