Agda-2.5.2: A dependently typed functional programming language and proof assistant

Safe HaskellNone
LanguageHaskell2010

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

Documentation

class ToAbstract concrete abstract | concrete -> abstract where #

Things that can be translated to abstract syntax are instances of this class.

Minimal complete definition

toAbstract

Methods

toAbstract :: concrete -> ScopeM abstract #

Instances

ToAbstract RHS AbstractRHS # 
ToAbstract TypedBinding TypedBinding # 
ToAbstract TypedBindings TypedBindings # 
ToAbstract LamBinding LamBinding # 
ToAbstract Expr Expr # 

Methods

toAbstract :: Expr -> ScopeM Expr #

ToAbstract Clause Clause # 
ToAbstract NiceDeclaration Declaration # 
ToAbstract LeftHandSide LHS # 
ToAbstract AbstractRHS RHS # 
ToAbstract RightHandSide AbstractRHS # 
ToAbstract OldModuleName ModuleName # 
ToAbstract NewModuleQName ModuleName # 
ToAbstract NewModuleName ModuleName # 
ToAbstract PatName APatName # 
ToAbstract OldQName Expr # 
ToAbstract Pragma [Pragma] # 
ToAbstract LHSCore (LHSCore' Expr) # 
ToAbstract Pattern (Pattern' Expr) # 
ToAbstract LetDef [LetBinding] # 
ToAbstract LetDefs [LetBinding] # 
ToAbstract ModuleAssignment (ModuleName, [LetBinding]) # 
ToAbstract (TopLevel [Declaration]) TopLevelInfo #

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

(Show a, ToQName a) => ToAbstract (OldName a) QName # 
ToAbstract (NewName Name) Name # 
ToAbstract (NewName BoundName) Name # 
ToAbstract c a => ToAbstract [c] [a] # 

Methods

toAbstract :: [c] -> ScopeM [a] #

ToAbstract [Declaration] [Declaration] # 
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) # 

Methods

toAbstract :: Maybe c -> ScopeM (Maybe a) #

ToAbstract c a => ToAbstract (Arg c) (Arg a) # 

Methods

toAbstract :: Arg c -> ScopeM (Arg a) #

ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) # 
ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a) # 
ToAbstract (Pattern' Expr) (Pattern' Expr) # 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) # 
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (Either c1 c2) (Either a1 a2) # 

Methods

toAbstract :: Either c1 c2 -> ScopeM (Either a1 a2) #

(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) # 

Methods

toAbstract :: (c1, c2) -> ScopeM (a1, a2) #

ToAbstract c a => ToAbstract (Named name c) (Named name a) # 

Methods

toAbstract :: Named name c -> ScopeM (Named name a) #

(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) # 

Methods

toAbstract :: (c1, c2, c3) -> ScopeM (a1, a2, a3) #

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

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

newtype OldName a #

Constructors

OldName a 

Instances

(Show a, ToQName a) => ToAbstract (OldName a) QName # 

data TopLevel a #

Temporary data type to scope check a file.

Constructors

TopLevel 

Fields

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo #

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

data TopLevelInfo #

Constructors

TopLevelInfo 

Fields

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo #

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

topLevelModuleName :: TopLevelInfo -> ModuleName #

The top-level module name.