lambda-pi-0.0.3: λΠ-calculus implemented in a few different ways.
Safe HaskellNone
LanguageHaskell2010

Language.LambdaPi.Syntax.Abs

Description

The abstract syntax of language Syntax.

Synopsis

Documentation

type Program = Program' BNFC'Position Source #

data Program' a Source #

Constructors

AProgram a [Command' a] 

Instances

Instances details
Foldable Program' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fold :: Monoid m => Program' m -> m #

foldMap :: Monoid m => (a -> m) -> Program' a -> m #

foldMap' :: Monoid m => (a -> m) -> Program' a -> m #

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

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

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

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

foldr1 :: (a -> a -> a) -> Program' a -> a #

foldl1 :: (a -> a -> a) -> Program' a -> a #

toList :: Program' a -> [a] #

null :: Program' a -> Bool #

length :: Program' a -> Int #

elem :: Eq a => a -> Program' a -> Bool #

maximum :: Ord a => Program' a -> a #

minimum :: Ord a => Program' a -> a #

sum :: Num a => Program' a -> a #

product :: Num a => Program' a -> a #

Traversable Program' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

sequenceA :: Applicative f => Program' (f a) -> f (Program' a) #

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

sequence :: Monad m => Program' (m a) -> m (Program' a) #

Functor Program' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fmap :: (a -> b) -> Program' a -> Program' b #

(<$) :: a -> Program' b -> Program' a #

HasPosition Program Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Program -> BNFC'Position Source #

Data a => Data (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Program' a -> c (Program' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Program' a) #

toConstr :: Program' a -> Constr #

dataTypeOf :: Program' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Program' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Program' a)) #

gmapT :: (forall b. Data b => b -> b) -> Program' a -> Program' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Program' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Program' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Program' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Program' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Program' a -> m (Program' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Program' a -> m (Program' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Program' a -> m (Program' a) #

Generic (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep (Program' a) 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Program' a) = D1 ('MetaData "Program'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "AProgram" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Command' a])))

Methods

from :: Program' a -> Rep (Program' a) x #

to :: Rep (Program' a) x -> Program' a #

Read a => Read (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS (Program' a) #

readList :: ReadS [Program' a] #

readPrec :: ReadPrec (Program' a) #

readListPrec :: ReadPrec [Program' a] #

Show a => Show (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> Program' a -> ShowS #

show :: Program' a -> String #

showList :: [Program' a] -> ShowS #

Eq a => Eq (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

(==) :: Program' a -> Program' a -> Bool #

(/=) :: Program' a -> Program' a -> Bool #

Ord a => Ord (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: Program' a -> Program' a -> Ordering #

(<) :: Program' a -> Program' a -> Bool #

(<=) :: Program' a -> Program' a -> Bool #

(>) :: Program' a -> Program' a -> Bool #

(>=) :: Program' a -> Program' a -> Bool #

max :: Program' a -> Program' a -> Program' a #

min :: Program' a -> Program' a -> Program' a #

Print (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> Program' a -> Doc Source #

type Rep (Program' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Program' a) = D1 ('MetaData "Program'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "AProgram" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Command' a])))

type Command = Command' BNFC'Position Source #

data Command' a Source #

Constructors

CommandCheck a (Term' a) (Term' a) 
CommandCompute a (Term' a) (Term' a) 

Instances

Instances details
Foldable Command' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fold :: Monoid m => Command' m -> m #

foldMap :: Monoid m => (a -> m) -> Command' a -> m #

foldMap' :: Monoid m => (a -> m) -> Command' a -> m #

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

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

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

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

foldr1 :: (a -> a -> a) -> Command' a -> a #

foldl1 :: (a -> a -> a) -> Command' a -> a #

toList :: Command' a -> [a] #

null :: Command' a -> Bool #

length :: Command' a -> Int #

elem :: Eq a => a -> Command' a -> Bool #

maximum :: Ord a => Command' a -> a #

minimum :: Ord a => Command' a -> a #

sum :: Num a => Command' a -> a #

product :: Num a => Command' a -> a #

Traversable Command' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

sequenceA :: Applicative f => Command' (f a) -> f (Command' a) #

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

sequence :: Monad m => Command' (m a) -> m (Command' a) #

Functor Command' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fmap :: (a -> b) -> Command' a -> Command' b #

(<$) :: a -> Command' b -> Command' a #

HasPosition Command Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Command -> BNFC'Position Source #

Data a => Data (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Command' a -> c (Command' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Command' a) #

toConstr :: Command' a -> Constr #

dataTypeOf :: Command' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Command' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Command' a)) #

gmapT :: (forall b. Data b => b -> b) -> Command' a -> Command' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Command' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Command' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Command' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Command' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Command' a -> m (Command' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Command' a -> m (Command' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Command' a -> m (Command' a) #

Generic (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep (Command' a) 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Command' a) = D1 ('MetaData "Command'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "CommandCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "CommandCompute" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))

Methods

from :: Command' a -> Rep (Command' a) x #

to :: Rep (Command' a) x -> Command' a #

Read a => Read (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS (Command' a) #

readList :: ReadS [Command' a] #

readPrec :: ReadPrec (Command' a) #

readListPrec :: ReadPrec [Command' a] #

Show a => Show (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> Command' a -> ShowS #

show :: Command' a -> String #

showList :: [Command' a] -> ShowS #

Eq a => Eq (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

(==) :: Command' a -> Command' a -> Bool #

(/=) :: Command' a -> Command' a -> Bool #

Ord a => Ord (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: Command' a -> Command' a -> Ordering #

(<) :: Command' a -> Command' a -> Bool #

(<=) :: Command' a -> Command' a -> Bool #

(>) :: Command' a -> Command' a -> Bool #

(>=) :: Command' a -> Command' a -> Bool #

max :: Command' a -> Command' a -> Command' a #

min :: Command' a -> Command' a -> Command' a #

Print (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> Command' a -> Doc Source #

Print [Command' a] Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> [Command' a] -> Doc Source #

type Rep (Command' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Command' a) = D1 ('MetaData "Command'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "CommandCheck" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "CommandCompute" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))

type Term = Term' BNFC'Position Source #

data Term' a Source #

Constructors

Var a VarIdent 
Pi a (Pattern' a) (Term' a) (ScopedTerm' a) 
Lam a (Pattern' a) (ScopedTerm' a) 
App a (Term' a) (Term' a) 
Product a (Term' a) (Term' a) 
Pair a (Term' a) (Term' a) 
First a (Term' a) 
Second a (Term' a) 
Universe a 

Instances

Instances details
Foldable Term' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fold :: Monoid m => Term' m -> m #

foldMap :: Monoid m => (a -> m) -> Term' a -> m #

foldMap' :: Monoid m => (a -> m) -> Term' a -> m #

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

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

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

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

foldr1 :: (a -> a -> a) -> Term' a -> a #

foldl1 :: (a -> a -> a) -> Term' a -> a #

toList :: Term' a -> [a] #

null :: Term' a -> Bool #

length :: Term' a -> Int #

elem :: Eq a => a -> Term' a -> Bool #

maximum :: Ord a => Term' a -> a #

minimum :: Ord a => Term' a -> a #

sum :: Num a => Term' a -> a #

product :: Num a => Term' a -> a #

Traversable Term' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

sequenceA :: Applicative f => Term' (f a) -> f (Term' a) #

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

sequence :: Monad m => Term' (m a) -> m (Term' a) #

Functor Term' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fmap :: (a -> b) -> Term' a -> Term' b #

(<$) :: a -> Term' b -> Term' a #

HasPosition Term Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Term -> BNFC'Position Source #

Data a => Data (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Term' a -> c (Term' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Term' a) #

toConstr :: Term' a -> Constr #

dataTypeOf :: Term' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Term' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Term' a)) #

gmapT :: (forall b. Data b => b -> b) -> Term' a -> Term' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Term' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Term' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Term' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Term' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Term' a -> m (Term' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Term' a -> m (Term' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Term' a -> m (Term' a) #

Generic (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep (Term' a) 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Term' a) = D1 ('MetaData "Term'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarIdent)) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ScopedTerm' a))))) :+: (C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ScopedTerm' a)))) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))) :+: ((C1 ('MetaCons "Product" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "Pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))) :+: (C1 ('MetaCons "First" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))) :+: (C1 ('MetaCons "Second" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))) :+: C1 ('MetaCons "Universe" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))))

Methods

from :: Term' a -> Rep (Term' a) x #

to :: Rep (Term' a) x -> Term' a #

Read a => Read (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS (Term' a) #

readList :: ReadS [Term' a] #

readPrec :: ReadPrec (Term' a) #

readListPrec :: ReadPrec [Term' a] #

Show a => Show (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> Term' a -> ShowS #

show :: Term' a -> String #

showList :: [Term' a] -> ShowS #

Eq a => Eq (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

(==) :: Term' a -> Term' a -> Bool #

(/=) :: Term' a -> Term' a -> Bool #

Ord a => Ord (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: Term' a -> Term' a -> Ordering #

(<) :: Term' a -> Term' a -> Bool #

(<=) :: Term' a -> Term' a -> Bool #

(>) :: Term' a -> Term' a -> Bool #

(>=) :: Term' a -> Term' a -> Bool #

max :: Term' a -> Term' a -> Term' a #

min :: Term' a -> Term' a -> Term' a #

Print (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> Term' a -> Doc Source #

type Rep (Term' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Term' a) = D1 ('MetaData "Term'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (((C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarIdent)) :+: C1 ('MetaCons "Pi" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a))) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ScopedTerm' a))))) :+: (C1 ('MetaCons "Lam" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ScopedTerm' a)))) :+: C1 ('MetaCons "App" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))) :+: ((C1 ('MetaCons "Product" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "Pair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))) :+: (C1 ('MetaCons "First" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))) :+: (C1 ('MetaCons "Second" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))) :+: C1 ('MetaCons "Universe" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))))

type ScopedTerm = ScopedTerm' BNFC'Position Source #

data ScopedTerm' a Source #

Constructors

AScopedTerm a (Term' a) 

Instances

Instances details
Foldable ScopedTerm' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fold :: Monoid m => ScopedTerm' m -> m #

foldMap :: Monoid m => (a -> m) -> ScopedTerm' a -> m #

foldMap' :: Monoid m => (a -> m) -> ScopedTerm' a -> m #

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

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

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

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

foldr1 :: (a -> a -> a) -> ScopedTerm' a -> a #

foldl1 :: (a -> a -> a) -> ScopedTerm' a -> a #

toList :: ScopedTerm' a -> [a] #

null :: ScopedTerm' a -> Bool #

length :: ScopedTerm' a -> Int #

elem :: Eq a => a -> ScopedTerm' a -> Bool #

maximum :: Ord a => ScopedTerm' a -> a #

minimum :: Ord a => ScopedTerm' a -> a #

sum :: Num a => ScopedTerm' a -> a #

product :: Num a => ScopedTerm' a -> a #

Traversable ScopedTerm' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

sequenceA :: Applicative f => ScopedTerm' (f a) -> f (ScopedTerm' a) #

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

sequence :: Monad m => ScopedTerm' (m a) -> m (ScopedTerm' a) #

Functor ScopedTerm' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fmap :: (a -> b) -> ScopedTerm' a -> ScopedTerm' b #

(<$) :: a -> ScopedTerm' b -> ScopedTerm' a #

HasPosition ScopedTerm Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: ScopedTerm -> BNFC'Position Source #

Data a => Data (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ScopedTerm' a -> c (ScopedTerm' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ScopedTerm' a) #

toConstr :: ScopedTerm' a -> Constr #

dataTypeOf :: ScopedTerm' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ScopedTerm' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ScopedTerm' a)) #

gmapT :: (forall b. Data b => b -> b) -> ScopedTerm' a -> ScopedTerm' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ScopedTerm' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ScopedTerm' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> ScopedTerm' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> ScopedTerm' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> ScopedTerm' a -> m (ScopedTerm' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopedTerm' a -> m (ScopedTerm' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ScopedTerm' a -> m (ScopedTerm' a) #

Generic (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep (ScopedTerm' a) 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (ScopedTerm' a) = D1 ('MetaData "ScopedTerm'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "AScopedTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))

Methods

from :: ScopedTerm' a -> Rep (ScopedTerm' a) x #

to :: Rep (ScopedTerm' a) x -> ScopedTerm' a #

Read a => Read (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS (ScopedTerm' a) #

readList :: ReadS [ScopedTerm' a] #

readPrec :: ReadPrec (ScopedTerm' a) #

readListPrec :: ReadPrec [ScopedTerm' a] #

Show a => Show (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> ScopedTerm' a -> ShowS #

show :: ScopedTerm' a -> String #

showList :: [ScopedTerm' a] -> ShowS #

Eq a => Eq (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

(==) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

(/=) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

Ord a => Ord (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: ScopedTerm' a -> ScopedTerm' a -> Ordering #

(<) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

(<=) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

(>) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

(>=) :: ScopedTerm' a -> ScopedTerm' a -> Bool #

max :: ScopedTerm' a -> ScopedTerm' a -> ScopedTerm' a #

min :: ScopedTerm' a -> ScopedTerm' a -> ScopedTerm' a #

Print (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> ScopedTerm' a -> Doc Source #

type Rep (ScopedTerm' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (ScopedTerm' a) = D1 ('MetaData "ScopedTerm'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "AScopedTerm" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))

type Pattern = Pattern' BNFC'Position Source #

data Pattern' a Source #

Constructors

PatternWildcard a 
PatternVar a VarIdent 
PatternPair a (Pattern' a) (Pattern' a) 

Instances

Instances details
Foldable Pattern' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

foldMap :: Monoid m => (a -> m) -> Pattern' a -> 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 # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

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

Functor Pattern' Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

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

HasPosition Pattern Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Pattern -> BNFC'Position Source #

Data a => Data (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Pattern' a -> c (Pattern' a) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Pattern' a) #

toConstr :: Pattern' a -> Constr #

dataTypeOf :: Pattern' a -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Pattern' a)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Pattern' a)) #

gmapT :: (forall b. Data b => b -> b) -> Pattern' a -> Pattern' a #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' a -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Pattern' a -> r #

gmapQ :: (forall d. Data d => d -> u) -> Pattern' a -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Pattern' a -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Pattern' a -> m (Pattern' a) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' a -> m (Pattern' a) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Pattern' a -> m (Pattern' a) #

Generic (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep (Pattern' a) 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Pattern' a) = D1 ('MetaData "Pattern'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "PatternWildcard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "PatternVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarIdent)) :+: C1 ('MetaCons "PatternPair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a))))))

Methods

from :: Pattern' a -> Rep (Pattern' a) x #

to :: Rep (Pattern' a) x -> Pattern' a #

Read a => Read (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS (Pattern' a) #

readList :: ReadS [Pattern' a] #

readPrec :: ReadPrec (Pattern' a) #

readListPrec :: ReadPrec [Pattern' a] #

Show a => Show (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> Pattern' a -> ShowS #

show :: Pattern' a -> String #

showList :: [Pattern' a] -> ShowS #

Eq a => Eq (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

(==) :: Pattern' a -> Pattern' a -> Bool #

(/=) :: Pattern' a -> Pattern' a -> Bool #

Ord a => Ord (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: Pattern' a -> Pattern' a -> Ordering #

(<) :: Pattern' a -> Pattern' a -> Bool #

(<=) :: Pattern' a -> Pattern' a -> Bool #

(>) :: Pattern' a -> Pattern' a -> Bool #

(>=) :: Pattern' a -> Pattern' a -> Bool #

max :: Pattern' a -> Pattern' a -> Pattern' a #

min :: Pattern' a -> Pattern' a -> Pattern' a #

Print (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> Pattern' a -> Doc Source #

type Rep (Pattern' a) Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep (Pattern' a) = D1 ('MetaData "Pattern'" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'False) (C1 ('MetaCons "PatternWildcard" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "PatternVar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarIdent)) :+: C1 ('MetaCons "PatternPair" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a))))))

newtype VarIdent Source #

Constructors

VarIdent String 

Instances

Instances details
Data VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarIdent -> c VarIdent #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarIdent #

toConstr :: VarIdent -> Constr #

dataTypeOf :: VarIdent -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarIdent) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarIdent) #

gmapT :: (forall b. Data b => b -> b) -> VarIdent -> VarIdent #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent -> r #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent -> r #

gmapQ :: (forall d. Data d => d -> u) -> VarIdent -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> VarIdent -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent #

IsString VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

fromString :: String -> VarIdent #

Generic VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Associated Types

type Rep VarIdent 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep VarIdent = D1 ('MetaData "VarIdent" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'True) (C1 ('MetaCons "VarIdent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

Methods

from :: VarIdent -> Rep VarIdent x #

to :: Rep VarIdent x -> VarIdent #

Read VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

readsPrec :: Int -> ReadS VarIdent #

readList :: ReadS [VarIdent] #

readPrec :: ReadPrec VarIdent #

readListPrec :: ReadPrec [VarIdent] #

Show VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

showsPrec :: Int -> VarIdent -> ShowS #

show :: VarIdent -> String #

showList :: [VarIdent] -> ShowS #

Eq VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

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

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

Ord VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

compare :: VarIdent -> VarIdent -> Ordering #

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

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

(>) :: VarIdent -> VarIdent -> Bool #

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

max :: VarIdent -> VarIdent -> VarIdent #

min :: VarIdent -> VarIdent -> VarIdent #

Print VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Print

Methods

prt :: Int -> VarIdent -> Doc Source #

type Rep VarIdent Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

type Rep VarIdent = D1 ('MetaData "VarIdent" "Language.LambdaPi.Syntax.Abs" "lambda-pi-0.0.3-7GwYCUqrluZKwNszUSptwm" 'True) (C1 ('MetaCons "VarIdent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

type BNFC'Position = Maybe (Int, Int) Source #

Start position (line, column) of something.

pattern BNFC'NoPosition :: BNFC'Position Source #

pattern BNFC'Position :: Int -> Int -> BNFC'Position Source #

class HasPosition a where Source #

Get the start position of something.

Methods

hasPosition :: a -> BNFC'Position Source #

Instances

Instances details
HasPosition Command Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Command -> BNFC'Position Source #

HasPosition Pattern Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Pattern -> BNFC'Position Source #

HasPosition Program Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Program -> BNFC'Position Source #

HasPosition ScopedTerm Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: ScopedTerm -> BNFC'Position Source #

HasPosition Term Source # 
Instance details

Defined in Language.LambdaPi.Syntax.Abs

Methods

hasPosition :: Term -> BNFC'Position Source #