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

Safe HaskellNone
LanguageHaskell2010

Agda.Compiler.JS.Syntax

Documentation

data Exp #

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 
PlainJS String

Arbitrary JS code.

Instances
Show Exp # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Exp -> ShowS #

show :: Exp -> String #

showList :: [Exp] -> ShowS #

Globals Exp # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId #

Uses Exp # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] #

Pretty Exp # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> Exp -> String #

newtype LocalId #

Constructors

LocalId Nat 
Instances
Eq LocalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord LocalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: LocalId -> LocalId -> Ordering #

(<) :: LocalId -> LocalId -> Bool #

(<=) :: LocalId -> LocalId -> Bool #

(>) :: LocalId -> LocalId -> Bool #

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

max :: LocalId -> LocalId -> LocalId #

min :: LocalId -> LocalId -> LocalId #

Show LocalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> LocalId -> ShowS #

show :: LocalId -> String #

showList :: [LocalId] -> ShowS #

Pretty LocalId # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> LocalId -> String #

newtype GlobalId #

Constructors

GlobalId [String] 
Instances
Eq GlobalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord GlobalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: GlobalId -> GlobalId -> Ordering #

(<) :: GlobalId -> GlobalId -> Bool #

(<=) :: GlobalId -> GlobalId -> Bool #

(>) :: GlobalId -> GlobalId -> Bool #

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

max :: GlobalId -> GlobalId -> GlobalId #

min :: GlobalId -> GlobalId -> GlobalId #

Show GlobalId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> GlobalId -> ShowS #

show :: GlobalId -> String #

showList :: [GlobalId] -> ShowS #

Pretty GlobalId # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> GlobalId -> String #

newtype MemberId #

Constructors

MemberId String 
Instances
Eq MemberId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord MemberId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: MemberId -> MemberId -> Ordering #

(<) :: MemberId -> MemberId -> Bool #

(<=) :: MemberId -> MemberId -> Bool #

(>) :: MemberId -> MemberId -> Bool #

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

max :: MemberId -> MemberId -> MemberId #

min :: MemberId -> MemberId -> MemberId #

Show MemberId # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> MemberId -> ShowS #

show :: MemberId -> String #

showList :: [MemberId] -> ShowS #

Pretty MemberId # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> MemberId -> String #

data Export #

Constructors

Export 

Fields

Instances
Show Export # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Export -> ShowS #

show :: Export -> String #

showList :: [Export] -> ShowS #

Globals Export # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId #

Uses Export # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] #

data Module #

Constructors

Module 

Fields

Instances
Show Module # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Module -> ShowS #

show :: Module -> String #

showList :: [Module] -> ShowS #

Globals Module # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId #

Pretty Module # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: Nat -> Int -> Module -> String #

class Uses a where #

Minimal complete definition

uses

Methods

uses :: a -> Set [MemberId] #

Instances
Uses Export # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] #

Uses Exp # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] #

Uses a => Uses [a] # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: [a] -> Set [MemberId] #

Uses a => Uses (Map k a) # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Map k a -> Set [MemberId] #

class Globals a where #

Minimal complete definition

globals

Methods

globals :: a -> Set GlobalId #

Instances
Globals Module # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId #

Globals Export # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId #

Globals Exp # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId #

Globals a => Globals [a] # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: [a] -> Set GlobalId #

Globals a => Globals (Map k a) # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Map k a -> Set GlobalId #