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 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.

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 (^.. _Dcl) 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.

sample usage, sample module md:

>>> pp $ head $ (^.. _Mod) $ fromRight' $ (ezipper $ Mod md) >>= focus
module Main where
a = \x . 2
b = \x [y] z . x 2
k = \x . frec x
f = \x . a x
g = \x . c x
hh = \yy . a (\a . x a)
j = \y . a (\a . x (\a . a))
frec = \y . frec (\a . x (\a . a))
>>> pp $ head $ (^.. _Dcl) $ fromRight' $ (ezipper $ Mod md) >>= toDecl 3 >>= focus
f = \x . a x
>>> pp $ head $ (^.. _Dcl) $ fromRight' $ refactor $ (rzipper $ Mod md) >>= toDecl 3 >>= focus
f = \x . a x
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod md) >>= toDecl 3 >>= right >>= focus
\x . a x
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod md) >>= toDecl 3 >>= right >>= body >>= focus
a x
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod md) >>= toDecl 3 >>= right >>= body >>= left >>= focus
a
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 3, Rhs, Body, Lhs] >>= focus
a

parsed as an absy:

>>> tst' <- (runExceptT $ getModules ["samples"] "Test") >>= return . last . fromRight'
Parsing File "samples/Nat.pi"
Parsing File "samples/Sample.pi"
Parsing File "samples/Test.pi"
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod tst') >>= navigate [Decl 3, Rhs, Body, Lhs] >>= focus
a

Synopsis

Documentation

md :: Module Text Text Source #

sample module, for experimenting w/ navigation:

data RefactorState t Source #

Constructors

RS 

Fields

newtype Refactor t a Source #

Instances

MonadError RefactorError (Refactor t) Source # 
Monad (Refactor t) Source # 

Methods

(>>=) :: Refactor t a -> (a -> Refactor t b) -> Refactor t b #

(>>) :: Refactor t a -> Refactor t b -> Refactor t b #

return :: a -> Refactor t a #

fail :: String -> Refactor t a #

Functor (Refactor t) Source # 

Methods

fmap :: (a -> b) -> Refactor t a -> Refactor t b #

(<$) :: a -> Refactor t b -> Refactor t a #

Applicative (Refactor t) Source # 

Methods

pure :: a -> Refactor t a #

(<*>) :: Refactor t (a -> b) -> Refactor t a -> Refactor t b #

liftA2 :: (a -> b -> c) -> Refactor t a -> Refactor t b -> Refactor t c #

(*>) :: Refactor t a -> Refactor t b -> Refactor t b #

(<*) :: Refactor t a -> Refactor t b -> Refactor t a #

Refactoring (Refactor t) Source # 
MonadState (RefactorState t) (Refactor t) Source # 

Methods

get :: Refactor t (RefactorState t) #

put :: RefactorState t -> Refactor t () #

state :: (RefactorState t -> (a, RefactorState t)) -> Refactor t a #

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

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

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

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

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

rzipper :: Term a a -> Refactor t (Zipper a) Source #

given a term t, rzipper t yields a zipper in the Refactor monad (with state ie.)

rzipper's most general type (according to its implementation) would be

rzipper :: t' -> Refactor t (t', [a])

and that would do as well, but we have restricted its type here, to make it more obvious that rzipper indeed creates a zipper

_fst :: Term t a -> Term t a Source #

try to make use of Tree t a instead of Tr t a pb however:

cannot use Exp_ (Expr t a, TT t a)

w/ deriveEq1 etc (a inly in the last pos)

solution:

Exp_ (Expr t a) (TT t a)

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

_to :: String -> Lens' (TT t a) (TT t a) Source #

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

eto :: String -> Expr t a -> Lens' (TT t a) (TT 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 #

_match :: Int -> Lens' (Expr t a) (Match t 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 #

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

eg.

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

_rhspair :: Decl t1 t -> (Expr t1 a -> Decl t1 a, Expr t1 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 #

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 #

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

>>> (^. _Ide) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= focus
"x"
>>> (^. _Ide) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 1] >>= focus
"y"
>>> (^. _Ide) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 2] >>= focus
"z"

can go up of course, at any point

>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0, Up] >>= focus
\x [y] z . x 2

(and these examples should work the same the the parsed modules mm, mm' as above)

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

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

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

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

_left :: Lens' (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

>>> (^. _Ide) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= focus
"x"
>>> pp $ head $ (^.. _Exp) $ fromRight' $ (ezipper $ Mod $ t2s md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= upToBinding' "x" >>= focus
\x [y] z . x 2
>>> pp $ head $ (^.. _Mod) $ fromRight' $ (ezipper $ Mod $ t2s md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= upToBinding' "a" >>= focus
module Main where
a = \x . 2
b = \x [y] z . x 2
k = \x . frec x
f = \x . a x
g = \x . c x
hh = \yy . a (\a . x a)
j = \y . a (\a . x (\a . a))
frec = \y . frec (\a . x (\a . a))

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 $ Mod $ 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 $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ tst) >>= navigate [Decl 5, Rhs, Rhs, Rhs, Rhs, Rhs, Rhs, Meat] >>= focus
V "a"
>>> pp $ head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ 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 #

upToBinding :: (Eq t, MonadState (RefactorState t) m, Refactoring m) => Zipper t -> m (Zipper t) Source #

this version of upToBinding takes one parameter less, but needs MonadState, as it records the name found in the state

>>> (^. _Ide) $ fromRight' $ (ezipper $ Mod md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= focus
"x"
>>> pp $ head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 1, Rhs, Bndr 0] >>= upToBinding >>= focus
\x [y] z . x 2

we are now going to look at the a found [Decl 5, Rhs, Body, Lhs], walking down there step by step first (to not loose our sense of orientation :-))

>>> pp $ head $ (^.. _Dcl) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 5] >>= focus
hh = \yy . a (\a . x a)
>>> pp $ head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 5, Rhs] >>= focus
\yy . a (\a . x a)
>>> pp $ head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 5, Rhs, Body] >>= focus
a (\a . x a)
>>> pp $ head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 5, Rhs, Body, Lhs] >>= focus
a
>>> pp $ head $ (^.. _Mod) $ fromRight' $ refactor $ (rzipper $ Mod $ md) >>= navigate [Decl 5, Rhs, Body, Lhs] >>= upToBinding >>= focus
module Main where
a = \x . 2
b = \x [y] z . x 2
k = \x . frec x
f = \x . a x
g = \x . c x
hh = \yy . a (\a . x a)
j = \y . a (\a . x (\a . a))
frec = \y . frec (\a . x (\a . a))

these should work as well:

module parsed in white space aware manner

>>> tst <- (runExceptT $ getModules ["samples"] "Test") >>= return . last . fromRight'
Parsing File "samples/Nat.pi"
Parsing File "samples/Sample.pi"
Parsing File "samples/Test.pi"
>>> head $ (^.. _Exp) $ fromRight' $ refactor $ (rzipper $ Mod $ tst) >>= navigate [Decl 5, Rhs, Body, Lhs] >>= focus
V "a"

and this should take us up to the module level (output omitted here):

>>> pp $ head $ (^.. _Mod) $ fromRight' $ refactor $ (rzipper $ Mod $ tst) >>= navigate [Decl 5, Rhs, Body, Lhs] >>= upToBinding >>= focus
...

further examples in LineColumn Navigation

without parsing a complete module

>>> fromRight' $ (ezipper $ Exp $ nopos $ parse expr "(x:A) -> B") >>= navigate [Binding]
(Exp (Ann (V "x") (V "A")),[Term... -> Term...])

etc

requires MonadState (RefactorState t) m (among others)

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 
Df String 
Bndr Int 
Match' Int 
Arg' Int 
Binding 
Rhs 
Lhs 
Body 
Meat 

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

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