module Agda.Compiler.JS.Syntax where

import Data.Map ( Map )
import qualified Data.Map as Map

import Data.Set ( Set, empty, singleton, union )

import Agda.Syntax.Common ( Nat )

-- An untyped lambda calculus with records,
-- and a special self-binder for recursive declarations

data Exp =
  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.
  deriving Int -> Exp -> ShowS
[Exp] -> ShowS
Exp -> String
(Int -> Exp -> ShowS)
-> (Exp -> String) -> ([Exp] -> ShowS) -> Show Exp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Exp] -> ShowS
$cshowList :: [Exp] -> ShowS
show :: Exp -> String
$cshow :: Exp -> String
showsPrec :: Int -> Exp -> ShowS
$cshowsPrec :: Int -> Exp -> ShowS
Show

-- Local identifiers are named by De Bruijn indices.
-- Global identifiers are named by string lists.
-- Object members are named by strings.

newtype LocalId = LocalId Nat
  deriving (LocalId -> LocalId -> Bool
(LocalId -> LocalId -> Bool)
-> (LocalId -> LocalId -> Bool) -> Eq LocalId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: LocalId -> LocalId -> Bool
$c/= :: LocalId -> LocalId -> Bool
== :: LocalId -> LocalId -> Bool
$c== :: LocalId -> LocalId -> Bool
Eq, Eq LocalId
Eq LocalId
-> (LocalId -> LocalId -> Ordering)
-> (LocalId -> LocalId -> Bool)
-> (LocalId -> LocalId -> Bool)
-> (LocalId -> LocalId -> Bool)
-> (LocalId -> LocalId -> Bool)
-> (LocalId -> LocalId -> LocalId)
-> (LocalId -> LocalId -> LocalId)
-> Ord LocalId
LocalId -> LocalId -> Bool
LocalId -> LocalId -> Ordering
LocalId -> LocalId -> LocalId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: LocalId -> LocalId -> LocalId
$cmin :: LocalId -> LocalId -> LocalId
max :: LocalId -> LocalId -> LocalId
$cmax :: LocalId -> LocalId -> LocalId
>= :: LocalId -> LocalId -> Bool
$c>= :: LocalId -> LocalId -> Bool
> :: LocalId -> LocalId -> Bool
$c> :: LocalId -> LocalId -> Bool
<= :: LocalId -> LocalId -> Bool
$c<= :: LocalId -> LocalId -> Bool
< :: LocalId -> LocalId -> Bool
$c< :: LocalId -> LocalId -> Bool
compare :: LocalId -> LocalId -> Ordering
$ccompare :: LocalId -> LocalId -> Ordering
$cp1Ord :: Eq LocalId
Ord, Int -> LocalId -> ShowS
[LocalId] -> ShowS
LocalId -> String
(Int -> LocalId -> ShowS)
-> (LocalId -> String) -> ([LocalId] -> ShowS) -> Show LocalId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [LocalId] -> ShowS
$cshowList :: [LocalId] -> ShowS
show :: LocalId -> String
$cshow :: LocalId -> String
showsPrec :: Int -> LocalId -> ShowS
$cshowsPrec :: Int -> LocalId -> ShowS
Show)

newtype GlobalId = GlobalId [String]
  deriving (GlobalId -> GlobalId -> Bool
(GlobalId -> GlobalId -> Bool)
-> (GlobalId -> GlobalId -> Bool) -> Eq GlobalId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: GlobalId -> GlobalId -> Bool
$c/= :: GlobalId -> GlobalId -> Bool
== :: GlobalId -> GlobalId -> Bool
$c== :: GlobalId -> GlobalId -> Bool
Eq, Eq GlobalId
Eq GlobalId
-> (GlobalId -> GlobalId -> Ordering)
-> (GlobalId -> GlobalId -> Bool)
-> (GlobalId -> GlobalId -> Bool)
-> (GlobalId -> GlobalId -> Bool)
-> (GlobalId -> GlobalId -> Bool)
-> (GlobalId -> GlobalId -> GlobalId)
-> (GlobalId -> GlobalId -> GlobalId)
-> Ord GlobalId
GlobalId -> GlobalId -> Bool
GlobalId -> GlobalId -> Ordering
GlobalId -> GlobalId -> GlobalId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: GlobalId -> GlobalId -> GlobalId
$cmin :: GlobalId -> GlobalId -> GlobalId
max :: GlobalId -> GlobalId -> GlobalId
$cmax :: GlobalId -> GlobalId -> GlobalId
>= :: GlobalId -> GlobalId -> Bool
$c>= :: GlobalId -> GlobalId -> Bool
> :: GlobalId -> GlobalId -> Bool
$c> :: GlobalId -> GlobalId -> Bool
<= :: GlobalId -> GlobalId -> Bool
$c<= :: GlobalId -> GlobalId -> Bool
< :: GlobalId -> GlobalId -> Bool
$c< :: GlobalId -> GlobalId -> Bool
compare :: GlobalId -> GlobalId -> Ordering
$ccompare :: GlobalId -> GlobalId -> Ordering
$cp1Ord :: Eq GlobalId
Ord, Int -> GlobalId -> ShowS
[GlobalId] -> ShowS
GlobalId -> String
(Int -> GlobalId -> ShowS)
-> (GlobalId -> String) -> ([GlobalId] -> ShowS) -> Show GlobalId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [GlobalId] -> ShowS
$cshowList :: [GlobalId] -> ShowS
show :: GlobalId -> String
$cshow :: GlobalId -> String
showsPrec :: Int -> GlobalId -> ShowS
$cshowsPrec :: Int -> GlobalId -> ShowS
Show)

newtype MemberId = MemberId String
  deriving (MemberId -> MemberId -> Bool
(MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> Bool) -> Eq MemberId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MemberId -> MemberId -> Bool
$c/= :: MemberId -> MemberId -> Bool
== :: MemberId -> MemberId -> Bool
$c== :: MemberId -> MemberId -> Bool
Eq, Eq MemberId
Eq MemberId
-> (MemberId -> MemberId -> Ordering)
-> (MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> MemberId)
-> (MemberId -> MemberId -> MemberId)
-> Ord MemberId
MemberId -> MemberId -> Bool
MemberId -> MemberId -> Ordering
MemberId -> MemberId -> MemberId
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: MemberId -> MemberId -> MemberId
$cmin :: MemberId -> MemberId -> MemberId
max :: MemberId -> MemberId -> MemberId
$cmax :: MemberId -> MemberId -> MemberId
>= :: MemberId -> MemberId -> Bool
$c>= :: MemberId -> MemberId -> Bool
> :: MemberId -> MemberId -> Bool
$c> :: MemberId -> MemberId -> Bool
<= :: MemberId -> MemberId -> Bool
$c<= :: MemberId -> MemberId -> Bool
< :: MemberId -> MemberId -> Bool
$c< :: MemberId -> MemberId -> Bool
compare :: MemberId -> MemberId -> Ordering
$ccompare :: MemberId -> MemberId -> Ordering
$cp1Ord :: Eq MemberId
Ord, Int -> MemberId -> ShowS
[MemberId] -> ShowS
MemberId -> String
(Int -> MemberId -> ShowS)
-> (MemberId -> String) -> ([MemberId] -> ShowS) -> Show MemberId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MemberId] -> ShowS
$cshowList :: [MemberId] -> ShowS
show :: MemberId -> String
$cshow :: MemberId -> String
showsPrec :: Int -> MemberId -> ShowS
$cshowsPrec :: Int -> MemberId -> ShowS
Show)

-- The top-level compilation unit is a module, which names
-- the GId of its exports, and a list of definitions

data Export = Export { Export -> [MemberId]
expName :: [MemberId], Export -> Exp
defn :: Exp }
  deriving Int -> Export -> ShowS
[Export] -> ShowS
Export -> String
(Int -> Export -> ShowS)
-> (Export -> String) -> ([Export] -> ShowS) -> Show Export
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Export] -> ShowS
$cshowList :: [Export] -> ShowS
show :: Export -> String
$cshow :: Export -> String
showsPrec :: Int -> Export -> ShowS
$cshowsPrec :: Int -> Export -> ShowS
Show

data Module = Module { Module -> GlobalId
modName :: GlobalId, Module -> [Export]
exports :: [Export], Module -> Maybe Exp
postscript :: Maybe Exp }
  deriving Int -> Module -> ShowS
[Module] -> ShowS
Module -> String
(Int -> Module -> ShowS)
-> (Module -> String) -> ([Module] -> ShowS) -> Show Module
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Module] -> ShowS
$cshowList :: [Module] -> ShowS
show :: Module -> String
$cshow :: Module -> String
showsPrec :: Int -> Module -> ShowS
$cshowsPrec :: Int -> Module -> ShowS
Show

-- Note that modules are allowed to be recursive, via the Self expression,
-- which is bound to the exported module.

-- Top-level uses of the form exports.l1....lN.

class Uses a where
  uses :: a -> Set [MemberId]

instance Uses a => Uses [a] where
  uses :: [a] -> Set [MemberId]
uses = (a -> Set [MemberId] -> Set [MemberId])
-> Set [MemberId] -> [a] -> Set [MemberId]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
union (Set [MemberId] -> Set [MemberId] -> Set [MemberId])
-> (a -> Set [MemberId]) -> a -> Set [MemberId] -> Set [MemberId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses) Set [MemberId]
forall a. Set a
empty

instance Uses a => Uses (Map k a) where
  uses :: Map k a -> Set [MemberId]
uses = (a -> Set [MemberId] -> Set [MemberId])
-> Set [MemberId] -> Map k a -> Set [MemberId]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
union (Set [MemberId] -> Set [MemberId] -> Set [MemberId])
-> (a -> Set [MemberId]) -> a -> Set [MemberId] -> Set [MemberId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses) Set [MemberId]
forall a. Set a
empty

instance Uses Exp where
  uses :: Exp -> Set [MemberId]
uses (Object Map MemberId Exp
o)     = (Exp -> Set [MemberId] -> Set [MemberId])
-> Set [MemberId] -> Map MemberId Exp -> Set [MemberId]
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
union (Set [MemberId] -> Set [MemberId] -> Set [MemberId])
-> (Exp -> Set [MemberId])
-> Exp
-> Set [MemberId]
-> Set [MemberId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses) Set [MemberId]
forall a. Set a
empty Map MemberId Exp
o
  uses (Apply Exp
e [Exp]
es)   = (Exp -> Set [MemberId] -> Set [MemberId])
-> Set [MemberId] -> [Exp] -> Set [MemberId]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
union (Set [MemberId] -> Set [MemberId] -> Set [MemberId])
-> (Exp -> Set [MemberId])
-> Exp
-> Set [MemberId]
-> Set [MemberId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses) (Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e) [Exp]
es
  uses (Lookup Exp
e MemberId
l)   = Exp -> [MemberId] -> Set [MemberId]
uses' Exp
e [MemberId
l] where
      uses' :: Exp -> [MemberId] -> Set [MemberId]
uses' Exp
Self         [MemberId]
ls = [MemberId] -> Set [MemberId]
forall a. a -> Set a
singleton [MemberId]
ls
      uses' (Lookup Exp
e MemberId
l) [MemberId]
ls = Exp -> [MemberId] -> Set [MemberId]
uses' Exp
e (MemberId
l MemberId -> [MemberId] -> [MemberId]
forall a. a -> [a] -> [a]
: [MemberId]
ls)
      uses' Exp
e            [MemberId]
ls = Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e
  uses (If Exp
e Exp
f Exp
g)     = Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
f Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
g
  uses (BinOp Exp
e String
op Exp
f) = Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
f
  uses (PreOp String
op Exp
e)   = Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e
  uses Exp
e              = Set [MemberId]
forall a. Set a
empty

instance Uses Export where
  uses :: Export -> Set [MemberId]
uses (Export [MemberId]
_ Exp
e) = Exp -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Exp
e

-- All global ids

class Globals a where
  globals :: a -> Set GlobalId

instance Globals a => Globals [a] where
  globals :: [a] -> Set GlobalId
globals = (a -> Set GlobalId -> Set GlobalId)
-> Set GlobalId -> [a] -> Set GlobalId
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
union (Set GlobalId -> Set GlobalId -> Set GlobalId)
-> (a -> Set GlobalId) -> a -> Set GlobalId -> Set GlobalId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals) Set GlobalId
forall a. Set a
empty

instance Globals a => Globals (Map k a) where
  globals :: Map k a -> Set GlobalId
globals = (a -> Set GlobalId -> Set GlobalId)
-> Set GlobalId -> Map k a -> Set GlobalId
forall a b k. (a -> b -> b) -> b -> Map k a -> b
Map.foldr (Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
union (Set GlobalId -> Set GlobalId -> Set GlobalId)
-> (a -> Set GlobalId) -> a -> Set GlobalId -> Set GlobalId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals) Set GlobalId
forall a. Set a
empty

instance Globals Exp where
  globals :: Exp -> Set GlobalId
globals (Global GlobalId
i) = GlobalId -> Set GlobalId
forall a. a -> Set a
singleton GlobalId
i
  globals (Lambda Int
n Exp
e) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e
  globals (Object Map MemberId Exp
o) = Map MemberId Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Map MemberId Exp
o
  globals (Apply Exp
e [Exp]
es) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`union` [Exp] -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals [Exp]
es
  globals (Lookup Exp
e MemberId
l) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e
  globals (If Exp
e Exp
f Exp
g) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
f Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
g
  globals (BinOp Exp
e String
op Exp
f) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`union` Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
f
  globals (PreOp String
op Exp
e) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e
  globals Exp
_ = Set GlobalId
forall a. Set a
empty

instance Globals Export where
  globals :: Export -> Set GlobalId
globals (Export [MemberId]
_ Exp
e) = Exp -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals Exp
e

instance Globals Module where
  globals :: Module -> Set GlobalId
globals (Module GlobalId
m [Export]
es Maybe Exp
_) = [Export] -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals [Export]
es