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

Safe Haskell | None

Agda.Compiler.JS.Syntax

# Documentation

data Exp

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 |

Instances

Show Exp |
Typeable Exp |
Globals Exp |
Uses Exp |
Pretty Exp |
EmbPrj Exp |

newtype LocalId

Constructors

LocalId Nat |

Instances

Eq LocalId |
Ord LocalId |
Show LocalId |
Typeable LocalId |
Pretty LocalId |
EmbPrj LocalId |

newtype GlobalId

Constructors

GlobalId [String] |

Instances

Eq GlobalId |
Ord GlobalId |
Show GlobalId |
Typeable GlobalId |
Pretty GlobalId |
EmbPrj GlobalId |

newtype MemberId

Constructors

MemberId String |

Instances

Eq MemberId |
Ord MemberId |
Show MemberId |
Typeable MemberId |
Pretty MemberId |
EmbPrj MemberId |

data Export

Constructors

Export |
Fields expName :: [MemberId] defn :: Exp

Instances

Show Export |
Typeable Export |
Globals Export |
Uses Export |

data Module

Constructors

Module |
Fields modName :: GlobalId exports :: [Export]

Instances

Show Module |
Typeable Module |
Globals Module |
Pretty Module |

class Uses a where

Methods

uses :: a -> Set [MemberId]

Instances

Uses Export |
Uses Exp |
Uses a => Uses [a] |
Uses a => Uses (Map k a) |

class Globals a where

Methods

globals :: a -> Set GlobalId

Instances

Globals Module |
Globals Export |
Globals Exp |
Globals a => Globals [a] |
Globals a => Globals (Map k a) |