Safe Haskell	Safe-Inferred
Language	Haskell2010

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) -> 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) -> 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) -> 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) -> [(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) -> 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) -> 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 expName :: JSQName defn :: Exp

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) -> [(GlobalId, Export)] -> Doc Source #

type JSQName = List1 MemberId Source #

data Module Source #

Constructors

Module
Fields modName :: GlobalId imports :: [GlobalId] exports :: [Export] callMain :: Maybe Exp

Instances

Instances details

Pretty Module Source #
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: (Nat, Bool) -> 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 #