pire-0.2.5

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

OldNavigation

Description

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

Documentation

data Direction Source #

Constructors

Top 
Up 
Decl Int

Decl here as a constructor for a 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 OldNavigation

Show Direction Source # 
Instance details

Defined in OldNavigation

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

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

eg.

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

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

_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 #

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

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

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

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

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 :: Term a a -> RE (Zipper a) 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

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

body :: (Eq a, Refactoring m) => Zipper a -> m (Zipper a) 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 #

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

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 #

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

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 #