{-# LANGUAGE DeriveDataTypeable #-}

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 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 (Eq, Ord, Show)

newtype GlobalId = GlobalId [String]
  deriving (Eq, Ord, Show)

newtype MemberId = MemberId String
  deriving (Eq, Ord, Show)

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

data Export = Export { expName :: [MemberId], defn :: Exp }
  deriving Show

data Module = Module { modName :: GlobalId, exports :: [Export], postscript :: Maybe Exp }
  deriving 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 = foldr (union . uses) empty

instance Uses a => Uses (Map k a) where
  uses = Map.foldr (union . uses) empty

instance Uses Exp where
  uses (Object o)     = Map.foldr (union . uses) empty o
  uses (Apply e es)   = foldr (union . uses) (uses e) es
  uses (Lookup e l)   = uses' e [l] where
      uses' Self         ls = singleton ls
      uses' (Lookup e l) ls = uses' e (l : ls)
      uses' e            ls = uses e
  uses (If e f g)     = uses e `union` uses f `union` uses g
  uses (BinOp e op f) = uses e `union` uses f
  uses (PreOp op e)   = uses e
  uses e              = empty

instance Uses Export where
  uses (Export _ e) = uses e

-- All global ids

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

instance Globals a => Globals [a] where
  globals = foldr (union . globals) empty

instance Globals a => Globals (Map k a) where
  globals = Map.foldr (union . globals) empty

instance Globals Exp where
  globals (Global i) = singleton i
  globals (Lambda n e) = globals e
  globals (Object o) = globals o
  globals (Apply e es) = globals e `union` globals es
  globals (Lookup e l) = globals e
  globals (If e f g) = globals e `union` globals f `union` globals g
  globals (BinOp e op f) = globals e `union` globals f
  globals (PreOp op e) = globals e
  globals _ = empty

instance Globals Export where
  globals (Export _ e) = globals e

instance Globals Module where
  globals (Module m es _) = globals es