Copyright | (c) Andreas Reuleaux 2015 |
---|---|

License | BSD2 |

Maintainer | Andreas Reuleaux <rx@a-rx.info> |

Stability | experimental |

Portability | non-portable |

Safe Haskell | None |

Language | Haskell2010 |

allow for wrapping (unwrapping) bound variables in scopes with their textual representations, this is a temporary adjustment for calculating position information

# Documentation

`>>>`

Node [Pair (Token "\") (Ws " ") ,Node [Pair (Binder "x") (Ws " ")] ,Pair (Token ".") (Ws " ") ,Abstract ["x"] (Scope (Pair (Pair (Id (B 0)) (Ws " ")) (Pair (Id (F (Id "a"))) (Ws ""))))]`prettyPrint $ snd $ nopos $ parse expr_ "\\ x . x a"`

see how the bound variable `x`

in the scope gets wrapped with its textual representation, ie. `B 0`

above becomes `Bnd "x" (Id (B 0)))`

`>>>`

Node [Pair (Token "\") (Ws " ") ,Node [Pair (Binder "x") (Ws " ")] ,Pair (Token ".") (Ws " ") ,Abstract_ (Scope (Pair (Pair (Bnd "x" (Id (B 0))) (Ws " ")) (Pair (Id (F (Id "a"))) (Ws ""))))]`prettyPrint $ wrap $ snd $ nopos $ parse expr_ "\\ x . x a"`

wrap $ nopos $ parse expr_ "\ x . x a" LamPAs_ (LamTok "\" (Ws " ")) [(RuntimeP,Binder_ "x" (Ws " "),Annot_ Nothing (Ws ""))] (Dot "." (Ws " ")) (Scope (Ws_ (BndV "x" (V (B 0))) (Ws " ") :@ Ws_ (V (F (V "a"))) (Ws "")))

wrap $ nopos $ parse expr_ "\yy . a (\a . x a)"
LamPAs_ (LamTok "\" (Ws "")) [(RuntimeP,Binder_ "yy" (Ws " "),Annot_ Nothing (Ws ""))] (Dot "." (Ws " ")) (Scope (Ws_ (V (F (V "a"))) (Ws " ") :` Paren_ (ParenOpen "(" (Ws "")) (LamPAs_ (LamTok "\" (Ws "")) [(RuntimeP,Binder_ "a" (Ws " "),Annot_ Nothing (Ws ""))] (Dot "." (Ws " ")) (Scope (Ws_ (V (F (V (F (V "x"))))) (Ws " ") :`

Ws_ (BndV "a" (V (B 0))) (Ws "")))) (ParenClose ")" (Ws ""))))

wrapping of PiP - expr first

wrap $ nopos $ parse expr "(x:A) -> B x" PiP RuntimeP "x" (V A) (Scope (V (F (V B)) :@ BndV "x" (V (B ()))))

now w/ expr_, that's more interesting

wrap $ nopos $ parse expr_ "A -> B" PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V A) (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V B))) (Ws "")))

unwrap $ wrap $ nopos $ parse expr_ "A -> B" PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V A) (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V B))) (Ws ""))) >>>

wrap $ nopos $ parse expr_ "(x:A) -> B x" PiP_ RuntimeP (Ann_ (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnnBnd_ (Binder_ "x" (Ws "")) (Colon ":" (Ws "")) (Ws_ (V A) (Ws ""))) (ParenClose ")" (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V B))) (Ws " ") :@ Ws_ (BndV "x" (V (B ()))) (Ws "")))

unwrap $ wrap $ nopos $ parse expr_ "(x:A) -> B x" PiP_ RuntimeP (Ann_ (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnnBnd_ (Binder_ "x" (Ws "")) (Colon ":" (Ws "")) (Ws_ (V A) (Ws ""))) (ParenClose ")" (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V B))) (Ws " ") :@ Ws_ (V (B ())) (Ws "")))

wrap $ nopos $ parse expr_ "(B -> C) -> A" PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 1) (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (InvisibleBinder 0) (Ws_ (V B) (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V C))) (Ws "")))) (ParenClose ")" (Ws " "))))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V A))) (Ws ""))) >>>