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 |

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

## Synopsis

- isBindingVarIn :: (Eq a, Show a, Pretty (Expr a a)) => a -> Expr a a -> Bool
- isBindingVarInMatch :: (Eq a, Show a, Pretty (Expr a a)) => a -> Match a a -> Bool
- renameExpr :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Expr a a -> RE (Expr a a)
- renameDecl :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Decl a a -> RE (Decl a a)
- renameTele :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Telescope a a -> RE (Telescope a a)
- renameConstructorDef :: Eq d => d -> d -> ConstructorDef d d -> ConstructorDef d d
- renameMatch :: Eq d => d -> d -> Match d d -> Match d d
- renameZ :: (Eq a, Show a, Pretty a, Pretty (Expr a a)) => a -> a -> Zipper a -> RE (Zipper a)

# Documentation

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

: see, if `isBindingVarIn`

x e`x`

is a binding variable in `e`

(used in

)`renameExpr`

`>>>`

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

`>>>`

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

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`

`>>>`

False`"y" `isBindingVarIn` c`

OK?

`>>>`

False`"Succ" `isBindingVarIn` c`

`>>>`

True`"n'" `isBindingVarIn` c`

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:

renames `renameExpr`

old new e`old`

to `new`

in `e`

.

`>>>`

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

or explicitly in the `RE`

monad:

`>>>`

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

name capture are detected, and renaming then rejected:

`>>>`

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

`>>>`

Left_ (NameCaptureBindingVar "y" "\\y . x")`renameExpr "x" "y" $ lam "y" $ V "x"`

now try several renamings, for example lambda `l`

:

`>>>`

`let l = lam "a" $ lam "b" $ lam "c" $ lam "y" $ V "x"`

`>>>`

\a . \b . \c . \y . x`pp l`

renaming has no effect if `y`

is *bound*

`>>>`

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

and works fine if `x`

is *free*

`>>>`

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

further examples of name capture:

detect name capture deep down inside:

`>>>`

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

another example:

`>>>`

`let l' = lam "a" $ V "foo" :@ (lam "c" $ V "a" :@ V "c")`

`>>>`

\a . foo (\c . a c)`pp l'`

`>>>`

Left_ (NameCaptureBindingVar "c" "\\a . foo (\\c . a c)")`renameExpr "a" "c" $ l'`

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

`>>>`

`let l = nopos $ t2s $ parse expr "\\a b . \\c . \\y . x"`

`>>>`

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"))))))))))))`ppr l`

`>>>`

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

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

renaming declarations:

renames `renameDecl`

old new d`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:

renames `renameTele`

old new t`old`

to `new`

in `t`

.

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

renaming constructor definitions