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

    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
    /= :: 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
    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)

    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
    showList :: [Comment] -> ShowS
    $cshowList :: [Comment] -> ShowS
    show :: Comment -> String
    $cshow :: Comment -> String
    showsPrec :: Int -> Comment -> ShowS
    $cshowsPrec :: Int -> 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
    stimes :: forall b. Integral b => b -> Comment -> Comment
    $cstimes :: forall b. Integral b => b -> Comment -> Comment
    sconcat :: NonEmpty Comment -> Comment
    $csconcat :: NonEmpty Comment -> Comment
    <> :: Comment -> Comment -> Comment
    $c<> :: Comment -> 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
    mconcat :: [Comment] -> Comment
    $cmconcat :: [Comment] -> Comment
    mappend :: Comment -> Comment -> Comment
    $cmappend :: Comment -> Comment -> Comment
    mempty :: Comment
    $cmempty :: 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
    showList :: [Export] -> ShowS
    $cshowList :: [Export] -> ShowS
    show :: Export -> String
    $cshow :: Export -> String
    showsPrec :: Int -> Export -> ShowS
    $cshowsPrec :: Int -> 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
    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 JSQName

      default uses :: (a ~ t b, Foldable t, Uses b) => a -> Set JSQName
      uses = (b -> Set JSQName) -> t b -> Set JSQName
    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 (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)