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

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 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.

newtype OldName Source

Constructors

OldName Name 

newtype TopLevel a Source

Constructors

TopLevel a 

topLevelModuleName :: TopLevelInfo -> ModuleNameSource

The top-level module name.