diff --git a/CREDITS b/CREDITS new file mode 100644 --- /dev/null +++ b/CREDITS @@ -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 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +import Distribution.Simple + +main = defaultMain diff --git a/examples/AST.hs b/examples/AST.hs new file mode 100644 --- /dev/null +++ b/examples/AST.hs @@ -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 + diff --git a/examples/ASTEditor.hs b/examples/ASTEditor.hs new file mode 100644 --- /dev/null +++ b/examples/ASTEditor.hs @@ -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" diff --git a/examples/ASTZipper.hs b/examples/ASTZipper.hs new file mode 100644 --- /dev/null +++ b/examples/ASTZipper.hs @@ -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 + + + diff --git a/src/Generics/MultiRec/Zipper.hs b/src/Generics/MultiRec/Zipper.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MultiRec/Zipper.hs @@ -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 diff --git a/src/Generics/MultiRec/Zipper/TEq.hs b/src/Generics/MultiRec/Zipper/TEq.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MultiRec/Zipper/TEq.hs @@ -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 diff --git a/zipper.cabal b/zipper.cabal new file mode 100644 --- /dev/null +++ b/zipper.cabal @@ -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