Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.JS.Syntax

Documentation

data Exp Source #

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

Instances details
Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Exp -> Doc 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 JSQName Source #

Show Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Exp -> ShowS #

show :: Exp -> String #

showList :: [Exp] -> ShowS #

Eq Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

newtype LocalId Source #

Constructors

LocalId Nat 

Instances

Instances details
Pretty LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

Show LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> LocalId -> ShowS #

show :: LocalId -> String #

showList :: [LocalId] -> ShowS #

Eq LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord LocalId Source # 
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 #

newtype GlobalId Source #

Constructors

GlobalId [String] 

Instances

Instances details
Pretty GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

Show GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> GlobalId -> ShowS #

show :: GlobalId -> String #

showList :: [GlobalId] -> ShowS #

Eq GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord GlobalId Source # 
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 #

Pretty [(GlobalId, Export)] Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

data MemberId Source #

Constructors

MemberId String 
MemberIndex Int Comment 

Instances

Instances details
Pretty MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

Show MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> MemberId -> ShowS #

show :: MemberId -> String #

showList :: [MemberId] -> ShowS #

Eq MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord MemberId Source # 
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 #

newtype Comment Source #

Constructors

Comment String 

Instances

Instances details
Pretty Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

Globals Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Comment -> Set GlobalId Source #

Uses Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Comment -> Set JSQName Source #

Monoid Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

mempty :: Comment #

mappend :: Comment -> Comment -> Comment #

mconcat :: [Comment] -> Comment #

Semigroup Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

sconcat :: NonEmpty Comment -> Comment #

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

Show Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Comment -> ShowS #

show :: Comment -> String #

showList :: [Comment] -> ShowS #

Eq Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Ord Comment Source # 
Instance details

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 Source #

Constructors

Export 

Fields

Instances

Instances details
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 JSQName Source #

Show Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Export -> ShowS #

show :: Export -> String #

showList :: [Export] -> ShowS #

Pretty [(GlobalId, Export)] Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

type JSQName = List1 MemberId Source #

data Module Source #

Constructors

Module 

Fields

Instances

Instances details
Pretty Module Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

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

Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId Source #

Show Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

showsPrec :: Int -> Module -> ShowS #

show :: Module -> String #

showList :: [Module] -> ShowS #

class Uses a where Source #

Minimal complete definition

Nothing

Methods

uses :: a -> Set JSQName Source #

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

Instances

Instances details
Uses Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Comment -> Set JSQName Source #

Uses Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Exp -> Set JSQName Source #

Uses Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Export -> Set JSQName Source #

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

Defined in Agda.Compiler.JS.Syntax

Methods

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

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

Defined in Agda.Compiler.JS.Syntax

Methods

uses :: Map k a -> Set JSQName Source #

(Uses a, Uses b) => Uses (a, b) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

(Uses a, Uses b, Uses c) => Uses (a, b, c) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

class Globals a where Source #

Minimal complete definition

Nothing

Methods

globals :: a -> Set GlobalId Source #

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

Instances

Instances details
Globals Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Comment -> Set GlobalId Source #

Globals Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Exp -> Set GlobalId Source #

Globals Export Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Export -> Set GlobalId Source #

Globals Module Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Module -> Set GlobalId Source #

Globals a => Globals (Maybe a) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

globals :: Maybe a -> 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 #

(Globals a, Globals b) => Globals (a, b) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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

(Globals a, Globals b, Globals c) => Globals (a, b, c) Source # 
Instance details

Defined in Agda.Compiler.JS.Syntax

Methods

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