Agda-2.4.2.5: 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 Source

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

Methods

toAbstract :: concrete -> ScopeM abstract Source

Instances

ToAbstract RHS AbstractRHS Source 
ToAbstract TypedBinding TypedBinding Source 
ToAbstract TypedBindings TypedBindings Source 
ToAbstract LamBinding LamBinding Source 
ToAbstract Expr Expr Source 
ToAbstract ArgInfo ArgInfo Source 
ToAbstract Clause Clause Source 
ToAbstract NiceDeclaration Declaration Source 
ToAbstract LeftHandSide LHS Source 
ToAbstract AbstractRHS RHS Source 
ToAbstract RightHandSide AbstractRHS Source 
ToAbstract OldModuleName ModuleName Source 
ToAbstract NewModuleQName ModuleName Source 
ToAbstract NewModuleName ModuleName Source 
ToAbstract PatName APatName Source 
ToAbstract OldName QName Source 
ToAbstract OldQName Expr Source 
ToAbstract Pragma [Pragma] Source 
ToAbstract LHSCore (LHSCore' Expr) Source 
ToAbstract Pattern (Pattern' Expr) Source 
ToAbstract LetDef [LetBinding] Source 
ToAbstract LetDefs [LetBinding] Source 
ToAbstract (TopLevel [Declaration]) TopLevelInfo Source

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

ToAbstract (NewName Name) Name Source 
ToAbstract (NewName BoundName) Name Source 
ToAbstract c a => ToAbstract [c] [a] Source 
ToAbstract [Declaration] [Declaration] Source 
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) Source 
ToAbstract c a => ToAbstract (WithHiding c) (WithHiding a) Source 
ToAbstract c a => ToAbstract (Arg c) (Arg a) Source 
ToAbstract (Pattern' Expr) (Pattern' Expr) Source 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) Source 
ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a) Source 
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) Source 
ToAbstract c a => ToAbstract (Named name c) (Named name a) Source 
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) 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.

newtype OldName Source

Constructors

OldName Name 

data TopLevel a Source

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.

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo Source

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

data TopLevelInfo Source

Instances

ToAbstract (TopLevel [Declaration]) TopLevelInfo Source

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 Source

The top-level module name.