Agda-2.6.3.20230805: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
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 Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr Source #

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent Source #

ToAbstract LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore Source #

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding Source #

ToAbstract ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon ModuleAssignment Source #

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern 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 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 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 NewModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NewModuleName Source #

ToAbstract NewModuleQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon NewModuleQName Source #

ToAbstract OldModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldModuleName Source #

ToAbstract OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldQName Source #

ToAbstract PatName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon PatName Source #

ToAbstract () Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon () Source #

Methods

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

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) Source #

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) 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 (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) Source #

ToAbstract (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name) 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 c => ToAbstract (List1 c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (List1 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 [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 (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 (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 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) when optImportSorts. Prop is added when optProp, and SSet when optTwoLevel.

checkAttributes :: Attributes -> ScopeM () Source #

Raises an error if the list of attributes contains an unsupported attribute.