pire-0.2.5

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

Parser

Contents

Description

parser, ported to Pire from Pi-Forall, adapted to Trifectra from Parsec

Synopsis

Documentation

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 #

newtype InnerParser a Source #

Constructors

InnerParser 

Fields

Instances

Monad InnerParser Source # 
Functor InnerParser Source # 

Methods

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

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

Applicative InnerParser Source # 

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 # 
MonadPlus InnerParser Source # 
TokenParsing InnerParser Source # 
LookAheadParsing InnerParser Source # 
CharParsing InnerParser Source # 
Parsing InnerParser Source # 
DeltaParsing InnerParser Source # 

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

variables or zero-argument constructors

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> varOrCon ) piPrelude) beginning " {-foo-} Nat{-bar-}{-baz-}x "
TCon "Nat" []
>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> varOrCon ) piPrelude) beginning " {-foo-} Zero{-bar-}{-baz-}x "
DCon "Zero" [] Nothing
>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> varOrCon ) piPrelude) beginning " {-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"))))

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 a, Show t) => Show (InParens t a) Source # 

Methods

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

show :: InParens t a -> String #

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

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