pire-0.2.5

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

Syntax

Contents

Description

Pire's flavour of Pi-forall syntax, copied from Pi-forall, and adapted to Bound, Bound usage inspired by Ermine

Synopsis

Documentation

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 #

data Pattern t Source #

Constructors

PatCon t [(Eps, Pattern t)] 
PatVar t 
WildcardP t 
WildP 
Witnessed (Pattern t) 
SizeP (Size t) 

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 #

data Expr t a Source #

Constructors

V a

variables

BndV t (Expr t a) 
SizeE (Size t) 
Paren (Expr t a) 
Type

type of types

(Expr t a) :@ (Expr t a) infixl 9

application

ErasedApp (Expr t a) (Expr t a) 
Lam t (Annot t a) (Scope () (Expr t) a)

abstraction

Lam' t (Scope (Name String ()) (Expr t) a) 
Lams' [t] (Scope (Name String Int) (Expr t) a) 
ErasedLam t (Scope () (Expr t) a) 
Lams [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) 
Pi t (Expr t a) (Scope () (Expr t) a) 
PiP Eps (Pattern t) (Expr t a) (Scope () (Expr t) a) 
Position Delta (Expr t a) 
TrustMe (Annot t a)

an axiom TRUSTME, inhabits all types

TyUnit 
LitUnit 
TyBool 
LitBool Bool 
If (Expr t a) (Expr t a) (Expr t a) (Annot t a) 
Sigma t (Expr t a) (Scope () (Expr t) a)

sigma type `{ x : A | B }`

Prod (Expr t a) (Expr t a) (Annot t a)

introduction for sigmas `( a , b )`

Pcase (Expr t a) (t, t) (Scope Int (Expr t) a) (Annot t a)

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

Let t (Expr t a) (Scope () (Expr t) a) 
TyEq (Expr t a) (Expr t a) 
Refl (Annot t a) 
Subst (Expr t a) (Expr t a) (Annot t a) 
Contra (Expr t a) (Annot t a) 
TCon a [Expr t a] 
DCon t [Arg t a] (Annot t a) 
Nat Integer 
Case (Expr t a) [Match t a] (Annot t a) 
Ann (Expr t a) (Expr t a)

Annotated terms `( x : 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 #

Ord a => SSubstitutable a (Expr a a) Source # 

Methods

sapply :: SSubst a -> Expr a a -> Expr a a Source #

fsv :: Expr a a -> Set (SVar a) Source #

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, TT t a) Source # 

Methods

nopos :: (Expr t a, TT t a) -> (Expr t a, TT t a) Source #

NoPos (Expr t a) Source # 

Methods

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

S2T (Expr String String) (Expr Text Text) 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 #

type Annot t a = Maybe (Expr t a) Source #

data Annot_ t a Source #

Constructors

Annot_ (Maybe (Expr t a)) 

Instances

Monad (Annot_ t) Source # 

Methods

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

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

return :: a -> Annot_ t a #

fail :: String -> Annot_ t a #

Functor (Annot_ t) Source # 

Methods

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

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

Applicative (Annot_ t) Source # 

Methods

pure :: a -> Annot_ t a #

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

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

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

(<*) :: Annot_ t 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) #

data Match t a Source #

Constructors

Match (Pattern 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 #

S2T (Match String String) (Match Text Text) Source # 

bitraverseMatch :: Applicative f => (a -> f c) -> (b -> f d) -> Match a b -> f (Match c d) 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, TT t a) Source # 

Methods

nopos :: (Arg t a, TT t a) -> (Arg t a, TT t a) Source #

NoPos (Arg t a) Source # 

Methods

nopos :: 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 Decl t a Source #

Constructors

Sig t (Expr t a) 
Def t (Expr t a) 
RecDef t (Expr t a) 
Data t (Telescope t a) [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) #

Eq t => Eq1 (Decl t) Source # 

Methods

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

Ord t => Ord1 (Decl t) Source # 

Methods

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

Show t => Show1 (Decl t) Source # 

Methods

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

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

S2T [Decl String String] [Decl Text Text] 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, TT t a) Source # 

Methods

nopos :: (Decl t a, TT t a) -> (Decl t a, TT t a) Source #

NoPos (Decl t a) Source # 

Methods

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

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

data Telescope t a Source #

Constructors

EmptyTele 
ConsP Eps (Pattern t) (Expr t a) (Telescope t a) 
Constraint (Expr t a) (Expr t a) (Telescope t a) 

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 #

S2T (Telescope String String) (Telescope Text Text) 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

Constructors

ConstructorDef Delta t (Telescope t a) 
ConstructorDef' t (Telescope t a) 

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, TT t a) Source # 

Methods

nopos :: (ConstructorDef t a, TT t a) -> (ConstructorDef t a, TT t a) Source #

NoPos (ConstructorDef t a) Source # 
S2T (ConstructorDef String String) (ConstructorDef Text Text) Source # 

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 # 
S2T (ConstructorNames String) (ConstructorNames Text) Source # 
T2S (ConstructorNames Text) (ConstructorNames String) Source # 

emptyConstructorNames :: ConstructorNames Text Source #

empty set of constructor names

data ModuleImport t Source #

Constructors

ModuleImport t 

Instances

Functor ModuleImport Source # 

Methods

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

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

Foldable ModuleImport Source # 

Methods

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

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

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

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

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

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

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

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

toList :: ModuleImport a -> [a] #

null :: ModuleImport a -> Bool #

length :: ModuleImport a -> Int #

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

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

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

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

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

Traversable ModuleImport Source # 

Methods

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

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

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

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

Eq t => Eq (ModuleImport t) Source # 
Ord t => Ord (ModuleImport t) Source # 
Show t => Show (ModuleImport t) Source # 
S2T [ModuleImport String] [ModuleImport Text] Source # 
S2T (ModuleImport String) (ModuleImport Text) Source # 
T2S [ModuleImport Text] [ModuleImport String] Source # 
T2S (ModuleImport Text) (ModuleImport String) Source # 

data Module t a Source #

Constructors

Module 

Fields

Instances

Functor (Module t) Source # 

Methods

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

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

Foldable (Module t) Source # 

Methods

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

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

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

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

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

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

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

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

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

null :: Module t a -> Bool #

length :: Module t a -> Int #

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

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

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

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

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

Traversable (Module t) Source # 

Methods

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

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

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

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

Eq t => Eq1 (Module t) Source # 

Methods

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

Ord t => Ord1 (Module t) Source # 

Methods

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

Show t => Show1 (Module t) Source # 

Methods

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

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

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

Methods

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

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

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

Methods

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

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

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

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

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

max :: Module t a -> Module t a -> Module t a #

min :: Module t a -> Module t a -> Module t a #

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

Methods

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

show :: Module t a -> String #

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

NoPos (Module t a, TT t a) Source # 

Methods

nopos :: (Module t a, TT t a) -> (Module t a, TT t a) Source #

NoPos (Module t a) Source # 

Methods

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

S2T (Module String String) (Module Text Text) Source # 
T2S (Module Text Text, TT Text Text) (Module String String, TT String String) Source # 
T2S (Module Text Text) (Module String String) Source # 

mnm :: forall t a. Lens' (Module t a) t Source #

imports :: forall t a. Lens' (Module t a) [ModuleImport t] Source #

decls :: forall t a a. Lens (Module t a) (Module t a) [Decl t a] [Decl t a] Source #

constrs :: forall t a. Lens' (Module t a) (ConstructorNames t) 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, Expr 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 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) (a, [Expr 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) (Expr t a, Expr t a, 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, 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) (Expr t a, Expr t a, Annot t a) 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) (Expr t a, Expr t a, Expr t a, Annot t a) Source #

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

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

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

_TyUnit :: forall t a. Prism' (Expr 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, Pattern t, Expr t a, 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) ([(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) ([t], Scope Int (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) (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) () Source #

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

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

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

_V :: forall t a. Prism' (Expr t a) 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) (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) (t, Expr t a) Source #

_SizeP :: forall t. Prism' (Pattern t) (Size 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) t Source #

_PatCon :: forall t. Prism' (Pattern t) (t, [(Eps, Pattern t)]) 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 #