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 Pire's syntax tree with a zipper.

Navigation is mostly the about the zipper, but functions (lenses) of more general use are defined along the way.

## Synopsis

- type Path = [Direction]
- data Direction
- type Zipper a = (Term a a, [Term a a -> Term a a])
- _rhs :: Lens' (Decl t a) (Expr t a)
- _rhspair :: Decl t a -> (Expr t a -> Decl t a, Expr t a)
- _lhs :: Lens' (Decl t a) t
- _right :: Lens' (Expr t a) (Expr t a)
- _r :: Eq t => Lens' (Expr t t) (Expr t t)
- _b :: Eq t => Lens' (Match t t) (Expr t t)
- _match :: Int -> Lens' (Expr t a) (Match t a)
- _binder :: Int -> Lens' (Expr t a) t
- _dtele :: Lens' (Decl t a) (Telescope t a)
- _cdef :: Int -> Lens' (Decl t a) (ConstructorDef t a)
- _tele :: Lens' (ConstructorDef t a) (Telescope t a)
- _left :: Lens' (Expr t a) (Expr t a)
- focus :: Refactoring m => (a, t) -> m a
- ezipper :: Term a a -> Either RefactorError (Zipper a)
- rzipper :: Term a a -> RE (Zipper a)
- toDecl :: Refactoring m => Int -> Zipper a -> m (Zipper a)
- toSig :: (Refactoring m, Eq a, IsString a) => String -> Zipper a -> m (Zipper a)
- toDef :: (Monad m, IsString t, Eq t, Eq a) => String -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t a])
- toMatch :: Refactoring m => Int -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t a])
- toArg :: Monad m => Int -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t 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)
- 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

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

toDef :: (Monad m, IsString t, Eq t, Eq a) => String -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t a]) Source #

toMatch :: Refactoring m => Int -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t a]) Source #

toArg :: Monad m => Int -> (Term t a, [Term t a -> Term t a]) -> m (Term t a, [Term t a -> Term t 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, i.e. we create an annotation Ann

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

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

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