Safe Haskell	None
Language	Haskell2010

LambdaCube.SystemFw.Ast

Documentation

data ExtLCTerm Source #

Constructors

ExtLCVar Text
ExtLCLam Text ExtLCType ExtLCTerm
ExtLCApp ExtLCTerm ExtLCTerm infixl 6
ExtLCTLam Text ExtLCKind ExtLCTerm
ExtLCTApp ExtLCTerm ExtLCType infixl 6
ExtLCMVar String

Instances

Instances details

Eq ExtLCTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: ExtLCTerm -> ExtLCTerm -> Bool # (/=) :: ExtLCTerm -> ExtLCTerm -> Bool #
Data ExtLCTerm Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> ExtLCTerm -> ShowS # show :: ExtLCTerm -> String # showList :: [ExtLCTerm] -> ShowS #
Lift ExtLCTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: ExtLCTerm -> Q Exp # liftTyped :: ExtLCTerm -> Q (TExp ExtLCTerm) #

data ExtLCType Source #

Constructors

ExtLCBase
ExtLCTVar Text
ExtLCArr ExtLCType ExtLCType infixr 5
ExtLCUniv Text ExtLCKind ExtLCType
ExtLCTTLam Text ExtLCKind ExtLCType
ExtLCTTApp ExtLCType ExtLCType infixl 6
ExtLCMTVar String

Instances

Instances details

Eq ExtLCType Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: ExtLCType -> ExtLCType -> Bool # (/=) :: ExtLCType -> ExtLCType -> Bool #
Data ExtLCType Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> ExtLCType -> ShowS # show :: ExtLCType -> String # showList :: [ExtLCType] -> ShowS #
Lift ExtLCType Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: ExtLCType -> Q Exp # liftTyped :: ExtLCType -> Q (TExp ExtLCType) #

data ExtLCKind Source #

Constructors

ExtLCStar
ExtLCKArr ExtLCKind ExtLCKind infixr 5
ExtLCMKVar String

Instances

Instances details

Eq ExtLCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: ExtLCKind -> ExtLCKind -> Bool # (/=) :: ExtLCKind -> ExtLCKind -> Bool #
Data ExtLCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ExtLCKind -> c ExtLCKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ExtLCKind # toConstr :: ExtLCKind -> Constr # dataTypeOf :: ExtLCKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ExtLCKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ExtLCKind) # gmapT :: (forall b. Data b => b -> b) -> ExtLCKind -> ExtLCKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ExtLCKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ExtLCKind -> r # gmapQ :: (forall d. Data d => d -> u) -> ExtLCKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ExtLCKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ExtLCKind -> m ExtLCKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLCKind -> m ExtLCKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ExtLCKind -> m ExtLCKind #
Show ExtLCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> ExtLCKind -> ShowS # show :: ExtLCKind -> String # showList :: [ExtLCKind] -> ShowS #
Lift ExtLCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: ExtLCKind -> Q Exp # liftTyped :: ExtLCKind -> Q (TExp ExtLCKind) #

data LCTerm Source #

Constructors

LCVar Int
LCLam LCType LCTerm
LCApp LCTerm LCTerm infixl 6
LCTLam LCKind LCTerm
LCTApp LCTerm LCType infixl 6

Instances

Instances details

Eq LCTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCTerm -> LCTerm -> Bool # (/=) :: LCTerm -> LCTerm -> Bool #
Data LCTerm Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCTerm -> ShowS # show :: LCTerm -> String # showList :: [LCTerm] -> ShowS #
Lift LCTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCTerm -> Q Exp # liftTyped :: LCTerm -> Q (TExp LCTerm) #

data LCType Source #

Constructors

LCBase
LCTVar Int
LCArr LCType LCType infixr 5
LCUniv LCKind LCType
LCTTLam LCKind LCType
LCTTApp LCType LCType infixl 6

Instances

Instances details

Eq LCType Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCType -> LCType -> Bool # (/=) :: LCType -> LCType -> Bool #
Data LCType Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCType -> ShowS # show :: LCType -> String # showList :: [LCType] -> ShowS #
Lift LCType Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCType -> Q Exp # liftTyped :: LCType -> Q (TExp LCType) #

data LCKind Source #

Constructors

LCStar
LCKArr LCKind LCKind infixr 5

Instances

Instances details

Eq LCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCKind -> LCKind -> Bool # (/=) :: LCKind -> LCKind -> Bool #
Data LCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LCKind -> c LCKind # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c LCKind # toConstr :: LCKind -> Constr # dataTypeOf :: LCKind -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c LCKind) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c LCKind) # gmapT :: (forall b. Data b => b -> b) -> LCKind -> LCKind # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LCKind -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LCKind -> r # gmapQ :: (forall d. Data d => d -> u) -> LCKind -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LCKind -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LCKind -> m LCKind # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LCKind -> m LCKind # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LCKind -> m LCKind #
Show LCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCKind -> ShowS # show :: LCKind -> String # showList :: [LCKind] -> ShowS #
Lift LCKind Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCKind -> Q Exp # liftTyped :: LCKind -> Q (TExp LCKind) #

data LCValue Source #

Constructors

LCValLam LCType LCTerm
LCValTLam LCKind LCTerm

Instances

Instances details

Eq LCValue Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCValue -> LCValue -> Bool # (/=) :: LCValue -> LCValue -> Bool #
Data LCValue Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCValue -> ShowS # show :: LCValue -> String # showList :: [LCValue] -> ShowS #
Lift LCValue Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCValue -> Q Exp # liftTyped :: LCValue -> Q (TExp LCValue) #

data LCNormalTerm Source #

Constructors

LCNormLam LCType LCNormalTerm
LCNormTLam LCKind LCNormalTerm
LCNormNeut LCNeutralTerm

Instances

Instances details

Eq LCNormalTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCNormalTerm -> LCNormalTerm -> Bool # (/=) :: LCNormalTerm -> LCNormalTerm -> Bool #
Data LCNormalTerm Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCNormalTerm -> ShowS # show :: LCNormalTerm -> String # showList :: [LCNormalTerm] -> ShowS #
Lift LCNormalTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCNormalTerm -> Q Exp # liftTyped :: LCNormalTerm -> Q (TExp LCNormalTerm) #

data LCNeutralTerm Source #

Constructors

LCNeutVar Int
LCNeutApp LCNeutralTerm LCNormalTerm infixl 6
LCNeutTApp LCNeutralTerm LCType infixl 6

Instances

Instances details

Eq LCNeutralTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods (==) :: LCNeutralTerm -> LCNeutralTerm -> Bool # (/=) :: LCNeutralTerm -> LCNeutralTerm -> Bool #
Data LCNeutralTerm Source #
Instance details Defined in LambdaCube.SystemFw.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 Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods showsPrec :: Int -> LCNeutralTerm -> ShowS # show :: LCNeutralTerm -> String # showList :: [LCNeutralTerm] -> ShowS #
Lift LCNeutralTerm Source #
Instance details Defined in LambdaCube.SystemFw.Ast Methods lift :: LCNeutralTerm -> Q Exp # liftTyped :: LCNeutralTerm -> Q (TExp LCNeutralTerm) #