Agda-2.6.1: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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

Arbitrary JS code.

Instances

Instances details
Show Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Exp -> ShowS Source #

show :: Exp -> String Source #

showList :: [Exp] -> ShowS Source #

Globals Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId Source #

Uses Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

newtype LocalId Source #

Constructors

LocalId Nat 

Instances

Instances details
Eq LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: LocalId -> LocalId -> Ordering Source #

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

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

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

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

max :: LocalId -> LocalId -> LocalId Source #

min :: LocalId -> LocalId -> LocalId Source #

Show LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> LocalId -> ShowS Source #

show :: LocalId -> String Source #

showList :: [LocalId] -> ShowS Source #

Pretty LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

newtype GlobalId Source #

Constructors

GlobalId [String] 

Instances

Instances details
Eq GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: GlobalId -> GlobalId -> Ordering Source #

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

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

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

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

max :: GlobalId -> GlobalId -> GlobalId Source #

min :: GlobalId -> GlobalId -> GlobalId Source #

Show GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> GlobalId -> ShowS Source #

show :: GlobalId -> String Source #

showList :: [GlobalId] -> ShowS Source #

Pretty GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

newtype MemberId Source #

Constructors

MemberId String 

Instances

Instances details
Eq MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: MemberId -> MemberId -> Ordering Source #

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

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

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

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

max :: MemberId -> MemberId -> MemberId Source #

min :: MemberId -> MemberId -> MemberId Source #

Show MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> MemberId -> ShowS Source #

show :: MemberId -> String Source #

showList :: [MemberId] -> ShowS Source #

Pretty MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

data Export Source #

Constructors

Export 

Fields

Instances

Instances details
Show Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Export -> ShowS Source #

show :: Export -> String Source #

showList :: [Export] -> ShowS Source #

Globals Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId Source #

Uses Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] Source #

data Module Source #

Constructors

Module 

Fields

Instances

Instances details
Show Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Module -> ShowS Source #

show :: Module -> String Source #

showList :: [Module] -> ShowS Source #

Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId Source #

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

class Uses a where Source #

Methods

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

Instances

Instances details
Uses Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set [MemberId] Source #

Uses Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set [MemberId] Source #

Uses a => Uses [a] Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Defined in Agda.Compiler.JS.Syntax

Methods

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

class Globals a where Source #

Methods

globals :: a -> Set GlobalId Source #

Instances

Instances details
Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId Source #

Globals Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId Source #

Globals Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId Source #

Globals a => Globals [a] Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: [a] -> Set GlobalId Source #

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

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Map k a -> Set GlobalId Source #