    -- | Main module for JS backend.

    module Agda.Compiler.JS.Compiler where

    import Prelude hiding ( null, writeFile )

    import Control.DeepSeq
    import Control.Monad.Trans

    import Data.Char     ( isSpace )
    import Data.Foldable ( forM_ )
    import Data.Functor  ( (<&>) )
    import Data.List     ( dropWhileEnd, elemIndex, intercalate, partition )
    import Data.Maybe    ( listToMaybe )
    import Data.Set      ( Set )

    import qualified Data.Set as Set
    import qualified Data.Map as Map
    import qualified Data.Text as T

    import GHC.Generics (Generic)

    import System.Directory   ( createDirectoryIfMissing )
    import System.Environment ( setEnv )
    import System.FilePath    ( splitFileName, (</>) )
    import System.Process     ( callCommand )

    import Agda.Setup         ( getDataDir )

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name ( isNoName )
    import Agda.Syntax.Abstract.Name
      ( QName,
        mnameToList, qnameName, qnameModule, nameId )
    import Agda.Syntax.Internal
      ( Name, Type
      , nameFixity, unDom, telToList )
    import Agda.Syntax.Literal       ( Literal(..) )
    import Agda.Syntax.TopLevelModuleName (TopLevelModuleName, TopLevelModuleName'(..))
    import Agda.Syntax.Treeless      ( ArgUsage(..), filterUsed )
    import qualified Agda.Syntax.Treeless as T

    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Reduce ( instantiateFull )
    import Agda.TypeChecking.Substitute as TC ( TelV(..), raise, subst )
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Telescope ( telViewPath )
    import Agda.TypeChecking.Warnings  ( warning )

    import Agda.Utils.FileName ( isNewerThan )
    import Agda.Utils.Function ( iterate' )
    import Agda.Utils.List ( downFrom, headWithDefault )
    import Agda.Utils.List1 ( List1, pattern (:|) )
    import qualified Agda.Utils.List1 as List1
    import Agda.Utils.Maybe ( boolToMaybe, catMaybes, caseMaybeM, fromMaybe, whenNothing )
    import Agda.Utils.Monad ( ifM, when, whenM )
    import Agda.Utils.Null  ( null )
    import Agda.Syntax.Common.Pretty (prettyShow, render)
    import qualified Agda.Syntax.Common.Pretty as P
    import Agda.Utils.IO.Directory
    import Agda.Utils.IO.UTF8 ( writeFile )
    import Agda.Utils.Singleton ( singleton )
    import Agda.Utils.Size (size)

    import Agda.Compiler.Common as CC
    import Agda.Compiler.ToTreeless
    import Agda.Compiler.Treeless.EliminateDefaults
    import Agda.Compiler.Treeless.EliminateLiteralPatterns
    import Agda.Compiler.Treeless.GuardsToPrims
    import Agda.Compiler.Treeless.Erase ( computeErasedConstructorArgs, isErasable )
    import Agda.Compiler.Treeless.Subst ()
    import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Recompile(..))

    import Agda.Compiler.JS.Syntax
      ( Exp(Self,Local,Global,Undefined,Null,String,Char,Integer,Double,Lambda,Object,Array,Apply,Lookup,If,BinOp,PlainJS),
        LocalId(LocalId), GlobalId(GlobalId), MemberId(MemberId,MemberIndex), Export(Export), Module(Module, modName, callMain), Comment(Comment),
        modName, expName, uses
      , JSQName
      )
    import Agda.Compiler.JS.Substitution
      ( curriedLambda, curriedApply, emp, apply, substShift )
    import qualified Agda.Compiler.JS.Pretty as JSPretty
    import Agda.Compiler.JS.Pretty (JSModuleStyle(..))

    import Agda.Utils.Impossible (__IMPOSSIBLE__)

    --------------------------------------------------
    -- Entry point into the compiler
    --------------------------------------------------

    jsBackend :: Backend
    jsBackend :: Backend
    jsBackend = Backend'_boot
      Definition
      (TCMT IO)
      JSOptions
      JSOptions
      JSModuleEnv
      Module
      (Maybe Export)
    -> Backend
    forall opts definition (tcm :: * -> *) env menv mod def.
    NFData opts =>
    Backend'_boot definition tcm opts env menv mod def
    -> Backend_boot definition tcm
    Backend Backend'_boot
      Definition
      (TCMT IO)
      JSOptions
      JSOptions
      JSModuleEnv
      Module
      (Maybe Export)
    jsBackend'

    jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
    jsBackend' :: Backend'_boot
      Definition
      (TCMT IO)
      JSOptions
      JSOptions
      JSModuleEnv
      Module
      (Maybe Export)
    jsBackend' = Backend'
      { backendName :: Text
    backendName           = Text
    jsBackendName
      , backendVersion :: Maybe Text
    backendVersion        = Maybe Text
    forall a. Maybe a
    Nothing
      , options :: JSOptions
    options               = JSOptions
    defaultJSOptions
      , commandLineFlags :: [OptDescr (Flag JSOptions)]
    commandLineFlags      = [OptDescr (Flag JSOptions)]
    jsCommandLineFlags
      , isEnabled :: JSOptions -> Bool
    isEnabled             = JSOptions -> Bool
    optJSCompile
      , preCompile :: JSOptions -> TCMT IO JSOptions
    preCompile            = JSOptions -> TCMT IO JSOptions
    jsPreCompile
      , postCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
    postCompile           = JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
    jsPostCompile
      , preModule :: JSOptions
    -> IsMain
    -> TopLevelModuleName
    -> Maybe String
    -> TCMT IO (Recompile JSModuleEnv Module)
    preModule             = JSOptions
    -> IsMain
    -> TopLevelModuleName
    -> Maybe String
    -> TCMT IO (Recompile JSModuleEnv Module)
    jsPreModule
      , postModule :: JSOptions
    -> JSModuleEnv
    -> IsMain
    -> TopLevelModuleName
    -> [Maybe Export]
    -> TCMT IO Module
    postModule            = JSOptions
    -> JSModuleEnv
    -> IsMain
    -> TopLevelModuleName
    -> [Maybe Export]
    -> TCMT IO Module
    jsPostModule
      , compileDef :: JSOptions
    -> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
    compileDef            = JSOptions
    -> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
    jsCompileDef
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    False
      , mayEraseType :: QName -> TCMT IO Bool
    mayEraseType          = TCMT IO Bool -> QName -> TCMT IO Bool
    forall a b. a -> b -> a
    const (TCMT IO Bool -> QName -> TCMT IO Bool)
    -> TCMT IO Bool -> QName -> TCMT IO Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
          -- Andreas, 2019-05-09, see issue #3732.
          -- If you want to use JS data structures generated from Agda
          -- @data@/@record@, you might want to tell the treeless compiler
          -- not to erase these types even if they have no content,
          -- to get a stable interface.
      , backendInteractTop :: Maybe (BackendCommandTop (TCMT IO))
    backendInteractTop    = Maybe (BackendCommandTop (TCMT IO))
    forall a. Maybe a
    Nothing
      , backendInteractHole :: Maybe (BackendCommandHole (TCMT IO))
    backendInteractHole   = Maybe (BackendCommandHole (TCMT IO))
    forall a. Maybe a
    Nothing
      }

    --- Options ---

    data JSOptions = JSOptions
      { JSOptions -> Bool
    optJSCompile  :: Bool
      , JSOptions -> Bool
    optJSOptimize :: Bool
      , JSOptions -> Bool
    optJSMinify   :: Bool
          -- ^ Remove spaces etc. See https://en.wikipedia.org/wiki/Minification_(programming).
      , JSOptions -> Bool
    optJSVerify   :: Bool
          -- ^ Run generated code through interpreter.
      , JSOptions -> JSModuleStyle
    optJSModuleStyle :: JSModuleStyle
      }
      deriving (forall x. JSOptions -> Rep JSOptions x)
    -> (forall x. Rep JSOptions x -> JSOptions) -> Generic JSOptions
    forall x. Rep JSOptions x -> JSOptions
    forall x. JSOptions -> Rep JSOptions x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. JSOptions -> Rep JSOptions x
    from :: forall x. JSOptions -> Rep JSOptions x
    $cto :: forall x. Rep JSOptions x -> JSOptions
    to :: forall x. Rep JSOptions x -> JSOptions
    Generic

    instance NFData JSModuleStyle

    instance NFData JSOptions

    defaultJSOptions :: JSOptions
    defaultJSOptions :: JSOptions
    defaultJSOptions = JSOptions
      { optJSCompile :: Bool
    optJSCompile  = Bool
    False
      , optJSOptimize :: Bool
    optJSOptimize = Bool
    False
      , optJSMinify :: Bool
    optJSMinify   = Bool
    False
      , optJSVerify :: Bool
    optJSVerify   = Bool
    False
      , optJSModuleStyle :: JSModuleStyle
    optJSModuleStyle = JSModuleStyle
    JSCJS
      }

    jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
    jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
    jsCommandLineFlags =
        [ String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    enable) String
    "compile program using the JS backend"
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-optimize"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    enableOpt) String
    "turn on optimizations during JS code generation"
        -- Minification is described at https://en.wikipedia.org/wiki/Minification_(programming)
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-minify"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    enableMin) String
    "minify generated JS code"
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-verify"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    enableVerify) String
    "except for main module, run generated JS modules through `node` (needs to be in PATH)"
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-es6"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    setES6) String
    "use ES6 module style for JS"
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-cjs"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    setCJS) String
    "use CommonJS module style (default)"
        , String
    -> [String]
    -> ArgDescr (Flag JSOptions)
    -> String
    -> OptDescr (Flag JSOptions)
    forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
    Option [] [String
    "js-amd"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
    forall a. a -> ArgDescr a
    NoArg Flag JSOptions
    forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
    setAMD) String
    "use AMD module style for JS"
        ]
      where
        enable :: JSOptions -> f JSOptions
    enable       JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSCompile  = True }
        enableOpt :: JSOptions -> f JSOptions
    enableOpt    JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSOptimize = True }
        enableMin :: JSOptions -> f JSOptions
    enableMin    JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSMinify   = True }
        enableVerify :: JSOptions -> f JSOptions
    enableVerify JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSVerify   = True }
        setES6 :: JSOptions -> f JSOptions
    setES6       JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSModuleStyle = JSES6 }
        setCJS :: JSOptions -> f JSOptions
    setCJS       JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSModuleStyle = JSCJS }
        setAMD :: JSOptions -> f JSOptions
    setAMD       JSOptions
    o = JSOptions -> f JSOptions
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSModuleStyle = JSAMD }

    --- Top-level compilation ---

    jsPreCompile :: JSOptions -> TCM JSOptions
    jsPreCompile :: JSOptions -> TCMT IO JSOptions
    jsPreCompile JSOptions
    opts = JSOptions
    opts JSOptions -> TCMT IO () -> TCMT IO JSOptions
    forall a b. a -> TCMT IO b -> TCMT IO a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ do
      (Cubical -> TCMT IO (ZonkAny 0)) -> Maybe Cubical -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (TypeError -> TCMT IO (ZonkAny 0)
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO (ZonkAny 0))
    -> (Cubical -> TypeError) -> Cubical -> TCMT IO (ZonkAny 0)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Cubical -> TypeError
    CubicalCompilationNotSupported) (Maybe Cubical -> TCMT IO ())
    -> TCMT IO (Maybe Cubical) -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption

    -- | After all modules have been compiled, copy RTE modules and verify compiled modules.

    jsPostCompile ::
      JSOptions -> IsMain -> Map.Map TopLevelModuleName Module -> TCM ()
    jsPostCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
    jsPostCompile JSOptions
    opts IsMain
    _ Map TopLevelModuleName Module
    ms = do

      -- Copy RTE modules.

      compDir  <- TCMT IO String
    forall (m :: * -> *). HasOptions m => m String
    compileDir
      liftIO $ do
        dataDir <- getDataDir
        let fname = case JSOptions -> JSModuleStyle
    optJSModuleStyle JSOptions
    opts of
              JSModuleStyle
    JSCJS -> String
    "agda-rts.js"
              JSModuleStyle
    JSAMD -> String
    "agda-rts.amd.js"
              JSModuleStyle
    JSES6 -> String
    "agda-rts.mjs"
            srcPath = String
    dataDir String -> String -> String
    </> String
    "JS" String -> String -> String
    </> String
    fname
            compPath = String
    compDir String -> String -> String
    </> String
    fname
        copyIfChanged srcPath compPath

      -- Verify generated JS modules (except for main).

      reportSLn "compile.js.verify" 10 $ "Considering to verify generated JS modules"
      when (optJSVerify opts) $ do

        reportSLn "compile.js.verify" 10 $ "Verifying generated JS modules"
        liftIO $ setEnv "NODE_PATH" compDir

        forM_ ms $ \ Module{ GlobalId
    modName :: Module -> GlobalId
    modName :: GlobalId
    modName, Maybe Exp
    callMain :: Module -> Maybe Exp
    callMain :: Maybe Exp
    callMain } -> do
          jsFile <- JSModuleStyle -> GlobalId -> TCMT IO String
    outFile (JSOptions -> JSModuleStyle
    optJSModuleStyle JSOptions
    opts) GlobalId
    modName
          reportSLn "compile.js.verify" 30 $ unwords [ "Considering JS module:" , jsFile ]

          -- Since we do not run a JS program for real, we skip all modules that could
          -- have a call to main.
          -- Atm, modules whose compilation was skipped are also skipped during verification
          -- (they appear here as main modules).
          whenNothing callMain $ do
            -- node needs to see whether the extension is .js or .mjs,
            -- so we pass input explicitly, not via stdin
            let cmd = [String] -> String
    unwords [ String
    "node", String
    jsFile ]
            reportSLn "compile.js.verify" 20 $ unwords [ "calling:", cmd ]
            liftIO $ callCommand cmd

    --- Module compilation ---

    data JSModuleEnv = JSModuleEnv
      { JSModuleEnv -> Maybe CoinductionKit
    jsCoinductionKit :: Maybe CoinductionKit
      , JSModuleEnv -> Bool
    jsCompile        :: Bool
        -- ^ Should this module be compiled?
      }

    jsPreModule ::
      JSOptions -> IsMain -> TopLevelModuleName -> Maybe FilePath ->
      TCM (Recompile JSModuleEnv Module)
    jsPreModule :: JSOptions
    -> IsMain
    -> TopLevelModuleName
    -> Maybe String
    -> TCMT IO (Recompile JSModuleEnv Module)
    jsPreModule JSOptions
    opts IsMain
    _ TopLevelModuleName
    m Maybe String
    mifile = do
      cubical <- TCMT IO (Maybe Cubical)
    forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
    cubicalOption
      let compile = case Maybe Cubical
    cubical of
            -- Code that uses --cubical is not compiled.
            Just Cubical
    CFull   -> Bool
    False
            Just Cubical
    CErased -> Bool
    True
            Maybe Cubical
    Nothing      -> Bool
    True
      ifM uptodate noComp (yesComp compile)
      where
        outFile_ :: TCMT IO String
    outFile_ = do
          m <- TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
          outFile (optJSModuleStyle opts) (jsMod m)

        uptodate :: TCMT IO Bool
    uptodate = case Maybe String
    mifile of
          Maybe String
    Nothing -> Bool -> TCMT IO Bool
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
          Just String
    ifile -> IO Bool -> TCMT IO Bool
    forall a. IO a -> TCMT IO a
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCMT IO Bool) -> TCMT IO (IO Bool) -> TCMT IO Bool
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< String -> String -> IO Bool
    isNewerThan (String -> String -> IO Bool)
    -> TCMT IO String -> TCMT IO (String -> IO Bool)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO String
    outFile_ TCMT IO (String -> IO Bool) -> TCMT IO String -> TCMT IO (IO Bool)
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> TCMT IO String
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure String
    ifile
        ifileDesc :: String
    ifileDesc = String -> Maybe String -> String
    forall a. a -> Maybe a -> a
    fromMaybe String
    "(memory)" Maybe String
    mifile

        noComp :: TCMT IO (Recompile JSModuleEnv Module)
    noComp = do
          String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js" Int
    2 (String -> TCMT IO ())
    -> (TopLevelModuleName -> String)
    -> TopLevelModuleName
    -> TCMT IO ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " : no compilation is needed.") (String -> String)
    -> (TopLevelModuleName -> String) -> TopLevelModuleName -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TopLevelModuleName -> String
    forall a. Pretty a => a -> String
    prettyShow (TopLevelModuleName -> TCMT IO ())
    -> TCMT IO TopLevelModuleName -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
          Recompile JSModuleEnv Module
    -> TCMT IO (Recompile JSModuleEnv Module)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Recompile JSModuleEnv Module
     -> TCMT IO (Recompile JSModuleEnv Module))
    -> Recompile JSModuleEnv Module
    -> TCMT IO (Recompile JSModuleEnv Module)
    forall a b. (a -> b) -> a -> b
    $ Module -> Recompile JSModuleEnv Module
    forall menv mod. mod -> Recompile menv mod
    Skip Module
    skippedModule

        -- A skipped module acts as a fake main module, to be skipped by --js-verify as well.
        skippedModule :: Module
    skippedModule = GlobalId -> [GlobalId] -> [Export] -> Maybe Exp -> Module
    Module (TopLevelModuleName -> GlobalId
    jsMod TopLevelModuleName
    m) [GlobalId]
    forall a. Monoid a => a
    mempty [Export]
    forall a. Monoid a => a
    mempty (Exp -> Maybe Exp
    forall a. a -> Maybe a
    Just Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__)

        yesComp :: Bool -> TCMT IO (Recompile JSModuleEnv Module)
    yesComp Bool
    compile = do
          m   <- TopLevelModuleName -> String
    forall a. Pretty a => a -> String
    prettyShow (TopLevelModuleName -> String)
    -> TCMT IO TopLevelModuleName -> TCMT IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
          out <- outFile_
          alwaysReportSLn "compile.js" 1 $ repl [m, ifileDesc, out] "Compiling <<0>> in <<1>> to <<2>>"
          kit <- coinductionKit
          return $ Recompile $ JSModuleEnv
            { jsCoinductionKit = kit
            , jsCompile        = compile
            }

    jsPostModule ::
      JSOptions -> JSModuleEnv -> IsMain -> TopLevelModuleName ->
      [Maybe Export] -> TCM Module
    jsPostModule :: JSOptions
    -> JSModuleEnv
    -> IsMain
    -> TopLevelModuleName
    -> [Maybe Export]
    -> TCMT IO Module
    jsPostModule JSOptions
    opts JSModuleEnv
    _ IsMain
    isMain TopLevelModuleName
    _ [Maybe Export]
    defs = do
      m  <- TopLevelModuleName -> GlobalId
    jsMod (TopLevelModuleName -> GlobalId)
    -> TCMT IO TopLevelModuleName -> TCMT IO GlobalId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO TopLevelModuleName
    forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
    curMName
      is <- map (jsMod . fst) . iImportedModules <$> curIF
      let mod = GlobalId -> [GlobalId] -> [Export] -> Maybe Exp -> Module
    Module GlobalId
    m [GlobalId]
    is ([Export] -> [Export]
    reorder [Export]
    es) Maybe Exp
    callMain
      writeModule (optJSMinify opts) (optJSModuleStyle opts) mod
      return mod
      where
      es :: [Export]
    es       = [Maybe Export] -> [Export]
    forall a. [Maybe a] -> [a]
    catMaybes [Maybe Export]
    defs
      main :: MemberId
    main     = String -> MemberId
    MemberId String
    "main"
      -- Andreas, 2020-10-27, only add invocation of "main" if such function is defined.
      -- This allows loading of generated .js files into an interpreter
      -- even if they do not define "main".
      hasMain :: Bool
    hasMain  = IsMain
    isMain IsMain -> IsMain -> Bool
    forall a. Eq a => a -> a -> Bool
    == IsMain
    IsMain Bool -> Bool -> Bool
    && (Export -> Bool) -> [Export] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any ((MemberId -> JSQName
    forall el coll. Singleton el coll => el -> coll
    singleton MemberId
    main JSQName -> JSQName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) (JSQName -> Bool) -> (Export -> JSQName) -> Export -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Export -> JSQName
    expName) [Export]
    es
      callMain :: Maybe Exp
      callMain :: Maybe Exp
    callMain = Bool -> Exp -> Maybe Exp
    forall a. Bool -> a -> Maybe a
    boolToMaybe Bool
    hasMain (Exp -> Maybe Exp) -> Exp -> Maybe Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    Apply (Exp -> MemberId -> Exp
    Lookup Exp
    Self MemberId
    main) [Int -> Exp -> Exp
    Lambda Int
    1 Exp
    emp]

    jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
    jsCompileDef :: JSOptions
    -> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
    jsCompileDef JSOptions
    opts JSModuleEnv
    kit IsMain
    _isMain Definition
    def = EnvWithOpts -> (QName, Definition) -> TCMT IO (Maybe Export)
    definition (JSOptions
    opts, JSModuleEnv
    kit) (Definition -> QName
    defName Definition
    def, Definition
    def)

    --------------------------------------------------
    -- Naming
    --------------------------------------------------

    prefix :: [Char]
    prefix :: String
    prefix = String
    "jAgda"

    jsMod :: TopLevelModuleName -> GlobalId
    jsMod :: TopLevelModuleName -> GlobalId
    jsMod TopLevelModuleName
    m =
      [String] -> GlobalId
    GlobalId (String
    prefix String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (Text -> String) -> [Text] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Text -> String
    T.unpack (TopLevelModuleNameParts -> [Item TopLevelModuleNameParts]
    forall l. IsList l => l -> [Item l]
    List1.toList (TopLevelModuleName -> TopLevelModuleNameParts
    forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
    moduleNameParts TopLevelModuleName
    m)))

    jsFileName :: JSModuleStyle -> GlobalId -> String
    jsFileName :: JSModuleStyle -> GlobalId -> String
    jsFileName JSModuleStyle
    JSES6 (GlobalId [String]
    ms) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "." [String]
    ms String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    ".mjs" -- Hint that file is ES6, not old js
    jsFileName JSModuleStyle
    _     (GlobalId [String]
    ms) = String -> [String] -> String
    forall a. [a] -> [[a]] -> [a]
    intercalate String
    "." [String]
    ms String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++  String
    ".js"

    jsMember :: Name -> MemberId
    jsMember :: Name -> MemberId
    jsMember Name
    n
      -- Anonymous fields are used for where clauses,
      -- and they're all given the concrete name "_",
      -- so we disambiguate them using their name id.
      | Name -> Bool
    forall a. IsNoName a => a -> Bool
    isNoName Name
    n = String -> MemberId
    MemberId (String
    "_" String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ NameId -> String
    forall a. Show a => a -> String
    show (Name -> NameId
    nameId Name
    n))
      | Bool
    otherwise  = String -> MemberId
    MemberId (String -> MemberId) -> String -> MemberId
    forall a b. (a -> b) -> a -> b
    $ Name -> String
    forall a. Pretty a => a -> String
    prettyShow Name
    n

    global' :: QName -> TCM (Exp, JSQName)
    global' :: QName -> TCM (Exp, JSQName)
    global' QName
    q = do
      i   <- Interface -> TopLevelModuleName
    iTopLevelModuleName (Interface -> TopLevelModuleName)
    -> TCMT IO Interface -> TCMT IO TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      top <- CC.topLevelModuleName (qnameModule q)
      let
        -- Global module prefix
        qms = ModuleName -> [Name]
    mnameToList (ModuleName -> [Name]) -> ModuleName -> [Name]
    forall a b. (a -> b) -> a -> b
    $ QName -> ModuleName
    qnameModule QName
    q
        -- File-local module prefix
        localms = Int -> [Name] -> [Name]
    forall a. Int -> [a] -> [a]
    drop (TopLevelModuleName -> Int
    forall a. Sized a => a -> Int
    size TopLevelModuleName
    top) [Name]
    qms
        nm = (Name -> MemberId) -> NonEmpty Name -> JSQName
    forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Name -> MemberId
    jsMember (NonEmpty Name -> JSQName) -> NonEmpty Name -> JSQName
    forall a b. (a -> b) -> a -> b
    $ [Name] -> Name -> NonEmpty Name
    forall a. [a] -> a -> List1 a
    List1.snoc [Name]
    localms (Name -> NonEmpty Name) -> Name -> NonEmpty Name
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q
      if top == i
        then return (Self, nm)
        else return (Global (jsMod top), nm)

    global :: QName -> TCM (Exp, JSQName)
    global :: QName -> TCM (Exp, JSQName)
    global QName
    q = do
      d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case d of
        Defn { theDef :: Definition -> Defn
    theDef = Constructor { conData :: Defn -> QName
    conData = QName
    p } } -> do
          QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    p TCMT IO Definition
    -> (Definition -> TCM (Exp, JSQName)) -> TCM (Exp, JSQName)
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
            -- Andreas, 2020-10-27, comment quotes outdated fact.
            -- anon. constructors are now M.R.constructor.
            -- We could simplify/remove the workaround by switching "record"
            -- to "constructor", but this changes the output of the JS compiler
            -- maybe in ways that break user's developments
            -- (if they link to Agda-generated JS).
            -- -- Rather annoyingly, the anonymous constructor of a record R in module M
            -- -- is given the name M.recCon, but a named constructor C
            -- -- is given the name M.R.C, sigh. This causes a lot of hoop-jumping
            -- -- in the map from Agda names to JS names, which we patch by renaming
            -- -- anonymous constructors to M.R.record.
            Defn { theDef :: Definition -> Defn
    theDef = Record { recNamedCon :: Defn -> Bool
    recNamedCon = Bool
    False } } -> do
              (m,ls) <- QName -> TCM (Exp, JSQName)
    global' QName
    p
              return (m, ls <> singleton (MemberId "record"))
            Definition
    _ -> QName -> TCM (Exp, JSQName)
    global' (Definition -> QName
    defName Definition
    d)
        Definition
    _ -> QName -> TCM (Exp, JSQName)
    global' (Definition -> QName
    defName Definition
    d)

    -- Reorder a list of exports to ensure def-before-use.
    -- Note that this can diverge in the case when there is no such reordering.

    -- Only top-level values are evaluated before definitions are added to the
    -- module, so we put those last, ordered in dependency order. There can't be
    -- any recursion between top-level values (unless termination checking has been
    -- disabled and someone's written a non-sensical program), so reordering will
    -- terminate.

    reorder :: [Export] -> [Export]
    reorder :: [Export] -> [Export]
    reorder [Export]
    es = [Export]
    datas [Export] -> [Export] -> [Export]
    forall a. [a] -> [a] -> [a]
    ++ [Export]
    funs [Export] -> [Export] -> [Export]
    forall a. [a] -> [a] -> [a]
    ++ Set JSQName -> [Export] -> [Export]
    reorder' ([JSQName] -> Set JSQName
    forall a. Ord a => [a] -> Set a
    Set.fromList ([JSQName] -> Set JSQName) -> [JSQName] -> Set JSQName
    forall a b. (a -> b) -> a -> b
    $ (Export -> JSQName) -> [Export] -> [JSQName]
    forall a b. (a -> b) -> [a] -> [b]
    map Export -> JSQName
    expName ([Export] -> [JSQName]) -> [Export] -> [JSQName]
    forall a b. (a -> b) -> a -> b
    $ [Export]
    datas [Export] -> [Export] -> [Export]
    forall a. [a] -> [a] -> [a]
    ++ [Export]
    funs) [Export]
    vals
      where
        ([Export]
    vs, [Export]
    funs)    = (Export -> Bool) -> [Export] -> ([Export], [Export])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Export -> Bool
    isTopLevelValue [Export]
    es
        ([Export]
    datas, [Export]
    vals) = (Export -> Bool) -> [Export] -> ([Export], [Export])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    partition Export -> Bool
    isEmptyObject [Export]
    vs

    reorder' :: Set JSQName -> [Export] -> [Export]
    reorder' :: Set JSQName -> [Export] -> [Export]
    reorder' Set JSQName
    defs [] = []
    reorder' Set JSQName
    defs (Export
    e : [Export]
    es) =
      let us :: Set JSQName
    us = Export -> Set JSQName
    forall a. Uses a => a -> Set JSQName
    uses Export
    e Set JSQName -> Set JSQName -> Set JSQName
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.difference` Set JSQName
    defs
      in  if Set JSQName -> Bool
    forall a. Null a => a -> Bool
    null Set JSQName
    us
            then Export
    e Export -> [Export] -> [Export]
    forall a. a -> [a] -> [a]
    : (Set JSQName -> [Export] -> [Export]
    reorder' (JSQName -> Set JSQName -> Set JSQName
    forall a. Ord a => a -> Set a -> Set a
    Set.insert (Export -> JSQName
    expName Export
    e) Set JSQName
    defs) [Export]
    es)
            else Set JSQName -> [Export] -> [Export]
    reorder' Set JSQName
    defs (Set JSQName -> Export -> [Export] -> [Export]
    insertAfter Set JSQName
    us Export
    e [Export]
    es)

    isTopLevelValue :: Export -> Bool
    isTopLevelValue :: Export -> Bool
    isTopLevelValue (Export JSQName
    _ Exp
    e) = case Exp
    e of
      Object Map MemberId Exp
    m | MemberId
    flatName MemberId -> Map MemberId Exp -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `Map.member` Map MemberId Exp
    m -> Bool
    False
      Lambda{} -> Bool
    False
      Exp
    _        -> Bool
    True

    isEmptyObject :: Export -> Bool
    isEmptyObject :: Export -> Bool
    isEmptyObject (Export JSQName
    _ Exp
    e) = case Exp
    e of
      Object Map MemberId Exp
    m -> Map MemberId Exp -> Bool
    forall a. Null a => a -> Bool
    null Map MemberId Exp
    m
      Lambda{} -> Bool
    True
      Exp
    _        -> Bool
    False

    insertAfter :: Set JSQName -> Export -> [Export] -> [Export]
    insertAfter :: Set JSQName -> Export -> [Export] -> [Export]
    insertAfter Set JSQName
    us Export
    e []                   = [Export
    e]
    insertAfter Set JSQName
    us Export
    e (Export
    f : [Export]
    fs) | Set JSQName -> Bool
    forall a. Null a => a -> Bool
    null Set JSQName
    us   = Export
    e Export -> [Export] -> [Export]
    forall a. a -> [a] -> [a]
    : Export
    f Export -> [Export] -> [Export]
    forall a. a -> [a] -> [a]
    : [Export]
    fs
    insertAfter Set JSQName
    us Export
    e (Export
    f : [Export]
    fs) | Bool
    otherwise =
      Export
    f Export -> [Export] -> [Export]
    forall a. a -> [a] -> [a]
    : Set JSQName -> Export -> [Export] -> [Export]
    insertAfter (JSQName -> Set JSQName -> Set JSQName
    forall a. Ord a => a -> Set a -> Set a
    Set.delete (Export -> JSQName
    expName Export
    f) Set JSQName
    us) Export
    e [Export]
    fs

    --------------------------------------------------
    -- Main compiling clauses
    --------------------------------------------------

    type EnvWithOpts = (JSOptions, JSModuleEnv)

    definition :: EnvWithOpts -> (QName,Definition) -> TCM (Maybe Export)
    definition :: EnvWithOpts -> (QName, Definition) -> TCMT IO (Maybe Export)
    definition EnvWithOpts
    kit (QName
    q,Definition
    d) = do
      String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.js" Int
    10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "compiling def:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
      (_,ls) <- QName -> TCM (Exp, JSQName)
    global QName
    q
      d <- instantiateFull d

      definition' kit q d (defType d) ls

    -- | Ensure that there is at most one pragma for a name.
    checkCompilerPragmas :: QName -> TCM ()
    checkCompilerPragmas :: QName -> TCMT IO ()
    checkCompilerPragmas QName
    q =
      TCMT IO (Maybe CompilerPragma)
    -> TCMT IO () -> (CompilerPragma -> TCMT IO ()) -> TCMT IO ()
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (Text -> QName -> TCMT IO (Maybe CompilerPragma)
    getUniqueCompilerPragma Text
    jsBackendName QName
    q) (() -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()) ((CompilerPragma -> TCMT IO ()) -> TCMT IO ())
    -> (CompilerPragma -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ (CompilerPragma Range
    r String
    s) -> do
      Range -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r do
        -- Issue #3545: Warn user about ignored COMPILE pragma for defined functions.
        QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q TCMT IO Definition -> (Definition -> Defn) -> TCMT IO Defn
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> Definition -> Defn
    theDef TCMT IO Defn -> (Defn -> TCMT IO ()) -> TCMT IO ()
    forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \case
          FunctionDefn{} -> TCMT IO Bool -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
    whenM (QName -> TCMT IO Bool
    isErasable QName
    q) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Warning -> TCMT IO ()
    forall (m :: * -> *).
    (HasCallStack, MonadWarning m) =>
    Warning -> m ()
    warning (Warning -> TCMT IO ()) -> Warning -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ Text -> QName -> Warning
    PragmaCompileErased Text
    jsBackendName QName
    q
          Defn
    _ -> () -> TCMT IO ()
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return()
        -- If the pragma is not of the form "q = bla", complain.
        Bool -> TCMT IO () -> TCMT IO ()
    forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
    when ([String] -> Maybe String
    forall a. [a] -> Maybe a
    listToMaybe (String -> [String]
    words String
    s) Maybe String -> Maybe String -> Bool
    forall a. Eq a => a -> a -> Bool
    /= String -> Maybe String
    forall a. a -> Maybe a
    Just String
    "=") do
          TypeError -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> TCMT IO ()) -> TypeError -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ JSBackendError -> TypeError
    JSBackendError JSBackendError
    BadCompilePragma

    defJSDef :: Definition -> Maybe String
    defJSDef :: Definition -> Maybe String
    defJSDef Definition
    def =
      case Text -> Definition -> [CompilerPragma]
    defCompilerPragmas Text
    jsBackendName Definition
    def of
        [CompilerPragma Range
    _ String
    s] -> String -> Maybe String
    forall a. a -> Maybe a
    Just (String -> String
    dropEquals String
    s)
        []                   -> Maybe String
    forall a. Maybe a
    Nothing
        CompilerPragma
    _:CompilerPragma
    _:[CompilerPragma]
    _                -> Maybe String
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        dropEquals :: String -> String
    dropEquals = (Char -> Bool) -> String -> String
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile ((Char -> Bool) -> String -> String)
    -> (Char -> Bool) -> String -> String
    forall a b. (a -> b) -> a -> b
    $ \ Char
    c -> Char -> Bool
    isSpace Char
    c Bool -> Bool -> Bool
    || Char
    c Char -> Char -> Bool
    forall a. Eq a => a -> a -> Bool
    == Char
    '='

    definition' :: EnvWithOpts -> QName -> Definition -> Type -> JSQName -> TCM (Maybe Export)
    definition' :: EnvWithOpts
    -> QName -> Definition -> Type -> JSQName -> TCMT IO (Maybe Export)
    definition' EnvWithOpts
    kit QName
    q Definition
    d Type
    t JSQName
    ls =
      if Bool -> Bool
    not (JSModuleEnv -> Bool
    jsCompile (EnvWithOpts -> JSModuleEnv
    forall a b. (a, b) -> b
    snd EnvWithOpts
    kit)) Bool -> Bool -> Bool
    || Bool -> Bool
    not (Definition -> Bool
    forall a. LensModality a => a -> Bool
    usableModality Definition
    d)
      then Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Export
    forall a. Maybe a
    Nothing
      else do
      QName -> TCMT IO ()
    checkCompilerPragmas QName
    q
      case Definition -> Defn
    theDef Definition
    d of
        -- coinduction
        Constructor{}
          | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == (CoinductionKit -> QName
    nameOfSharp (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> JSModuleEnv -> Maybe CoinductionKit
    jsCoinductionKit (EnvWithOpts -> JSModuleEnv
    forall a b. (a, b) -> b
    snd EnvWithOpts
    kit)) -> do
          Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Export
    forall a. Maybe a
    Nothing
        Function{}
          | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == (CoinductionKit -> QName
    nameOfFlat (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> JSModuleEnv -> Maybe CoinductionKit
    jsCoinductionKit (EnvWithOpts -> JSModuleEnv
    forall a b. (a, b) -> b
    snd EnvWithOpts
    kit)) -> do
          Exp -> TCMT IO (Maybe Export)
    ret (Exp -> TCMT IO (Maybe Export)) -> Exp -> TCMT IO (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ Int -> Exp -> Exp
    Lambda Int
    1 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    Apply (Exp -> MemberId -> Exp
    Lookup (Int -> Exp
    local Int
    0) MemberId
    flatName) []

        DataOrRecSig{} -> TCMT IO (Maybe Export)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

        Axiom{} | Just String
    e <- Definition -> Maybe String
    defJSDef Definition
    d -> String -> TCMT IO (Maybe Export)
    plainJS String
    e
        Axiom{} | Bool
    otherwise -> Exp -> TCMT IO (Maybe Export)
    ret Exp
    Undefined

        GeneralizableVar{} -> Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Export
    forall a. Maybe a
    Nothing

        Function{} | Just String
    e <- Definition -> Maybe String
    defJSDef Definition
    d -> String -> TCMT IO (Maybe Export)
    plainJS String
    e
        Function{} | Bool
    otherwise -> do

          String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.js" Int
    5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "compiling fun:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> QName -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => QName -> m Doc
    prettyTCM QName
    q
          let mTreeless :: TCM (Maybe TTerm)
    mTreeless = EvaluationStrategy -> QName -> TCM (Maybe TTerm)
    toTreeless EvaluationStrategy
    T.EagerEvaluation QName
    q
          TCM (Maybe TTerm)
    -> TCMT IO (Maybe Export)
    -> (TTerm -> TCMT IO (Maybe Export))
    -> TCMT IO (Maybe Export)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM TCM (Maybe TTerm)
    mTreeless (Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Export
    forall a. Maybe a
    Nothing) ((TTerm -> TCMT IO (Maybe Export)) -> TCMT IO (Maybe Export))
    -> (TTerm -> TCMT IO (Maybe Export)) -> TCMT IO (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ \ TTerm
    treeless -> do
            used <- [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
    forall a. a -> Maybe a -> a
    fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
    -> TCMT IO (Maybe [ArgUsage]) -> TCMT IO [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO (Maybe [ArgUsage])
    forall (m :: * -> *).
    HasConstInfo m =>
    QName -> m (Maybe [ArgUsage])
    getCompiledArgUse QName
    q
            funBody <- eliminateCaseDefaults =<<
              eliminateLiteralPatterns
              (convertGuards treeless)
            reportSDoc "compile.js" 30 $ " compiled treeless fun:" <+> pretty funBody
            reportSDoc "compile.js" 40 $ " argument usage:" <+> (text . show) used

            funBody' <- compileTerm kit funBody

            reportSDoc "compile.js" 30 $ " compiled JS fun:" <+> (text . show) funBody'
            return $
              if funBody' == Null then Nothing
              else Just $ Export ls funBody'

        Primitive{primName :: Defn -> PrimitiveId
    primName = PrimitiveId
    p}
          | PrimitiveId
    p PrimitiveId -> PrimitiveId -> Bool
    forall a. Eq a => a -> a -> Bool
    == PrimitiveId
    builtin_glueU ->
            -- The string prim^glueU is not a valid JS name.
            String -> TCMT IO (Maybe Export)
    plainJS String
    "agdaRTS.prim_glueU"
          | PrimitiveId
    p PrimitiveId -> PrimitiveId -> Bool
    forall a. Eq a => a -> a -> Bool
    == PrimitiveId
    builtin_unglueU ->
            -- The string prim^unglueU is not a valid JS name.
            String -> TCMT IO (Maybe Export)
    plainJS String
    "agdaRTS.prim_unglueU"
          | PrimitiveId
    p PrimitiveId -> Set PrimitiveId -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set PrimitiveId
    primitives ->
            String -> TCMT IO (Maybe Export)
    plainJS (String -> TCMT IO (Maybe Export))
    -> String -> TCMT IO (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ String
    "agdaRTS." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ PrimitiveId -> String
    forall a. IsBuiltin a => a -> String
    getBuiltinId PrimitiveId
    p
          | Just String
    e <- Definition -> Maybe String
    defJSDef Definition
    d ->
            String -> TCMT IO (Maybe Export)
    plainJS String
    e
          | Bool
    otherwise ->
            Exp -> TCMT IO (Maybe Export)
    ret Exp
    Undefined
        PrimitiveSort{} -> Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Export
    forall a. Maybe a
    Nothing

        Datatype{} -> do
            QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
            Exp -> TCMT IO (Maybe Export)
    ret Exp
    emp
        Record{} -> do
            QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
            Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe Export
    forall a. Maybe a
    Nothing

        Constructor{} | Just String
    e <- Definition -> Maybe String
    defJSDef Definition
    d -> String -> TCMT IO (Maybe Export)
    plainJS String
    e
        -- Implements Scott-Encoding of constructor definitions
        -- (see the note "Implementing data types")
        Constructor{conData :: Defn -> QName
    conData = QName
    p, conPars :: Defn -> Int
    conPars = Int
    nc} -> do
          TelV tel _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
          let nargs = [Dom (String, Type)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Tele (Dom Type) -> [Dom (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Tele (Dom Type)
    tel) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    nc
              args = [ LocalId -> Exp
    Local (LocalId -> Exp) -> LocalId -> Exp
    forall a b. (a -> b) -> a -> b
    $ Int -> LocalId
    LocalId (Int -> LocalId) -> Int -> LocalId
    forall a b. (a -> b) -> a -> b
    $ Int
    nargs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    i | Int
    i <- [Int
    0 .. Int
    nargsInt -> Int -> Int
    forall a. Num a => a -> a -> a
    -Int
    1] ]
          d <- getConstInfo p
          let l = JSQName -> MemberId
    forall a. NonEmpty a -> a
    List1.last JSQName
    ls
          ret
            $ curriedLambda nargs
            $ (case theDef d of
                  Record {} -> Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp)
    -> (Exp -> Map MemberId Exp) -> Exp -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . MemberId -> Exp -> Map MemberId Exp
    forall k a. k -> a -> Map k a
    Map.singleton MemberId
    l
                  Defn
    dt -> Exp -> Exp
    forall a. a -> a
    id)
            $  Lambda 1 $ Apply (Lookup (Local (LocalId 0)) l) args

        AbstractDefn{} -> TCMT IO (Maybe Export)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        ret :: Exp -> TCMT IO (Maybe Export)
    ret = Maybe Export -> TCMT IO (Maybe Export)
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Export -> TCMT IO (Maybe Export))
    -> (Exp -> Maybe Export) -> Exp -> TCMT IO (Maybe Export)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Export -> Maybe Export
    forall a. a -> Maybe a
    Just (Export -> Maybe Export) -> (Exp -> Export) -> Exp -> Maybe Export
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . JSQName -> Exp -> Export
    Export JSQName
    ls
        plainJS :: String -> TCMT IO (Maybe Export)
    plainJS = Exp -> TCMT IO (Maybe Export)
    ret (Exp -> TCMT IO (Maybe Export))
    -> (String -> Exp) -> String -> TCMT IO (Maybe Export)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Exp
    PlainJS

    -- Implementing data types
    --------------------------

    -- Data types are implemented using a variant of Scott Encoding,
    -- which uses JavaScript dicts instead of some lambda-expressions

    -- For example, given the data type
    --
    --      data Foo : Set where
    --        c1 : Foo
    --        c2 : X -> Y -> Foo
    --        c3 : Foo -> Foo
    --
    -- here is how "Foo" is compiled:
    --
    --  * A constructor definition, e.g.
    --
    --        c2 : X -> Y -> Foo
    --
    --    compiles to
    --
    --        exports["Foo"]["c2"] = x => y => k => k["c2"](x,y)
    --
    --  * A constructor application, e.g.
    --
    --        c2 x y
    --
    --    compiles to
    --
    --        exports["Foo"]["c2"](x)(y)
    --
    --  * A case split, e.g.
    --
    --        case p of
    --          (c1    ) -> E1
    --          (c2 x y) -> E2
    --          (c3 f  ) -> E3
    --
    --    compiles to
    --
    --        p(
    --          { "c1": ()    => E1
    --          , "c2": (x,y) => E2
    --          , "c3": f     => E3
    --          })

    compileTerm :: EnvWithOpts -> T.TTerm -> TCM Exp
    compileTerm :: EnvWithOpts -> TTerm -> TCM Exp
    compileTerm EnvWithOpts
    kit TTerm
    t = TTerm -> TCM Exp
    go TTerm
    t
      where
        go :: T.TTerm -> TCM Exp
        go :: TTerm -> TCM Exp
    go = \case
          T.TVar Int
    x -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ LocalId -> Exp
    Local (LocalId -> Exp) -> LocalId -> Exp
    forall a b. (a -> b) -> a -> b
    $ Int -> LocalId
    LocalId Int
    x
          T.TDef QName
    q -> do
            d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
            case theDef d of
              -- Datatypes and records are erased
              Datatype {} -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Exp
    String Text
    "*")
              Record {} -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Exp
    String Text
    "*")
              Defn
    _ -> QName -> TCM Exp
    qname QName
    q
          T.TApp (T.TCon QName
    q) [TTerm
    x]
            | QName -> Maybe QName
    forall a. a -> Maybe a
    Just QName
    q Maybe QName -> Maybe QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == (CoinductionKit -> QName
    nameOfSharp (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> JSModuleEnv -> Maybe CoinductionKit
    jsCoinductionKit (EnvWithOpts -> JSModuleEnv
    forall a b. (a, b) -> b
    snd EnvWithOpts
    kit)) -> do
            x <- TTerm -> TCM Exp
    go TTerm
    x
            let evalThunk = [String] -> String
    unlines
                  [ String
    "function() {"
                  , String
    "  delete this.flat;"
                  , String
    "  var result = this.__flat_helper();"
                  , String
    "  delete this.__flat_helper;"
                  , String
    "  this.flat = function() { return result; };"
                  , String
    "  return result;"
                  , String
    "}"
                  ]
            return $ Object $ Map.fromListWith __IMPOSSIBLE__
              [(flatName, PlainJS evalThunk)
              ,(MemberId "__flat_helper", Lambda 0 x)]
          T.TApp TTerm
    t [TTerm]
    xs -> do
                Exp -> [Exp] -> Exp
    curriedApply (Exp -> [Exp] -> Exp) -> TCM Exp -> TCMT IO ([Exp] -> Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM Exp
    go TTerm
    t TCMT IO ([Exp] -> Exp) -> TCMT IO [Exp] -> TCM Exp
    forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM Exp) -> [TTerm] -> TCMT IO [Exp]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM TTerm -> TCM Exp
    go [TTerm]
    xs
          T.TLam TTerm
    t -> Int -> Exp -> Exp
    Lambda Int
    1 (Exp -> Exp) -> TCM Exp -> TCM Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM Exp
    go TTerm
    t
          -- `let x = t in e` is compiled to `(x => e[x()/x])(() => t)` so that `t`
          -- is only evaluated inside the body
          T.TLet TTerm
    t TTerm
    e -> do
            t' <- Int -> Exp -> Exp
    Lambda Int
    0 (Exp -> Exp) -> TCM Exp -> TCM Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> TCM Exp
    go TTerm
    t
            e' <- substShift 1 1 [Apply (Local (LocalId 0)) []] <$> go e
            return $ Apply (Lambda 1 e') [t']
          T.TLit Literal
    l -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ Literal -> Exp
    literal Literal
    l
          -- Implements Scott-Encoding of constructor applications
          -- (see the note "Implementing data types")
          T.TCon QName
    q -> QName -> TCM Exp
    qname QName
    q
        -- Implements Scott-Encoding of case splits
        -- (see the note "Implementing data types")
          T.TCase Int
    sc CaseInfo
    ct TTerm
    def [TAlt]
    alts | T.CTData QName
    dt <- CaseInfo -> CaseType
    T.caseType CaseInfo
    ct -> do
            dt <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    dt
            alts' <- traverse (compileAlt kit) alts
            let cs  = Defn -> [QName]
    defConstructors (Defn -> [QName]) -> Defn -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    dt
                obj = Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Exp -> Exp -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [(MemberId, Exp)]
    alts'
            case (theDef dt, defJSDef dt) of
              (Defn
    _, Just String
    e) -> do
                Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    apply (String -> Exp
    PlainJS String
    e) [LocalId -> Exp
    Local (Int -> LocalId
    LocalId Int
    sc), Exp
    obj]
              (Record{}, Maybe String
    _) -> do
                memId <- QName -> TCM MemberId
    visitorName (QName -> TCM MemberId) -> QName -> TCM MemberId
    forall a b. (a -> b) -> a -> b
    $ Defn -> QName
    recCon (Defn -> QName) -> Defn -> QName
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    dt
                return $ apply (Lookup (Local $ LocalId sc) memId) [obj]
              (Datatype{}, Maybe String
    _) -> do
                Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    curriedApply (LocalId -> Exp
    Local (Int -> LocalId
    LocalId Int
    sc)) [Exp
    obj]
              (Defn, Maybe String)
    _ -> TCM Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          T.TCase Int
    _ CaseInfo
    _ TTerm
    _ [TAlt]
    _ -> TCM Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__

          T.TPrim TPrim
    p -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ TPrim -> Exp
    compilePrim TPrim
    p
          TTerm
    T.TUnit -> TCM Exp
    unit
          TTerm
    T.TSort -> TCM Exp
    unit
          TTerm
    T.TErased -> TCM Exp
    unit
          T.TError TError
    T.TUnreachable -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp
    Undefined
          T.TError T.TMeta{}      -> Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp
    Undefined
          T.TCoerce TTerm
    t -> TTerm -> TCM Exp
    go TTerm
    t

        getDef :: TTerm -> Maybe (Either QName QName)
    getDef (T.TDef QName
    f) = Either QName QName -> Maybe (Either QName QName)
    forall a. a -> Maybe a
    Just (QName -> Either QName QName
    forall a b. a -> Either a b
    Left QName
    f)
        getDef (T.TCon QName
    c) = Either QName QName -> Maybe (Either QName QName)
    forall a. a -> Maybe a
    Just (QName -> Either QName QName
    forall a b. b -> Either a b
    Right QName
    c)
        getDef (T.TCoerce TTerm
    x) = TTerm -> Maybe (Either QName QName)
    getDef TTerm
    x
        getDef TTerm
    _ = Maybe (Either QName QName)
    forall a. Maybe a
    Nothing

        unit :: TCM Exp
    unit = Exp -> TCM Exp
    forall a. a -> TCMT IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Exp
    Null

        mkArray :: [(Comment, Exp)] -> Exp
    mkArray [(Comment, Exp)]
    xs
            | Int
    2 Int -> Int -> Int
    forall a. Num a => a -> a -> a
    * [(Comment, Exp)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (((Comment, Exp) -> Bool) -> [(Comment, Exp)] -> [(Comment, Exp)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Exp -> Exp -> Bool
    forall a. Eq a => a -> a -> Bool
    == Exp
    Null) (Exp -> Bool) -> ((Comment, Exp) -> Exp) -> (Comment, Exp) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Comment, Exp) -> Exp
    forall a b. (a, b) -> b
    snd) [(Comment, Exp)]
    xs) Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= [(Comment, Exp)] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [(Comment, Exp)]
    xs = [(Comment, Exp)] -> Exp
    Array [(Comment, Exp)]
    xs
            | Bool
    otherwise = Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Exp -> Exp -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                [ (Int -> Comment -> MemberId
    MemberIndex Int
    i Comment
    c, Exp
    x) | (Int
    i, (Comment
    c, Exp
    x)) <- [Int] -> [(Comment, Exp)] -> [(Int, (Comment, Exp))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip [Int
    0..] [(Comment, Exp)]
    xs, Exp
    x Exp -> Exp -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Exp
    Null ]

    compilePrim :: T.TPrim -> Exp
    compilePrim :: TPrim -> Exp
    compilePrim TPrim
    p =
      case TPrim
    p of
        TPrim
    T.PIf -> Int -> Exp -> Exp
    curriedLambda Int
    3 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> Exp -> Exp -> Exp
    If (Int -> Exp
    local Int
    2) (Int -> Exp
    local Int
    1) (Int -> Exp
    local Int
    0)
        TPrim
    T.PEqI -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerEqual"
        TPrim
    T.PEqF -> String -> Exp
    binOp String
    "agdaRTS.uprimFloatEquality"
        TPrim
    T.PEqQ -> String -> Exp
    binOp String
    "agdaRTS.uprimQNameEquality"
        TPrim
    T.PEqS -> Exp
    primEq
        TPrim
    T.PEqC -> Exp
    primEq
        TPrim
    T.PGeq -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerGreaterOrEqualThan"
        TPrim
    T.PLt -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerLessThan"
        TPrim
    T.PAdd -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerPlus"
        TPrim
    T.PSub -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerMinus"
        TPrim
    T.PMul -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerMultiply"
        TPrim
    T.PRem -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerRem"
        TPrim
    T.PQuot -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerQuot"
        TPrim
    T.PAdd64 -> String -> Exp
    binOp String
    "agdaRTS.uprimWord64Plus"
        TPrim
    T.PSub64 -> String -> Exp
    binOp String
    "agdaRTS.uprimWord64Minus"
        TPrim
    T.PMul64 -> String -> Exp
    binOp String
    "agdaRTS.uprimWord64Multiply"
        TPrim
    T.PRem64 -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerRem"     -- -|
        TPrim
    T.PQuot64 -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerQuot"   --  > These can use the integer functions
        TPrim
    T.PEq64 -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerEqual"    --  |
        TPrim
    T.PLt64 -> String -> Exp
    binOp String
    "agdaRTS.uprimIntegerLessThan" -- -|
        TPrim
    T.PITo64 -> String -> Exp
    unOp String
    "agdaRTS.primWord64FromNat"
        TPrim
    T.P64ToI -> String -> Exp
    unOp String
    "agdaRTS.primWord64ToNat"
        TPrim
    T.PSeq -> String -> Exp
    binOp String
    "agdaRTS.primSeq"
      where binOp :: String -> Exp
    binOp String
    js = Int -> Exp -> Exp
    curriedLambda Int
    2 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    apply (String -> Exp
    PlainJS String
    js) [Int -> Exp
    local Int
    1, Int -> Exp
    local Int
    0]
            unOp :: String -> Exp
    unOp String
    js  = Int -> Exp -> Exp
    curriedLambda Int
    1 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    apply (String -> Exp
    PlainJS String
    js) [Int -> Exp
    local Int
    0]
            primEq :: Exp
    primEq   = Int -> Exp -> Exp
    curriedLambda Int
    2 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> String -> Exp -> Exp
    BinOp (Int -> Exp
    local Int
    1) String
    "===" (Int -> Exp
    local Int
    0)

    -- Implements Scott-Encoding of case split cases
    -- (see the note "Implementing data types")
    compileAlt :: EnvWithOpts -> T.TAlt -> TCM (MemberId, Exp)
    compileAlt :: EnvWithOpts -> TAlt -> TCMT IO (MemberId, Exp)
    compileAlt EnvWithOpts
    kit = \case
      T.TACon QName
    con Int
    nargs TTerm
    body -> do
        memId <- QName -> TCM MemberId
    visitorName QName
    con
        body <- Lambda nargs <$> compileTerm kit body
        return (memId, body)
      TAlt
    _ -> TCMT IO (MemberId, Exp)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    visitorName :: QName -> TCM MemberId
    visitorName :: QName -> TCM MemberId
    visitorName QName
    q = JSQName -> MemberId
    forall a. NonEmpty a -> a
    List1.last (JSQName -> MemberId)
    -> ((Exp, JSQName) -> JSQName) -> (Exp, JSQName) -> MemberId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Exp, JSQName) -> JSQName
    forall a b. (a, b) -> b
    snd ((Exp, JSQName) -> MemberId) -> TCM (Exp, JSQName) -> TCM MemberId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCM (Exp, JSQName)
    global QName
    q

    flatName :: MemberId
    flatName :: MemberId
    flatName = String -> MemberId
    MemberId String
    "flat"

    local :: Nat -> Exp
    local :: Int -> Exp
    local = LocalId -> Exp
    Local (LocalId -> Exp) -> (Int -> LocalId) -> Int -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> LocalId
    LocalId

    qname :: QName -> TCM Exp
    qname :: QName -> TCM Exp
    qname QName
    q = do
      (e,ls) <- QName -> TCM (Exp, JSQName)
    global QName
    q
      return (foldl Lookup e ls)

    literal :: Literal -> Exp
    literal :: Literal -> Exp
    literal = \case
      (LitNat    Integer
    x) -> Integer -> Exp
    Integer Integer
    x
      (LitWord64 Word64
    x) -> Integer -> Exp
    Integer (Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    x)
      (LitFloat  Double
    x) -> Double -> Exp
    Double  Double
    x
      (LitString Text
    x) -> Text -> Exp
    String  Text
    x
      (LitChar   Char
    x) -> Char -> Exp
    Char    Char
    x
      (LitQName  QName
    x) -> QName -> Exp
    litqname QName
    x
      (LitMeta TopLevelModuleName
    _ MetaId
    m) -> MetaId -> Exp
    litmeta MetaId
    m

    litqname :: QName -> Exp
    litqname :: QName -> Exp
    litqname QName
    q =
      Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Exp -> Exp -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        [ (String -> MemberId
    mem String
    "id", Integer -> Exp
    Integer (Integer -> Exp) -> Integer -> Exp
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    n)
        , (String -> MemberId
    mem String
    "moduleId", Integer -> Exp
    Integer (Integer -> Exp) -> Integer -> Exp
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    m)
        , (String -> MemberId
    mem String
    "name", Text -> Exp
    String (Text -> Exp) -> Text -> Exp
    forall a b. (a -> b) -> a -> b
    $ String -> Text
    T.pack (String -> Text) -> String -> Text
    forall a b. (a -> b) -> a -> b
    $ QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q)
        , (String -> MemberId
    mem String
    "fixity", Fixity -> Exp
    litfixity Fixity
    fx)]
      where
        mem :: String -> MemberId
    mem = String -> MemberId
    MemberId
        NameId Word64
    n (ModuleNameHash Word64
    m) = Name -> NameId
    nameId (Name -> NameId) -> Name -> NameId
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q
        fx :: Fixity
    fx = Fixity' -> Fixity
    theFixity (Fixity' -> Fixity) -> Fixity' -> Fixity
    forall a b. (a -> b) -> a -> b
    $ Name -> Fixity'
    nameFixity (Name -> Fixity') -> Name -> Fixity'
    forall a b. (a -> b) -> a -> b
    $ QName -> Name
    qnameName QName
    q

        litfixity :: Fixity -> Exp
        litfixity :: Fixity -> Exp
    litfixity Fixity
    fx = Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Exp -> Exp -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          [ (String -> MemberId
    mem String
    "assoc", Associativity -> Exp
    litAssoc (Associativity -> Exp) -> Associativity -> Exp
    forall a b. (a -> b) -> a -> b
    $ Fixity -> Associativity
    fixityAssoc Fixity
    fx)
          , (String -> MemberId
    mem String
    "prec", FixityLevel -> Exp
    litPrec (FixityLevel -> Exp) -> FixityLevel -> Exp
    forall a b. (a -> b) -> a -> b
    $ Fixity -> FixityLevel
    fixityLevel Fixity
    fx)]

        -- TODO this will probably not work well together with the necessary FFI bindings
        litAssoc :: Associativity -> Exp
    litAssoc Associativity
    NonAssoc   = Text -> Exp
    String Text
    "non-assoc"
        litAssoc Associativity
    LeftAssoc  = Text -> Exp
    String Text
    "left-assoc"
        litAssoc Associativity
    RightAssoc = Text -> Exp
    String Text
    "right-assoc"

        litPrec :: FixityLevel -> Exp
    litPrec FixityLevel
    Unrelated   = Text -> Exp
    String Text
    "unrelated"
        litPrec (Related Double
    l) = Double -> Exp
    Double Double
    l

    litmeta :: MetaId -> Exp
    litmeta :: MetaId -> Exp
    litmeta (MetaId Word64
    m ModuleNameHash
    h) =
      Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Exp -> Exp -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        [ (String -> MemberId
    MemberId String
    "id", Integer -> Exp
    Integer (Integer -> Exp) -> Integer -> Exp
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Word64
    m)
        , (String -> MemberId
    MemberId String
    "module", Integer -> Exp
    Integer (Integer -> Exp) -> Integer -> Exp
    forall a b. (a -> b) -> a -> b
    $ Word64 -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral (Word64 -> Integer) -> Word64 -> Integer
    forall a b. (a -> b) -> a -> b
    $ ModuleNameHash -> Word64
    moduleNameHash ModuleNameHash
    h) ]

    --------------------------------------------------
    -- Writing out an ECMAScript module
    --------------------------------------------------

    writeModule :: Bool -> JSModuleStyle -> Module -> TCM ()
    writeModule :: Bool -> JSModuleStyle -> Module -> TCMT IO ()
    writeModule Bool
    minify JSModuleStyle
    ms Module
    m = do
      out <- JSModuleStyle -> GlobalId -> TCMT IO String
    outFile JSModuleStyle
    ms (Module -> GlobalId
    modName Module
    m)
      liftIO (writeFile out (JSPretty.prettyShow minify ms m))

    outFile :: JSModuleStyle -> GlobalId -> TCM FilePath
    outFile :: JSModuleStyle -> GlobalId -> TCMT IO String
    outFile JSModuleStyle
    ms GlobalId
    m = do
      mdir <- TCMT IO String
    forall (m :: * -> *). HasOptions m => m String
    compileDir
      let (fdir, fn) = splitFileName (jsFileName ms m)
      let dir = String
    mdir String -> String -> String
    </> String
    fdir
          fp  = String
    dir String -> String -> String
    </> String
    fn
      liftIO $ createDirectoryIfMissing True dir
      return fp

    -- | Primitives implemented in the JS Agda RTS.
    --
    -- TODO: Primitives that are not part of this set, and for which
    -- 'defJSDef' does not return anything, are silently compiled to
    -- 'Undefined'. A better approach might be to list exactly those
    -- primitives which should be compiled to 'Undefined'.
    primitives :: Set PrimitiveId
    primitives :: Set PrimitiveId
    primitives = [PrimitiveId] -> Set PrimitiveId
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [ PrimitiveId
    PrimShowInteger

      -- Natural number functions
      -- , PrimNatPlus                 -- missing
      , PrimitiveId
    PrimNatMinus
      -- , PrimNatTimes                -- missing
      -- , PrimNatDivSucAux            -- missing
      -- , PrimNatModSucAux            -- missing
      -- , PrimNatEquality             -- missing
      -- , PrimNatLess                 -- missing
      -- , PrimShowNat                 -- missing

      -- Machine words
      , PrimitiveId
    PrimWord64ToNat
      , PrimitiveId
    PrimWord64FromNat
      -- , PrimWord64ToNatInjective    -- missing

      -- Level functions
      -- , PrimLevelZero               -- missing
      -- , PrimLevelSuc                -- missing
      -- , PrimLevelMax                -- missing

      -- Floating point functions
      , PrimitiveId
    PrimFloatEquality
      , PrimitiveId
    PrimFloatInequality
      , PrimitiveId
    PrimFloatLess
      , PrimitiveId
    PrimFloatIsInfinite
      , PrimitiveId
    PrimFloatIsNaN
      , PrimitiveId
    PrimFloatIsNegativeZero
      , PrimitiveId
    PrimFloatIsSafeInteger
      , PrimitiveId
    PrimFloatToWord64
      -- , PrimFloatToWord64Injective  -- missing
      , PrimitiveId
    PrimNatToFloat
      , PrimitiveId
    PrimIntToFloat
      -- , PrimFloatRound              -- in Agda.Builtin.Float
      -- , PrimFloatFloor              -- in Agda.Builtin.Float
      -- , PrimFloatCeiling            -- in Agda.Builtin.Float
      -- , PrimFloatToRatio            -- in Agda.Builtin.Float
      , PrimitiveId
    PrimRatioToFloat
      -- , PrimFloatDecode             -- in Agda.Builtin.Float
      -- , PrimFloatEncode             -- in Agda.Builtin.Float
      , PrimitiveId
    PrimShowFloat
      , PrimitiveId
    PrimFloatPlus
      , PrimitiveId
    PrimFloatMinus
      , PrimitiveId
    PrimFloatTimes
      , PrimitiveId
    PrimFloatNegate
      , PrimitiveId
    PrimFloatDiv
      , PrimitiveId
    PrimFloatSqrt
      , PrimitiveId
    PrimFloatExp
      , PrimitiveId
    PrimFloatLog
      , PrimitiveId
    PrimFloatSin
      , PrimitiveId
    PrimFloatCos
      , PrimitiveId
    PrimFloatTan
      , PrimitiveId
    PrimFloatASin
      , PrimitiveId
    PrimFloatACos
      , PrimitiveId
    PrimFloatATan
      , PrimitiveId
    PrimFloatATan2
      , PrimitiveId
    PrimFloatSinh
      , PrimitiveId
    PrimFloatCosh
      , PrimitiveId
    PrimFloatTanh
      , PrimitiveId
    PrimFloatASinh
      , PrimitiveId
    PrimFloatACosh
      , PrimitiveId
    PrimFloatATanh
      , PrimitiveId
    PrimFloatPow

      -- Character functions
      -- , PrimCharEquality            -- missing
      -- , PrimIsLower                 -- missing
      -- , PrimIsDigit                 -- missing
      -- , PrimIsAlpha                 -- missing
      -- , PrimIsSpace                 -- missing
      -- , PrimIsAscii                 -- missing
      -- , PrimIsLatin1                -- missing
      -- , PrimIsPrint                 -- missing
      -- , PrimIsHexDigit              -- missing
      -- , PrimToUpper                 -- missing
      -- , PrimToLower                 -- missing
      -- , PrimCharToNat               -- missing
      -- , PrimCharToNatInjective      -- missing
      -- , PrimNatToChar               -- missing
      -- , PrimShowChar                -- in Agda.Builtin.String

      -- String functions
      -- , PrimStringToList            -- in Agda.Builtin.String
      -- , PrimStringToListInjective   -- missing
      -- , PrimStringFromList          -- in Agda.Builtin.String
      -- , PrimStringFromListInjective -- missing
      -- , PrimStringAppend            -- in Agda.Builtin.String
      -- , PrimStringEquality          -- in Agda.Builtin.String
      -- , PrimShowString              -- in Agda.Builtin.String
      -- , PrimStringUncons            -- in Agda.Builtin.String

      -- Other stuff
      -- , PrimEraseEquality           -- missing
      -- , PrimForce                   -- missing
      -- , PrimForceLemma              -- missing
      , PrimitiveId
    PrimQNameEquality
      , PrimitiveId
    PrimQNameLess
      , PrimitiveId
    PrimShowQName
      , PrimitiveId
    PrimQNameFixity
      -- , PrimQNameToWord64s          -- missing
      -- , PrimQNameToWord64sInjective -- missing
      , PrimitiveId
    PrimMetaEquality
      , PrimitiveId
    PrimMetaLess
      , PrimitiveId
    PrimShowMeta
      , PrimitiveId
    PrimMetaToNat
      -- , PrimMetaToNatInjective      -- missing
      , PrimitiveId
    builtinIMin
      , PrimitiveId
    builtinIMax
      , PrimitiveId
    builtinINeg
      , PrimitiveId
    PrimPartial
      , PrimitiveId
    PrimPartialP
      , PrimitiveId
    builtinPOr
      , PrimitiveId
    builtinComp
      , PrimitiveId
    builtinTrans
      , PrimitiveId
    builtinHComp
      , PrimitiveId
    builtinSubOut
      , PrimitiveId
    builtin_glueU
      , PrimitiveId
    builtin_unglueU
      , PrimitiveId
    builtinFaceForall
      -- , builtinGlue                   -- missing
      -- , builtin_glue                  -- missing
      -- , builtin_unglue                -- missing
      ]