pire-0.2.5

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

Renaming

Description

basic refactorings: renaming, built upon the zipper navigation in the syntax tree

Synopsis

Documentation

isBindingVarIn :: (Eq a, Show a, Pretty (Expr a a)) => a -> Expr a a -> Bool Source #

isBindingVarIn x e : see, if x is a binding variable in e (used in renameExpr)

>>> "x" `isBindingVarIn` (lam "x" $ V "y")
True
>>> "y" `isBindingVarIn` (lam "x" $ V "y")
False

The next example seems fine to me, let c be a case expression (cf. samples/Nat.pi):

case n of
  Zero -> Zero
  Succ n' -> n'
>>> let c = Case (V "n") [Match (PatCon "Zero" []) (Scope (DCon "Zero" [] Nothing)),Match (PatCon "Succ" [(RuntimeP, PatVar "n'")]) (Scope (V (B 0)))] Nothing
>>> "y" `isBindingVarIn` c
False

OK?

>>> "Succ" `isBindingVarIn` c
False
>>> "n'" `isBindingVarIn` c
True

test coverage is maybe not exhaustive enough: think eg. of some case, where we would have to recurse into the rhs of a match: Zero -> \x. n, ie. recurse into the lambda: \x. n then, etc.)

isBindingVarInMatch :: (Eq a, Show a, Pretty (Expr a a)) => a -> Match a a -> Bool Source #

helper function, for the above isBindingVarIn

renameExpr :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Expr a a -> RE (Expr a a) Source #

renaming expressions: renameExpr old new e renames old to new in e.

>>> renameExpr "x" "z" $ lam "y" $ V "x"
Re (Lam "y" Nothing (Scope (V (F (V "z")))))

or explicitly in the RE monad:

>>> (pure $ lam "y" $ V "x") >>= renameExpr "x" "z"
Re (Lam "y" Nothing (Scope (V (F (V "z")))))

name capture are detected, and renaming then rejected:

>>> renameExpr "a" "x" $ lam "y" $ V "x"
Left_ (NameCaptureFV "x" "\\y . x")
>>> renameExpr "x" "y" $ lam "y" $ V "x"
Left_ (NameCaptureBindingVar "y" "\\y . x")

now try several renamings, for example lambda l:

>>> let l = lam "a" $ lam "b" $ lam "c" $ lam "y" $ V "x"
>>> pp l
\a . \b . \c . \y . x

renaming has no effect if y is bound

>>> pp $ fromRe $ renameExpr "y" "YY" $ l
\a . \b . \c . \y . x

and works fine if x is free

>>> pp $ fromRe $ renameExpr "x" "zzz" $ l
\a . \b . \c . \y . zzz

further examples of name capture:

detect name capture deep down inside:

>>> renameExpr "x" "b" $ l
Left_ (NameCaptureBindingVar "b" "\\a . \\b . \\c . \\y . x")

another example:

>>> let l' = lam "a" $ V "foo" :@ (lam "c" $ V "a" :@ V "c")
>>> pp l'
\a . foo (\c . a c)
>>> renameExpr "a" "c" $ l'
Left_ (NameCaptureBindingVar "c" "\\a . foo (\\c . a c)")

and similar to the above example, but parsed and not desugared: LamPAs

>>> let l = nopos $ t2s $ parse expr "\\a b . \\c . \\y . x"
>>> ppr l
LamPAs [(RuntimeP,"a",Nothing),(RuntimeP,"b",Nothing)]
       (Scope (LamPAs [(RuntimeP,"c",Nothing)]
                      (Scope (LamPAs [(RuntimeP,"y",Nothing)]
                                     (Scope (V (F (V (F (V (F (V "x"))))))))))))
>>> renameExpr "a" "c" $ l
Left_ (NameCaptureBindingVar "c" "\\a b . \\c . \\y . x")

renameDecl :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Decl a a -> RE (Decl a a) Source #

renaming declarations: renameDecl old new d renames old to new in d.

renameTele :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Telescope a a -> RE (Telescope a a) Source #

renaming telescopes: renameTele old new t renames old to new in t.

renameConstructorDef :: Eq d => d -> d -> ConstructorDef d d -> ConstructorDef d d Source #

renaming constructor definitions

renameMatch :: Eq d => d -> d -> Match d d -> Match d d Source #

renaming matches

renameZ :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Zipper a -> RE (Zipper a) Source #