Agda.Compiler.JS.Syntax

Documentation

data Exp

Constructors

Self

Local LocalId

Global GlobalId

Undefined

Null

String Text

Char Char

Integer Integer

Double Double

Lambda Nat Exp

Object (Map MemberId Exp)

Array [(Comment, 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

Pretty Exp

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Exp -> Doc

Globals Exp

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId

Uses Exp

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set JSQName

Show Exp

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Exp -> ShowS

show :: Exp -> String

showList :: [Exp] -> ShowS

Eq Exp

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

newtype LocalId

Constructors

LocalId Nat

Instances

Pretty LocalId

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> LocalId -> Doc

Show LocalId

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> LocalId -> ShowS

show :: LocalId -> String

showList :: [LocalId] -> ShowS

Eq LocalId

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord LocalId

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

newtype GlobalId

Constructors

GlobalId [String]

Instances

Pretty GlobalId

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> GlobalId -> Doc

Show GlobalId

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> GlobalId -> ShowS

show :: GlobalId -> String

showList :: [GlobalId] -> ShowS

Eq GlobalId

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord GlobalId

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

Pretty [(GlobalId, Export)]

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> [(GlobalId, Export)] -> Doc

data MemberId

Constructors

MemberId String

MemberIndex Int Comment

Instances

Pretty MemberId

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> MemberId -> Doc

Show MemberId

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> MemberId -> ShowS

show :: MemberId -> String

showList :: [MemberId] -> ShowS

Eq MemberId

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord MemberId

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

newtype Comment

Constructors

Comment String

Instances

Pretty Comment

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Comment -> Doc

Globals Comment

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Comment -> Set GlobalId

Uses Comment

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Comment -> Set JSQName

Monoid Comment

Defined in Agda.Compiler.JS.Syntax

Methods

mempty :: Comment

mappend :: Comment -> Comment -> Comment

mconcat :: [Comment] -> Comment

Semigroup Comment

Defined in Agda.Compiler.JS.Syntax

Methods

(<>) :: Comment -> Comment -> Comment

sconcat :: NonEmpty Comment -> Comment

stimes :: Integral b => b -> Comment -> Comment

Show Comment

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Comment -> ShowS

show :: Comment -> String

showList :: [Comment] -> ShowS

Eq Comment

Defined in Agda.Compiler.JS.Syntax

Methods

(==) :: Comment -> Comment -> Bool

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

Ord Comment

Defined in Agda.Compiler.JS.Syntax

Methods

compare :: Comment -> Comment -> Ordering

(<) :: Comment -> Comment -> Bool

(<=) :: Comment -> Comment -> Bool

(>) :: Comment -> Comment -> Bool

(>=) :: Comment -> Comment -> Bool

max :: Comment -> Comment -> Comment

min :: Comment -> Comment -> Comment

data Export

Constructors

Export

Fields

• expName :: JSQName
• defn :: Exp

Instances

Globals Export

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId

Uses Export

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set JSQName

Show Export

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Export -> ShowS

show :: Export -> String

showList :: [Export] -> ShowS

Pretty [(GlobalId, Export)]

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> [(GlobalId, Export)] -> Doc

type JSQName = List1 MemberId

data Module

Constructors

Module

Fields

• modName :: GlobalId
• imports :: [GlobalId]
• exports :: [Export]
• callMain :: Maybe Exp

Instances

Pretty Module

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Module -> Doc

Globals Module

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId

Show Module

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Module -> ShowS

show :: Module -> String

showList :: [Module] -> ShowS

class Uses a where

Minimal complete definition

Nothing

Methods

uses :: a -> Set JSQName

default uses :: (a ~ t b, Foldable t, Uses b) => a -> Set JSQName

Instances

Uses Comment

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Comment -> Set JSQName

Uses Exp

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set JSQName

Uses Export

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set JSQName

Uses a => Uses [a]

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: [a] -> Set JSQName

Uses a => Uses (Map k a)

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Map k a -> Set JSQName

(Uses a, Uses b) => Uses (a, b)

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: (a, b) -> Set JSQName

(Uses a, Uses b, Uses c) => Uses (a, b, c)

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: (a, b, c) -> Set JSQName

class Globals a where

Minimal complete definition

Nothing

Methods

globals :: a -> Set GlobalId

default globals :: (a ~ t b, Foldable t, Globals b) => a -> Set GlobalId

Instances

Globals Comment

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Comment -> Set GlobalId

Globals Exp

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId

Globals Export

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId

Globals Module

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId

Globals a => Globals (Maybe a)

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Maybe a -> Set GlobalId

Globals a => Globals [a]

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: [a] -> Set GlobalId

Globals a => Globals (Map k a)

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Map k a -> Set GlobalId

(Globals a, Globals b) => Globals (a, b)

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: (a, b) -> Set GlobalId

(Globals a, Globals b, Globals c) => Globals (a, b, c)

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: (a, b, c) -> Set GlobalId