Agda-2.4.2.1: 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 
ToAbstract TypedBinding TypedBinding 
ToAbstract TypedBindings TypedBindings 
ToAbstract LamBinding LamBinding 
ToAbstract Expr Expr 
ToAbstract ArgInfo ArgInfo 
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 OldName QName 
ToAbstract OldQName Expr 
ToAbstract Pragma [Pragma] 
ToAbstract LHSCore (LHSCore' Expr) 
ToAbstract Pattern (Pattern' Expr) 
ToAbstract LetDef [LetBinding] 
ToAbstract LetDefs [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

ToAbstract (NewName Name) Name 
ToAbstract (NewName BoundName) Name 
ToAbstract c a => ToAbstract [c] [a] 
ToAbstract [Declaration] [Declaration] 
ToAbstract c a => ToAbstract (Maybe c) (Maybe a) 
ToAbstract c a => ToAbstract (Arg c) (Arg a) 
ToAbstract (Pattern' Expr) (Pattern' Expr) 
ToAbstract (LHSCore' Expr) (LHSCore' Expr) 
ToAbstract c a => ToAbstract (NamedArg c) (NamedArg a) 
(ToAbstract c1 a1, ToAbstract c2 a2) => ToAbstract (c1, c2) (a1, a2) 
ToAbstract c a => ToAbstract (Named name c) (Named name a) 
(ToAbstract c1 a1, ToAbstract c2 a2, ToAbstract c3 a3) => ToAbstract (c1, c2, c3) (a1, a2, a3) 

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

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

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.