Agda-2.6.20240714: 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 Expr Source #

Scope check an expression.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Expr 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract HoleContent Source #

Content of interaction hole.

Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon HoleContent 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LHSCore Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LHSCore 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract LamBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon LamBinding 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract ModuleAssignment Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pattern Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pattern 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Pragma Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Pragma 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon RHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract RewriteEqn Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract TypedBinding Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract Clause Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon Clause 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NiceDeclaration Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract AbstractRHS Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon AbstractRHS 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract NewModuleQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract OldModuleName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldQName 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract PatName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon PatName 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract () Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon () 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon () = ()

Methods

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

ToAbstract (LHSCore' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (LHSCore' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (Pattern' Expr) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Pattern' Expr) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Arg c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Arg c) = Arg (AbsOfCon c)

Methods

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

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Ranged c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (WithHiding c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName)) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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]) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (List1 c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (List1 c) = List1 (AbsOfCon c)
ToAbstract c => ToAbstract (Maybe c) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Maybe c) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Maybe c) = Maybe (AbsOfCon c)
ToAbstract c => ToAbstract [c] Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon [c] 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon [c] = [AbsOfCon c]

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) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Named name c) = Named name (AbsOfCon c)

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) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (Either c1 c2) = Either (AbsOfCon c1) (AbsOfCon c2)

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) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (c1, c2) = (AbsOfCon c1, AbsOfCon c2)

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) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (c1, c2, c3) = (AbsOfCon c1, AbsOfCon c2, AbsOfCon c3)

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

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]) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 #

Instances

Instances details
Functor NewName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Methods

fmap :: (a -> b) -> NewName a -> NewName b

(<$) :: a -> NewName b -> NewName a #

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (Binder' (NewName BoundName)) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName BoundName) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

ToAbstract (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon (NewName Name) 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName BoundName) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

type AbsOfCon (NewName Name) Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

data OldQName Source #

Instances

Instances details
ToAbstract OldQName Source # 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

Associated Types

type AbsOfCon OldQName 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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 
Instance details

Defined in Agda.Syntax.Translation.ConcreteToAbstract

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.