pire-0.2.5

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

OldSyntax

Contents

Description

Pire's old syntax

Synopsis

Documentation

data Ws t Source #

Constructors

Ws t 
NoWs 

Instances

Functor Ws Source # 

Methods

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

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

Foldable Ws Source # 

Methods

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

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

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

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

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

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

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

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

toList :: Ws a -> [a] #

null :: Ws a -> Bool #

length :: Ws a -> Int #

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

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

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

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

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

Traversable Ws Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Ws a -> f (Ws b) #

sequenceA :: Applicative f => Ws (f a) -> f (Ws a) #

mapM :: Monad m => (a -> m b) -> Ws a -> m (Ws b) #

sequence :: Monad m => Ws (m a) -> m (Ws a) #

Eq1 Ws Source # 

Methods

liftEq :: (a -> b -> Bool) -> Ws a -> Ws b -> Bool #

Eq t => Eq (Ws t) Source # 

Methods

(==) :: Ws t -> Ws t -> Bool #

(/=) :: Ws t -> Ws t -> Bool #

Ord t => Ord (Ws t) Source # 

Methods

compare :: Ws t -> Ws t -> Ordering #

(<) :: Ws t -> Ws t -> Bool #

(<=) :: Ws t -> Ws t -> Bool #

(>) :: Ws t -> Ws t -> Bool #

(>=) :: Ws t -> Ws t -> Bool #

max :: Ws t -> Ws t -> Ws t #

min :: Ws t -> Ws t -> Ws t #

Read t => Read (Ws t) Source # 
Show t => Show (Ws t) Source # 

Methods

showsPrec :: Int -> Ws t -> ShowS #

show :: Ws t -> String #

showList :: [Ws t] -> ShowS #

data Token ty t where Source #

Constructors

LamTok :: t -> Ws t -> Token LamTokTy t 
Dot :: t -> Ws t -> Token DotTy t 
LetTok :: t -> Ws t -> Token LetTokTy t 
BracketOpen :: t -> Ws t -> Token BracketOpenTy t 
BracketClose :: t -> Ws t -> Token BracketCloseTy t 
ParenOpen :: t -> Ws t -> Token ParenOpenTy t 
ParenClose :: t -> Ws t -> Token ParenCloseTy t 
BraceOpen :: t -> Ws t -> Token BraceOpenTy t 
BraceClose :: t -> Ws t -> Token BraceCloseTy t 
VBar :: t -> Ws t -> Token VBarTy t 
IfTok :: t -> Ws t -> Token IfTokTy t 
ThenTok :: t -> Ws t -> Token ThenTokTy t 
ElseTok :: t -> Ws t -> Token ElseTokTy t 
Equal :: t -> Ws t -> Token EqualTy t 
In :: t -> Ws t -> Token InTy t 
Arrow :: t -> Ws t -> Token ArrowTy t 
Colon :: t -> Ws t -> Token ColonTy t 
SemiColon :: t -> Ws t -> Token SemiColonTy t 
Comma :: t -> Ws t -> Token CommaTy t 
Of :: t -> Ws t -> Token OfTy t 
CaseTok :: t -> Ws t -> Token CaseTokTy t 
PcaseTok :: t -> Ws t -> Token PcaseTokTy t 
SubstTok :: t -> Ws t -> Token SubstTokTy t 
ContraTok :: t -> Ws t -> Token ContraTokTy t 
By :: t -> Ws t -> Token ByTy t 
Where :: t -> Ws t -> Token WhereTy t 
ModuleTok :: t -> Ws t -> Token ModuleTokTy t 
ImportTok :: t -> Ws t -> Token ImportTokTy t 
DataTok :: t -> Ws t -> Token DataTokTy t 

Instances

Functor (Token ty) Source # 

Methods

fmap :: (a -> b) -> Token ty a -> Token ty b #

(<$) :: a -> Token ty b -> Token ty a #

Foldable (Token ty) Source # 

Methods

fold :: Monoid m => Token ty m -> m #

foldMap :: Monoid m => (a -> m) -> Token ty a -> m #

foldr :: (a -> b -> b) -> b -> Token ty a -> b #

foldr' :: (a -> b -> b) -> b -> Token ty a -> b #

foldl :: (b -> a -> b) -> b -> Token ty a -> b #

foldl' :: (b -> a -> b) -> b -> Token ty a -> b #

foldr1 :: (a -> a -> a) -> Token ty a -> a #

foldl1 :: (a -> a -> a) -> Token ty a -> a #

toList :: Token ty a -> [a] #

null :: Token ty a -> Bool #

length :: Token ty a -> Int #

elem :: Eq a => a -> Token ty a -> Bool #

maximum :: Ord a => Token ty a -> a #

minimum :: Ord a => Token ty a -> a #

sum :: Num a => Token ty a -> a #

product :: Num a => Token ty a -> a #

Traversable (Token ty) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Token ty a -> f (Token ty b) #

sequenceA :: Applicative f => Token ty (f a) -> f (Token ty a) #

mapM :: Monad m => (a -> m b) -> Token ty a -> m (Token ty b) #

sequence :: Monad m => Token ty (m a) -> m (Token ty a) #

Eq t => Eq (Token ty t) Source # 

Methods

(==) :: Token ty t -> Token ty t -> Bool #

(/=) :: Token ty t -> Token ty t -> Bool #

(Eq t, Ord t) => Ord (Token ty t) Source # 

Methods

compare :: Token ty t -> Token ty t -> Ordering #

(<) :: Token ty t -> Token ty t -> Bool #

(<=) :: Token ty t -> Token ty t -> Bool #

(>) :: Token ty t -> Token ty t -> Bool #

(>=) :: Token ty t -> Token ty t -> Bool #

max :: Token ty t -> Token ty t -> Token ty t #

min :: Token ty t -> Token ty t -> Token ty t #

Show t => Show (Token ty t) Source # 

Methods

showsPrec :: Int -> Token ty t -> ShowS #

show :: Token ty t -> String #

showList :: [Token ty t] -> ShowS #

NoPos (ConstructorDef t a, Maybe (Token SemiColonTy t)) Source # 
Forget (Maybe (Token SemiColonTy t), Match t a) (Match t a) Source # 

Methods

forget :: (Maybe (Token SemiColonTy t), Match t a) -> Match t a Source #

Forget (Token SemiColonTy t, Match t a) (Match t a) Source # 

Methods

forget :: (Token SemiColonTy t, Match t a) -> Match t a Source #

Forget (ConstructorDef t a, Maybe (Token SemiColonTy t)) (ConstructorDef t a) Source # 
Forget (Match t a, Token SemiColonTy t) (Match t a) Source # 

Methods

forget :: (Match t a, Token SemiColonTy t) -> Match t a Source #

Forget (Match t a, Maybe (Token SemiColonTy t)) (Match t a) Source # 

Methods

forget :: (Match t a, Maybe (Token SemiColonTy t)) -> Match t a Source #

toLiteral :: Token ty t -> t Source #

toWs :: Token ty t -> Ws t Source #

cmp :: Ord t => Token ty t -> Token ty t -> Ordering Source #

ordering :: Ord t => Token ty t -> Token ty t -> Ordering Source #

data Eps Source #

Constructors

ErasedP 
RuntimeP 

Instances

Eq Eps Source # 

Methods

(==) :: Eps -> Eps -> Bool #

(/=) :: Eps -> Eps -> Bool #

Ord Eps Source # 

Methods

compare :: Eps -> Eps -> Ordering #

(<) :: Eps -> Eps -> Bool #

(<=) :: Eps -> Eps -> Bool #

(>) :: Eps -> Eps -> Bool #

(>=) :: Eps -> Eps -> Bool #

max :: Eps -> Eps -> Eps #

min :: Eps -> Eps -> Eps #

Read Eps Source # 
Show Eps Source # 

Methods

showsPrec :: Int -> Eps -> ShowS #

show :: Eps -> String #

showList :: [Eps] -> ShowS #

Forget (Expr t a, Eps) (Expr t a, Eps) Source # 

Methods

forget :: (Expr t a, Eps) -> (Expr t a, Eps) Source #

data Nm t Source #

Constructors

Nm t 
Nm_ t (Ws t) 

Instances

Functor Nm Source # 

Methods

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

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

Foldable Nm Source # 

Methods

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

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

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

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

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

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

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

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

toList :: Nm a -> [a] #

null :: Nm a -> Bool #

length :: Nm a -> Int #

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

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

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

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

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

Traversable Nm Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Nm a -> f (Nm b) #

sequenceA :: Applicative f => Nm (f a) -> f (Nm a) #

mapM :: Monad m => (a -> m b) -> Nm a -> m (Nm b) #

sequence :: Monad m => Nm (m a) -> m (Nm a) #

Eq t => Eq (Nm t) Source # 

Methods

(==) :: Nm t -> Nm t -> Bool #

(/=) :: Nm t -> Nm t -> Bool #

Ord t => Ord (Nm t) Source # 

Methods

compare :: Nm t -> Nm t -> Ordering #

(<) :: Nm t -> Nm t -> Bool #

(<=) :: Nm t -> Nm t -> Bool #

(>) :: Nm t -> Nm t -> Bool #

(>=) :: Nm t -> Nm t -> Bool #

max :: Nm t -> Nm t -> Nm t #

min :: Nm t -> Nm t -> Nm t #

Read t => Read (Nm t) Source # 
Show t => Show (Nm t) Source # 

Methods

showsPrec :: Int -> Nm t -> ShowS #

show :: Nm t -> String #

showList :: [Nm t] -> ShowS #

data Pattern t Source #

Instances

Functor Pattern Source # 

Methods

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

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

Foldable Pattern Source # 

Methods

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

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

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

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

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

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

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

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

toList :: Pattern a -> [a] #

null :: Pattern a -> Bool #

length :: Pattern a -> Int #

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

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

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

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

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

Traversable Pattern Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Pattern a -> f (Pattern b) #

sequenceA :: Applicative f => Pattern (f a) -> f (Pattern a) #

mapM :: Monad m => (a -> m b) -> Pattern a -> m (Pattern b) #

sequence :: Monad m => Pattern (m a) -> m (Pattern a) #

Eq t => Eq (Pattern t) Source # 

Methods

(==) :: Pattern t -> Pattern t -> Bool #

(/=) :: Pattern t -> Pattern t -> Bool #

Ord t => Ord (Pattern t) Source # 

Methods

compare :: Pattern t -> Pattern t -> Ordering #

(<) :: Pattern t -> Pattern t -> Bool #

(<=) :: Pattern t -> Pattern t -> Bool #

(>) :: Pattern t -> Pattern t -> Bool #

(>=) :: Pattern t -> Pattern t -> Bool #

max :: Pattern t -> Pattern t -> Pattern t #

min :: Pattern t -> Pattern t -> Pattern t #

Show t => Show (Pattern t) Source # 

Methods

showsPrec :: Int -> Pattern t -> ShowS #

show :: Pattern t -> String #

showList :: [Pattern t] -> ShowS #

NoPos (Pattern t) Source # 

Methods

nopos :: Pattern t -> Pattern t Source #

Forget (Pattern t) (Pattern t) Source # 

Methods

forget :: Pattern t -> Pattern t Source #

data Expr t a Source #

Constructors

V a 
Ws_ (Expr t a) (Ws t) 
BndV t (Expr t a) 
Brackets_ (Token BracketOpenTy t) (Expr t a) (Token BracketCloseTy t) 
Paren (Expr t a) 
Paren_ (Token ParenOpenTy t) (Expr t a) (Token ParenCloseTy t) 
Type 
Type_ t (Ws t) 
(Expr t a) :@ (Expr t a) infixl 9 
ErasedApp (Expr t a) (Expr t a) 
Lam t (Annot t a) (Scope () (Expr t) a) 
Lam_ (Token LamTokTy t) (Pattern t) (Token DotTy t) (Scope () (Expr t) a) 
Lam' t (Scope (Name String ()) (Expr t) a) 
Lams' [t] (Scope (Name String Int) (Expr t) a) 
ErasedLam t (Scope () (Expr t) a) 
ErasedLam_ (Token LamTokTy t) (Pattern t) (Token DotTy t) (Scope () (Expr t) a) 
Lams [t] (Scope Int (Expr t) a) 
Lams_ (Token LamTokTy t) [Pattern t] (Token DotTy t) (Scope Int (Expr t) a) 
LamPA (Eps, t, Annot t a) (Scope () (Expr t) a) 
LamPAs [(Eps, t, Annot t a)] (Scope Int (Expr t) a) 
LamPAs_ (Token LamTokTy t) [(Eps, Pattern t, Annot t a)] (Token DotTy t) (Scope Int (Expr t) a) 
Pi t (Expr t a) (Scope () (Expr t) a) 
Pi_ (Expr t a) (Token ArrowTy t) (Scope () (Expr t) a) 
PiP Eps (Pattern t) (Expr t a) (Scope () (Expr t) a) 
PiP_ Eps (Expr t a) (Token ArrowTy t) (Scope () (Expr t) a) 
Position Delta (Expr t a) 
TrustMe (Annot t a) 
TrustMe_ t (Ws t) (Annot t a) 
TyUnit 
TyUnit_ t (Ws t) 
LitUnit 
LitUnit_ t (Ws t) 
TyBool 
TyBool_ t (Ws t) 
LitBool Bool 
LitBool_ Bool t (Ws t) 
If (Expr t a) (Expr t a) (Expr t a) (Annot t a) 
If_ (Token IfTokTy t) (Expr t a) (Token ThenTokTy t) (Expr t a) (Token ElseTokTy t) (Expr t a) (Annot t a) 
Sigma t (Expr t a) (Scope () (Expr t) a)

sigma types `{ x : A | B }`

Sigma_ (Token BraceOpenTy t) (Pattern t) (Token ColonTy t) (Expr t a) (Token VBarTy t) (Scope () (Expr t) a) (Token BraceCloseTy t) 
Prod (Expr t a) (Expr t a) (Annot t a)

introduction for sigmas `( a , b )`

Prod_ (Token ParenOpenTy t) (Expr t a) (Token CommaTy t) (Expr t a) (Token ParenCloseTy t) (Annot t a) 
Pcase (Expr t a) (t, t) (Scope Int (Expr t) a) (Annot t a)

elimination form `pcase p of (x,y) -> p`

Pcase_ (Token PcaseTokTy t) (Expr t a) (Token OfTy t) (Token ParenOpenTy t) (Pattern t) (Token CommaTy t) (Pattern t) (Token ParenCloseTy t) (Token ArrowTy t) (Scope Int (Expr t) a) (Annot t a) 
Let t (Expr t a) (Scope () (Expr t) a) 
Let_ (Token LetTokTy t) (Pattern t) (Token EqualTy t) (Expr t a) (Token InTy t) (Scope () (Expr t) a) 
TyEq (Expr t a) (Expr t a)

Equality type `a = b`

TyEq_ (Expr t a) (Token EqualTy t) (Expr t a) 
Refl (Annot t a)

Proof of equality

Refl_ t (Ws t) (Annot t a) 
Subst (Expr t a) (Expr t a) (Annot t a)

equality elimination

Subst_ (Token SubstTokTy t) (Expr t a) (Token ByTy t) (Expr t a) (Annot t a) 
Contra (Expr t a) (Annot t a)

witness to an equality contradiction

Contra_ (Token ContraTokTy t) (Expr t a) (Annot t a) 
TCon a [Expr t a]

datatypes: type constructors (fully applied)

TCon_ (Expr t a) [Expr t a] 
DCon t [Arg t a] (Annot t a)

datatypes: term constructors

DCon_ (Nm t) [Arg t a] (Annot t a) 
Nat Integer 
Nat_ Integer t (Ws t) 
Case (Expr t a) [Match t a] (Annot t a)

case analysis (fully applied, erased arguments first)

Case_ (Token CaseTokTy t) (Expr t a) (Token OfTy t) (Block Match t a) (Annot t a) 
Ann (Expr t a) (Expr t a)

Annotated terms `( x : A )`

WitnessedAnnEx_ (Expr t a) (Token ColonTy t) (Expr t a) 
InferredAnnBnd_ (Pattern t) (Expr t a) 
WitnessedAnnBnd_ (Pattern t) (Token ColonTy t) (Expr t a) 
Ann_ (Expr t a) 

Instances

Bitraversable Expr Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Expr a b -> f (Expr c d) #

Bifoldable Expr Source # 

Methods

bifold :: Monoid m => Expr m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Expr a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Expr a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Expr a b -> c #

Bifunctor Expr Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Expr a c -> Expr b d #

first :: (a -> b) -> Expr a c -> Expr b c #

second :: (b -> c) -> Expr a b -> Expr a c #

Monad (Expr t) Source # 

Methods

(>>=) :: Expr t a -> (a -> Expr t b) -> Expr t b #

(>>) :: Expr t a -> Expr t b -> Expr t b #

return :: a -> Expr t a #

fail :: String -> Expr t a #

Functor (Expr t) Source # 

Methods

fmap :: (a -> b) -> Expr t a -> Expr t b #

(<$) :: a -> Expr t b -> Expr t a #

Applicative (Expr t) Source # 

Methods

pure :: a -> Expr t a #

(<*>) :: Expr t (a -> b) -> Expr t a -> Expr t b #

liftA2 :: (a -> b -> c) -> Expr t a -> Expr t b -> Expr t c #

(*>) :: Expr t a -> Expr t b -> Expr t b #

(<*) :: Expr t a -> Expr t b -> Expr t a #

Foldable (Expr t) Source # 

Methods

fold :: Monoid m => Expr t m -> m #

foldMap :: Monoid m => (a -> m) -> Expr t a -> m #

foldr :: (a -> b -> b) -> b -> Expr t a -> b #

foldr' :: (a -> b -> b) -> b -> Expr t a -> b #

foldl :: (b -> a -> b) -> b -> Expr t a -> b #

foldl' :: (b -> a -> b) -> b -> Expr t a -> b #

foldr1 :: (a -> a -> a) -> Expr t a -> a #

foldl1 :: (a -> a -> a) -> Expr t a -> a #

toList :: Expr t a -> [a] #

null :: Expr t a -> Bool #

length :: Expr t a -> Int #

elem :: Eq a => a -> Expr t a -> Bool #

maximum :: Ord a => Expr t a -> a #

minimum :: Ord a => Expr t a -> a #

sum :: Num a => Expr t a -> a #

product :: Num a => Expr t a -> a #

Traversable (Expr t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Expr t a -> f (Expr t b) #

sequenceA :: Applicative f => Expr t (f a) -> f (Expr t a) #

mapM :: Monad m => (a -> m b) -> Expr t a -> m (Expr t b) #

sequence :: Monad m => Expr t (m a) -> m (Expr t a) #

Eq t => Eq1 (Expr t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Expr t a -> Expr t b -> Bool #

Ord t => Ord1 (Expr t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Expr t a -> Expr t b -> Ordering #

Show t => Show1 (Expr t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Expr t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Expr t a] -> ShowS #

(Eq t, Eq a) => Eq (Expr t a) Source # 

Methods

(==) :: Expr t a -> Expr t a -> Bool #

(/=) :: Expr t a -> Expr t a -> Bool #

(Ord t, Ord a) => Ord (Expr t a) Source # 

Methods

compare :: Expr t a -> Expr t a -> Ordering #

(<) :: Expr t a -> Expr t a -> Bool #

(<=) :: Expr t a -> Expr t a -> Bool #

(>) :: Expr t a -> Expr t a -> Bool #

(>=) :: Expr t a -> Expr t a -> Bool #

max :: Expr t a -> Expr t a -> Expr t a #

min :: Expr t a -> Expr t a -> Expr t a #

(Show t, Show a) => Show (Expr t a) Source # 

Methods

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

show :: Expr t a -> String #

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

NoPos (Expr t a) Source # 

Methods

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

Forget (Expr t a, Eps) (Expr t a, Eps) Source # 

Methods

forget :: (Expr t a, Eps) -> (Expr t a, Eps) Source #

Forget (Expr t a) (Expr t a) Source # 

Methods

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

T2S (Expr Text Text) (Expr String String) Source # 

bitraverseExpr :: Applicative f => (a -> f c) -> (b -> f d) -> Expr a b -> f (Expr c d) Source #

data Annot t a Source #

Constructors

Annot (Maybe (Expr t a)) 

Instances

Bitraversable Annot Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Annot a b -> f (Annot c d) #

Bifoldable Annot Source # 

Methods

bifold :: Monoid m => Annot m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Annot a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Annot a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Annot a b -> c #

Bifunctor Annot Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Annot a c -> Annot b d #

first :: (a -> b) -> Annot a c -> Annot b c #

second :: (b -> c) -> Annot a b -> Annot a c #

Functor (Annot t) Source # 

Methods

fmap :: (a -> b) -> Annot t a -> Annot t b #

(<$) :: a -> Annot t b -> Annot t a #

Foldable (Annot t) Source # 

Methods

fold :: Monoid m => Annot t m -> m #

foldMap :: Monoid m => (a -> m) -> Annot t a -> m #

foldr :: (a -> b -> b) -> b -> Annot t a -> b #

foldr' :: (a -> b -> b) -> b -> Annot t a -> b #

foldl :: (b -> a -> b) -> b -> Annot t a -> b #

foldl' :: (b -> a -> b) -> b -> Annot t a -> b #

foldr1 :: (a -> a -> a) -> Annot t a -> a #

foldl1 :: (a -> a -> a) -> Annot t a -> a #

toList :: Annot t a -> [a] #

null :: Annot t a -> Bool #

length :: Annot t a -> Int #

elem :: Eq a => a -> Annot t a -> Bool #

maximum :: Ord a => Annot t a -> a #

minimum :: Ord a => Annot t a -> a #

sum :: Num a => Annot t a -> a #

product :: Num a => Annot t a -> a #

Traversable (Annot t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Annot t a -> f (Annot t b) #

sequenceA :: Applicative f => Annot t (f a) -> f (Annot t a) #

mapM :: Monad m => (a -> m b) -> Annot t a -> m (Annot t b) #

sequence :: Monad m => Annot t (m a) -> m (Annot t a) #

Eq t => Eq1 (Annot t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Annot t a -> Annot t b -> Bool #

Ord t => Ord1 (Annot t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Annot t a -> Annot t b -> Ordering #

Show t => Show1 (Annot t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Annot t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Annot t a] -> ShowS #

(Eq t, Eq a) => Eq (Annot t a) Source # 

Methods

(==) :: Annot t a -> Annot t a -> Bool #

(/=) :: Annot t a -> Annot t a -> Bool #

(Ord t, Ord a) => Ord (Annot t a) Source # 

Methods

compare :: Annot t a -> Annot t a -> Ordering #

(<) :: Annot t a -> Annot t a -> Bool #

(<=) :: Annot t a -> Annot t a -> Bool #

(>) :: Annot t a -> Annot t a -> Bool #

(>=) :: Annot t a -> Annot t a -> Bool #

max :: Annot t a -> Annot t a -> Annot t a #

min :: Annot t a -> Annot t a -> Annot t a #

(Show t, Show a) => Show (Annot t a) Source # 

Methods

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

show :: Annot t a -> String #

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

Forget (Annot t a) (Annot t a) Source # 

Methods

forget :: Annot t a -> Annot t a Source #

bitraverseAnnot :: Applicative f => (a -> f c) -> (b -> f d) -> Annot a b -> f (Annot c d) Source #

data Match t a Source #

Constructors

Match (Pattern t) (Scope Int (Expr t) a) 
Match_ (Pattern t) (Token ArrowTy t) (Scope Int (Expr t) a) 

Instances

Bitraversable Match Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Match a b -> f (Match c d) #

Bifoldable Match Source # 

Methods

bifold :: Monoid m => Match m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Match a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Match a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Match a b -> c #

Bifunctor Match Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Match a c -> Match b d #

first :: (a -> b) -> Match a c -> Match b c #

second :: (b -> c) -> Match a b -> Match a c #

Functor (Match t) Source # 

Methods

fmap :: (a -> b) -> Match t a -> Match t b #

(<$) :: a -> Match t b -> Match t a #

Foldable (Match t) Source # 

Methods

fold :: Monoid m => Match t m -> m #

foldMap :: Monoid m => (a -> m) -> Match t a -> m #

foldr :: (a -> b -> b) -> b -> Match t a -> b #

foldr' :: (a -> b -> b) -> b -> Match t a -> b #

foldl :: (b -> a -> b) -> b -> Match t a -> b #

foldl' :: (b -> a -> b) -> b -> Match t a -> b #

foldr1 :: (a -> a -> a) -> Match t a -> a #

foldl1 :: (a -> a -> a) -> Match t a -> a #

toList :: Match t a -> [a] #

null :: Match t a -> Bool #

length :: Match t a -> Int #

elem :: Eq a => a -> Match t a -> Bool #

maximum :: Ord a => Match t a -> a #

minimum :: Ord a => Match t a -> a #

sum :: Num a => Match t a -> a #

product :: Num a => Match t a -> a #

Traversable (Match t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Match t a -> f (Match t b) #

sequenceA :: Applicative f => Match t (f a) -> f (Match t a) #

mapM :: Monad m => (a -> m b) -> Match t a -> m (Match t b) #

sequence :: Monad m => Match t (m a) -> m (Match t a) #

Eq t => Eq1 (Match t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Match t a -> Match t b -> Bool #

Ord t => Ord1 (Match t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Match t a -> Match t b -> Ordering #

Show t => Show1 (Match t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Match t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Match t a] -> ShowS #

(Eq t, Eq a) => Eq (Match t a) Source # 

Methods

(==) :: Match t a -> Match t a -> Bool #

(/=) :: Match t a -> Match t a -> Bool #

(Ord t, Ord a) => Ord (Match t a) Source # 

Methods

compare :: Match t a -> Match t a -> Ordering #

(<) :: Match t a -> Match t a -> Bool #

(<=) :: Match t a -> Match t a -> Bool #

(>) :: Match t a -> Match t a -> Bool #

(>=) :: Match t a -> Match t a -> Bool #

max :: Match t a -> Match t a -> Match t a #

min :: Match t a -> Match t a -> Match t a #

(Show t, Show a) => Show (Match t a) Source # 

Methods

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

show :: Match t a -> String #

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

NoPos (Match t a) Source # 

Methods

nopos :: Match t a -> Match t a Source #

Forget (Maybe (Token SemiColonTy t), Match t a) (Match t a) Source # 

Methods

forget :: (Maybe (Token SemiColonTy t), Match t a) -> Match t a Source #

Forget (Token SemiColonTy t, Match t a) (Match t a) Source # 

Methods

forget :: (Token SemiColonTy t, Match t a) -> Match t a Source #

Forget (Match t a, Token SemiColonTy t) (Match t a) Source # 

Methods

forget :: (Match t a, Token SemiColonTy t) -> Match t a Source #

Forget (Match t a, Maybe (Token SemiColonTy t)) (Match t a) Source # 

Methods

forget :: (Match t a, Maybe (Token SemiColonTy t)) -> Match t a Source #

Forget (Match t a) (Match t a) Source # 

Methods

forget :: Match t a -> Match t a Source #

Forget (Block Match t a) [Match t a] Source # 

Methods

forget :: Block Match t a -> [Match t a] Source #

bitraverseMatch :: Applicative f => (a -> f c) -> (b -> f d) -> Match a b -> f (Match c d) Source #

data Elem sep constr t a Source #

Constructors

Elem (constr t a) 
Separator sep 

Instances

Functor (constr t) => Functor (Elem sep constr t) Source # 

Methods

fmap :: (a -> b) -> Elem sep constr t a -> Elem sep constr t b #

(<$) :: a -> Elem sep constr t b -> Elem sep constr t a #

Foldable (constr t) => Foldable (Elem sep constr t) Source # 

Methods

fold :: Monoid m => Elem sep constr t m -> m #

foldMap :: Monoid m => (a -> m) -> Elem sep constr t a -> m #

foldr :: (a -> b -> b) -> b -> Elem sep constr t a -> b #

foldr' :: (a -> b -> b) -> b -> Elem sep constr t a -> b #

foldl :: (b -> a -> b) -> b -> Elem sep constr t a -> b #

foldl' :: (b -> a -> b) -> b -> Elem sep constr t a -> b #

foldr1 :: (a -> a -> a) -> Elem sep constr t a -> a #

foldl1 :: (a -> a -> a) -> Elem sep constr t a -> a #

toList :: Elem sep constr t a -> [a] #

null :: Elem sep constr t a -> Bool #

length :: Elem sep constr t a -> Int #

elem :: Eq a => a -> Elem sep constr t a -> Bool #

maximum :: Ord a => Elem sep constr t a -> a #

minimum :: Ord a => Elem sep constr t a -> a #

sum :: Num a => Elem sep constr t a -> a #

product :: Num a => Elem sep constr t a -> a #

Traversable (constr t) => Traversable (Elem sep constr t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Elem sep constr t a -> f (Elem sep constr t b) #

sequenceA :: Applicative f => Elem sep constr t (f a) -> f (Elem sep constr t a) #

mapM :: Monad m => (a -> m b) -> Elem sep constr t a -> m (Elem sep constr t b) #

sequence :: Monad m => Elem sep constr t (m a) -> m (Elem sep constr t a) #

(Eq (constr t a), Eq sep) => Eq (Elem sep constr t a) Source # 

Methods

(==) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

(/=) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

(Ord (constr t a), Ord sep) => Ord (Elem sep constr t a) Source # 

Methods

compare :: Elem sep constr t a -> Elem sep constr t a -> Ordering #

(<) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

(<=) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

(>) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

(>=) :: Elem sep constr t a -> Elem sep constr t a -> Bool #

max :: Elem sep constr t a -> Elem sep constr t a -> Elem sep constr t a #

min :: Elem sep constr t a -> Elem sep constr t a -> Elem sep constr t a #

(Show (constr t a), Show sep) => Show (Elem sep constr t a) Source # 

Methods

showsPrec :: Int -> Elem sep constr t a -> ShowS #

show :: Elem sep constr t a -> String #

showList :: [Elem sep constr t a] -> ShowS #

data Block constr t a Source #

Constructors

IndentedList [constr t a] 
Block (Token BraceOpenTy t) [Elem (Token SemiColonTy t) constr t a] (Token BraceCloseTy t) 

Instances

Functor (constr t) => Functor (Block constr t) Source # 

Methods

fmap :: (a -> b) -> Block constr t a -> Block constr t b #

(<$) :: a -> Block constr t b -> Block constr t a #

Foldable (constr t) => Foldable (Block constr t) Source # 

Methods

fold :: Monoid m => Block constr t m -> m #

foldMap :: Monoid m => (a -> m) -> Block constr t a -> m #

foldr :: (a -> b -> b) -> b -> Block constr t a -> b #

foldr' :: (a -> b -> b) -> b -> Block constr t a -> b #

foldl :: (b -> a -> b) -> b -> Block constr t a -> b #

foldl' :: (b -> a -> b) -> b -> Block constr t a -> b #

foldr1 :: (a -> a -> a) -> Block constr t a -> a #

foldl1 :: (a -> a -> a) -> Block constr t a -> a #

toList :: Block constr t a -> [a] #

null :: Block constr t a -> Bool #

length :: Block constr t a -> Int #

elem :: Eq a => a -> Block constr t a -> Bool #

maximum :: Ord a => Block constr t a -> a #

minimum :: Ord a => Block constr t a -> a #

sum :: Num a => Block constr t a -> a #

product :: Num a => Block constr t a -> a #

Traversable (constr t) => Traversable (Block constr t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Block constr t a -> f (Block constr t b) #

sequenceA :: Applicative f => Block constr t (f a) -> f (Block constr t a) #

mapM :: Monad m => (a -> m b) -> Block constr t a -> m (Block constr t b) #

sequence :: Monad m => Block constr t (m a) -> m (Block constr t a) #

(Eq t, Eq1 (c t)) => Eq1 (Block c t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Block c t a -> Block c t b -> Bool #

(Eq t, Ord1 (c t)) => Ord1 (Block c t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Block c t a -> Block c t b -> Ordering #

Show1 (c t) => Show1 (Block c t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Block c t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Block c t a] -> ShowS #

(Eq (constr t a), Eq t) => Eq (Block constr t a) Source # 

Methods

(==) :: Block constr t a -> Block constr t a -> Bool #

(/=) :: Block constr t a -> Block constr t a -> Bool #

(Ord (constr t a), Ord t) => Ord (Block constr t a) Source # 

Methods

compare :: Block constr t a -> Block constr t a -> Ordering #

(<) :: Block constr t a -> Block constr t a -> Bool #

(<=) :: Block constr t a -> Block constr t a -> Bool #

(>) :: Block constr t a -> Block constr t a -> Bool #

(>=) :: Block constr t a -> Block constr t a -> Bool #

max :: Block constr t a -> Block constr t a -> Block constr t a #

min :: Block constr t a -> Block constr t a -> Block constr t a #

(Show (constr t a), Show t) => Show (Block constr t a) Source # 

Methods

showsPrec :: Int -> Block constr t a -> ShowS #

show :: Block constr t a -> String #

showList :: [Block constr t a] -> ShowS #

NoPos (c t a) => NoPos (Block c t a) Source # 

Methods

nopos :: Block c t a -> Block c t a Source #

Forget (Block ConstructorDef t a) [ConstructorDef t a] Source # 
Forget (Block Match t a) [Match t a] Source # 

Methods

forget :: Block Match t a -> [Match t a] Source #

data Arg t a Source #

Constructors

Arg Eps (Expr t a) 

Instances

Bitraversable Arg Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Arg a b -> f (Arg c d) #

Bifoldable Arg Source # 

Methods

bifold :: Monoid m => Arg m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Arg a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Arg a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Arg a b -> c #

Bifunctor Arg Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Arg a c -> Arg b d #

first :: (a -> b) -> Arg a c -> Arg b c #

second :: (b -> c) -> Arg a b -> Arg a c #

Functor (Arg t) Source # 

Methods

fmap :: (a -> b) -> Arg t a -> Arg t b #

(<$) :: a -> Arg t b -> Arg t a #

Foldable (Arg t) Source # 

Methods

fold :: Monoid m => Arg t m -> m #

foldMap :: Monoid m => (a -> m) -> Arg t a -> m #

foldr :: (a -> b -> b) -> b -> Arg t a -> b #

foldr' :: (a -> b -> b) -> b -> Arg t a -> b #

foldl :: (b -> a -> b) -> b -> Arg t a -> b #

foldl' :: (b -> a -> b) -> b -> Arg t a -> b #

foldr1 :: (a -> a -> a) -> Arg t a -> a #

foldl1 :: (a -> a -> a) -> Arg t a -> a #

toList :: Arg t a -> [a] #

null :: Arg t a -> Bool #

length :: Arg t a -> Int #

elem :: Eq a => a -> Arg t a -> Bool #

maximum :: Ord a => Arg t a -> a #

minimum :: Ord a => Arg t a -> a #

sum :: Num a => Arg t a -> a #

product :: Num a => Arg t a -> a #

Traversable (Arg t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Arg t a -> f (Arg t b) #

sequenceA :: Applicative f => Arg t (f a) -> f (Arg t a) #

mapM :: Monad m => (a -> m b) -> Arg t a -> m (Arg t b) #

sequence :: Monad m => Arg t (m a) -> m (Arg t a) #

Eq t => Eq1 (Arg t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Arg t a -> Arg t b -> Bool #

Ord t => Ord1 (Arg t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Arg t a -> Arg t b -> Ordering #

Show t => Show1 (Arg t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Arg t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Arg t a] -> ShowS #

(Eq t, Eq a) => Eq (Arg t a) Source # 

Methods

(==) :: Arg t a -> Arg t a -> Bool #

(/=) :: Arg t a -> Arg t a -> Bool #

(Ord t, Ord a) => Ord (Arg t a) Source # 

Methods

compare :: Arg t a -> Arg t a -> Ordering #

(<) :: Arg t a -> Arg t a -> Bool #

(<=) :: Arg t a -> Arg t a -> Bool #

(>) :: Arg t a -> Arg t a -> Bool #

(>=) :: Arg t a -> Arg t a -> Bool #

max :: Arg t a -> Arg t a -> Arg t a #

min :: Arg t a -> Arg t a -> Arg t a #

(Show t, Show a) => Show (Arg t a) Source # 

Methods

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

show :: Arg t a -> String #

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

NoPos (Arg t a) Source # 

Methods

nopos :: Arg t a -> Arg t a Source #

Forget (Arg t a) (Arg t a) Source # 

Methods

forget :: Arg t a -> Arg t a Source #

bitraverseArg :: Applicative f => (a -> f c) -> (b -> f d) -> Arg a b -> f (Arg c d) Source #

data Telescope t a Source #

Instances

Bitraversable Telescope Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Telescope a b -> f (Telescope c d) #

Bifoldable Telescope Source # 

Methods

bifold :: Monoid m => Telescope m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Telescope a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Telescope a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Telescope a b -> c #

Bifunctor Telescope Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Telescope a c -> Telescope b d #

first :: (a -> b) -> Telescope a c -> Telescope b c #

second :: (b -> c) -> Telescope a b -> Telescope a c #

Functor (Telescope t) Source # 

Methods

fmap :: (a -> b) -> Telescope t a -> Telescope t b #

(<$) :: a -> Telescope t b -> Telescope t a #

Foldable (Telescope t) Source # 

Methods

fold :: Monoid m => Telescope t m -> m #

foldMap :: Monoid m => (a -> m) -> Telescope t a -> m #

foldr :: (a -> b -> b) -> b -> Telescope t a -> b #

foldr' :: (a -> b -> b) -> b -> Telescope t a -> b #

foldl :: (b -> a -> b) -> b -> Telescope t a -> b #

foldl' :: (b -> a -> b) -> b -> Telescope t a -> b #

foldr1 :: (a -> a -> a) -> Telescope t a -> a #

foldl1 :: (a -> a -> a) -> Telescope t a -> a #

toList :: Telescope t a -> [a] #

null :: Telescope t a -> Bool #

length :: Telescope t a -> Int #

elem :: Eq a => a -> Telescope t a -> Bool #

maximum :: Ord a => Telescope t a -> a #

minimum :: Ord a => Telescope t a -> a #

sum :: Num a => Telescope t a -> a #

product :: Num a => Telescope t a -> a #

Traversable (Telescope t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Telescope t a -> f (Telescope t b) #

sequenceA :: Applicative f => Telescope t (f a) -> f (Telescope t a) #

mapM :: Monad m => (a -> m b) -> Telescope t a -> m (Telescope t b) #

sequence :: Monad m => Telescope t (m a) -> m (Telescope t a) #

Eq t => Eq1 (Telescope t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> Telescope t a -> Telescope t b -> Bool #

Ord t => Ord1 (Telescope t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> Telescope t a -> Telescope t b -> Ordering #

Show t => Show1 (Telescope t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Telescope t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Telescope t a] -> ShowS #

(Eq t, Eq a) => Eq (Telescope t a) Source # 

Methods

(==) :: Telescope t a -> Telescope t a -> Bool #

(/=) :: Telescope t a -> Telescope t a -> Bool #

(Ord t, Ord a) => Ord (Telescope t a) Source # 

Methods

compare :: Telescope t a -> Telescope t a -> Ordering #

(<) :: Telescope t a -> Telescope t a -> Bool #

(<=) :: Telescope t a -> Telescope t a -> Bool #

(>) :: Telescope t a -> Telescope t a -> Bool #

(>=) :: Telescope t a -> Telescope t a -> Bool #

max :: Telescope t a -> Telescope t a -> Telescope t a #

min :: Telescope t a -> Telescope t a -> Telescope t a #

(Show t, Show a) => Show (Telescope t a) Source # 

Methods

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

show :: Telescope t a -> String #

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

NoPos (Telescope t a) Source # 

Methods

nopos :: Telescope t a -> Telescope t a Source #

Forget (Telescope t a) (Telescope t a) Source # 

Methods

forget :: Telescope t a -> Telescope t a Source #

bitraverseTele :: Applicative f => (a -> f c) -> (b -> f d) -> Telescope a b -> f (Telescope c d) Source #

data ConstructorDef t a Source #

A Data constructor has a name and a telescope of arguments

Instances

Bitraversable ConstructorDef Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> ConstructorDef a b -> f (ConstructorDef c d) #

Bifoldable ConstructorDef Source # 

Methods

bifold :: Monoid m => ConstructorDef m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> ConstructorDef a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> ConstructorDef a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> ConstructorDef a b -> c #

Bifunctor ConstructorDef Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> ConstructorDef a c -> ConstructorDef b d #

first :: (a -> b) -> ConstructorDef a c -> ConstructorDef b c #

second :: (b -> c) -> ConstructorDef a b -> ConstructorDef a c #

Functor (ConstructorDef t) Source # 

Methods

fmap :: (a -> b) -> ConstructorDef t a -> ConstructorDef t b #

(<$) :: a -> ConstructorDef t b -> ConstructorDef t a #

Foldable (ConstructorDef t) Source # 

Methods

fold :: Monoid m => ConstructorDef t m -> m #

foldMap :: Monoid m => (a -> m) -> ConstructorDef t a -> m #

foldr :: (a -> b -> b) -> b -> ConstructorDef t a -> b #

foldr' :: (a -> b -> b) -> b -> ConstructorDef t a -> b #

foldl :: (b -> a -> b) -> b -> ConstructorDef t a -> b #

foldl' :: (b -> a -> b) -> b -> ConstructorDef t a -> b #

foldr1 :: (a -> a -> a) -> ConstructorDef t a -> a #

foldl1 :: (a -> a -> a) -> ConstructorDef t a -> a #

toList :: ConstructorDef t a -> [a] #

null :: ConstructorDef t a -> Bool #

length :: ConstructorDef t a -> Int #

elem :: Eq a => a -> ConstructorDef t a -> Bool #

maximum :: Ord a => ConstructorDef t a -> a #

minimum :: Ord a => ConstructorDef t a -> a #

sum :: Num a => ConstructorDef t a -> a #

product :: Num a => ConstructorDef t a -> a #

Traversable (ConstructorDef t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> ConstructorDef t a -> f (ConstructorDef t b) #

sequenceA :: Applicative f => ConstructorDef t (f a) -> f (ConstructorDef t a) #

mapM :: Monad m => (a -> m b) -> ConstructorDef t a -> m (ConstructorDef t b) #

sequence :: Monad m => ConstructorDef t (m a) -> m (ConstructorDef t a) #

Eq t => Eq1 (ConstructorDef t) Source # 

Methods

liftEq :: (a -> b -> Bool) -> ConstructorDef t a -> ConstructorDef t b -> Bool #

Ord t => Ord1 (ConstructorDef t) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> ConstructorDef t a -> ConstructorDef t b -> Ordering #

Show t => Show1 (ConstructorDef t) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ConstructorDef t a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ConstructorDef t a] -> ShowS #

(Eq t, Eq a) => Eq (ConstructorDef t a) Source # 
(Ord t, Ord a) => Ord (ConstructorDef t a) Source # 
(Show t, Show a) => Show (ConstructorDef t a) Source # 
NoPos (ConstructorDef t a, Maybe (Token SemiColonTy t)) Source # 
NoPos (ConstructorDef t a) Source # 
Forget (ConstructorDef t a, Maybe (Token SemiColonTy t)) (ConstructorDef t a) Source # 
Forget (ConstructorDef t a) (ConstructorDef t a) Source # 
Forget (Block ConstructorDef t a) [ConstructorDef t a] Source # 

data Decl t a Source #

Constructors

Sig t (Expr t a) 
Sig_ (Nm t) (Token ColonTy t) (Expr t a) 
Def t (Expr t a) 
Def_ (Nm t) (Token EqualTy t) (Expr t a) 
RecDef t (Expr t a) 
RecDef_ (Nm t) (Token EqualTy t) (Expr t a) 
Data t (Telescope t a) [ConstructorDef t a] 
Data_ (Token DataTokTy t) (Nm t) (Telescope t a) (Token ColonTy t) (Expr t a) (Token WhereTy t) (Block ConstructorDef t a) 

Instances

Bitraversable Decl Source # 

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Decl a b -> f (Decl c d) #

Bifoldable Decl Source # 

Methods

bifold :: Monoid m => Decl m m -> m #

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Decl a b -> m #

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Decl a b -> c #

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Decl a b -> c #

Bifunctor Decl Source # 

Methods

bimap :: (a -> b) -> (c -> d) -> Decl a c -> Decl b d #

first :: (a -> b) -> Decl a c -> Decl b c #

second :: (b -> c) -> Decl a b -> Decl a c #

Functor (Decl t) Source # 

Methods

fmap :: (a -> b) -> Decl t a -> Decl t b #

(<$) :: a -> Decl t b -> Decl t a #

Foldable (Decl t) Source # 

Methods

fold :: Monoid m => Decl t m -> m #

foldMap :: Monoid m => (a -> m) -> Decl t a -> m #

foldr :: (a -> b -> b) -> b -> Decl t a -> b #

foldr' :: (a -> b -> b) -> b -> Decl t a -> b #

foldl :: (b -> a -> b) -> b -> Decl t a -> b #

foldl' :: (b -> a -> b) -> b -> Decl t a -> b #

foldr1 :: (a -> a -> a) -> Decl t a -> a #

foldl1 :: (a -> a -> a) -> Decl t a -> a #

toList :: Decl t a -> [a] #

null :: Decl t a -> Bool #

length :: Decl t a -> Int #

elem :: Eq a => a -> Decl t a -> Bool #

maximum :: Ord a => Decl t a -> a #

minimum :: Ord a => Decl t a -> a #

sum :: Num a => Decl t a -> a #

product :: Num a => Decl t a -> a #

Traversable (Decl t) Source # 

Methods

traverse :: Applicative f => (a -> f b) -> Decl t a -> f (Decl t b) #

sequenceA :: Applicative f => Decl t (f a) -> f (Decl t a) #

mapM :: Monad m => (a -> m b) -> Decl t a -> m (Decl t b) #

sequence :: Monad m => Decl t (m a) -> m (Decl t a) #

Forget [Decl t a] [Decl t a] Source # 

Methods

forget :: [Decl t a] -> [Decl t a] Source #

T2S [Decl Text Text] [Decl String String] Source # 
(Eq t, Eq a) => Eq (Decl t a) Source # 

Methods

(==) :: Decl t a -> Decl t a -> Bool #

(/=) :: Decl t a -> Decl t a -> Bool #

(Ord t, Ord a) => Ord (Decl t a) Source # 

Methods

compare :: Decl t a -> Decl t a -> Ordering #

(<) :: Decl t a -> Decl t a -> Bool #

(<=) :: Decl t a -> Decl t a -> Bool #

(>) :: Decl t a -> Decl t a -> Bool #

(>=) :: Decl t a -> Decl t a -> Bool #

max :: Decl t a -> Decl t a -> Decl t a #

min :: Decl t a -> Decl t a -> Decl t a #

(Show t, Show a) => Show (Decl t a) Source # 

Methods

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

show :: Decl t a -> String #

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

NoPos (Decl t a) Source # 

Methods

nopos :: Decl t a -> Decl t a Source #

Forget (Decl t a) (Decl t a) Source # 

Methods

forget :: Decl t a -> Decl t a Source #

T2S (Decl Text Text) (Decl String String) Source # 

class Eq3 g where Source #

Minimal complete definition

liftEq3

Methods

liftEq3 :: (a -> b -> Bool) -> (c -> d -> Bool) -> (e -> f -> Bool) -> g a c e -> g b d f -> Bool Source #

Instances

Eq3 (,,) Source # 

Methods

liftEq3 :: (a -> b -> Bool) -> (c -> d -> Bool) -> (e -> f -> Bool) -> (a, c, e) -> (b, d, f) -> Bool Source #

class Eq3 g => Ord3 g where Source #

Minimal complete definition

liftCompare3

Methods

liftCompare3 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> (e -> f -> Ordering) -> g a c e -> g b d f -> Ordering Source #

Instances

Ord3 (,,) Source # 

Methods

liftCompare3 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> (e -> f -> Ordering) -> (a, c, e) -> (b, d, f) -> Ordering Source #

class Show3 f where Source #

Minimal complete definition

liftShowsPrec3

Methods

liftShowsPrec3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> Int -> f a b c -> ShowS Source #

liftShowList3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> [f a b c] -> ShowS Source #

Instances

Show3 (,,) Source # 

Methods

liftShowsPrec3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> Int -> (a, b, c) -> ShowS Source #

liftShowList3 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> (Int -> c -> ShowS) -> ([c] -> ShowS) -> [(a, b, c)] -> ShowS Source #

_Ann_ :: forall t a. Prism' (Expr t a) (Expr t a) Source #

_WitnessedAnnBnd_ :: forall t a. Prism' (Expr t a) (Pattern t, Token ColonTy t, Expr t a) Source #

_InferredAnnBnd_ :: forall t a. Prism' (Expr t a) (Pattern t, Expr t a) Source #

_WitnessedAnnEx_ :: forall t a. Prism' (Expr t a) (Expr t a, Token ColonTy t, Expr t a) Source #

_Ann :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Case_ :: forall t a. Prism' (Expr t a) (Token CaseTokTy t, Expr t a, Token OfTy t, Block Match t a, Annot t a) Source #

_Case :: forall t a. Prism' (Expr t a) (Expr t a, [Match t a], Annot t a) Source #

_Nat_ :: forall t a. Prism' (Expr t a) (Integer, t, Ws t) Source #

_Nat :: forall t a. Prism' (Expr t a) Integer Source #

_DCon_ :: forall t a. Prism' (Expr t a) (Nm t, [Arg t a], Annot t a) Source #

_DCon :: forall t a. Prism' (Expr t a) (t, [Arg t a], Annot t a) Source #

_TCon_ :: forall t a. Prism' (Expr t a) (Expr t a, [Expr t a]) Source #

_TCon :: forall t a. Prism' (Expr t a) (a, [Expr t a]) Source #

_Contra_ :: forall t a. Prism' (Expr t a) (Token ContraTokTy t, Expr t a, Annot t a) Source #

_Contra :: forall t a. Prism' (Expr t a) (Expr t a, Annot t a) Source #

_Subst_ :: forall t a. Prism' (Expr t a) (Token SubstTokTy t, Expr t a, Token ByTy t, Expr t a, Annot t a) Source #

_Subst :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Annot t a) Source #

_Refl_ :: forall t a. Prism' (Expr t a) (t, Ws t, Annot t a) Source #

_Refl :: forall t a. Prism' (Expr t a) (Annot t a) Source #

_TyEq_ :: forall t a. Prism' (Expr t a) (Expr t a, Token EqualTy t, Expr t a) Source #

_TyEq :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Let_ :: forall t a. Prism' (Expr t a) (Token LetTokTy t, Pattern t, Token EqualTy t, Expr t a, Token InTy t, Scope () (Expr t) a) Source #

_Let :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_Pcase :: forall t a. Prism' (Expr t a) (Expr t a, (t, t), Scope Int (Expr t) a, Annot t a) Source #

_Prod_ :: forall t a. Prism' (Expr t a) (Token ParenOpenTy t, Expr t a, Token CommaTy t, Expr t a, Token ParenCloseTy t, Annot t a) Source #

_Prod :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Annot t a) Source #

_Sigma_ :: forall t a. Prism' (Expr t a) (Token BraceOpenTy t, Pattern t, Token ColonTy t, Expr t a, Token VBarTy t, Scope () (Expr t) a, Token BraceCloseTy t) Source #

_Sigma :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_If_ :: forall t a. Prism' (Expr t a) (Token IfTokTy t, Expr t a, Token ThenTokTy t, Expr t a, Token ElseTokTy t, Expr t a, Annot t a) Source #

_If :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a, Expr t a, Annot t a) Source #

_LitBool_ :: forall t a. Prism' (Expr t a) (Bool, t, Ws t) Source #

_LitBool :: forall t a. Prism' (Expr t a) Bool Source #

_TyBool_ :: forall t a. Prism' (Expr t a) (t, Ws t) Source #

_TyBool :: forall t a. Prism' (Expr t a) () Source #

_LitUnit_ :: forall t a. Prism' (Expr t a) (t, Ws t) Source #

_LitUnit :: forall t a. Prism' (Expr t a) () Source #

_TyUnit_ :: forall t a. Prism' (Expr t a) (t, Ws t) Source #

_TyUnit :: forall t a. Prism' (Expr t a) () Source #

_TrustMe_ :: forall t a. Prism' (Expr t a) (t, Ws t, Annot t a) Source #

_TrustMe :: forall t a. Prism' (Expr t a) (Annot t a) Source #

_Position :: forall t a. Prism' (Expr t a) (Delta, Expr t a) Source #

_PiP_ :: forall t a. Prism' (Expr t a) (Eps, Expr t a, Token ArrowTy t, Scope () (Expr t) a) Source #

_PiP :: forall t a. Prism' (Expr t a) (Eps, Pattern t, Expr t a, Scope () (Expr t) a) Source #

_Pi_ :: forall t a. Prism' (Expr t a) (Expr t a, Token ArrowTy t, Scope () (Expr t) a) Source #

_Pi :: forall t a. Prism' (Expr t a) (t, Expr t a, Scope () (Expr t) a) Source #

_LamPAs_ :: forall t a. Prism' (Expr t a) (Token LamTokTy t, [(Eps, Pattern t, Annot t a)], Token DotTy t, Scope Int (Expr t) a) Source #

_LamPAs :: forall t a. Prism' (Expr t a) ([(Eps, t, Annot t a)], Scope Int (Expr t) a) Source #

_LamPA :: forall t a. Prism' (Expr t a) ((Eps, t, Annot t a), Scope () (Expr t) a) Source #

_Lams_ :: forall t a. Prism' (Expr t a) (Token LamTokTy t, [Pattern t], Token DotTy t, Scope Int (Expr t) a) Source #

_Lams :: forall t a. Prism' (Expr t a) ([t], Scope Int (Expr t) a) Source #

_ErasedLam_ :: forall t a. Prism' (Expr t a) (Token LamTokTy t, Pattern t, Token DotTy t, Scope () (Expr t) a) Source #

_ErasedLam :: forall t a. Prism' (Expr t a) (t, Scope () (Expr t) a) Source #

_Lams' :: forall t a. Prism' (Expr t a) ([t], Scope (Name String Int) (Expr t) a) Source #

_Lam' :: forall t a. Prism' (Expr t a) (t, Scope (Name String ()) (Expr t) a) Source #

_Lam_ :: forall t a. Prism' (Expr t a) (Token LamTokTy t, Pattern t, Token DotTy t, Scope () (Expr t) a) Source #

_Lam :: forall t a. Prism' (Expr t a) (t, Annot t a, Scope () (Expr t) a) Source #

_ErasedApp :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

(.:@) :: forall t a. Prism' (Expr t a) (Expr t a, Expr t a) Source #

_Type_ :: forall t a. Prism' (Expr t a) (t, Ws t) Source #

_Type :: forall t a. Prism' (Expr t a) () Source #

_Paren_ :: forall t a. Prism' (Expr t a) (Token ParenOpenTy t, Expr t a, Token ParenCloseTy t) Source #

_Paren :: forall t a. Prism' (Expr t a) (Expr t a) Source #

_BndV :: forall t a. Prism' (Expr t a) (t, Expr t a) Source #

_Ws_ :: forall t a. Prism' (Expr t a) (Expr t a, Ws t) Source #

_V :: forall t a. Prism' (Expr t a) a Source #

_Annot :: forall t a t a. Iso (Annot t a) (Annot t a) (Maybe (Expr t a)) (Maybe (Expr t a)) Source #

_Binder_ :: forall t. Prism' (Pattern t) (t, Ws t) Source #

_Binder :: forall t. Prism' (Pattern t) t Source #

_Witnessed :: forall t. Prism' (Pattern t) (Pattern t) Source #

_WildP :: forall t. Prism' (Pattern t) () Source #

_WildcardP :: forall t. Prism' (Pattern t) t Source #

_PatVar_ :: forall t. Prism' (Pattern t) (Nm t) Source #

_PatVar :: forall t. Prism' (Pattern t) t Source #

_PatCon_ :: forall t. Prism' (Pattern t) (Nm t, [(Eps, Pattern t)]) Source #

_PatCon :: forall t. Prism' (Pattern t) (t, [(Eps, Pattern t)]) Source #

_Data_ :: forall t a. Prism' (Decl t a) (Token DataTokTy t, Nm t, Telescope t a, Token ColonTy t, Expr t a, Token WhereTy t, Block ConstructorDef t a) Source #

_Data :: forall t a. Prism' (Decl t a) (t, Telescope t a, [ConstructorDef t a]) Source #

_RecDef_ :: forall t a. Prism' (Decl t a) (Nm t, Token EqualTy t, Expr t a) Source #

_RecDef :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

_Def_ :: forall t a. Prism' (Decl t a) (Nm t, Token EqualTy t, Expr t a) Source #

_Def :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

_Sig_ :: forall t a. Prism' (Decl t a) (Nm t, Token ColonTy t, Expr t a) Source #

_Sig :: forall t a. Prism' (Decl t a) (t, Expr t a) Source #

Orphan instances

(Eq a, Eq b) => Eq1 ((,,) a b) Source # 

Methods

liftEq :: (a -> b -> Bool) -> (a, b, a) -> (a, b, b) -> Bool #

(Ord a, Ord b) => Ord1 ((,,) a b) Source # 

Methods

liftCompare :: (a -> b -> Ordering) -> (a, b, a) -> (a, b, b) -> Ordering #

(Show a, Show b) => Show1 ((,,) a b) Source # 

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> (a, b, a) -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [(a, b, a)] -> ShowS #