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

Agda.Compiler.JS.Syntax

Documentation

data Exp Source

Constructors

Self
Local LocalId
Global GlobalId
Undefined
String String
Char Char
Integer Integer
Double Double
Lambda Nat Exp
Object (Map MemberId Exp)
Apply Exp [Exp]
Lookup Exp MemberId
If Exp Exp Exp
BinOp Exp String Exp
PreOp String Exp
Const String

Instances

Data Exp
Show Exp
Typeable Exp
Globals Exp
Uses Exp
Pretty Exp
EmbPrj Exp

newtype LocalId Source

Constructors

Instances

Eq LocalId
Data LocalId
Ord LocalId
Show LocalId
Typeable LocalId
Pretty LocalId
EmbPrj LocalId

newtype GlobalId Source

Constructors

GlobalId [String]

Instances

Eq GlobalId
Data GlobalId
Ord GlobalId
Show GlobalId
Typeable GlobalId
Pretty GlobalId
EmbPrj GlobalId

newtype MemberId Source

Constructors

MemberId String

Instances

Eq MemberId
Data MemberId
Ord MemberId
Show MemberId
Typeable MemberId
Pretty MemberId
EmbPrj MemberId

data Export Source

Constructors

Export
Fields expName :: [MemberId] defn :: Exp

Instances

Data Export
Show Export
Typeable Export
Globals Export
Uses Export

data Module Source

Constructors

Module
Fields modName :: GlobalId exports :: [Export]

Instances

Data Module
Show Module
Typeable Module
Globals Module
Pretty Module

class Uses a whereSource

Methods

uses :: a -> Set [MemberId]Source

Instances

Uses Export
Uses Exp
Uses a => Uses [a]
Uses a => Uses (Map k a)

class Globals a whereSource

Methods

globals :: a -> Set GlobalId Source

Instances

Globals Module
Globals Export
Globals Exp
Globals a => Globals [a]
Globals a => Globals (Map k a)