Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

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 where Source

Things that can be translated to abstract syntax are instances of this class. Methods toAbstract :: concrete -> ScopeM abstract Source

localToAbstract :: ToAbstract c a => c -> (a -> ScopeM b) -> ScopeM b Source

This operation does not affect the scope, i.e. the original scope is restored upon completion.

concreteToAbstract_ :: ToAbstract c a => c -> ScopeM a Source

Computes the range of all the "to" keywords used in a renaming directive.

concreteToAbstract :: ToAbstract c a => ScopeInfo -> c -> ScopeM a Source

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 -> ModuleName Source

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