pire-0.2.5

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

OldWrap

Description

bound variables can be wrapped (and unwrapped) with their textual representation, for they can contribute to the calculation of their position info

Synopsis

Documentation

class UnWrap a where Source #

Minimal complete definition

unwrap

Methods

unwrap :: a -> a Source #

Instances
Eq a => UnWrap [Decl a a] Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: [Decl a a] -> [Decl a a] Source #

Eq t => UnWrap (Pattern t) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Pattern t -> Pattern t Source #

Eq a => UnWrap (ConstructorDef a a, b) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: (ConstructorDef a a, b) -> (ConstructorDef a a, b) Source #

Eq a => UnWrap (Module a a) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Module a a -> Module a a Source #

Eq a => UnWrap (Decl a a) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Decl a a -> Decl a a Source #

Eq a => UnWrap (ConstructorDef a a) Source # 
Instance details

Defined in OldWrap

Eq a => UnWrap (Telescope a a) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Telescope a a -> Telescope a a Source #

Eq a => UnWrap (Match a a) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Match a a -> Match a a Source #

Eq a => UnWrap (Expr t a) Source # 
Instance details

Defined in OldWrap

Methods

unwrap :: Expr t a -> Expr t a Source #

class Wrap a where Source #

>>> nopos $ parse expr_ "\\  x . x  a"
LamPAs_ (LamTok "\\" (Ws "  ")) [(RuntimeP,Binder_ "x" (Ws " "),Annot Nothing)] (Dot "." (Ws " ")) (Scope (Ws_ (V (B 0)) (Ws "  ") :@ Ws_ (V (F (V "a"))) (Ws "")))
>>> wrap $ nopos $ parse expr_ "\\  x . x  a"
LamPAs_ (LamTok "\\" (Ws "  ")) [(RuntimeP,Binder_ "x" (Ws " "),Annot Nothing)] (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)] (Dot "." (Ws " ")) (Scope (Ws_ (V (F (V "a"))) (Ws " ") :@ Paren_ (ParenOpen "(" (Ws "")) (LamPAs_ (LamTok "\\" (Ws "")) [(RuntimeP,Binder_ "a" (Ws " "),Annot Nothing)] (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 (PatVar "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_ (Binder "_") (Ws_ (V A) (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V B))) (Ws "")))
  • - -- >>> 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_ "A -> B"
PiP_ RuntimeP (InferredAnn_ (V "_") (Ws_ (V "A") (Ws " "))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V "B"))) (Ws "")))
  • - -- >>> unwrap $ wrap $ nopos $ parse expr_ "A -> B"
  • - -- PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_") (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 "")))
>>> unwrap $ wrap $ nopos $ parse expr_ "A -> B"
PiP_ RuntimeP (InferredAnn_ (V "_") (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 "")))
>>> unwrap $ wrap $ nopos $ parse expr_ "(x:A) -> B x"
PiP_ RuntimeP (Paren_ (ParenOpen "(" (Ws "")) (WitnessedAnn_ (Ws_ (V "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_ (Binder "_1") (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (Ann_ (InferredAnnBnd_ (Binder "_") (Ws_ (V B) (Ws " ")))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V C))) (Ws "")))) (ParenClose ")" (Ws " "))))) (Arrow "->" (Ws " ")) (Scope (Ws_ (V (F (V A))) (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 "")))
>>> wrap $ nopos $ parse expr_ "(B -> C) -> A"
PiP_ RuntimeP (InferredAnn_ (V "_1") (Paren_ (ParenOpen "(" (Ws "")) (PiP_ RuntimeP (InferredAnn_ (V "_") (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 [Decl a a] Source # 
Instance details

Defined in OldWrap

Methods

wrap :: [Decl a a] -> [Decl a a] Source #

Eq t => Wrap (Pattern t) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Pattern t -> Pattern t Source #

Eq a => Wrap (ConstructorDef a a, b) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: (ConstructorDef a a, b) -> (ConstructorDef a a, b) Source #

Eq a => Wrap (Module a a) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Module a a -> Module a a Source #

Eq a => Wrap (Decl a a) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Decl a a -> Decl a a Source #

Eq a => Wrap (ConstructorDef a a) Source # 
Instance details

Defined in OldWrap

Eq a => Wrap (Telescope a a) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Telescope a a -> Telescope a a Source #

Eq a => Wrap (Match a a) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Match a a -> Match a a Source #

Eq a => Wrap (Expr a a) Source # 
Instance details

Defined in OldWrap

Methods

wrap :: Expr a a -> Expr a a Source #

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

wrapMatch :: Eq a => Match a a -> Match a a Source #

wrapDecl :: (Wrap (Expr t a), Wrap (Telescope t a), Wrap (ConstructorDef t a)) => Decl t a -> Decl t a Source #

wrapM :: Wrap [Decl t a2] => Module t a2 -> Module t a2 Source #

wrapTele :: Eq a => Telescope a a -> Telescope a a Source #

unwrap' :: Expr t a -> Expr t a Source #

unwrapDecl :: (Eq a, UnWrap (Telescope t a), UnWrap (ConstructorDef t a)) => Decl t a -> Decl t a Source #

unwrapM :: UnWrap [Decl t a2] => Module t a2 -> Module t a2 Source #