pire-0.2.5

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

OldParser

Contents

Description

Pire's old parser

Synopsis

Documentation

class MkVisible t where Source #

Minimal complete definition

mkVisible

Methods

mkVisible :: Text -> Integer -> t Source #

bracketOpen_ :: (TokParsing m, DeltaParsing m) => m (Token BracketOpenTy Text) Source #

>>> parse bracketOpen_ "[{-foo-}y]  x  "
BracketOpen "[" (Ws "{-foo-}")

bracketClose_ :: (TokParsing m, DeltaParsing m) => m (Token BracketCloseTy Text) Source #

>>> parse bracketClose_ "]{-bar-}x  "
BracketClose "]" (Ws "{-bar-}")

parenOpen_ :: (TokParsing m, DeltaParsing m) => m (Token ParenOpenTy Text) Source #

>>> parse parenOpen_ "({-foo-}y)  x  "
ParenOpen "(" (Ws "{-foo-}")

impOrExpVar :: (TokParsing m, DeltaParsing m, MonadState PiState m) => m (Expr Text Text, Eps) Source #

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> impOrExpVar) piPrelude) beginning " [ a ]{-foo-}this rocks "
(V "a",ErasedP)
>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> impOrExpVar) piPrelude) beginning " a {-foo-}this rocks "
(V "a",RuntimeP)

impOrExpVar_ :: (TokParsing m, DeltaParsing m, MonadState PiState m) => m (Expr Text Text, Eps) Source #

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> impOrExpVar_) piPrelude) beginning " [{-foo-} y{-bar-}]{-baz-}x "
(Brackets_ (BracketOpen "[" (Ws "{-foo-} ")) (Ws_ (V "y") (Ws "{-bar-}")) (BracketClose "]" (Ws "{-baz-}")),ErasedP)

setTraversal :: Ord b => Traversal (Set a) (Set b) a b Source #

data ConstructorNames a Source #

Constructors

ConstructorNames 

Fields

Instances

Foldable ConstructorNames Source # 

Methods

fold :: Monoid m => ConstructorNames m -> m #

foldMap :: Monoid m => (a -> m) -> ConstructorNames a -> m #

foldr :: (a -> b -> b) -> b -> ConstructorNames a -> b #

foldr' :: (a -> b -> b) -> b -> ConstructorNames a -> b #

foldl :: (b -> a -> b) -> b -> ConstructorNames a -> b #

foldl' :: (b -> a -> b) -> b -> ConstructorNames a -> b #

foldr1 :: (a -> a -> a) -> ConstructorNames a -> a #

foldl1 :: (a -> a -> a) -> ConstructorNames a -> a #

toList :: ConstructorNames a -> [a] #

null :: ConstructorNames a -> Bool #

length :: ConstructorNames a -> Int #

elem :: Eq a => a -> ConstructorNames a -> Bool #

maximum :: Ord a => ConstructorNames a -> a #

minimum :: Ord a => ConstructorNames a -> a #

sum :: Num a => ConstructorNames a -> a #

product :: Num a => ConstructorNames a -> a #

Eq a => Eq (ConstructorNames a) Source # 
Ord a => Ord (ConstructorNames a) Source # 
(Ord a, Read a) => Read (ConstructorNames a) Source # 
Show a => Show (ConstructorNames a) Source # 

emptyConstructorNames :: ConstructorNames Text Source #

empty set of constructor names

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 # 

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

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

parse a variable (in a white space aware manner)

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> var_) piPrelude) beginning "  wow{-foo-} this rocks "
Ws_ (V "wow") (Ws "{-foo-} ")

var2_ :: (TokenParsing m, Monad m, DeltaParsing m, MonadState PiState m) => m (Text, Ws Text) Source #

but often only need a (String, Ws) pair... "2" for pair

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

reserved_ :: (TokenParsing m, Monad m, DeltaParsing m) => String -> m (Ws Text) Source #

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> reserved_ "in") piInit) beginning "  in{-foo-}this rocks "
Ws "{-foo-}"

reservedOp_ :: (TokParsing m, DeltaParsing m) => String -> m (Ws Text) Source #

>>> fromSuccess $ parseString (runInnerParser $ evalStateT (whiteSpace *> reservedOp_ "wow") piPrelude) beginning "  wow{-foo-}this rocks "
Ws "{-foo-}"

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

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

simple lambda

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

extract :: Expr t a -> a Source #

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

>>> nopos $ parse (whiteSpace *> lambdaPAs) " \\x [y] . y"
LamPAs [(RuntimeP,"x",Annot Nothing),(ErasedP,"y",Annot Nothing)] (Scope (V (B 1)))
>>> nopos $ parse (whiteSpace *> lambdaPAs) " \\x [y] . y a"
LamPAs [(RuntimeP,"x",Annot Nothing),(ErasedP,"y",Annot 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 (whiteSpace *> impProd) "    [x:A] -> B "
PiP ErasedP (PatVar "x") (V "A") (Scope (V (F (V "B"))))
>>> nopos $ parse (whiteSpace *> impProd) "    [A] -> B "
PiP ErasedP (WildcardP "_") (V "A") (Scope (V (F (V "B"))))

sepBy_ :: (Monad m, Alternative m) => m (c t a) -> m sep -> m [Elem sep c t a] Source #

sepBy1_ :: (Monad m, Alternative m) => m (c t a) -> m sep -> m [Elem sep c t a] Source #

>>> parse (sepBy1_ (nopos <$> expr) semiColon_)   "a ; b ; c"
[Elem (V "a"),Separator (SemiColon ";" (Ws " ")),Elem (V "b"),Separator (SemiColon ";" (Ws " ")),Elem (V "c")]
>>> parsep (match `sepBy1_` semiColon_)   "Succ n -> bar ; Zero -> baz"
[Elem (Match (PatCon "Succ" [(RuntimeP,PatVar "n")]) (Scope (V (F (V "bar"))))),Separator (SemiColon ";" (Ws " ")),Elem (Match (PatCon "Zero" []) (Scope (V (F (V "baz")))))]

sepByNonEmpty_ :: (Monad m, Alternative m) => m (c t a) -> m sep -> m (NonEmpty (Elem sep c t a)) Source #

>>> parsep match  "Succ n -> bar"
Match (PatCon "Succ" [(RuntimeP,PatVar "n")]) (Scope (V (F (V "bar"))))
>>> parse (sepByNonEmpty_ (nopos <$> expr) semiColon_)   "a ; b ; c"
Elem (V "a") :| [Separator (SemiColon ";" (Ws " ")),Elem (V "b"),Separator (SemiColon ";" (Ws " ")),Elem (V "c")]
>>> parsep (sepByNonEmpty_ match semiColon_)   "Succ n -> bar ; Zero -> baz"
Elem (Match (PatCon "Succ" [(RuntimeP,PatVar "n")]) (Scope (V (F (V "bar"))))) :| [Separator (SemiColon ";" (Ws " ")),Elem (Match (PatCon "Zero" []) (Scope (V (F (V "baz")))))]

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

for testing

>>> let natstr = unlines [ "data Nat : Type where", "  Zero", "  Succ of (Nat)" ]
>>> putStr natstr
data Nat : Type where
  Zero
  Succ of (Nat)
>>> ppr $ nopos $ parse dataDef natstr
Data "Nat" EmptyTele [ConstructorDef' "Zero" EmptyTele
                     ,ConstructorDef' "Succ" (ConsP RuntimeP (WildcardP "_")
                                                             (TCon "Nat" [])
                                                             EmptyTele)]
>>> nopos $ parse dataDef_ natstr
Data_ (DataTok "data" (Ws " ")) (Nm_ "Nat" (Ws " ")) EmptyTele (Colon ":" (Ws " ")) (Type_ "Type" (Ws " ")) (Where "where" (Ws "\n  ")) (IndentedList [ConstructorDef'_ (Nm_ "Zero" (Ws "\n  ")) Nothing EmptyTele,ConstructorDef'_ (Nm_ "Succ" (Ws " ")) (Just (Of "of" (Ws " "))) (ConsWildInParens_ RuntimeP (ParenOpen "(" (Ws "")) (WildcardP "_") (TCon_ (Ws_ (V "Nat") (Ws "")) []) (ParenClose ")" (Ws "\n")) EmptyTele)])

the pretty printed version is certainly more readable, watchout however, (Where "where" (Ws "n ")) get translated to (Where "where" (Ws " ")):

>>> ppr $ nopos $ parse dataDef_ natstr
Data_ (DataTok "data" (Ws " "))
      (Nm_ "Nat" (Ws " "))
      EmptyTele (Colon ":" (Ws " "))
                (Type_ "Type" (Ws " "))
                (Where "where" (Ws "   "))
                (IndentedList [ConstructorDef'_ (Nm_ "Zero" (Ws "   "))
                                                Nothing EmptyTele
                              ,ConstructorDef'_ (Nm_ "Succ" (Ws " "))
                                                (Just (Of "of" (Ws " ")))
                                                (ConsWildInParens_ RuntimeP (ParenOpen "(" (Ws ""))
                                                                            (WildcardP "_")
                                                                            (TCon_ (Ws_ (V "Nat")
                                                                                        (Ws ""))
                                                                                   [])
                                                                            (ParenClose ")" (Ws "
                                                                                                "))
                                                                            EmptyTele)])