module Agda.Compiler.JS.Syntax where

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

import Data.Text (Text)

import Agda.Syntax.Common ( Nat )

import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
import qualified Agda.Utils.List1 as List1

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

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

-- 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
$c== :: LocalId -> LocalId -> Bool
== :: LocalId -> LocalId -> Bool
$c/= :: LocalId -> LocalId -> Bool
/= :: 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
$ccompare :: LocalId -> LocalId -> Ordering
compare :: LocalId -> LocalId -> Ordering
$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
>= :: LocalId -> LocalId -> Bool
$cmax :: LocalId -> LocalId -> LocalId
max :: LocalId -> LocalId -> LocalId
$cmin :: LocalId -> LocalId -> LocalId
min :: LocalId -> LocalId -> 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
$cshowsPrec :: Int -> LocalId -> ShowS
showsPrec :: Int -> LocalId -> ShowS
$cshow :: LocalId -> String
show :: LocalId -> String
$cshowList :: [LocalId] -> ShowS
showList :: [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
$c== :: GlobalId -> GlobalId -> Bool
== :: GlobalId -> GlobalId -> Bool
$c/= :: GlobalId -> GlobalId -> Bool
/= :: 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
$ccompare :: GlobalId -> GlobalId -> Ordering
compare :: GlobalId -> GlobalId -> Ordering
$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
>= :: GlobalId -> GlobalId -> Bool
$cmax :: GlobalId -> GlobalId -> GlobalId
max :: GlobalId -> GlobalId -> GlobalId
$cmin :: GlobalId -> GlobalId -> GlobalId
min :: GlobalId -> GlobalId -> 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
$cshowsPrec :: Int -> GlobalId -> ShowS
showsPrec :: Int -> GlobalId -> ShowS
$cshow :: GlobalId -> String
show :: GlobalId -> String
$cshowList :: [GlobalId] -> ShowS
showList :: [GlobalId] -> ShowS
Show)

data MemberId
    = MemberId String
    | MemberIndex Int Comment
  deriving (MemberId -> MemberId -> Bool
(MemberId -> MemberId -> Bool)
-> (MemberId -> MemberId -> Bool) -> Eq MemberId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MemberId -> MemberId -> Bool
== :: MemberId -> MemberId -> Bool
$c/= :: MemberId -> MemberId -> Bool
/= :: 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
$ccompare :: MemberId -> MemberId -> Ordering
compare :: MemberId -> MemberId -> Ordering
$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
>= :: MemberId -> MemberId -> Bool
$cmax :: MemberId -> MemberId -> MemberId
max :: MemberId -> MemberId -> MemberId
$cmin :: MemberId -> MemberId -> MemberId
min :: MemberId -> MemberId -> 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
$cshowsPrec :: Int -> MemberId -> ShowS
showsPrec :: Int -> MemberId -> ShowS
$cshow :: MemberId -> String
show :: MemberId -> String
$cshowList :: [MemberId] -> ShowS
showList :: [MemberId] -> ShowS
Show)

newtype Comment = Comment String
  deriving (Int -> Comment -> ShowS
[Comment] -> ShowS
Comment -> String
(Int -> Comment -> ShowS)
-> (Comment -> String) -> ([Comment] -> ShowS) -> Show Comment
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Comment -> ShowS
showsPrec :: Int -> Comment -> ShowS
$cshow :: Comment -> String
show :: Comment -> String
$cshowList :: [Comment] -> ShowS
showList :: [Comment] -> ShowS
Show, NonEmpty Comment -> Comment
Comment -> Comment -> Comment
(Comment -> Comment -> Comment)
-> (NonEmpty Comment -> Comment)
-> (forall b. Integral b => b -> Comment -> Comment)
-> Semigroup Comment
forall b. Integral b => b -> Comment -> Comment
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: Comment -> Comment -> Comment
<> :: Comment -> Comment -> Comment
$csconcat :: NonEmpty Comment -> Comment
sconcat :: NonEmpty Comment -> Comment
$cstimes :: forall b. Integral b => b -> Comment -> Comment
stimes :: forall b. Integral b => b -> Comment -> Comment
Semigroup, Semigroup Comment
Comment
Semigroup Comment
-> Comment
-> (Comment -> Comment -> Comment)
-> ([Comment] -> Comment)
-> Monoid Comment
[Comment] -> Comment
Comment -> Comment -> Comment
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: Comment
mempty :: Comment
$cmappend :: Comment -> Comment -> Comment
mappend :: Comment -> Comment -> Comment
$cmconcat :: [Comment] -> Comment
mconcat :: [Comment] -> Comment
Monoid)

instance Eq Comment where Comment
_ == :: Comment -> Comment -> Bool
== Comment
_ = Bool
True
instance Ord Comment where compare :: Comment -> Comment -> Ordering
compare Comment
_ Comment
_ = Ordering
EQ

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

data Export = Export { Export -> JSQName
expName :: JSQName, 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
$cshowsPrec :: Int -> Export -> ShowS
showsPrec :: Int -> Export -> ShowS
$cshow :: Export -> String
show :: Export -> String
$cshowList :: [Export] -> ShowS
showList :: [Export] -> ShowS
Show

type JSQName = List1 MemberId

data Module = Module
  { Module -> GlobalId
modName  :: GlobalId
  , Module -> [GlobalId]
imports  :: [GlobalId]
  , Module -> [Export]
exports  :: [Export]
  , Module -> Maybe Exp
callMain :: 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
$cshowsPrec :: Int -> Module -> ShowS
showsPrec :: Int -> Module -> ShowS
$cshow :: Module -> String
show :: Module -> String
$cshowList :: [Module] -> ShowS
showList :: [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 JSQName

  default uses :: (a ~ t b, Foldable t, Uses b) => a -> Set JSQName
  uses = (b -> Set JSQName) -> t b -> Set JSQName
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses

instance Uses a => Uses [a]
instance Uses a => Uses (Map k a)

instance (Uses a, Uses b) => Uses (a, b) where
  uses :: (a, b) -> Set JSQName
uses (a
a, b
b) = a -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses a
a Set JSQName -> Set JSQName -> Set JSQName
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` b -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses b
b

instance (Uses a, Uses b, Uses c) => Uses (a, b, c) where
  uses :: (a, b, c) -> Set JSQName
uses (a
a, b
b, c
c) = a -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses a
a Set JSQName -> Set JSQName -> Set JSQName
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` b -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses b
b Set JSQName -> Set JSQName -> Set JSQName
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` c -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses c
c

instance Uses Comment where
  uses :: Comment -> Set JSQName
uses Comment
_ = Set JSQName
forall a. Set a
Set.empty

instance Uses Exp where
  uses :: Exp -> Set JSQName
uses (Object Map MemberId Exp
o)     = Map MemberId Exp -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses Map MemberId Exp
o
  uses (Array [(Comment, Exp)]
es)     = [(Comment, Exp)] -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses [(Comment, Exp)]
es
  uses (Apply Exp
e [Exp]
es)   = (Exp, [Exp]) -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses (Exp
e, [Exp]
es)
  uses (Lookup Exp
e MemberId
l)   = Exp -> JSQName -> Set JSQName
uses' Exp
e (MemberId -> JSQName
forall a. a -> NonEmpty a
List1.singleton MemberId
l)
    where
      uses' :: Exp -> JSQName -> Set JSQName
      uses' :: Exp -> JSQName -> Set JSQName
uses' Exp
Self         JSQName
ls = JSQName -> Set JSQName
forall a. a -> Set a
Set.singleton JSQName
ls
      uses' (Lookup Exp
e MemberId
l) JSQName
ls = Exp -> JSQName -> Set JSQName
uses' Exp
e (MemberId
l MemberId -> JSQName -> JSQName
forall a. a -> NonEmpty a -> NonEmpty a
<| JSQName
ls)
      uses' Exp
e            JSQName
ls = Exp -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses Exp
e
  uses (If Exp
e Exp
f Exp
g)     = (Exp, Exp, Exp) -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses (Exp
e, Exp
f, Exp
g)
  uses (BinOp Exp
e String
op Exp
f) = (Exp, Exp) -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses (Exp
e, Exp
f)
  uses (PreOp String
op Exp
e)   = Exp -> Set JSQName
forall a. Uses a => a -> Set JSQName
uses Exp
e
  uses Exp
e              = Set JSQName
forall a. Set a
Set.empty

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

-- All global ids

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

  default globals :: (a ~ t b, Foldable t, Globals b) => a -> Set GlobalId
  globals = (b -> Set GlobalId) -> t b -> Set GlobalId
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap b -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals

instance Globals a => Globals [a]
instance Globals a => Globals (Maybe a)
instance Globals a => Globals (Map k a)

instance (Globals a, Globals b) => Globals (a, b) where
  globals :: (a, b) -> Set GlobalId
globals (a
a, b
b) = a -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals a
a Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` b -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals b
b

instance (Globals a, Globals b, Globals c) => Globals (a, b, c) where
  globals :: (a, b, c) -> Set GlobalId
globals (a
a, b
b, c
c) = a -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals a
a Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` b -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals b
b Set GlobalId -> Set GlobalId -> Set GlobalId
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` c -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals c
c

instance Globals Comment where
  globals :: Comment -> Set GlobalId
globals Comment
_ = Set GlobalId
forall a. Set a
Set.empty

instance Globals Exp where
  globals :: Exp -> Set GlobalId
globals (Global GlobalId
i) = GlobalId -> Set GlobalId
forall a. a -> Set a
Set.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 (Array [(Comment, Exp)]
es) = [(Comment, Exp)] -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals [(Comment, Exp)]
es
  globals (Apply Exp
e [Exp]
es) = (Exp, [Exp]) -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals (Exp
e, [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, Exp, Exp) -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals (Exp
e, Exp
f, Exp
g)
  globals (BinOp Exp
e String
op Exp
f) = (Exp, Exp) -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals (Exp
e, 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
Set.empty

instance Globals Export where
  globals :: Export -> Set GlobalId
globals (Export JSQName
_ 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
_ [GlobalId]
_ [Export]
es Maybe Exp
me) = ([Export], Maybe Exp) -> Set GlobalId
forall a. Globals a => a -> Set GlobalId
globals ([Export]
es, Maybe Exp
me)