Agda-2.8.0: A dependently typed functional programming language and proof assistant

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

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 #
Show LocalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> LocalId -> ShowS Source # show :: LocalId -> String Source # showList :: [LocalId] -> ShowS Source #
Eq LocalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (==) :: LocalId -> LocalId -> Bool Source # (/=) :: LocalId -> LocalId -> Bool Source #
Ord LocalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods compare :: LocalId -> LocalId -> Ordering Source # (<) :: LocalId -> LocalId -> Bool Source # (<=) :: LocalId -> LocalId -> Bool Source # (>) :: LocalId -> LocalId -> Bool Source # (>=) :: LocalId -> LocalId -> Bool Source # max :: LocalId -> LocalId -> LocalId Source # min :: LocalId -> LocalId -> LocalId Source #

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 #
Show GlobalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> GlobalId -> ShowS Source # show :: GlobalId -> String Source # showList :: [GlobalId] -> ShowS Source #
Eq GlobalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (==) :: GlobalId -> GlobalId -> Bool Source # (/=) :: GlobalId -> GlobalId -> Bool Source #
Ord GlobalId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods compare :: GlobalId -> GlobalId -> Ordering Source # (<) :: GlobalId -> GlobalId -> Bool Source # (<=) :: GlobalId -> GlobalId -> Bool Source # (>) :: GlobalId -> GlobalId -> Bool Source # (>=) :: GlobalId -> GlobalId -> Bool Source # max :: GlobalId -> GlobalId -> GlobalId Source # min :: GlobalId -> GlobalId -> GlobalId Source #
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 Comment |

#### 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 #
Show MemberId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> MemberId -> ShowS Source # show :: MemberId -> String Source # showList :: [MemberId] -> ShowS Source #
Eq MemberId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (==) :: MemberId -> MemberId -> Bool Source # (/=) :: MemberId -> MemberId -> Bool Source #
Ord MemberId Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods compare :: MemberId -> MemberId -> Ordering Source # (<) :: MemberId -> MemberId -> Bool Source # (<=) :: MemberId -> MemberId -> Bool Source # (>) :: MemberId -> MemberId -> Bool Source # (>=) :: MemberId -> MemberId -> Bool Source # max :: MemberId -> MemberId -> MemberId Source # min :: MemberId -> MemberId -> MemberId Source #

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 # prettyPrec :: Int -> (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 Source # mappend :: Comment -> Comment -> Comment Source # mconcat :: [Comment] -> Comment Source #
Semigroup Comment Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (<>) :: Comment -> Comment -> Comment Source # sconcat :: NonEmpty Comment -> Comment Source # stimes :: Integral b => b -> Comment -> Comment Source #
Show Comment Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods showsPrec :: Int -> Comment -> ShowS Source # show :: Comment -> String Source # showList :: [Comment] -> ShowS Source #
Eq Comment Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods (==) :: Comment -> Comment -> Bool Source # (/=) :: Comment -> Comment -> Bool Source #
Ord Comment Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods compare :: Comment -> Comment -> Ordering Source # (<) :: Comment -> Comment -> Bool Source # (<=) :: Comment -> Comment -> Bool Source # (>) :: Comment -> Comment -> Bool Source # (>=) :: Comment -> Comment -> Bool Source # max :: Comment -> Comment -> Comment Source # min :: Comment -> Comment -> Comment Source #

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 Source # show :: Export -> String Source # showList :: [Export] -> ShowS Source #
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 Source # show :: Module -> String Source # showList :: [Module] -> ShowS Source #

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 #