LambdaCube.STLC.Ast

Documentation

data ExtLCTerm

Constructors

ExtLCVar Text

ExtLCLam Text ExtLCType ExtLCTerm

ExtLCApp ExtLCTerm ExtLCTerm infixl 6

ExtLCMVar String

Instances

Eq ExtLCTerm

Defined in LambdaCube.STLC.Ast

Methods

(==) :: ExtLCTerm -> ExtLCTerm -> Bool

(/=) :: ExtLCTerm -> ExtLCTerm -> Bool

Data ExtLCTerm

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: ExtLCTerm -> Constr

dataTypeOf :: ExtLCTerm -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> ExtLCTerm -> ExtLCTerm

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

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

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

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

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

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

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

Show ExtLCTerm

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> ExtLCTerm -> ShowS

show :: ExtLCTerm -> String

showList :: [ExtLCTerm] -> ShowS

Lift ExtLCTerm

Defined in LambdaCube.STLC.Ast

Methods

lift :: ExtLCTerm -> Q Exp

liftTyped :: ExtLCTerm -> Q (TExp ExtLCTerm)

data ExtLCType

Constructors

ExtLCBase

ExtLCArr ExtLCType ExtLCType infixr 5

ExtLCMTVar String

Instances

Eq ExtLCType

Defined in LambdaCube.STLC.Ast

Methods

(==) :: ExtLCType -> ExtLCType -> Bool

(/=) :: ExtLCType -> ExtLCType -> Bool

Data ExtLCType

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: ExtLCType -> Constr

dataTypeOf :: ExtLCType -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> ExtLCType -> ExtLCType

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

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

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

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

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

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

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

Show ExtLCType

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> ExtLCType -> ShowS

show :: ExtLCType -> String

showList :: [ExtLCType] -> ShowS

Lift ExtLCType

Defined in LambdaCube.STLC.Ast

Methods

lift :: ExtLCType -> Q Exp

liftTyped :: ExtLCType -> Q (TExp ExtLCType)

data LCTerm

Constructors

LCVar Int

LCLam LCType LCTerm

LCApp LCTerm LCTerm infixl 6

Instances

Eq LCTerm

Defined in LambdaCube.STLC.Ast

Methods

(==) :: LCTerm -> LCTerm -> Bool

(/=) :: LCTerm -> LCTerm -> Bool

Data LCTerm

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: LCTerm -> Constr

dataTypeOf :: LCTerm -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> LCTerm -> LCTerm

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

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

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

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

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

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

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

Show LCTerm

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> LCTerm -> ShowS

show :: LCTerm -> String

showList :: [LCTerm] -> ShowS

Lift LCTerm

Defined in LambdaCube.STLC.Ast

Methods

lift :: LCTerm -> Q Exp

liftTyped :: LCTerm -> Q (TExp LCTerm)

data LCType

Constructors

LCBase

LCArr LCType LCType infixr 5

Instances

Eq LCType

Defined in LambdaCube.STLC.Ast

Methods

(==) :: LCType -> LCType -> Bool

(/=) :: LCType -> LCType -> Bool

Data LCType

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: LCType -> Constr

dataTypeOf :: LCType -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> LCType -> LCType

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

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

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

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

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

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

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

Show LCType

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> LCType -> ShowS

show :: LCType -> String

showList :: [LCType] -> ShowS

Lift LCType

Defined in LambdaCube.STLC.Ast

Methods

lift :: LCType -> Q Exp

liftTyped :: LCType -> Q (TExp LCType)

data LCValue

Constructors

LCValLam LCType LCTerm

Instances

Eq LCValue

Defined in LambdaCube.STLC.Ast

Methods

(==) :: LCValue -> LCValue -> Bool

(/=) :: LCValue -> LCValue -> Bool

Data LCValue

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: LCValue -> Constr

dataTypeOf :: LCValue -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> LCValue -> LCValue

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

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

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

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

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

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

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

Show LCValue

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> LCValue -> ShowS

show :: LCValue -> String

showList :: [LCValue] -> ShowS

Lift LCValue

Defined in LambdaCube.STLC.Ast

Methods

lift :: LCValue -> Q Exp

liftTyped :: LCValue -> Q (TExp LCValue)

data LCNormalTerm

Constructors

LCNormLam LCType LCNormalTerm

LCNormNeut LCNeutralTerm

Instances

Eq LCNormalTerm

Defined in LambdaCube.STLC.Ast

Methods

(==) :: LCNormalTerm -> LCNormalTerm -> Bool

(/=) :: LCNormalTerm -> LCNormalTerm -> Bool

Data LCNormalTerm

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: LCNormalTerm -> Constr

dataTypeOf :: LCNormalTerm -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> LCNormalTerm -> LCNormalTerm

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

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

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

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

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

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

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

Show LCNormalTerm

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> LCNormalTerm -> ShowS

show :: LCNormalTerm -> String

showList :: [LCNormalTerm] -> ShowS

Lift LCNormalTerm

Defined in LambdaCube.STLC.Ast

Methods

lift :: LCNormalTerm -> Q Exp

liftTyped :: LCNormalTerm -> Q (TExp LCNormalTerm)

data LCNeutralTerm

Constructors

LCNeutVar Int

LCNeutApp LCNeutralTerm LCNormalTerm infixl 6

Instances

Eq LCNeutralTerm

Defined in LambdaCube.STLC.Ast

Methods

(==) :: LCNeutralTerm -> LCNeutralTerm -> Bool

(/=) :: LCNeutralTerm -> LCNeutralTerm -> Bool

Data LCNeutralTerm

Defined in LambdaCube.STLC.Ast

Methods

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

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

toConstr :: LCNeutralTerm -> Constr

dataTypeOf :: LCNeutralTerm -> DataType

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

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

gmapT :: (forall b. Data b => b -> b) -> LCNeutralTerm -> LCNeutralTerm

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

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

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

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

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

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

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

Show LCNeutralTerm

Defined in LambdaCube.STLC.Ast

Methods

showsPrec :: Int -> LCNeutralTerm -> ShowS

show :: LCNeutralTerm -> String

showList :: [LCNeutralTerm] -> ShowS

Lift LCNeutralTerm

Defined in LambdaCube.STLC.Ast

Methods

lift :: LCNeutralTerm -> Q Exp

liftTyped :: LCNeutralTerm -> Q (TExp LCNeutralTerm)