Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Utils.Haskell.Syntax

Description

ASTs for subset of GHC Haskell syntax.

Synopsis

Modules

data Module Source #

Instances

Instances details
MakeStrict Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ModulePragma Source #

Constructors

LanguagePragma [Name] 
OtherPragma String

Unstructured pragma (Andreas, 2017-08-23, issue #2712).

Instances

Instances details
Pretty ModulePragma Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ImportSpec Source #

Constructors

IVar Name 

Instances

Instances details
Pretty ImportSpec Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Declarations

data Decl Source #

Constructors

TypeDecl Name [TyVarBind] Type 
DataDecl DataOrNew Name [TyVarBind] [ConDecl] [Deriving] 
TypeSig [Name] Type 
FunBind [Match]

Should not be used when LocalBind could be used.

LocalBind Strictness Name Rhs

Should only be used in let or where.

PatSyn Pat Pat 
FakeDecl String 
Comment String 

Instances

Instances details
MakeStrict Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Decl -> Decl Source #

Pretty Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Decl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Decl -> Decl -> Bool #

(/=) :: Decl -> Decl -> Bool #

data DataOrNew Source #

Constructors

DataType 
NewType 

Instances

Instances details
Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq DataOrNew Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

data ConDecl Source #

Constructors

ConDecl Name [(Maybe Strictness, Type)] 

Instances

Instances details
Pretty ConDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq ConDecl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: ConDecl -> ConDecl -> Bool #

(/=) :: ConDecl -> ConDecl -> Bool #

data Strictness Source #

Constructors

Lazy 
Strict 

Instances

Instances details
Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Strictness Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

type Deriving = (QName, [Type]) Source #

data Binds Source #

Constructors

BDecls [Decl] 

Instances

Instances details
MakeStrict Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Binds Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Binds -> Binds -> Bool #

(/=) :: Binds -> Binds -> Bool #

data Rhs Source #

Instances

Instances details
MakeStrict Rhs Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Rhs -> Rhs Source #

Eq Rhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Rhs -> Rhs -> Bool #

(/=) :: Rhs -> Rhs -> Bool #

data GuardedRhs Source #

Constructors

GuardedRhs [Stmt] Exp 

Instances

Instances details
MakeStrict GuardedRhs Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Eq GuardedRhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 

Instances

Instances details
MakeStrict Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Match Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Match -> Match -> Bool #

(/=) :: Match -> Match -> Bool #

Expressions

data Type Source #

Instances

Instances details
Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Type Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Type -> Type -> Bool #

(/=) :: Type -> Type -> Bool #

data Pat Source #

Instances

Instances details
MakeStrict Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Pat -> Pat Source #

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Pat Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Pat -> Pat -> Bool #

(/=) :: Pat -> Pat -> Bool #

data Stmt Source #

Constructors

Qualifier Exp 
Generator Pat Exp 

Instances

Instances details
MakeStrict Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Stmt -> Stmt Source #

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Stmt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Stmt -> Stmt -> Bool #

(/=) :: Stmt -> Stmt -> Bool #

data Exp Source #

Instances

Instances details
MakeStrict Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Exp -> Exp Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Exp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Exp -> Exp -> Bool #

(/=) :: Exp -> Exp -> Bool #

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) 

Instances

Instances details
MakeStrict Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Alt -> Alt Source #

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Alt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Alt -> Alt -> Bool #

(/=) :: Alt -> Alt -> Bool #

data Literal Source #

Instances

Instances details
Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Literal Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Literal -> Literal -> Bool #

(/=) :: Literal -> Literal -> Bool #

Names

data QName Source #

Constructors

Qual ModuleName Name 
UnQual Name 

Instances

Instances details
Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq QName Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: QName -> QName -> Bool #

(/=) :: QName -> QName -> Bool #

data Name Source #

Constructors

Ident String 
Symbol String 

Instances

Instances details
Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq Name Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Name -> Name -> Bool #

(/=) :: Name -> Name -> Bool #

data QOp Source #

Constructors

QVarOp QName 

Instances

Instances details
Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq QOp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: QOp -> QOp -> Bool #

(/=) :: QOp -> QOp -> Bool #

data TyVarBind Source #

Constructors

UnkindedVar Name 

Instances

Instances details
Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Eq TyVarBind Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax