Agda-2.6.2.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 c where Source #

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

Associated Types

type AbsOfCon c Source #

Methods

toAbstract :: c -> ScopeM (AbsOfCon c) Source #

Instances

Instances details
ToAbstract () Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon () Source #

Methods

toAbstract :: () -> ScopeM (AbsOfCon ()) Source #

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

ToAbstract Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma Source #

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS Source #

ToAbstract LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore Source #

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RewriteEqn Source #

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon TypedBinding Source #

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding Source #

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern Source #

ToAbstract Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr Source #

ToAbstract ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ModuleAssignment Source #

ToAbstract Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Clause Source #

ToAbstract NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NiceDeclaration Source #

ToAbstract AbstractRHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon AbstractRHS Source #

ToAbstract OldModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldModuleName Source #

ToAbstract NewModuleQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NewModuleQName Source #

ToAbstract NewModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NewModuleName Source #

ToAbstract PatName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon PatName Source #

ToAbstract OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldQName Source #

ToAbstract c => ToAbstract [c] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon [c] Source #

Methods

toAbstract :: [c] -> ScopeM (AbsOfCon [c]) Source #

ToAbstract c => ToAbstract (Maybe c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Maybe c) Source #

ToAbstract c => ToAbstract (List1 c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (List1 c) Source #

ToAbstract c => ToAbstract (Arg c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Arg c) Source #

Methods

toAbstract :: Arg c -> ScopeM (AbsOfCon (Arg c)) Source #

ToAbstract c => ToAbstract (WithHiding c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (WithHiding c) Source #

ToAbstract (Binder' (NewName BoundName)) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName)) Source #

ToAbstract c => ToAbstract (FieldAssignment' c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (FieldAssignment' c) Source #

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) Source #

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

ToAbstract (TopLevel [Declaration]) Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration]) Source #

ToAbstract (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name) Source #

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) Source #

(ToAbstract c1, ToAbstract c2) => ToAbstract (Either c1 c2) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Either c1 c2) Source #

Methods

toAbstract :: Either c1 c2 -> ScopeM (AbsOfCon (Either c1 c2)) Source #

(ToAbstract c1, ToAbstract c2) => ToAbstract (c1, c2) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (c1, c2) Source #

Methods

toAbstract :: (c1, c2) -> ScopeM (AbsOfCon (c1, c2)) Source #

ToAbstract c => ToAbstract (Named name c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Named name c) Source #

Methods

toAbstract :: Named name c -> ScopeM (AbsOfCon (Named name c)) Source #

(ToAbstract c1, ToAbstract c2, ToAbstract c3) => ToAbstract (c1, c2, c3) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (c1, c2, c3) Source #

Methods

toAbstract :: (c1, c2, c3) -> ScopeM (AbsOfCon (c1, c2, c3)) Source #

ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source #

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

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

data TopLevel a Source #

Temporary data type to scope check a file.

Constructors

TopLevel 

Fields

Instances

Instances details
ToAbstract (TopLevel [Declaration]) Source #

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

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (TopLevel [Declaration]) Source #

type AbsOfCon (TopLevel [Declaration]) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data TopLevelInfo Source #

Constructors

TopLevelInfo 

Fields

topLevelModuleName :: TopLevelInfo -> ModuleName Source #

The top-level module name.

data NewName a Source #

data OldQName Source #

Instances

Instances details
ToAbstract OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldQName Source #

type AbsOfCon OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data PatName Source #

Instances

Instances details
ToAbstract PatName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon PatName Source #

type AbsOfCon PatName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

importPrimitives :: ScopeM [Declaration] Source #

Declaration open import Agda.Primitive using (Set; Prop) when optImportSorts.