Safe Haskell	Safe-Inferred
Language	Haskell2010

Language.Rzk.Syntax.Abs

Description

The abstract syntax of language Syntax.

Synopsis

type Module = Module' BNFC'Position
data Module' a = Module a (LanguageDecl' a) [Command' a]
type HoleIdent = HoleIdent' BNFC'Position
data HoleIdent' a = HoleIdent a HoleIdentToken
type VarIdent = VarIdent' BNFC'Position
data VarIdent' a = VarIdent a VarIdentToken
type LanguageDecl = LanguageDecl' BNFC'Position
data LanguageDecl' a = LanguageDecl a (Language' a)
type Language = Language' BNFC'Position
data Language' a = Rzk1 a
type Command = Command' BNFC'Position
data Command' a
- = CommandSetOption a String String
- | CommandUnsetOption a String
- | CommandCheck a (Term' a) (Term' a)
- | CommandCompute a (Term' a)
- | CommandComputeWHNF a (Term' a)
- | CommandComputeNF a (Term' a)
- | CommandPostulate a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a)
- | CommandAssume a [VarIdent' a] (Term' a)
- | CommandSection a (SectionName' a)
- | CommandSectionEnd a (SectionName' a)
- | CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)
type DeclUsedVars = DeclUsedVars' BNFC'Position
data DeclUsedVars' a = DeclUsedVars a [VarIdent' a]
type SectionName = SectionName' BNFC'Position
data SectionName' a
- = NoSectionName a
- | SomeSectionName a (VarIdent' a)
type Pattern = Pattern' BNFC'Position
data Pattern' a
- = PatternUnit a
- | PatternVar a (VarIdent' a)
- | PatternPair a (Pattern' a) (Pattern' a)
type Param = Param' BNFC'Position
data Param' a
- = ParamPattern a (Pattern' a)
- | ParamPatternType a [Pattern' a] (Term' a)
- | ParamPatternShape a [Pattern' a] (Term' a) (Term' a)
- | ParamPatternShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
type ParamDecl = ParamDecl' BNFC'Position
data ParamDecl' a
- = ParamType a (Term' a)
- | ParamTermType a (Term' a) (Term' a)
- | ParamTermShape a (Term' a) (Term' a) (Term' a)
- | ParamTermTypeDeprecated a (Pattern' a) (Term' a)
- | ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)
type Restriction = Restriction' BNFC'Position
data Restriction' a
- = Restriction a (Term' a) (Term' a)
- | ASCII_Restriction a (Term' a) (Term' a)
type Term = Term' BNFC'Position
data Term' a
- = Universe a
- | UniverseCube a
- | UniverseTope a
- | CubeUnit a
- | CubeUnitStar a
- | Cube2 a
- | Cube2_0 a
- | Cube2_1 a
- | CubeProduct a (Term' a) (Term' a)
- | TopeTop a
- | TopeBottom a
- | TopeEQ a (Term' a) (Term' a)
- | TopeLEQ a (Term' a) (Term' a)
- | TopeAnd a (Term' a) (Term' a)
- | TopeOr a (Term' a) (Term' a)
- | RecBottom a
- | RecOr a [Restriction' a]
- | RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
- | TypeFun a (ParamDecl' a) (Term' a)
- | TypeSigma a (Pattern' a) (Term' a) (Term' a)
- | TypeUnit a
- | TypeId a (Term' a) (Term' a) (Term' a)
- | TypeIdSimple a (Term' a) (Term' a)
- | TypeRestricted a (Term' a) [Restriction' a]
- | TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
- | App a (Term' a) (Term' a)
- | Lambda a [Param' a] (Term' a)
- | Pair a (Term' a) (Term' a)
- | First a (Term' a)
- | Second a (Term' a)
- | Unit a
- | Refl a
- | ReflTerm a (Term' a)
- | ReflTermType a (Term' a) (Term' a)
- | IdJ a (Term' a) (Term' a) (Term' a) (Term' a) (Term' a) (Term' a)
- | Hole a (HoleIdent' a)
- | Var a (VarIdent' a)
- | TypeAsc a (Term' a) (Term' a)
- | ASCII_CubeUnitStar a
- | ASCII_Cube2_0 a
- | ASCII_Cube2_1 a
- | ASCII_TopeTop a
- | ASCII_TopeBottom a
- | ASCII_TopeEQ a (Term' a) (Term' a)
- | ASCII_TopeLEQ a (Term' a) (Term' a)
- | ASCII_TopeAnd a (Term' a) (Term' a)
- | ASCII_TopeOr a (Term' a) (Term' a)
- | ASCII_TypeFun a (ParamDecl' a) (Term' a)
- | ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)
- | ASCII_Lambda a [Param' a] (Term' a)
- | ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
- | ASCII_First a (Term' a)
- | ASCII_Second a (Term' a)
commandPostulateNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Command' a
commandVariable :: a -> VarIdent' a -> Term' a -> Command' a
commandVariables :: a -> [VarIdent' a] -> Term' a -> Command' a
commandDefineNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
commandDef :: a -> VarIdent' a -> DeclUsedVars' a -> [Param' a] -> Term' a -> Term' a -> Command' a
commandDefNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
noDeclUsedVars :: a -> DeclUsedVars' a
paramVarShapeDeprecated :: a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a
ascii_CubeProduct :: a -> Term' a -> Term' a -> Term' a
unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
newtype VarIdentToken = VarIdentToken String
newtype HoleIdentToken = HoleIdentToken String
type BNFC'Position = Maybe (Int, Int)
pattern BNFC'NoPosition :: BNFC'Position
pattern BNFC'Position :: Int -> Int -> BNFC'Position
class HasPosition a where
- hasPosition :: a -> BNFC'Position

Documentation

type Module = Module' BNFC'Position Source #

data Module' a Source #

Constructors

Module a (LanguageDecl' a) [Command' a]

Instances

Instances details

Foldable Module' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => Module' m -> m # foldMap :: Monoid m => (a -> m) -> Module' a -> m # foldMap' :: Monoid m => (a -> m) -> Module' a -> m # foldr :: (a -> b -> b) -> b -> Module' a -> b # foldr' :: (a -> b -> b) -> b -> Module' a -> b # foldl :: (b -> a -> b) -> b -> Module' a -> b # foldl' :: (b -> a -> b) -> b -> Module' a -> b # foldr1 :: (a -> a -> a) -> Module' a -> a # foldl1 :: (a -> a -> a) -> Module' a -> a # toList :: Module' a -> [a] # null :: Module' a -> Bool # length :: Module' a -> Int # elem :: Eq a => a -> Module' a -> Bool # maximum :: Ord a => Module' a -> a # minimum :: Ord a => Module' a -> a # sum :: Num a => Module' a -> a # product :: Num a => Module' a -> a #
Traversable Module' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> Module' a -> f (Module' b) # sequenceA :: Applicative f => Module' (f a) -> f (Module' a) # mapM :: Monad m => (a -> m b) -> Module' a -> m (Module' b) # sequence :: Monad m => Module' (m a) -> m (Module' a) #
Functor Module' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Module' a -> Module' b # (<$) :: a -> Module' b -> Module' a #
HasPosition Module Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Module -> BNFC'Position Source #
Data a => Data (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Module' a -> c (Module' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Module' a) # toConstr :: Module' a -> Constr # dataTypeOf :: Module' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Module' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Module' a)) # gmapT :: (forall b. Data b => b -> b) -> Module' a -> Module' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Module' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Module' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Module' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Module' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Module' a -> m (Module' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Module' a -> m (Module' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Module' a -> m (Module' a) #
Generic (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (Module' a) :: Type -> Type # Methods from :: Module' a -> Rep (Module' a) x # to :: Rep (Module' a) x -> Module' a #
Read a => Read (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (Module' a) # readList :: ReadS [Module' a] # readPrec :: ReadPrec (Module' a) # readListPrec :: ReadPrec [Module' a] #
Show a => Show (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> Module' a -> ShowS # show :: Module' a -> String # showList :: [Module' a] -> ShowS #
Eq a => Eq (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: Module' a -> Module' a -> Bool # (/=) :: Module' a -> Module' a -> Bool #
Ord a => Ord (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: Module' a -> Module' a -> Ordering # (<) :: Module' a -> Module' a -> Bool # (<=) :: Module' a -> Module' a -> Bool # (>) :: Module' a -> Module' a -> Bool # (>=) :: Module' a -> Module' a -> Bool # max :: Module' a -> Module' a -> Module' a # min :: Module' a -> Module' a -> Module' a #
Print (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Module' a -> Doc Source #
type Rep (Module' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Module' a) = D1 ('MetaData "Module'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "Module" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (LanguageDecl' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Command' a]))))

type HoleIdent = HoleIdent' BNFC'Position Source #

data HoleIdent' a Source #

Constructors

HoleIdent a HoleIdentToken

Instances

Instances details

Foldable HoleIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => HoleIdent' m -> m # foldMap :: Monoid m => (a -> m) -> HoleIdent' a -> m # foldMap' :: Monoid m => (a -> m) -> HoleIdent' a -> m # foldr :: (a -> b -> b) -> b -> HoleIdent' a -> b # foldr' :: (a -> b -> b) -> b -> HoleIdent' a -> b # foldl :: (b -> a -> b) -> b -> HoleIdent' a -> b # foldl' :: (b -> a -> b) -> b -> HoleIdent' a -> b # foldr1 :: (a -> a -> a) -> HoleIdent' a -> a # foldl1 :: (a -> a -> a) -> HoleIdent' a -> a # toList :: HoleIdent' a -> [a] # null :: HoleIdent' a -> Bool # length :: HoleIdent' a -> Int # elem :: Eq a => a -> HoleIdent' a -> Bool # maximum :: Ord a => HoleIdent' a -> a # minimum :: Ord a => HoleIdent' a -> a # sum :: Num a => HoleIdent' a -> a # product :: Num a => HoleIdent' a -> a #
Traversable HoleIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> HoleIdent' a -> f (HoleIdent' b) # sequenceA :: Applicative f => HoleIdent' (f a) -> f (HoleIdent' a) # mapM :: Monad m => (a -> m b) -> HoleIdent' a -> m (HoleIdent' b) # sequence :: Monad m => HoleIdent' (m a) -> m (HoleIdent' a) #
Functor HoleIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> HoleIdent' a -> HoleIdent' b # (<$) :: a -> HoleIdent' b -> HoleIdent' a #
HasPosition HoleIdent Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: HoleIdent -> BNFC'Position Source #
Data a => Data (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HoleIdent' a -> c (HoleIdent' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (HoleIdent' a) # toConstr :: HoleIdent' a -> Constr # dataTypeOf :: HoleIdent' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (HoleIdent' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (HoleIdent' a)) # gmapT :: (forall b. Data b => b -> b) -> HoleIdent' a -> HoleIdent' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdent' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdent' a -> r # gmapQ :: (forall d. Data d => d -> u) -> HoleIdent' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HoleIdent' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HoleIdent' a -> m (HoleIdent' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdent' a -> m (HoleIdent' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdent' a -> m (HoleIdent' a) #
Generic (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (HoleIdent' a) :: Type -> Type # Methods from :: HoleIdent' a -> Rep (HoleIdent' a) x # to :: Rep (HoleIdent' a) x -> HoleIdent' a #
Read a => Read (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (HoleIdent' a) # readList :: ReadS [HoleIdent' a] # readPrec :: ReadPrec (HoleIdent' a) # readListPrec :: ReadPrec [HoleIdent' a] #
Show a => Show (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> HoleIdent' a -> ShowS # show :: HoleIdent' a -> String # showList :: [HoleIdent' a] -> ShowS #
Eq a => Eq (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: HoleIdent' a -> HoleIdent' a -> Bool # (/=) :: HoleIdent' a -> HoleIdent' a -> Bool #
Ord a => Ord (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: HoleIdent' a -> HoleIdent' a -> Ordering # (<) :: HoleIdent' a -> HoleIdent' a -> Bool # (<=) :: HoleIdent' a -> HoleIdent' a -> Bool # (>) :: HoleIdent' a -> HoleIdent' a -> Bool # (>=) :: HoleIdent' a -> HoleIdent' a -> Bool # max :: HoleIdent' a -> HoleIdent' a -> HoleIdent' a # min :: HoleIdent' a -> HoleIdent' a -> HoleIdent' a #
Print (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> HoleIdent' a -> Doc Source #
type Rep (HoleIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (HoleIdent' a) = D1 ('MetaData "HoleIdent'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "HoleIdent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 HoleIdentToken)))

type VarIdent = VarIdent' BNFC'Position Source #

data VarIdent' a Source #

Constructors

VarIdent a VarIdentToken

Instances

Instances details

Foldable VarIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => VarIdent' m -> m # foldMap :: Monoid m => (a -> m) -> VarIdent' a -> m # foldMap' :: Monoid m => (a -> m) -> VarIdent' a -> m # foldr :: (a -> b -> b) -> b -> VarIdent' a -> b # foldr' :: (a -> b -> b) -> b -> VarIdent' a -> b # foldl :: (b -> a -> b) -> b -> VarIdent' a -> b # foldl' :: (b -> a -> b) -> b -> VarIdent' a -> b # foldr1 :: (a -> a -> a) -> VarIdent' a -> a # foldl1 :: (a -> a -> a) -> VarIdent' a -> a # toList :: VarIdent' a -> [a] # null :: VarIdent' a -> Bool # length :: VarIdent' a -> Int # elem :: Eq a => a -> VarIdent' a -> Bool # maximum :: Ord a => VarIdent' a -> a # minimum :: Ord a => VarIdent' a -> a # sum :: Num a => VarIdent' a -> a # product :: Num a => VarIdent' a -> a #
Traversable VarIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> VarIdent' a -> f (VarIdent' b) # sequenceA :: Applicative f => VarIdent' (f a) -> f (VarIdent' a) # mapM :: Monad m => (a -> m b) -> VarIdent' a -> m (VarIdent' b) # sequence :: Monad m => VarIdent' (m a) -> m (VarIdent' a) #
Functor VarIdent' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> VarIdent' a -> VarIdent' b # (<$) :: a -> VarIdent' b -> VarIdent' a #
HasPosition VarIdent Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: VarIdent -> BNFC'Position Source #
Data a => Data (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarIdent' a -> c (VarIdent' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (VarIdent' a) # toConstr :: VarIdent' a -> Constr # dataTypeOf :: VarIdent' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (VarIdent' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (VarIdent' a)) # gmapT :: (forall b. Data b => b -> b) -> VarIdent' a -> VarIdent' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent' a -> r # gmapQ :: (forall d. Data d => d -> u) -> VarIdent' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> VarIdent' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarIdent' a -> m (VarIdent' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent' a -> m (VarIdent' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent' a -> m (VarIdent' a) #
Generic (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (VarIdent' a) :: Type -> Type # Methods from :: VarIdent' a -> Rep (VarIdent' a) x # to :: Rep (VarIdent' a) x -> VarIdent' a #
Read a => Read (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (VarIdent' a) # readList :: ReadS [VarIdent' a] # readPrec :: ReadPrec (VarIdent' a) # readListPrec :: ReadPrec [VarIdent' a] #
Show a => Show (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> VarIdent' a -> ShowS # show :: VarIdent' a -> String # showList :: [VarIdent' a] -> ShowS #
Eq a => Eq (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: VarIdent' a -> VarIdent' a -> Bool # (/=) :: VarIdent' a -> VarIdent' a -> Bool #
Ord a => Ord (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: VarIdent' a -> VarIdent' a -> Ordering # (<) :: VarIdent' a -> VarIdent' a -> Bool # (<=) :: VarIdent' a -> VarIdent' a -> Bool # (>) :: VarIdent' a -> VarIdent' a -> Bool # (>=) :: VarIdent' a -> VarIdent' a -> Bool # max :: VarIdent' a -> VarIdent' a -> VarIdent' a # min :: VarIdent' a -> VarIdent' a -> VarIdent' a #
Print (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> VarIdent' a -> Doc Source #
Print [VarIdent' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [VarIdent' a] -> Doc Source #
type Rep (VarIdent' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (VarIdent' a) = D1 ('MetaData "VarIdent'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "VarIdent" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 VarIdentToken)))

type LanguageDecl = LanguageDecl' BNFC'Position Source #

data LanguageDecl' a Source #

Constructors

LanguageDecl a (Language' a)

Instances

Instances details

Foldable LanguageDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => LanguageDecl' m -> m # foldMap :: Monoid m => (a -> m) -> LanguageDecl' a -> m # foldMap' :: Monoid m => (a -> m) -> LanguageDecl' a -> m # foldr :: (a -> b -> b) -> b -> LanguageDecl' a -> b # foldr' :: (a -> b -> b) -> b -> LanguageDecl' a -> b # foldl :: (b -> a -> b) -> b -> LanguageDecl' a -> b # foldl' :: (b -> a -> b) -> b -> LanguageDecl' a -> b # foldr1 :: (a -> a -> a) -> LanguageDecl' a -> a # foldl1 :: (a -> a -> a) -> LanguageDecl' a -> a # toList :: LanguageDecl' a -> [a] # null :: LanguageDecl' a -> Bool # length :: LanguageDecl' a -> Int # elem :: Eq a => a -> LanguageDecl' a -> Bool # maximum :: Ord a => LanguageDecl' a -> a # minimum :: Ord a => LanguageDecl' a -> a # sum :: Num a => LanguageDecl' a -> a # product :: Num a => LanguageDecl' a -> a #
Traversable LanguageDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> LanguageDecl' a -> f (LanguageDecl' b) # sequenceA :: Applicative f => LanguageDecl' (f a) -> f (LanguageDecl' a) # mapM :: Monad m => (a -> m b) -> LanguageDecl' a -> m (LanguageDecl' b) # sequence :: Monad m => LanguageDecl' (m a) -> m (LanguageDecl' a) #
Functor LanguageDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> LanguageDecl' a -> LanguageDecl' b # (<$) :: a -> LanguageDecl' b -> LanguageDecl' a #
HasPosition LanguageDecl Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: LanguageDecl -> BNFC'Position Source #
Data a => Data (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> LanguageDecl' a -> c (LanguageDecl' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (LanguageDecl' a) # toConstr :: LanguageDecl' a -> Constr # dataTypeOf :: LanguageDecl' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (LanguageDecl' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (LanguageDecl' a)) # gmapT :: (forall b. Data b => b -> b) -> LanguageDecl' a -> LanguageDecl' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> LanguageDecl' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> LanguageDecl' a -> r # gmapQ :: (forall d. Data d => d -> u) -> LanguageDecl' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> LanguageDecl' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> LanguageDecl' a -> m (LanguageDecl' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> LanguageDecl' a -> m (LanguageDecl' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> LanguageDecl' a -> m (LanguageDecl' a) #
Generic (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (LanguageDecl' a) :: Type -> Type # Methods from :: LanguageDecl' a -> Rep (LanguageDecl' a) x # to :: Rep (LanguageDecl' a) x -> LanguageDecl' a #
Read a => Read (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (LanguageDecl' a) # readList :: ReadS [LanguageDecl' a] # readPrec :: ReadPrec (LanguageDecl' a) # readListPrec :: ReadPrec [LanguageDecl' a] #
Show a => Show (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> LanguageDecl' a -> ShowS # show :: LanguageDecl' a -> String # showList :: [LanguageDecl' a] -> ShowS #
Eq a => Eq (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: LanguageDecl' a -> LanguageDecl' a -> Bool # (/=) :: LanguageDecl' a -> LanguageDecl' a -> Bool #
Ord a => Ord (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: LanguageDecl' a -> LanguageDecl' a -> Ordering # (<) :: LanguageDecl' a -> LanguageDecl' a -> Bool # (<=) :: LanguageDecl' a -> LanguageDecl' a -> Bool # (>) :: LanguageDecl' a -> LanguageDecl' a -> Bool # (>=) :: LanguageDecl' a -> LanguageDecl' a -> Bool # max :: LanguageDecl' a -> LanguageDecl' a -> LanguageDecl' a # min :: LanguageDecl' a -> LanguageDecl' a -> LanguageDecl' a #
Print (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> LanguageDecl' a -> Doc Source #
type Rep (LanguageDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (LanguageDecl' a) = D1 ('MetaData "LanguageDecl'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "LanguageDecl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Language' a))))

type Language = Language' BNFC'Position Source #

data Language' a Source #

Constructors

Rzk1 a

Instances

Instances details

Foldable Language' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => Language' m -> m # foldMap :: Monoid m => (a -> m) -> Language' a -> m # foldMap' :: Monoid m => (a -> m) -> Language' a -> m # foldr :: (a -> b -> b) -> b -> Language' a -> b # foldr' :: (a -> b -> b) -> b -> Language' a -> b # foldl :: (b -> a -> b) -> b -> Language' a -> b # foldl' :: (b -> a -> b) -> b -> Language' a -> b # foldr1 :: (a -> a -> a) -> Language' a -> a # foldl1 :: (a -> a -> a) -> Language' a -> a # toList :: Language' a -> [a] # null :: Language' a -> Bool # length :: Language' a -> Int # elem :: Eq a => a -> Language' a -> Bool # maximum :: Ord a => Language' a -> a # minimum :: Ord a => Language' a -> a # sum :: Num a => Language' a -> a # product :: Num a => Language' a -> a #
Traversable Language' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> Language' a -> f (Language' b) # sequenceA :: Applicative f => Language' (f a) -> f (Language' a) # mapM :: Monad m => (a -> m b) -> Language' a -> m (Language' b) # sequence :: Monad m => Language' (m a) -> m (Language' a) #
Functor Language' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Language' a -> Language' b # (<$) :: a -> Language' b -> Language' a #
HasPosition Language Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Language -> BNFC'Position Source #
Data a => Data (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Language' a -> c (Language' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Language' a) # toConstr :: Language' a -> Constr # dataTypeOf :: Language' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Language' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Language' a)) # gmapT :: (forall b. Data b => b -> b) -> Language' a -> Language' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Language' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Language' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Language' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Language' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Language' a -> m (Language' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Language' a -> m (Language' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Language' a -> m (Language' a) #
Generic (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (Language' a) :: Type -> Type # Methods from :: Language' a -> Rep (Language' a) x # to :: Rep (Language' a) x -> Language' a #
Read a => Read (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (Language' a) # readList :: ReadS [Language' a] # readPrec :: ReadPrec (Language' a) # readListPrec :: ReadPrec [Language' a] #
Show a => Show (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> Language' a -> ShowS # show :: Language' a -> String # showList :: [Language' a] -> ShowS #
Eq a => Eq (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: Language' a -> Language' a -> Bool # (/=) :: Language' a -> Language' a -> Bool #
Ord a => Ord (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: Language' a -> Language' a -> Ordering # (<) :: Language' a -> Language' a -> Bool # (<=) :: Language' a -> Language' a -> Bool # (>) :: Language' a -> Language' a -> Bool # (>=) :: Language' a -> Language' a -> Bool # max :: Language' a -> Language' a -> Language' a # min :: Language' a -> Language' a -> Language' a #
Print (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Language' a -> Doc Source #
type Rep (Language' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Language' a) = D1 ('MetaData "Language'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "Rzk1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

type Command = Command' BNFC'Position Source #

data Command' a Source #

Constructors

CommandSetOption a String String
CommandUnsetOption a String
CommandCheck a (Term' a) (Term' a)
CommandCompute a (Term' a)
CommandComputeWHNF a (Term' a)
CommandComputeNF a (Term' a)
CommandPostulate a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a)
CommandAssume a [VarIdent' a] (Term' a)
CommandSection a (SectionName' a)
CommandSectionEnd a (SectionName' a)
CommandDefine a (VarIdent' a) (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)

Instances

Instances details

Foldable Command' Source #
Instance details Defined in Language.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Command' a -> Command' b # (<$) :: a -> Command' b -> Command' a #
HasPosition Command Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Command -> BNFC'Position Source #
Data a => Data (Command' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Abs Associated Types type Rep (Command' a) :: Type -> Type # 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.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods (==) :: Command' a -> Command' a -> Bool # (/=) :: Command' a -> Command' a -> Bool #
Ord a => Ord (Command' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Print Methods prt :: Int -> Command' a -> Doc Source #
Print [Command' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Command' a] -> Doc Source #
type Rep (Command' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Command' a) = D1 ('MetaData "Command'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (((C1 ('MetaCons "CommandSetOption" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: C1 ('MetaCons "CommandUnsetOption" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String))) :+: (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))) :+: C1 ('MetaCons "CommandComputeWHNF" '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 "CommandComputeNF" '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 "CommandPostulate" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (VarIdent' a))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DeclUsedVars' a)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Param' a]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))) :+: C1 ('MetaCons "CommandAssume" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VarIdent' a]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))) :+: (C1 ('MetaCons "CommandSection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SectionName' a))) :+: (C1 ('MetaCons "CommandSectionEnd" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (SectionName' a))) :+: C1 ('MetaCons "CommandDefine" 'PrefixI 'False) ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (VarIdent' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (DeclUsedVars' a)))) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Param' a]) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))))))

type DeclUsedVars = DeclUsedVars' BNFC'Position Source #

data DeclUsedVars' a Source #

Constructors

DeclUsedVars a [VarIdent' a]

Instances

Instances details

Foldable DeclUsedVars' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => DeclUsedVars' m -> m # foldMap :: Monoid m => (a -> m) -> DeclUsedVars' a -> m # foldMap' :: Monoid m => (a -> m) -> DeclUsedVars' a -> m # foldr :: (a -> b -> b) -> b -> DeclUsedVars' a -> b # foldr' :: (a -> b -> b) -> b -> DeclUsedVars' a -> b # foldl :: (b -> a -> b) -> b -> DeclUsedVars' a -> b # foldl' :: (b -> a -> b) -> b -> DeclUsedVars' a -> b # foldr1 :: (a -> a -> a) -> DeclUsedVars' a -> a # foldl1 :: (a -> a -> a) -> DeclUsedVars' a -> a # toList :: DeclUsedVars' a -> [a] # null :: DeclUsedVars' a -> Bool # length :: DeclUsedVars' a -> Int # elem :: Eq a => a -> DeclUsedVars' a -> Bool # maximum :: Ord a => DeclUsedVars' a -> a # minimum :: Ord a => DeclUsedVars' a -> a # sum :: Num a => DeclUsedVars' a -> a # product :: Num a => DeclUsedVars' a -> a #
Traversable DeclUsedVars' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> DeclUsedVars' a -> f (DeclUsedVars' b) # sequenceA :: Applicative f => DeclUsedVars' (f a) -> f (DeclUsedVars' a) # mapM :: Monad m => (a -> m b) -> DeclUsedVars' a -> m (DeclUsedVars' b) # sequence :: Monad m => DeclUsedVars' (m a) -> m (DeclUsedVars' a) #
Functor DeclUsedVars' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> DeclUsedVars' a -> DeclUsedVars' b # (<$) :: a -> DeclUsedVars' b -> DeclUsedVars' a #
HasPosition DeclUsedVars Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: DeclUsedVars -> BNFC'Position Source #
Data a => Data (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> DeclUsedVars' a -> c (DeclUsedVars' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (DeclUsedVars' a) # toConstr :: DeclUsedVars' a -> Constr # dataTypeOf :: DeclUsedVars' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (DeclUsedVars' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (DeclUsedVars' a)) # gmapT :: (forall b. Data b => b -> b) -> DeclUsedVars' a -> DeclUsedVars' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> DeclUsedVars' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> DeclUsedVars' a -> r # gmapQ :: (forall d. Data d => d -> u) -> DeclUsedVars' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> DeclUsedVars' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> DeclUsedVars' a -> m (DeclUsedVars' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclUsedVars' a -> m (DeclUsedVars' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> DeclUsedVars' a -> m (DeclUsedVars' a) #
Generic (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (DeclUsedVars' a) :: Type -> Type # Methods from :: DeclUsedVars' a -> Rep (DeclUsedVars' a) x # to :: Rep (DeclUsedVars' a) x -> DeclUsedVars' a #
Read a => Read (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (DeclUsedVars' a) # readList :: ReadS [DeclUsedVars' a] # readPrec :: ReadPrec (DeclUsedVars' a) # readListPrec :: ReadPrec [DeclUsedVars' a] #
Show a => Show (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> DeclUsedVars' a -> ShowS # show :: DeclUsedVars' a -> String # showList :: [DeclUsedVars' a] -> ShowS #
Eq a => Eq (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool # (/=) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool #
Ord a => Ord (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: DeclUsedVars' a -> DeclUsedVars' a -> Ordering # (<) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool # (<=) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool # (>) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool # (>=) :: DeclUsedVars' a -> DeclUsedVars' a -> Bool # max :: DeclUsedVars' a -> DeclUsedVars' a -> DeclUsedVars' a # min :: DeclUsedVars' a -> DeclUsedVars' a -> DeclUsedVars' a #
Print (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> DeclUsedVars' a -> Doc Source #
type Rep (DeclUsedVars' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (DeclUsedVars' a) = D1 ('MetaData "DeclUsedVars'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "DeclUsedVars" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [VarIdent' a])))

type SectionName = SectionName' BNFC'Position Source #

data SectionName' a Source #

Constructors

NoSectionName a
SomeSectionName a (VarIdent' a)

Instances

Instances details

Foldable SectionName' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => SectionName' m -> m # foldMap :: Monoid m => (a -> m) -> SectionName' a -> m # foldMap' :: Monoid m => (a -> m) -> SectionName' a -> m # foldr :: (a -> b -> b) -> b -> SectionName' a -> b # foldr' :: (a -> b -> b) -> b -> SectionName' a -> b # foldl :: (b -> a -> b) -> b -> SectionName' a -> b # foldl' :: (b -> a -> b) -> b -> SectionName' a -> b # foldr1 :: (a -> a -> a) -> SectionName' a -> a # foldl1 :: (a -> a -> a) -> SectionName' a -> a # toList :: SectionName' a -> [a] # null :: SectionName' a -> Bool # length :: SectionName' a -> Int # elem :: Eq a => a -> SectionName' a -> Bool # maximum :: Ord a => SectionName' a -> a # minimum :: Ord a => SectionName' a -> a # sum :: Num a => SectionName' a -> a # product :: Num a => SectionName' a -> a #
Traversable SectionName' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> SectionName' a -> f (SectionName' b) # sequenceA :: Applicative f => SectionName' (f a) -> f (SectionName' a) # mapM :: Monad m => (a -> m b) -> SectionName' a -> m (SectionName' b) # sequence :: Monad m => SectionName' (m a) -> m (SectionName' a) #
Functor SectionName' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> SectionName' a -> SectionName' b # (<$) :: a -> SectionName' b -> SectionName' a #
HasPosition SectionName Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: SectionName -> BNFC'Position Source #
Data a => Data (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> SectionName' a -> c (SectionName' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (SectionName' a) # toConstr :: SectionName' a -> Constr # dataTypeOf :: SectionName' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (SectionName' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (SectionName' a)) # gmapT :: (forall b. Data b => b -> b) -> SectionName' a -> SectionName' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> SectionName' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> SectionName' a -> r # gmapQ :: (forall d. Data d => d -> u) -> SectionName' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> SectionName' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> SectionName' a -> m (SectionName' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> SectionName' a -> m (SectionName' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> SectionName' a -> m (SectionName' a) #
Generic (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (SectionName' a) :: Type -> Type # Methods from :: SectionName' a -> Rep (SectionName' a) x # to :: Rep (SectionName' a) x -> SectionName' a #
Read a => Read (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (SectionName' a) # readList :: ReadS [SectionName' a] # readPrec :: ReadPrec (SectionName' a) # readListPrec :: ReadPrec [SectionName' a] #
Show a => Show (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> SectionName' a -> ShowS # show :: SectionName' a -> String # showList :: [SectionName' a] -> ShowS #
Eq a => Eq (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: SectionName' a -> SectionName' a -> Bool # (/=) :: SectionName' a -> SectionName' a -> Bool #
Ord a => Ord (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: SectionName' a -> SectionName' a -> Ordering # (<) :: SectionName' a -> SectionName' a -> Bool # (<=) :: SectionName' a -> SectionName' a -> Bool # (>) :: SectionName' a -> SectionName' a -> Bool # (>=) :: SectionName' a -> SectionName' a -> Bool # max :: SectionName' a -> SectionName' a -> SectionName' a # min :: SectionName' a -> SectionName' a -> SectionName' a #
Print (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> SectionName' a -> Doc Source #
type Rep (SectionName' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (SectionName' a) = D1 ('MetaData "SectionName'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "NoSectionName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "SomeSectionName" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (VarIdent' a))))

type Pattern = Pattern' BNFC'Position Source #

data Pattern' a Source #

Constructors

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

Instances

Instances details

Foldable Pattern' Source #
Instance details Defined in Language.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Pattern' a -> Pattern' b # (<$) :: a -> Pattern' b -> Pattern' a #
HasPosition Pattern Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Pattern -> BNFC'Position Source #
Data a => Data (Pattern' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Abs Associated Types type Rep (Pattern' a) :: Type -> Type # 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.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods (==) :: Pattern' a -> Pattern' a -> Bool # (/=) :: Pattern' a -> Pattern' a -> Bool #
Ord a => Ord (Pattern' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Print Methods prt :: Int -> Pattern' a -> Doc Source #
Print [Pattern' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Pattern' a] -> Doc Source #
type Rep (Pattern' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Pattern' a) = D1 ('MetaData "Pattern'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "PatternUnit" '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' a))) :+: 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))))))

type Param = Param' BNFC'Position Source #

data Param' a Source #

Constructors

ParamPattern a (Pattern' a)
ParamPatternType a [Pattern' a] (Term' a)
ParamPatternShape a [Pattern' a] (Term' a) (Term' a)
ParamPatternShapeDeprecated a (Pattern' a) (Term' a) (Term' a)

Instances

Instances details

Foldable Param' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => Param' m -> m # foldMap :: Monoid m => (a -> m) -> Param' a -> m # foldMap' :: Monoid m => (a -> m) -> Param' a -> m # foldr :: (a -> b -> b) -> b -> Param' a -> b # foldr' :: (a -> b -> b) -> b -> Param' a -> b # foldl :: (b -> a -> b) -> b -> Param' a -> b # foldl' :: (b -> a -> b) -> b -> Param' a -> b # foldr1 :: (a -> a -> a) -> Param' a -> a # foldl1 :: (a -> a -> a) -> Param' a -> a # toList :: Param' a -> [a] # null :: Param' a -> Bool # length :: Param' a -> Int # elem :: Eq a => a -> Param' a -> Bool # maximum :: Ord a => Param' a -> a # minimum :: Ord a => Param' a -> a # sum :: Num a => Param' a -> a # product :: Num a => Param' a -> a #
Traversable Param' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> Param' a -> f (Param' b) # sequenceA :: Applicative f => Param' (f a) -> f (Param' a) # mapM :: Monad m => (a -> m b) -> Param' a -> m (Param' b) # sequence :: Monad m => Param' (m a) -> m (Param' a) #
Functor Param' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Param' a -> Param' b # (<$) :: a -> Param' b -> Param' a #
HasPosition Param Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Param -> BNFC'Position Source #
Data a => Data (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Param' a -> c (Param' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Param' a) # toConstr :: Param' a -> Constr # dataTypeOf :: Param' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Param' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Param' a)) # gmapT :: (forall b. Data b => b -> b) -> Param' a -> Param' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Param' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Param' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Param' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Param' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Param' a -> m (Param' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Param' a -> m (Param' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Param' a -> m (Param' a) #
Generic (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (Param' a) :: Type -> Type # Methods from :: Param' a -> Rep (Param' a) x # to :: Rep (Param' a) x -> Param' a #
Read a => Read (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (Param' a) # readList :: ReadS [Param' a] # readPrec :: ReadPrec (Param' a) # readListPrec :: ReadPrec [Param' a] #
Show a => Show (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> Param' a -> ShowS # show :: Param' a -> String # showList :: [Param' a] -> ShowS #
Eq a => Eq (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: Param' a -> Param' a -> Bool # (/=) :: Param' a -> Param' a -> Bool #
Ord a => Ord (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: Param' a -> Param' a -> Ordering # (<) :: Param' a -> Param' a -> Bool # (<=) :: Param' a -> Param' a -> Bool # (>) :: Param' a -> Param' a -> Bool # (>=) :: Param' a -> Param' a -> Bool # max :: Param' a -> Param' a -> Param' a # min :: Param' a -> Param' a -> Param' a #
Print (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Param' a -> Doc Source #
Print [Param' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Param' a] -> Doc Source #
type Rep (Param' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Param' a) = D1 ('MetaData "Param'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) ((C1 ('MetaCons "ParamPattern" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Pattern' a))) :+: C1 ('MetaCons "ParamPatternType" '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))))) :+: (C1 ('MetaCons "ParamPatternShape" '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 (Term' a)))) :+: C1 ('MetaCons "ParamPatternShapeDeprecated" '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 (Term' a))))))

type ParamDecl = ParamDecl' BNFC'Position Source #

data ParamDecl' a Source #

Constructors

ParamType a (Term' a)
ParamTermType a (Term' a) (Term' a)
ParamTermShape a (Term' a) (Term' a) (Term' a)
ParamTermTypeDeprecated a (Pattern' a) (Term' a)
ParamVarShapeDeprecated a (Pattern' a) (Term' a) (Term' a)

Instances

Instances details

Foldable ParamDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => ParamDecl' m -> m # foldMap :: Monoid m => (a -> m) -> ParamDecl' a -> m # foldMap' :: Monoid m => (a -> m) -> ParamDecl' a -> m # foldr :: (a -> b -> b) -> b -> ParamDecl' a -> b # foldr' :: (a -> b -> b) -> b -> ParamDecl' a -> b # foldl :: (b -> a -> b) -> b -> ParamDecl' a -> b # foldl' :: (b -> a -> b) -> b -> ParamDecl' a -> b # foldr1 :: (a -> a -> a) -> ParamDecl' a -> a # foldl1 :: (a -> a -> a) -> ParamDecl' a -> a # toList :: ParamDecl' a -> [a] # null :: ParamDecl' a -> Bool # length :: ParamDecl' a -> Int # elem :: Eq a => a -> ParamDecl' a -> Bool # maximum :: Ord a => ParamDecl' a -> a # minimum :: Ord a => ParamDecl' a -> a # sum :: Num a => ParamDecl' a -> a # product :: Num a => ParamDecl' a -> a #
Traversable ParamDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> ParamDecl' a -> f (ParamDecl' b) # sequenceA :: Applicative f => ParamDecl' (f a) -> f (ParamDecl' a) # mapM :: Monad m => (a -> m b) -> ParamDecl' a -> m (ParamDecl' b) # sequence :: Monad m => ParamDecl' (m a) -> m (ParamDecl' a) #
Functor ParamDecl' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> ParamDecl' a -> ParamDecl' b # (<$) :: a -> ParamDecl' b -> ParamDecl' a #
HasPosition ParamDecl Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: ParamDecl -> BNFC'Position Source #
Data a => Data (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ParamDecl' a -> c (ParamDecl' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ParamDecl' a) # toConstr :: ParamDecl' a -> Constr # dataTypeOf :: ParamDecl' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (ParamDecl' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (ParamDecl' a)) # gmapT :: (forall b. Data b => b -> b) -> ParamDecl' a -> ParamDecl' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ParamDecl' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ParamDecl' a -> r # gmapQ :: (forall d. Data d => d -> u) -> ParamDecl' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ParamDecl' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ParamDecl' a -> m (ParamDecl' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ParamDecl' a -> m (ParamDecl' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ParamDecl' a -> m (ParamDecl' a) #
Generic (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (ParamDecl' a) :: Type -> Type # Methods from :: ParamDecl' a -> Rep (ParamDecl' a) x # to :: Rep (ParamDecl' a) x -> ParamDecl' a #
Read a => Read (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (ParamDecl' a) # readList :: ReadS [ParamDecl' a] # readPrec :: ReadPrec (ParamDecl' a) # readListPrec :: ReadPrec [ParamDecl' a] #
Show a => Show (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> ParamDecl' a -> ShowS # show :: ParamDecl' a -> String # showList :: [ParamDecl' a] -> ShowS #
Eq a => Eq (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: ParamDecl' a -> ParamDecl' a -> Bool # (/=) :: ParamDecl' a -> ParamDecl' a -> Bool #
Ord a => Ord (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: ParamDecl' a -> ParamDecl' a -> Ordering # (<) :: ParamDecl' a -> ParamDecl' a -> Bool # (<=) :: ParamDecl' a -> ParamDecl' a -> Bool # (>) :: ParamDecl' a -> ParamDecl' a -> Bool # (>=) :: ParamDecl' a -> ParamDecl' a -> Bool # max :: ParamDecl' a -> ParamDecl' a -> ParamDecl' a # min :: ParamDecl' a -> ParamDecl' a -> ParamDecl' a #
Print (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> ParamDecl' a -> Doc Source #
type Rep (ParamDecl' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (ParamDecl' a) = D1 ('MetaData "ParamDecl'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) ((C1 ('MetaCons "ParamType" '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 "ParamTermType" '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 "ParamTermShape" '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)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: (C1 ('MetaCons "ParamTermTypeDeprecated" '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)))) :+: C1 ('MetaCons "ParamVarShapeDeprecated" '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 (Term' a)))))))

type Restriction = Restriction' BNFC'Position Source #

data Restriction' a Source #

Constructors

Restriction a (Term' a) (Term' a)
ASCII_Restriction a (Term' a) (Term' a)

Instances

Instances details

Foldable Restriction' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fold :: Monoid m => Restriction' m -> m # foldMap :: Monoid m => (a -> m) -> Restriction' a -> m # foldMap' :: Monoid m => (a -> m) -> Restriction' a -> m # foldr :: (a -> b -> b) -> b -> Restriction' a -> b # foldr' :: (a -> b -> b) -> b -> Restriction' a -> b # foldl :: (b -> a -> b) -> b -> Restriction' a -> b # foldl' :: (b -> a -> b) -> b -> Restriction' a -> b # foldr1 :: (a -> a -> a) -> Restriction' a -> a # foldl1 :: (a -> a -> a) -> Restriction' a -> a # toList :: Restriction' a -> [a] # null :: Restriction' a -> Bool # length :: Restriction' a -> Int # elem :: Eq a => a -> Restriction' a -> Bool # maximum :: Ord a => Restriction' a -> a # minimum :: Ord a => Restriction' a -> a # sum :: Num a => Restriction' a -> a # product :: Num a => Restriction' a -> a #
Traversable Restriction' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods traverse :: Applicative f => (a -> f b) -> Restriction' a -> f (Restriction' b) # sequenceA :: Applicative f => Restriction' (f a) -> f (Restriction' a) # mapM :: Monad m => (a -> m b) -> Restriction' a -> m (Restriction' b) # sequence :: Monad m => Restriction' (m a) -> m (Restriction' a) #
Functor Restriction' Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Restriction' a -> Restriction' b # (<$) :: a -> Restriction' b -> Restriction' a #
HasPosition Restriction Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Restriction -> BNFC'Position Source #
Data a => Data (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Restriction' a -> c (Restriction' a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Restriction' a) # toConstr :: Restriction' a -> Constr # dataTypeOf :: Restriction' a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Restriction' a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Restriction' a)) # gmapT :: (forall b. Data b => b -> b) -> Restriction' a -> Restriction' a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Restriction' a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Restriction' a -> r # gmapQ :: (forall d. Data d => d -> u) -> Restriction' a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Restriction' a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Restriction' a -> m (Restriction' a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Restriction' a -> m (Restriction' a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Restriction' a -> m (Restriction' a) #
Generic (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep (Restriction' a) :: Type -> Type # Methods from :: Restriction' a -> Rep (Restriction' a) x # to :: Rep (Restriction' a) x -> Restriction' a #
Read a => Read (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS (Restriction' a) # readList :: ReadS [Restriction' a] # readPrec :: ReadPrec (Restriction' a) # readListPrec :: ReadPrec [Restriction' a] #
Show a => Show (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> Restriction' a -> ShowS # show :: Restriction' a -> String # showList :: [Restriction' a] -> ShowS #
Eq a => Eq (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: Restriction' a -> Restriction' a -> Bool # (/=) :: Restriction' a -> Restriction' a -> Bool #
Ord a => Ord (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: Restriction' a -> Restriction' a -> Ordering # (<) :: Restriction' a -> Restriction' a -> Bool # (<=) :: Restriction' a -> Restriction' a -> Bool # (>) :: Restriction' a -> Restriction' a -> Bool # (>=) :: Restriction' a -> Restriction' a -> Bool # max :: Restriction' a -> Restriction' a -> Restriction' a # min :: Restriction' a -> Restriction' a -> Restriction' a #
Print (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> Restriction' a -> Doc Source #
Print [Restriction' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Restriction' a] -> Doc Source #
type Rep (Restriction' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Restriction' a) = D1 ('MetaData "Restriction'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (C1 ('MetaCons "Restriction" '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 "ASCII_Restriction" '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

Universe a
UniverseCube a
UniverseTope a
CubeUnit a
CubeUnitStar a
Cube2 a
Cube2_0 a
Cube2_1 a
CubeProduct a (Term' a) (Term' a)
TopeTop a
TopeBottom a
TopeEQ a (Term' a) (Term' a)
TopeLEQ a (Term' a) (Term' a)
TopeAnd a (Term' a) (Term' a)
TopeOr a (Term' a) (Term' a)
RecBottom a
RecOr a [Restriction' a]
RecOrDeprecated a (Term' a) (Term' a) (Term' a) (Term' a)
TypeFun a (ParamDecl' a) (Term' a)
TypeSigma a (Pattern' a) (Term' a) (Term' a)
TypeUnit a
TypeId a (Term' a) (Term' a) (Term' a)
TypeIdSimple a (Term' a) (Term' a)
TypeRestricted a (Term' a) [Restriction' a]
TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
App a (Term' a) (Term' a)
Lambda a [Param' a] (Term' a)
Pair a (Term' a) (Term' a)
First a (Term' a)
Second a (Term' a)
Unit a
Refl a
ReflTerm a (Term' a)
ReflTermType a (Term' a) (Term' a)
IdJ a (Term' a) (Term' a) (Term' a) (Term' a) (Term' a) (Term' a)
Hole a (HoleIdent' a)
Var a (VarIdent' a)
TypeAsc a (Term' a) (Term' a)
ASCII_CubeUnitStar a
ASCII_Cube2_0 a
ASCII_Cube2_1 a
ASCII_TopeTop a
ASCII_TopeBottom a
ASCII_TopeEQ a (Term' a) (Term' a)
ASCII_TopeLEQ a (Term' a) (Term' a)
ASCII_TopeAnd a (Term' a) (Term' a)
ASCII_TopeOr a (Term' a) (Term' a)
ASCII_TypeFun a (ParamDecl' a) (Term' a)
ASCII_TypeSigma a (Pattern' a) (Term' a) (Term' a)
ASCII_Lambda a [Param' a] (Term' a)
ASCII_TypeExtensionDeprecated a (ParamDecl' a) (Term' a)
ASCII_First a (Term' a)
ASCII_Second a (Term' a)

Instances

Instances details

Foldable Term' Source #
Instance details Defined in Language.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods fmap :: (a -> b) -> Term' a -> Term' b # (<$) :: a -> Term' b -> Term' a #
HasPosition Term Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Term -> BNFC'Position Source #
Data a => Data (Term' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Abs Associated Types type Rep (Term' a) :: Type -> Type # 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.Rzk.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.Rzk.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.Rzk.Syntax.Abs Methods (==) :: Term' a -> Term' a -> Bool # (/=) :: Term' a -> Term' a -> Bool #
Ord a => Ord (Term' a) Source #
Instance details Defined in Language.Rzk.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.Rzk.Syntax.Print Methods prt :: Int -> Term' a -> Doc Source #
Print [Term' a] Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> [Term' a] -> Doc Source #
type Rep (Term' a) Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep (Term' a) = D1 ('MetaData "Term'" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'False) (((((C1 ('MetaCons "Universe" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "UniverseCube" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "UniverseTope" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) :+: (C1 ('MetaCons "CubeUnit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "CubeUnitStar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "Cube2" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))) :+: ((C1 ('MetaCons "Cube2_0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "Cube2_1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "CubeProduct" '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 "TopeTop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "TopeBottom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))) :+: (C1 ('MetaCons "TopeEQ" '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 "TopeLEQ" '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 "TopeAnd" '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 "TopeOr" '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 "RecBottom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) :+: (C1 ('MetaCons "RecOr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Restriction' a])) :+: (C1 ('MetaCons "RecOrDeprecated" '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)) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))) :+: C1 ('MetaCons "TypeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParamDecl' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))))) :+: ((C1 ('MetaCons "TypeSigma" '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 (Term' a)))) :+: (C1 ('MetaCons "TypeUnit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "TypeId" '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)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))) :+: ((C1 ('MetaCons "TypeIdSimple" '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 "TypeRestricted" '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 [Restriction' a])))) :+: (C1 ('MetaCons "TypeExtensionDeprecated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParamDecl' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' 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 "Lambda" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Param' 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 "Unit" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "Refl" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a))))) :+: ((C1 ('MetaCons "ReflTerm" '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 "ReflTermType" '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 "IdJ" '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)))) :: ((S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' 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 "Hole" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (HoleIdent' a))) :+: 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' a)))) :+: (C1 ('MetaCons "TypeAsc" '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 "ASCII_CubeUnitStar" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))))) :+: (((C1 ('MetaCons "ASCII_Cube2_0" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: (C1 ('MetaCons "ASCII_Cube2_1" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "ASCII_TopeTop" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))) :+: ((C1 ('MetaCons "ASCII_TopeBottom" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "ASCII_TopeEQ" '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 "ASCII_TopeLEQ" '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 "ASCII_TopeAnd" '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 "ASCII_TopeOr" '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 "ASCII_TypeFun" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParamDecl' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "ASCII_TypeSigma" '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 (Term' a)))))) :+: ((C1 ('MetaCons "ASCII_Lambda" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Param' a]) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))) :+: C1 ('MetaCons "ASCII_TypeExtensionDeprecated" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :: (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (ParamDecl' a)) :: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a))))) :+: (C1 ('MetaCons "ASCII_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 "ASCII_Second" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Term' a)))))))))

commandPostulateNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Command' a Source #

commandVariable :: a -> VarIdent' a -> Term' a -> Command' a Source #

commandVariables :: a -> [VarIdent' a] -> Term' a -> Command' a Source #

commandDefineNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a Source #

commandDef :: a -> VarIdent' a -> DeclUsedVars' a -> [Param' a] -> Term' a -> Term' a -> Command' a Source #

commandDefNoParams :: a -> VarIdent' a -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a Source #

noDeclUsedVars :: a -> DeclUsedVars' a Source #

paramVarShapeDeprecated :: a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a Source #

ascii_CubeProduct :: a -> Term' a -> Term' a -> Term' a Source #

unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a Source #

newtype VarIdentToken Source #

Constructors

VarIdentToken String

Instances

Instances details

Data VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> VarIdentToken -> c VarIdentToken # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarIdentToken # toConstr :: VarIdentToken -> Constr # dataTypeOf :: VarIdentToken -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarIdentToken) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarIdentToken) # gmapT :: (forall b. Data b => b -> b) -> VarIdentToken -> VarIdentToken # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarIdentToken -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarIdentToken -> r # gmapQ :: (forall d. Data d => d -> u) -> VarIdentToken -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> VarIdentToken -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarIdentToken -> m VarIdentToken # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdentToken -> m VarIdentToken # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdentToken -> m VarIdentToken #
IsString VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fromString :: String -> VarIdentToken #
Generic VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep VarIdentToken :: Type -> Type # Methods from :: VarIdentToken -> Rep VarIdentToken x # to :: Rep VarIdentToken x -> VarIdentToken #
Read VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS VarIdentToken # readList :: ReadS [VarIdentToken] # readPrec :: ReadPrec VarIdentToken # readListPrec :: ReadPrec [VarIdentToken] #
Show VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> VarIdentToken -> ShowS # show :: VarIdentToken -> String # showList :: [VarIdentToken] -> ShowS #
Eq VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: VarIdentToken -> VarIdentToken -> Bool # (/=) :: VarIdentToken -> VarIdentToken -> Bool #
Ord VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: VarIdentToken -> VarIdentToken -> Ordering # (<) :: VarIdentToken -> VarIdentToken -> Bool # (<=) :: VarIdentToken -> VarIdentToken -> Bool # (>) :: VarIdentToken -> VarIdentToken -> Bool # (>=) :: VarIdentToken -> VarIdentToken -> Bool # max :: VarIdentToken -> VarIdentToken -> VarIdentToken # min :: VarIdentToken -> VarIdentToken -> VarIdentToken #
Print VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> VarIdentToken -> Doc Source #
type Rep VarIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep VarIdentToken = D1 ('MetaData "VarIdentToken" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'True) (C1 ('MetaCons "VarIdentToken" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)))

newtype HoleIdentToken Source #

Constructors

HoleIdentToken String

Instances

Instances details

Data HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> HoleIdentToken -> c HoleIdentToken # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HoleIdentToken # toConstr :: HoleIdentToken -> Constr # dataTypeOf :: HoleIdentToken -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HoleIdentToken) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HoleIdentToken) # gmapT :: (forall b. Data b => b -> b) -> HoleIdentToken -> HoleIdentToken # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdentToken -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdentToken -> r # gmapQ :: (forall d. Data d => d -> u) -> HoleIdentToken -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HoleIdentToken -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HoleIdentToken -> m HoleIdentToken # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdentToken -> m HoleIdentToken # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdentToken -> m HoleIdentToken #
IsString HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods fromString :: String -> HoleIdentToken #
Generic HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Associated Types type Rep HoleIdentToken :: Type -> Type # Methods from :: HoleIdentToken -> Rep HoleIdentToken x # to :: Rep HoleIdentToken x -> HoleIdentToken #
Read HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods readsPrec :: Int -> ReadS HoleIdentToken # readList :: ReadS [HoleIdentToken] # readPrec :: ReadPrec HoleIdentToken # readListPrec :: ReadPrec [HoleIdentToken] #
Show HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods showsPrec :: Int -> HoleIdentToken -> ShowS # show :: HoleIdentToken -> String # showList :: [HoleIdentToken] -> ShowS #
Eq HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods (==) :: HoleIdentToken -> HoleIdentToken -> Bool # (/=) :: HoleIdentToken -> HoleIdentToken -> Bool #
Ord HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods compare :: HoleIdentToken -> HoleIdentToken -> Ordering # (<) :: HoleIdentToken -> HoleIdentToken -> Bool # (<=) :: HoleIdentToken -> HoleIdentToken -> Bool # (>) :: HoleIdentToken -> HoleIdentToken -> Bool # (>=) :: HoleIdentToken -> HoleIdentToken -> Bool # max :: HoleIdentToken -> HoleIdentToken -> HoleIdentToken # min :: HoleIdentToken -> HoleIdentToken -> HoleIdentToken #
Print HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Print Methods prt :: Int -> HoleIdentToken -> Doc Source #
type Rep HoleIdentToken Source #
Instance details Defined in Language.Rzk.Syntax.Abs type Rep HoleIdentToken = D1 ('MetaData "HoleIdentToken" "Language.Rzk.Syntax.Abs" "rzk-0.7.4-7FvkIVXfwQV9exNV6IKg4P" 'True) (C1 ('MetaCons "HoleIdentToken" '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.Rzk.Syntax.Abs Methods hasPosition :: Command -> BNFC'Position Source #
HasPosition DeclUsedVars Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: DeclUsedVars -> BNFC'Position Source #
HasPosition HoleIdent Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: HoleIdent -> BNFC'Position Source #
HasPosition Language Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Language -> BNFC'Position Source #
HasPosition LanguageDecl Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: LanguageDecl -> BNFC'Position Source #
HasPosition Module Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Module -> BNFC'Position Source #
HasPosition Param Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Param -> BNFC'Position Source #
HasPosition ParamDecl Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: ParamDecl -> BNFC'Position Source #
HasPosition Pattern Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Pattern -> BNFC'Position Source #
HasPosition Restriction Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Restriction -> BNFC'Position Source #
HasPosition SectionName Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: SectionName -> BNFC'Position Source #
HasPosition Term Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Term -> BNFC'Position Source #
HasPosition VarIdent Source #
Instance details Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: VarIdent -> BNFC'Position Source #