Agda-2.6.2.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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
Eq Decl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

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

data DataOrNew Source #

Constructors

DataType 
NewType 

Instances

Instances details
Eq DataOrNew Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ConDecl Source #

Constructors

ConDecl Name [(Maybe Strictness, Type)] 

Instances

Instances details
Eq ConDecl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty ConDecl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Strictness Source #

Constructors

Lazy 
Strict 

Instances

Instances details
Eq Strictness Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

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

data Binds Source #

Constructors

BDecls [Decl] 

Instances

Instances details
Eq Binds Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

MakeStrict Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Rhs Source #

Instances

Instances details
Eq Rhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

MakeStrict Rhs Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Methods

makeStrict :: Rhs -> Rhs Source #

data GuardedRhs Source #

Constructors

GuardedRhs [Stmt] Exp 

Instances

Instances details
Eq GuardedRhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

MakeStrict GuardedRhs Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 

Instances

Instances details
Eq Match Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

MakeStrict Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Strict

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Expressions

data Type Source #

Instances

Instances details
Eq Type Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Type Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Pat Source #

Instances

Instances details
Eq Pat Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

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

data Stmt Source #

Constructors

Qualifier Exp 
Generator Pat Exp 

Instances

Instances details
Eq Stmt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

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

data Exp Source #

Instances

Instances details
Eq Exp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

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

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) 

Instances

Instances details
Eq Alt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

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

data Literal Source #

Instances

Instances details
Eq Literal Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Literal Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Names

data QName Source #

Constructors

Qual ModuleName Name 
UnQual Name 

Instances

Instances details
Eq QName Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty QName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Name Source #

Constructors

Ident String 
Symbol String 

Instances

Instances details
Eq Name Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Name Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data QOp Source #

Constructors

QVarOp QName 

Instances

Instances details
Eq QOp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty QOp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data TyVarBind Source #

Constructors

UnkindedVar Name 

Instances

Instances details
Eq TyVarBind Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty