Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell2010

Agda.Utils.Haskell.Syntax

Contents

Description

ASTs for subset of GHC Haskell syntax.

Synopsis

Modules

data Module Source #

Instances
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).

data ImportDecl Source #

Constructors

ImportDecl 

Fields

data ImportSpec Source #

Constructors

IVar Name 

Declarations

data Decl Source #

Instances
Eq Decl Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Decl Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Decl -> Doc Source #

prettyPrec :: Int -> Decl -> Doc Source #

prettyList :: [Decl] -> Doc Source #

data DataOrNew Source #

Constructors

DataType 
NewType 
Instances
Eq DataOrNew Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: DataOrNew -> DataOrNew -> Bool

(/=) :: DataOrNew -> DataOrNew -> Bool

Pretty DataOrNew Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data ConDecl Source #

Constructors

ConDecl Name [(Maybe Strictness, Type)] 
Instances
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
Eq Strictness Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: Strictness -> Strictness -> Bool

(/=) :: Strictness -> Strictness -> Bool

Pretty Strictness Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

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

data Binds Source #

Constructors

BDecls [Decl] 
Instances
Eq Binds Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Binds Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data Rhs Source #

Instances
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
Eq GuardedRhs Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: GuardedRhs -> GuardedRhs -> Bool

(/=) :: GuardedRhs -> GuardedRhs -> Bool

data Match Source #

Constructors

Match Name [Pat] Rhs (Maybe Binds) 
Instances
Eq Match Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Match Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Expressions

data Type Source #

Instances
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

Methods

pretty :: Type -> Doc Source #

prettyPrec :: Int -> Type -> Doc Source #

prettyList :: [Type] -> Doc Source #

data Pat Source #

Instances
Eq Pat Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Pat Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Pat -> Doc Source #

prettyPrec :: Int -> Pat -> Doc Source #

prettyList :: [Pat] -> Doc Source #

data Stmt Source #

Constructors

Qualifier Exp 
Generator Pat Exp 
Instances
Eq Stmt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Stmt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Stmt -> Doc Source #

prettyPrec :: Int -> Stmt -> Doc Source #

prettyList :: [Stmt] -> Doc Source #

data Exp Source #

Instances
Eq Exp Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Exp -> Doc Source #

prettyPrec :: Int -> Exp -> Doc Source #

prettyList :: [Exp] -> Doc Source #

data Alt Source #

Constructors

Alt Pat Rhs (Maybe Binds) 
Instances
Eq Alt Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

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

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

Pretty Alt Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

Methods

pretty :: Alt -> Doc Source #

prettyPrec :: Int -> Alt -> Doc Source #

prettyList :: [Alt] -> Doc Source #

data Literal Source #

Constructors

Int Integer 
Frac Rational 
Char Char 
String String 
Instances
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 ModuleName Source #

Constructors

ModuleName String 
Instances
Eq ModuleName Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: ModuleName -> ModuleName -> Bool

(/=) :: ModuleName -> ModuleName -> Bool

Ord ModuleName Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Pretty ModuleName Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty

data QName Source #

Constructors

Qual ModuleName Name 
UnQual Name 
Instances
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
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

Methods

pretty :: Name -> Doc Source #

prettyPrec :: Int -> Name -> Doc Source #

prettyList :: [Name] -> Doc Source #

data QOp Source #

Constructors

QVarOp QName 
Instances
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

Methods

pretty :: QOp -> Doc Source #

prettyPrec :: Int -> QOp -> Doc Source #

prettyList :: [QOp] -> Doc Source #

data TyVarBind Source #

Constructors

UnkindedVar Name 
Instances
Eq TyVarBind Source # 
Instance details

Defined in Agda.Utils.Haskell.Syntax

Methods

(==) :: TyVarBind -> TyVarBind -> Bool

(/=) :: TyVarBind -> TyVarBind -> Bool

Pretty TyVarBind Source # 
Instance details

Defined in Agda.Compiler.MAlonzo.Pretty