pire-0.2.5

Copyright(c) Andreas Reuleaux 2015 - 2018
LicenseBSD2
MaintainerAndreas Reuleaux <rx@a-rx.info>
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Navigation

Description

navigation in the syntax tree by means of a lenses and a zipper.

concerning the examples / doctests below: one would typicall just call pp, eg.

pp $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= focus

however in this module, we are just defining navigation, PrettyNavigation building thereupon defines pretty printing for zippers then, and obviously we cannot import them here (cyclic deps).

thus no pp here yet, use the prism idioms (^.. _D) etc instead and then pretty print the decls/exprs..., eg.

(^. _Aa) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= focus

ie. nowhere here we rely on printing the zipper (defined in PrettyNavigation) we only print exprs/decls...

focusing on a zipper meanwhile yields a Term however (defined in Term), thus we might get by with importing PrettyTerm and using pp now.

Synopsis

Documentation

data Direction Source #

Constructors

Top 
Up 
Decl Int

Decl here as a constructor for Direction (not as the data type)

ToCDef Int

navigate to the i'th constructor def (in a data decl)

Sg String

signature

Df String

definition

Bndr Int 
Match' Int 
Arg' Int 
Binding 
Rhs 
Lhs 
Body 
Meat 
Instances
Eq Direction Source # 
Instance details

Defined in Navigation

Show Direction Source # 
Instance details

Defined in Navigation

type Zipper a = (Term a a, [Term a a -> Term a a]) Source #

md :: Module Text Text Source #

some sample modules

_decl :: Int -> Lens' (Module t a) (Decl t a) Source #

_rhs :: Lens' (Decl t a) (Expr t a) Source #

lens right hand side

for example

>>> :t (^. _rhs)
(^. _rhs) :: Decl t a -> Expr t a

_lhs :: Lens' (Decl t a) t Source #

_right :: Lens' (Expr t a) (Expr t a) Source #

_r :: Eq t => Lens' (Expr t t) (Expr t t) Source #

_left :: Lens' (Expr t a) (Expr t a) Source #

_match :: Int -> Lens' (Expr t a) (Match t a) Source #

_b :: Eq t => Lens' (Match t t) (Expr t t) Source #

_binder :: Int -> Lens' (Expr t a) t Source #

left_ :: Lens' (TT t a) (TT t a) Source #

right_ :: Lens' (TT t a) (TT t a) Source #

rhs_ :: Lens' (TT t a) (TT t a) Source #

decls_ :: Lens' (TT t a) (TT t a) Source #

cdefs_ :: Lens' (TT t a) (TT t a) Source #

eright :: Expr t a -> Lens' (TT t a) (TT t a) Source #

take a right turn, in context of an expression

eleft :: Expr t a -> Lens' (TT t a) (TT t a) Source #

take a left turn, in context of an expression

focus :: Refactoring m => (a, t) -> m a Source #

ezipper :: Term a a -> Either RefactorError (Zipper a) Source #

given a term t, ezipper t yields a zipper in the Either monad

type restricted here, to make it obvious that ezipper indeed creates a zipper

rzipper :: Monad m => a1 -> m (a1, [a2]) Source #

given a term t, rzipper t yields a zipper in our refactoring monad RE.

we have restricted its type here, to make it obvious that rzipper indeed creates a zipper

_snd :: Term t a -> TT t a Source #

_mod :: Term t a -> Module t a Source #

_dcl :: Term t a -> Decl t a Source #

_exp :: Term t a -> Expr t a Source #

toDecl :: Refactoring m => Int -> Zipper a -> m (Zipper a) Source #

toSig :: (Refactoring m, Eq a, IsString a) => String -> Zipper a -> m (Zipper a) Source #

toDef :: (Refactoring m, Eq a, IsString a) => String -> Zipper a -> m (Zipper a) Source #

toMatch :: Refactoring m => Int -> Zipper a -> m (Zipper a) Source #

toArg :: Refactoring m => Int -> Zipper a -> m (Zipper a) Source #

_beyondPosition_pair :: (Expr t a -> Expr t a, Expr t a) -> (Expr t a -> Expr t a, Expr t a) Source #

body :: (Eq a, Refactoring m) => Zipper a -> m (Zipper a) Source #

_rhspair :: Decl t1 t -> (Expr t1 a -> Decl t1 a, Expr t1 t) Source #

right :: (Eq a, Refactoring m) => Zipper a -> m (Zipper a) Source #

up :: Refactoring m => Zipper a -> m (Zipper a) Source #

top :: Refactoring m => Zipper a -> m (Zipper a) Source #

_binderpair :: Int -> Expr t a -> (t -> Expr t a, t) Source #

_bindingpair :: Expr t a -> (t -> Expr t a, t) Source #

binder :: Refactoring m => Int -> Zipper a -> m (Zipper a) Source #

go to the ith binder of a lambda

binding :: Refactoring m => Zipper a -> m (Zipper a) Source #

go to the binding of a lambda, pi-type, match, sigma etc

given eg a Pi type: (x:A) -> B, binding takes us to the (x, A) pair, ie we create an annotation Ann

lhspair :: Decl t a -> (t -> Decl t a, t) Source #

leftpair :: Expr t a -> (Expr t a -> Expr t a, Expr t a) Source #

left :: Refactoring m => Zipper a -> m (Zipper a) Source #

upToBinding' :: (Eq a, Refactoring m) => a -> Zipper a -> m (Zipper a) Source #

given a name and a zipper, go up to the binding of this name

upToBinding2 :: (Eq a, Refactoring m) => Zipper a -> m (a, Zipper a) Source #

like the above upToBinding', but even return the name v encountered thus make it possible to use renameZ' with the simpler ezipper like so:

module_ "pitestfiles/Nat.pi" >>= m -> return $ (ezipper $ M $ t2s m)  >>= lineColumn 21 3 >>= upToBinding2 >>= (old, z) -> renameZ old "predecessor" z

can still see where in the zipper upToBinding2 has taken us:

(this is in position 19 22, but navigation by line column number not available here yet):

>>> tst <- (runExceptT $ getModules ["samples"] "Test") >>= return . last . fromRight'
Parsing File "samples/Nat.pi"
Parsing File "samples/Sample.pi"
Parsing File "samples/Test.pi"
>>> head $ (^.. _E) $ fromRight' $ (ezipper $ M $ tst) >>= navigate [Decl 5, Rhs, Rhs, Rhs, Rhs, Rhs, Rhs, Meat] >>= focus
V "a"
>>> pp $ head $ (^.. _E) $ fromRight' $ (ezipper $ M $ tst) >>= navigate [Decl 5, Rhs, Rhs, Rhs, Rhs, Rhs, Rhs, Meat] >>= upToBinding2 >>= \(old, z) -> focus z
\a . x a

but this needs more care still: isBindingVar for Case/Case_

meat :: Refactoring m => Zipper a -> m (Zipper a) Source #

nav :: (Refactoring m, Eq a, IsString a) => Direction -> Zipper a -> m (Zipper a) Source #

navigate :: (Refactoring m, Eq a, IsString a) => [Direction] -> Zipper a -> m (Term a a, [Term a a -> Term a a]) Source #