pire-0.2.5

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

Parser

Description

Pire's (Pi-forall absy) parser, adapted from Parsec to Trifecta

Synopsis

Documentation

data InParens t a Source #

Constructors

Colon' (Expr t a) (Expr t a) 
Comma' (Expr t a) (Expr t a) 
Nope (Expr t a) 
Instances
(Show t, Show a) => Show (InParens t a) Source # 
Instance details

Defined in Parser

Methods

showsPrec :: Int -> InParens t a -> ShowS #

show :: InParens t a -> String #

showList :: [InParens t a] -> ShowS #

data PiState Source #

Instances
Show PiState Source # 
Instance details

Defined in Parser

newtype InnerParser a Source #

Constructors

InnerParser 

Fields

Instances
Monad InnerParser Source # 
Instance details

Defined in Parser

Functor InnerParser Source # 
Instance details

Defined in Parser

Methods

fmap :: (a -> b) -> InnerParser a -> InnerParser b #

(<$) :: a -> InnerParser b -> InnerParser a #

Applicative InnerParser Source # 
Instance details

Defined in Parser

Methods

pure :: a -> InnerParser a #

(<*>) :: InnerParser (a -> b) -> InnerParser a -> InnerParser b #

liftA2 :: (a -> b -> c) -> InnerParser a -> InnerParser b -> InnerParser c #

(*>) :: InnerParser a -> InnerParser b -> InnerParser b #

(<*) :: InnerParser a -> InnerParser b -> InnerParser a #

Alternative InnerParser Source # 
Instance details

Defined in Parser

MonadPlus InnerParser Source # 
Instance details

Defined in Parser

TokenParsing InnerParser Source # 
Instance details

Defined in Parser

LookAheadParsing InnerParser Source # 
Instance details

Defined in Parser

CharParsing InnerParser Source # 
Instance details

Defined in Parser

Parsing InnerParser Source # 
Instance details

Defined in Parser

DeltaParsing InnerParser Source # 
Instance details

Defined in Parser

ide :: (TokenParsing m, Monad m) => m Text Source #

parse an identifier

>>> parseTest (runInnerParser $ whiteSpace *> ide) "   wow  this rocks"
"wow"
>>> parseTest (runInnerParser $ whiteSpace *> many ide) "   wow  this rocks"
["wow","this","rocks"]

better parse w/ state

>>> parseTest (runInnerParser $ evalStateT (whiteSpace *> ide) piInit) "  wow this rocks"
"wow"
>>> parseTest (runInnerParser $ evalStateT (whiteSpace *> many ide) piInit) "  wow this rocks"
["wow","this","rocks"]
>>> parseString (runInnerParser $ evalStateT (whiteSpace *> ide) piInit) beginning "  wow this rocks "
Success "wow"

var :: (TokenParsing m, Monad m, MonadState PiState m) => m (Expr Text Text) Source #

parse a variable

>>> parseString (runInnerParser $ evalStateT (whiteSpace *> var) piPrelude) beginning "  wow this rocks "
Success (V "wow")

var' :: (TokenParsing m, MonadState PiState m) => m Text Source #

parse a variable somtimes we just want the string (T.Text) (but nevertheless be sure it's a var, not a dcon/tcon ie.)

reserved :: (TokenParsing m, Monad m) => String -> m () Source #

varOrCon :: (TokenParsing m, MonadState PiState m) => m (Expr Text Text) Source #

variables or zero-argument constructors

>>> parsep (whiteSpace *> varOrCon) " {-foo-} Nat{-bar-}{-baz-}x "
TCon "Nat" []
>>> parsep (whiteSpace *> varOrCon) " {-foo-} Zero{-bar-}{-baz-}x "
DCon "Zero" [] Nothing
>>> parsep (whiteSpace *> varOrCon) " {-foo-} Succ{-bar-}{-baz-}x "
DCon "Succ" [] Nothing

lambda :: (TokenParsing m, LookAheadParsing m, DeltaParsing m, MonadState PiState m, IndentationParsing m) => m (Expr Text Text) Source #

simple lambda

>>> nopos $ parse lambda "\\ x . y a "
Lam "x" Nothing (Scope (V (F (V "y")) :@ V (F (V "a"))))
>>> nopos $ parse lambda "\\ [ x ] . y a "
ErasedLam "x" (Scope (V (F (V "y")) :@ V (F (V "a"))))

lambdaPAs :: (TokenParsing m, LookAheadParsing m, DeltaParsing m, MonadState PiState m, IndentationParsing m) => m (Expr Text Text) Source #

parse lambdas (several: s) with runtime/erased pattern (P) and possible type annotations (A)

>>> nopos $ parse lambdaPAs "\\x [y] . y"
LamPAs [(RuntimeP,"x",Nothing),(ErasedP,"y",Nothing)] (Scope (V (B 1)))
>>> nopos $ parse lambdaPAs "\\x [y] . y a"
LamPAs [(RuntimeP,"x",Nothing),(ErasedP,"y",Nothing)] (Scope (V (B 1) :@ V (F (V "a"))))

impProd :: (TokenParsing m, Monad m, LookAheadParsing m, DeltaParsing m, MonadState PiState m, IndentationParsing m) => m (Expr Text Text) Source #

impProd - implicit dependent products These have the syntax [x:a] -> b or [a] -> b .

>>> nopos $ parse impProd "[x:A] -> B "
PiP ErasedP (PatVar "x") (V "A") (Scope (V (F (V "B"))))
>>> nopos $ parse impProd "[A] -> B "
PiP ErasedP (WildcardP "_") (V "A") (Scope (V (F (V "B"))))

caseExpr2 :: (TokenParsing m, MonadState PiState m, LookAheadParsing m, DeltaParsing m, IndentationParsing m) => m (Expr Text Text) Source #

>>> parsep caseExpr2 "case v of { Zero -> here ; Succ n -> there}"
Case (V "v") [Match (PatCon "Zero" []) (Scope (V (F (V "here")))),Match (PatCon "Succ" [(RuntimeP,PatVar "n")]) (Scope (V (F (V "there"))))] Nothing