pire-0.2.5

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

Wrap

Description

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

Synopsis

Documentation

class Wrap a where Source #

>>> prettyPrint $ snd $ nopos $ parse expr_ "\\  x . x  a"
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 ""))))]

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

>>> prettyPrint $ wrap $ snd $ nopos $ parse expr_ "\\  x . x  a"
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 ""))))]

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 ""))) >>>

Minimal complete definition

wrap

Methods

wrap :: a -> a Source #

Instances

Eq a => Wrap (TT a a) Source # 

Methods

wrap :: TT a a -> TT a a Source #

class UnWrap a where Source #

Minimal complete definition

unwrap

Methods

unwrap :: a -> a Source #

wrap' :: Eq a => TT a a -> TT a a Source #