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 [Exp]
MemberIdInString MemberId
Ternary Exp Exp Exp
Apply Exp [Exp]
Lookup Exp MemberId
If Exp Exp Exp
BinOp Exp String Exp
PreOp String Exp
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 # prettyPrec :: Int -> (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 #
Eq Exp Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods (==) :: Exp -> Exp -> Bool # (/=) :: Exp -> Exp -> Bool #
Show Exp Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> Exp -> ShowS # show :: Exp -> String # showList :: [Exp] -> ShowS #

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 # prettyPrec :: Int -> (Nat, Bool, JSModuleStyle) -> LocalId -> Doc Source #
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 #
Show LocalId Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> LocalId -> ShowS # show :: LocalId -> String # showList :: [LocalId] -> ShowS #

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 # prettyPrec :: Int -> (Nat, Bool, JSModuleStyle) -> GlobalId -> Doc Source #
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 #
Show GlobalId Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> GlobalId -> ShowS # show :: GlobalId -> String # showList :: [GlobalId] -> ShowS #
Pretty [(GlobalId, Export)] Source #
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: (Nat, Bool, JSModuleStyle) -> [(GlobalId, Export)] -> Doc Source # prettyPrec :: Int -> (Nat, Bool, JSModuleStyle) -> [(GlobalId, Export)] -> Doc Source #

data MemberId Source #

Constructors

MemberId String
MemberIndex Int

Instances

Instances details

Pretty MemberId Source #
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: (Nat, Bool, JSModuleStyle) -> MemberId -> Doc Source # prettyPrec :: Int -> (Nat, Bool, JSModuleStyle) -> MemberId -> Doc Source #
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 #
Show MemberId Source #
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> MemberId -> ShowS # show :: MemberId -> String # showList :: [MemberId] -> ShowS #

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 # prettyPrec :: Int -> (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 # prettyPrec :: Int -> (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 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 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 #