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.
- 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 {}
- 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
Instances
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
Constructors
| TopLevel a |
Instances
topLevelModuleName :: TopLevelInfo -> ModuleNameSource
The top-level module name.
data AbstractRHS Source
data NewModuleName Source
Instances
data OldModuleName Source
Instances
Instances
Instances
data LeftHandSide Source
Instances
data RightHandSide Source
Instances
Instances
Instances
Instances
Instances