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

Safe HaskellNone
LanguageHaskell98

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.

Methods

toAbstract :: concrete -> ScopeM abstract

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

Constructors

OldName Name 

data TopLevel a

Temporary data type to scope check a file.

Constructors

TopLevel 

Fields

topLevelPath :: AbsolutePath

The file path from which we loaded this module.

topLevelTheThing :: a

The file content.

topLevelModuleName :: TopLevelInfo -> ModuleName

The top-level module name.