Safe Haskell	None
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, 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 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, JSModuleStyle) -> [(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, 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 :: forall (t :: Type -> Type) b. (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 :: forall (t :: Type -> Type) b. (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 #