Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Syntax.Translation.ConcreteToAbstract
Description
Translation from Agda.Syntax.Concrete to Agda.Syntax.Abstract. Involves scope analysis, figuring out infix operator precedences and tidying up definitions.
Synopsis
class ToAbstract concrete abstract | concrete -> abstract where
toAbstract :: concrete -> ScopeM abstract
localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a
newtype NewModuleQName = NewModuleQName QName
newtype OldName = OldName Name
newtype TopLevel a = TopLevel a
data TopLevelInfo = TopLevelInfo {
topLevelDecls :: [Declaration]
outsideScope :: ScopeInfo
insideScope :: ScopeInfo
}
topLevelModuleName :: TopLevelInfo -> ModuleName
data AbstractRHS
data NewModuleName
data OldModuleName
data NewName a
data OldQName
data LeftHandSide
data RightHandSide
data PatName
data APatName
data LetDef
data LetDefs
Documentation
class ToAbstract concrete abstract | concrete -> abstract whereSource
Things that can be translated to abstract syntax are instances of this class.
Methods
toAbstract :: concrete -> ScopeM abstractSource
localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM bSource
This operation does not affect the scope, i.e. the original scope is restored upon completion.
concreteToAbstract_ :: ToAbstract c a => c -> ScopeM aSource
Computes the range of all the "to" keywords used in a renaming directive.
concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM aSource
newtype NewModuleQName Source
Constructors
NewModuleQName QName
newtype OldName Source
Constructors
OldName Name
newtype TopLevel a Source
Constructors
TopLevel a
data TopLevelInfo Source
Constructors
TopLevelInfo
topLevelDecls :: [Declaration]
outsideScope :: ScopeInfo
insideScope :: ScopeInfo
topLevelModuleName :: TopLevelInfo -> ModuleNameSource
The top-level module name.
data AbstractRHS Source
data NewModuleName Source
data OldModuleName Source
data NewName a Source
data OldQName Source
data LeftHandSide Source
data RightHandSide Source
data PatName Source
data APatName Source
data LetDef Source
data LetDefs Source
Produced by Haddock version 2.6.0