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 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 (DeclUsedVars' a) [Param' a] (Term' a)
- | CommandAssume a [VarIdent] (Term' a)
- | CommandSection a (SectionName' a) [Command' a] (SectionName' a)
- | CommandDefine a VarIdent (DeclUsedVars' a) [Param' a] (Term' a) (Term' a)
- type DeclUsedVars = DeclUsedVars' BNFC'Position
- data DeclUsedVars' a = DeclUsedVars a [VarIdent]
- type SectionName = SectionName' BNFC'Position
- data SectionName' a
- = NoSectionName a
- | SomeSectionName a VarIdent
- type Pattern = Pattern' BNFC'Position
- data Pattern' a
- = PatternWildcard a
- | PatternVar a VarIdent
- | 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)
- type ParamDecl = ParamDecl' BNFC'Position
- data ParamDecl' a
- = ParamType a (Term' a)
- | ParamWildcardType a (Term' a)
- | ParamVarType a (Pattern' a) (Term' a)
- | ParamVarShape a (Pattern' a) (Term' a) (Term' a)
- type Restriction = Restriction' BNFC'Position
- data Restriction' a = 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]
- | TypeFun a (ParamDecl' a) (Term' a)
- | TypeSigma a (Pattern' a) (Term' a) (Term' a)
- | TypeId a (Term' a) (Term' a) (Term' a)
- | TypeIdSimple a (Term' a) (Term' a)
- | TypeRestricted a (Term' a) [Restriction' 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)
- | 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
- | Var a VarIdent
- | TypeAsc a (Term' a) (Term' a)
- commandPostulateNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Command' a
- commandVariable :: a -> VarIdent -> Term' a -> Command' a
- commandVariables :: a -> [VarIdent] -> Term' a -> Command' a
- commandDefineNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
- commandDef :: a -> VarIdent -> DeclUsedVars' a -> [Param' a] -> Term' a -> Term' a -> Command' a
- commandDefNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a
- noDeclUsedVars :: a -> DeclUsedVars' a
- paramVarType :: a -> VarIdent -> Term' a -> ParamDecl' a
- paramVarShape :: a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a
- recOr :: a -> Term' a -> Term' a -> Term' a -> Term' a -> Term' a
- typeExtension :: a -> ParamDecl' a -> Term' a -> Term' a
- unicode_TypeFun :: a -> ParamDecl' a -> Term' a -> Term' a
- unicode_TypeSigma :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
- unicode_TypeSigmaAlt :: a -> Pattern' a -> Term' a -> Term' a -> Term' a
- newtype VarIdent = VarIdent String
- newtype HoleIdent = HoleIdent 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 #
Constructors
Module a (LanguageDecl' a) [Command' a] |
Instances
Foldable Module' Source # | |
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 # elem :: Eq a => a -> Module' a -> Bool # maximum :: Ord a => Module' a -> a # minimum :: Ord a => Module' a -> a # | |
Traversable Module' Source # | |
Functor Module' Source # | |
HasPosition Module Source # | |
Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Module -> BNFC'Position Source # | |
Data a => Data (Module' a) Source # | |
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 # | |
Read a => Read (Module' a) Source # | |
Show a => Show (Module' a) Source # | |
Eq a => Eq (Module' a) Source # | |
Ord a => Ord (Module' a) Source # | |
Print (Module' a) Source # | |
type Rep (Module' a) Source # | |
Defined in Language.Rzk.Syntax.Abs type Rep (Module' a) = D1 ('MetaData "Module'" "Language.Rzk.Syntax.Abs" "rzk-0.4.0-8Pp1pewE9GgDyybOGOKQ0t" '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])))) |
data LanguageDecl' a Source #
Constructors
LanguageDecl a (Language' a) |
Instances
type Language = Language' BNFC'Position Source #
Constructors
Rzk1 a |
Instances
Foldable Language' Source # | |
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] # length :: Language' a -> Int # elem :: Eq a => a -> Language' a -> Bool # maximum :: Ord a => Language' a -> a # minimum :: Ord a => Language' a -> a # | |
Traversable Language' Source # | |
Defined in Language.Rzk.Syntax.Abs | |
Functor Language' Source # | |
HasPosition Language Source # | |
Defined in Language.Rzk.Syntax.Abs Methods hasPosition :: Language -> BNFC'Position Source # | |
Data a => Data (Language' a) Source # | |
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 # | |
Read a => Read (Language' a) Source # | |
Show a => Show (Language' a) Source # | |
Eq a => Eq (Language' a) Source # | |
Ord a => Ord (Language' a) Source # | |
Defined in Language.Rzk.Syntax.Abs | |
Print (Language' a) Source # | |
type Rep (Language' a) Source # | |
Defined in Language.Rzk.Syntax.Abs |
type Command = Command' BNFC'Position 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 (DeclUsedVars' a) [Param' a] (Term' a) | |
CommandAssume a [VarIdent] (Term' a) | |
CommandSection a (SectionName' a) [Command' a] (SectionName' a) | |
CommandDefine a VarIdent (DeclUsedVars' a) [Param' a] (Term' a) (Term' a) |
Instances
data DeclUsedVars' a Source #
Constructors
DeclUsedVars a [VarIdent] |
Instances
type SectionName = SectionName' BNFC'Position Source #
data SectionName' a Source #
Constructors
NoSectionName a | |
SomeSectionName a VarIdent |
Instances
type Pattern = Pattern' BNFC'Position Source #
Constructors
PatternWildcard a | |
PatternVar a VarIdent | |
PatternPair a (Pattern' a) (Pattern' a) |
Instances
type Param = Param' BNFC'Position Source #
Constructors
ParamPattern a (Pattern' a) | |
ParamPatternType a [Pattern' a] (Term' a) | |
ParamPatternShape a (Pattern' a) (Term' a) (Term' a) |
Instances
type ParamDecl = ParamDecl' BNFC'Position Source #
data ParamDecl' a Source #
Constructors
ParamType a (Term' a) | |
ParamWildcardType a (Term' a) | |
ParamVarType a (Pattern' a) (Term' a) | |
ParamVarShape a (Pattern' a) (Term' a) (Term' a) |
Instances
type Restriction = Restriction' BNFC'Position Source #
data Restriction' a Source #
Constructors
Restriction a (Term' a) (Term' a) |
Instances
type Term = Term' BNFC'Position 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] | |
TypeFun a (ParamDecl' a) (Term' a) | |
TypeSigma a (Pattern' a) (Term' a) (Term' a) | |
TypeId a (Term' a) (Term' a) (Term' a) | |
TypeIdSimple a (Term' a) (Term' a) | |
TypeRestricted a (Term' a) [Restriction' 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) | |
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 | |
Var a VarIdent | |
TypeAsc a (Term' a) (Term' a) |
Instances
commandPostulateNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Command' a Source #
commandDefineNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a Source #
commandDef :: a -> VarIdent -> DeclUsedVars' a -> [Param' a] -> Term' a -> Term' a -> Command' a Source #
commandDefNoParams :: a -> VarIdent -> DeclUsedVars' a -> Term' a -> Term' a -> Command' a Source #
noDeclUsedVars :: a -> DeclUsedVars' a Source #
paramVarType :: a -> VarIdent -> Term' a -> ParamDecl' a Source #
paramVarShape :: a -> Pattern' a -> Term' a -> Term' a -> ParamDecl' a Source #
typeExtension :: a -> ParamDecl' a -> Term' a -> Term' a Source #
unicode_TypeFun :: a -> ParamDecl' a -> Term' a -> Term' a Source #
Instances
Data VarIdent Source # | |
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 -> c VarIdent # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c VarIdent # toConstr :: VarIdent -> Constr # dataTypeOf :: VarIdent -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c VarIdent) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c VarIdent) # gmapT :: (forall b. Data b => b -> b) -> VarIdent -> VarIdent # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> VarIdent -> r # gmapQ :: (forall d. Data d => d -> u) -> VarIdent -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> VarIdent -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> VarIdent -> m VarIdent # | |
IsString Term' Source # | |
Defined in Language.Rzk.Free.Syntax Methods fromString :: String -> Term' # | |
IsString VarIdent Source # | |
Defined in Language.Rzk.Syntax.Abs Methods fromString :: String -> VarIdent # | |
Generic VarIdent Source # | |
Read VarIdent Source # | |
Show Term' Source # | |
Show TermT' Source # | |
Show VarIdent Source # | |
Eq VarIdent Source # | |
Ord VarIdent Source # | |
Defined in Language.Rzk.Syntax.Abs | |
Print VarIdent Source # | |
Print [VarIdent] Source # | |
type Rep VarIdent Source # | |
Defined in Language.Rzk.Syntax.Abs |
Instances
Data HoleIdent Source # | |
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 -> c HoleIdent # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c HoleIdent # toConstr :: HoleIdent -> Constr # dataTypeOf :: HoleIdent -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c HoleIdent) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c HoleIdent) # gmapT :: (forall b. Data b => b -> b) -> HoleIdent -> HoleIdent # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdent -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> HoleIdent -> r # gmapQ :: (forall d. Data d => d -> u) -> HoleIdent -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> HoleIdent -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> HoleIdent -> m HoleIdent # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdent -> m HoleIdent # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> HoleIdent -> m HoleIdent # | |
IsString HoleIdent Source # | |
Defined in Language.Rzk.Syntax.Abs Methods fromString :: String -> HoleIdent # | |
Generic HoleIdent Source # | |
Read HoleIdent Source # | |
Show HoleIdent Source # | |
Eq HoleIdent Source # | |
Ord HoleIdent Source # | |
Print HoleIdent Source # | |
type Rep HoleIdent Source # | |
Defined in Language.Rzk.Syntax.Abs |
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 #