Copyright | (c) Andreas Reuleaux 2015 - 2018 |
---|---|

License | BSD2 |

Maintainer | Andreas Reuleaux <rx@a-rx.info> |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

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

- type Path = [Direction]
- data Direction
- type Zipper a = (Term a a, [Term a a -> Term a a])
- md :: Module Text Text
- sampleM :: Module Text Text
- _decl :: Int -> Lens' (Module t a) (Decl t a)
- _rhs :: Lens' (Decl t a) (Expr t a)
- _lhs :: Lens' (Decl t a) t
- _cdef :: Int -> Lens' (Decl t a) (ConstructorDef t a)
- _right :: Lens' (Expr t a) (Expr t a)
- _r :: Eq t => Lens' (Expr t t) (Expr t t)
- _left :: Lens' (Expr t a) (Expr t a)
- _match :: Int -> Lens' (Expr t a) (Match t a)
- _b :: Eq t => Lens' (Match t t) (Expr t t)
- _binder :: Int -> Lens' (Expr t a) t
- left_ :: Lens' (TT t a) (TT t a)
- right_ :: Lens' (TT t a) (TT t a)
- rhs_ :: Lens' (TT t a) (TT t a)
- decls_ :: Lens' (TT t a) (TT t a)
- cdefs_ :: Lens' (TT t a) (TT t a)
- eright :: Expr t a -> Lens' (TT t a) (TT t a)
- eleft :: Expr t a -> Lens' (TT t a) (TT t a)
- focus :: Refactoring m => (a, t) -> m a
- ezipper :: Term a a -> Either RefactorError (Zipper a)
- rzipper :: Monad m => a1 -> m (a1, [a2])
- _snd :: Term t a -> TT t a
- _mod :: Term t a -> Module t a
- _dcl :: Term t a -> Decl t a
- _exp :: Term t a -> Expr t a
- toDecl :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- toSig :: (Refactoring m, Eq a, IsString a) => String -> Zipper a -> m (Zipper a)
- toDef :: (Refactoring m, Eq a, IsString a) => String -> Zipper a -> m (Zipper a)
- toMatch :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- toArg :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- toConstructorDef :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- _beyondPosition_pair :: (Expr t a -> Expr t a, Expr t a) -> (Expr t a -> Expr t a, Expr t a)
- beyondPosition :: Refactoring m => Zipper a -> m (Zipper a)
- body :: (Eq a, Refactoring m) => Zipper a -> m (Zipper a)
- _rhspair :: Decl t1 t -> (Expr t1 a -> Decl t1 a, Expr t1 t)
- right :: (Eq a, Refactoring m) => Zipper a -> m (Zipper a)
- up :: Refactoring m => Zipper a -> m (Zipper a)
- top :: Refactoring m => Zipper a -> m (Zipper a)
- _binderpair :: Int -> Expr t a -> (t -> Expr t a, t)
- _bindingpair :: Expr t a -> (t -> Expr t a, t)
- binder :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- binding :: Refactoring m => Zipper a -> m (Zipper a)
- lhspair :: Decl t a -> (t -> Decl t a, t)
- leftpair :: Expr t a -> (Expr t a -> Expr t a, Expr t a)
- left :: Refactoring m => Zipper a -> m (Zipper a)
- upToBinding' :: (Eq a, Refactoring m) => a -> Zipper a -> m (Zipper a)
- upToBinding2 :: (Eq a, Refactoring m) => Zipper a -> m (a, Zipper a)
- meat :: Refactoring m => Zipper a -> m (Zipper a)
- upToBinding :: Refactoring m => Zipper a -> m (Zipper a)
- nav :: (Refactoring m, Eq a, IsString a) => Direction -> Zipper a -> m (Zipper a)
- navigate :: (Refactoring m, Eq a, IsString a) => [Direction] -> Zipper a -> m (Term a a, [Term a a -> Term a a])

# Documentation

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

lens right hand side

for example

`>>>`

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

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

take a right turn, in context of an expression

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

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

given a term `t`

,

yields a zipper in our refactoring monad `rzipper`

t

.`RE`

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

toConstructorDef :: 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 #

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

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

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

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):

`>>>`

Parsing File "samples/Nat.pi" Parsing File "samples/Sample.pi" Parsing File "samples/Test.pi"`tst <- (runExceptT $ getModules ["samples"] "Test") >>= return . last . fromRight'`

`>>>`

V "a"`head $ (^.. _E) $ fromRight' $ (ezipper $ M $ tst) >>= navigate [Decl 5, Rhs, Rhs, Rhs, Rhs, Rhs, Rhs, Meat] >>= focus`

`>>>`

\a . x a`pp $ head $ (^.. _E) $ fromRight' $ (ezipper $ M $ tst) >>= navigate [Decl 5, Rhs, Rhs, Rhs, Rhs, Rhs, Rhs, Meat] >>= upToBinding2 >>= \(old, z) -> focus z`

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

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