Agda-2.6.0.1: 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 |
String String |
Char Char |
Integer Integer |
Double Double |
Lambda Nat Exp |
Object (Map MemberId 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

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 #
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 [MemberId] Source #
Pretty Exp Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: Nat -> Int -> Exp -> String Source #

newtype LocalId Source #

Constructors

LocalId Nat |

Instances

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 #
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 #
Pretty LocalId Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: Nat -> Int -> LocalId -> String Source #

newtype GlobalId Source #

Constructors

GlobalId [String] |

Instances

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 #
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 #
Pretty GlobalId Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: Nat -> Int -> GlobalId -> String Source #

newtype MemberId Source #

Constructors

MemberId String |

Instances

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 #
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 #
Pretty MemberId Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: Nat -> Int -> MemberId -> String Source #

data Export Source #

Constructors

Export |

Fields

- expName :: [MemberId]
- defn :: Exp

Instances

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 #
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 [MemberId] Source #

data Module Source #

Constructors

Module |

Fields

- modName :: GlobalId
- exports :: [Export]
- postscript :: Maybe Exp

Instances

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 #
Globals Module Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods globals :: Module -> Set GlobalId Source #
Pretty Module Source # |
Instance details Defined in Agda.Compiler.JS.Pretty Methods pretty :: Nat -> Int -> Module -> String Source #

class Uses a where Source #

Methods

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

Instances

Uses Export Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods uses :: Export -> Set [MemberId] Source #
Uses Exp Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods uses :: Exp -> Set [MemberId] Source #
Uses a => Uses [a] Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods uses :: [a] -> Set [MemberId] Source #
Uses a => Uses (Map k a) Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods uses :: Map k a -> Set [MemberId] Source #

class Globals a where Source #

Methods

globals :: a -> Set GlobalId Source #

Instances

Globals Module Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods globals :: Module -> Set GlobalId Source #
Globals Export Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods globals :: Export -> Set GlobalId Source #
Globals Exp Source # |
Instance details Defined in Agda.Compiler.JS.Syntax Methods globals :: Exp -> 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 #