    -- | 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.List     ( dropWhileEnd, findIndex, intercalate, partition )
    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 Paths_Agda

    import Agda.Interaction.Options

    import Agda.Syntax.Common
    import Agda.Syntax.Concrete.Name ( isNoName )
    import Agda.Syntax.Abstract.Name
      ( ModuleName, QName,
        mnameToList, qnameName, qnameModule, nameId )
    import Agda.Syntax.Internal
      ( Name, Type
      , nameFixity, unDom, telToList )
    import Agda.Syntax.Literal       ( Literal(..) )
    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.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 )
    import Agda.Utils.Null  ( null )
    import Agda.Utils.Pretty (prettyShow, render)
    import qualified Agda.Utils.Pretty as P
    import Agda.Utils.IO.Directory
    import Agda.Utils.IO.UTF8 ( writeFile )
    import Agda.Utils.Singleton ( singleton )

    import Agda.Compiler.Common
    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 )
    import Agda.Compiler.Treeless.Subst ()
    import Agda.Compiler.Backend (Backend(..), Backend'(..), 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 )
    import qualified Agda.Compiler.JS.Pretty as JSPretty

    import Agda.Utils.Impossible (__IMPOSSIBLE__)

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

    jsBackend :: Backend
    jsBackend :: Backend
    jsBackend = Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
    -> Backend
    forall opts env menv mod def.
    NFData opts =>
    Backend' opts env menv mod def -> Backend
    Backend Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
    jsBackend'

    jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
    jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
    jsBackend' = Backend' :: forall opts env menv mod def.
    String
    -> Maybe String
    -> opts
    -> [OptDescr (Flag opts)]
    -> (opts -> Bool)
    -> (opts -> TCM env)
    -> (env -> IsMain -> Map ModuleName mod -> TCMT IO ())
    -> (env
        -> IsMain
        -> ModuleName
        -> Maybe String
        -> TCM (Recompile menv mod))
    -> (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod)
    -> (env -> menv -> IsMain -> Definition -> TCM def)
    -> Bool
    -> (QName -> TCM Bool)
    -> Backend' opts env menv mod def
    Backend'
      { backendName :: String
    backendName           = String
    jsBackendName
      , backendVersion :: Maybe String
    backendVersion        = Maybe String
    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 -> TCM JSOptions
    preCompile            = JSOptions -> TCM JSOptions
    jsPreCompile
      , postCompile :: JSOptions -> IsMain -> Map ModuleName Module -> TCMT IO ()
    postCompile           = JSOptions -> IsMain -> Map ModuleName Module -> TCMT IO ()
    jsPostCompile
      , preModule :: JSOptions
    -> IsMain
    -> ModuleName
    -> Maybe String
    -> TCM (Recompile JSModuleEnv Module)
    preModule             = JSOptions
    -> IsMain
    -> ModuleName
    -> Maybe String
    -> TCM (Recompile JSModuleEnv Module)
    jsPreModule
      , postModule :: JSOptions
    -> JSModuleEnv
    -> IsMain
    -> ModuleName
    -> [Maybe Export]
    -> TCM Module
    postModule            = JSOptions
    -> JSModuleEnv
    -> IsMain
    -> ModuleName
    -> [Maybe Export]
    -> TCM Module
    jsPostModule
      , compileDef :: JSOptions
    -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
    compileDef            = JSOptions
    -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
    jsCompileDef
      , scopeCheckingSuffices :: Bool
    scopeCheckingSuffices = Bool
    False
      , mayEraseType :: QName -> TCM Bool
    mayEraseType          = TCM Bool -> QName -> TCM Bool
    forall a b. a -> b -> a
    const (TCM Bool -> QName -> TCM Bool) -> TCM Bool -> QName -> TCM Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> TCM Bool
    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.
      }

    --- 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.
      }
      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
    $cto :: forall x. Rep JSOptions x -> JSOptions
    $cfrom :: forall x. JSOptions -> Rep JSOptions x
    Generic

    instance NFData JSOptions

    defaultJSOptions :: JSOptions
    defaultJSOptions :: JSOptions
    defaultJSOptions = JSOptions :: Bool -> Bool -> Bool -> Bool -> JSOptions
    JSOptions
      { optJSCompile :: Bool
    optJSCompile  = Bool
    False
      , optJSOptimize :: Bool
    optJSOptimize = Bool
    False
      , optJSMinify :: Bool
    optJSMinify   = Bool
    False
      , optJSVerify :: Bool
    optJSVerify   = Bool
    False
      }

    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)"
        ]
      where
        enable :: JSOptions -> f JSOptions
    enable       JSOptions
    o = JSOptions -> f JSOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSCompile :: Bool
    optJSCompile  = Bool
    True }
        enableOpt :: JSOptions -> f JSOptions
    enableOpt    JSOptions
    o = JSOptions -> f JSOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSOptimize :: Bool
    optJSOptimize = Bool
    True }
        enableMin :: JSOptions -> f JSOptions
    enableMin    JSOptions
    o = JSOptions -> f JSOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSMinify :: Bool
    optJSMinify   = Bool
    True }
        enableVerify :: JSOptions -> f JSOptions
    enableVerify JSOptions
    o = JSOptions -> f JSOptions
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure JSOptions
    o{ optJSVerify :: Bool
    optJSVerify   = Bool
    True }

    --- Top-level compilation ---

    jsPreCompile :: JSOptions -> TCM JSOptions
    jsPreCompile :: JSOptions -> TCM JSOptions
    jsPreCompile JSOptions
    opts = do
      Maybe Cubical
    cubical <- PragmaOptions -> Maybe Cubical
    optCubical (PragmaOptions -> Maybe Cubical)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe Cubical)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      let notSupported :: String -> m a
    notSupported String
    s =
            TypeError -> m a
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m a) -> TypeError -> m a
    forall a b. (a -> b) -> a -> b
    $ String -> TypeError
    GenericError (String -> TypeError) -> String -> TypeError
    forall a b. (a -> b) -> a -> b
    $
              String
    "Compilation of code that uses " String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    s String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    " is not supported."
      case Maybe Cubical
    cubical of
        Maybe Cubical
    Nothing      -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Just Cubical
    CErased -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        Just Cubical
    CFull   -> String -> TCMT IO ()
    forall {m :: * -> *} {a}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    String -> m a
    notSupported String
    "--cubical"

      JSOptions -> TCM JSOptions
    forall (m :: * -> *) a. Monad m => a -> m a
    return JSOptions
    opts

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

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

      -- Copy RTE modules.

      String
    compDir  <- TCMT IO String
    forall (m :: * -> *). HasOptions m => m String
    compileDir
      IO () -> TCMT IO ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
        String
    dataDir <- IO String
    getDataDir
        let srcDir :: String
    srcDir = String
    dataDir String -> String -> String
    </> String
    "JS"
        String -> String -> IO ()
    copyDirContent String
    srcDir String
    compDir

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

      String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js.verify" Int
    10 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Considering to verify generated JS modules"
      Bool -> TCMT IO () -> TCMT IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (JSOptions -> Bool
    optJSVerify JSOptions
    opts) (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do

        String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js.verify" Int
    10 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String
    "Verifying generated JS modules"
        IO () -> TCMT IO ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> String -> IO ()
    setEnv String
    "NODE_PATH" String
    compDir

        Map ModuleName Module -> (Module -> TCMT IO ()) -> TCMT IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ Map ModuleName Module
    ms ((Module -> TCMT IO ()) -> TCMT IO ())
    -> (Module -> TCMT IO ()) -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ \ Module{ GlobalId
    modName :: GlobalId
    modName :: Module -> GlobalId
    modName, Maybe Exp
    callMain :: Maybe Exp
    callMain :: Module -> Maybe Exp
    callMain } -> do
          String
    jsFile <- GlobalId -> TCMT IO String
    outFile GlobalId
    modName
          String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js.verify" Int
    30 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [ String
    "Considering JS module:" , String
    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).
          Maybe Exp -> TCMT IO () -> TCMT IO ()
    forall m a. Monoid m => Maybe a -> m -> m
    whenNothing Maybe Exp
    callMain (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ do
            let cmd :: String
    cmd = [String] -> String
    unwords [ String
    "node", String
    "-", String
    "<", String
    jsFile ]
            String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js.verify" Int
    20 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [ String
    "calling:", String
    cmd ]
            IO () -> TCMT IO ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ String -> IO ()
    callCommand String
    cmd

    mergeModules :: Map.Map ModuleName Module -> [(GlobalId, Export)]
    mergeModules :: Map ModuleName Module -> [(GlobalId, Export)]
    mergeModules Map ModuleName Module
    ms
        = [ (ModuleName -> GlobalId
    jsMod ModuleName
    n, Export
    e)
          | (ModuleName
    n, Module GlobalId
    _ [GlobalId]
    _ [Export]
    es Maybe Exp
    _) <- Map ModuleName Module -> [(ModuleName, Module)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map ModuleName Module
    ms
          , Export
    e <- [Export]
    es
          ]

    --- Module compilation ---

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

    jsPreModule :: JSOptions -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module)
    jsPreModule :: JSOptions
    -> IsMain
    -> ModuleName
    -> Maybe String
    -> TCM (Recompile JSModuleEnv Module)
    jsPreModule JSOptions
    _opts IsMain
    _ ModuleName
    m Maybe String
    mifile = do
      Maybe Cubical
    cubical <- PragmaOptions -> Maybe Cubical
    optCubical (PragmaOptions -> Maybe Cubical)
    -> TCMT IO PragmaOptions -> TCMT IO (Maybe Cubical)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO PragmaOptions
    forall (m :: * -> *). HasOptions m => m PragmaOptions
    pragmaOptions
      let compile :: Bool
    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
      TCM Bool
    -> TCM (Recompile JSModuleEnv Module)
    -> TCM (Recompile JSModuleEnv Module)
    -> TCM (Recompile JSModuleEnv Module)
    forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
    ifM TCM Bool
    uptodate TCM (Recompile JSModuleEnv Module)
    noComp (Bool -> TCM (Recompile JSModuleEnv Module)
    yesComp Bool
    compile)
      where
        uptodate :: TCM Bool
    uptodate = case Maybe String
    mifile of
          Maybe String
    Nothing -> Bool -> TCM Bool
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Bool
    False
          Just String
    ifile -> IO Bool -> TCM Bool
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (IO Bool -> TCM Bool) -> TCMT IO (IO Bool) -> TCM 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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> String -> TCMT IO String
    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 :: TCM (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 ())
    -> (ModuleName -> String) -> ModuleName -> 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)
    -> (ModuleName -> String) -> ModuleName -> String
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ModuleName -> String
    forall a. Pretty a => a -> String
    prettyShow (ModuleName -> TCMT IO ()) -> TCMT IO ModuleName -> TCMT IO ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
          Recompile JSModuleEnv Module -> TCM (Recompile JSModuleEnv Module)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Recompile JSModuleEnv Module
     -> TCM (Recompile JSModuleEnv Module))
    -> Recompile JSModuleEnv Module
    -> TCM (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 (ModuleName -> GlobalId
    jsMod ModuleName
    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 -> TCM (Recompile JSModuleEnv Module)
    yesComp Bool
    compile = do
          String
    m   <- ModuleName -> String
    forall a. Pretty a => a -> String
    prettyShow (ModuleName -> String) -> TCMT IO ModuleName -> TCMT IO String
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
          String
    out <- TCMT IO String
    outFile_
          String -> Int -> String -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> String -> m ()
    reportSLn String
    "compile.js" Int
    1 (String -> TCMT IO ()) -> String -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [String] -> String -> String
    repl [String
    m, String
    ifileDesc, String
    out] String
    "Compiling <<0>> in <<1>> to <<2>>"
          Maybe CoinductionKit
    kit <- TCM (Maybe CoinductionKit)
    coinductionKit
          Recompile JSModuleEnv Module -> TCM (Recompile JSModuleEnv Module)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Recompile JSModuleEnv Module
     -> TCM (Recompile JSModuleEnv Module))
    -> Recompile JSModuleEnv Module
    -> TCM (Recompile JSModuleEnv Module)
    forall a b. (a -> b) -> a -> b
    $ JSModuleEnv -> Recompile JSModuleEnv Module
    forall menv mod. menv -> Recompile menv mod
    Recompile (JSModuleEnv -> Recompile JSModuleEnv Module)
    -> JSModuleEnv -> Recompile JSModuleEnv Module
    forall a b. (a -> b) -> a -> b
    $ JSModuleEnv :: Maybe CoinductionKit -> Bool -> JSModuleEnv
    JSModuleEnv
            { jsCoinductionKit :: Maybe CoinductionKit
    jsCoinductionKit = Maybe CoinductionKit
    kit
            , jsCompile :: Bool
    jsCompile        = Bool
    compile
            }

    jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM Module
    jsPostModule :: JSOptions
    -> JSModuleEnv
    -> IsMain
    -> ModuleName
    -> [Maybe Export]
    -> TCM Module
    jsPostModule JSOptions
    opts JSModuleEnv
    _ IsMain
    isMain ModuleName
    _ [Maybe Export]
    defs = do
      GlobalId
    m             <- ModuleName -> GlobalId
    jsMod (ModuleName -> GlobalId) -> TCMT IO ModuleName -> TCMT IO GlobalId
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
      [GlobalId]
    is            <- ((ModuleName, Word64) -> GlobalId)
    -> [(ModuleName, Word64)] -> [GlobalId]
    forall a b. (a -> b) -> [a] -> [b]
    map (ModuleName -> GlobalId
    jsMod (ModuleName -> GlobalId)
    -> ((ModuleName, Word64) -> ModuleName)
    -> (ModuleName, Word64)
    -> GlobalId
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (ModuleName, Word64) -> ModuleName
    forall a b. (a, b) -> a
    fst) ([(ModuleName, Word64)] -> [GlobalId])
    -> (Interface -> [(ModuleName, Word64)]) -> Interface -> [GlobalId]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Interface -> [(ModuleName, Word64)]
    iImportedModules (Interface -> [GlobalId])
    -> TCMT IO Interface -> TCMT IO [GlobalId]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      let mod :: Module
    mod = GlobalId -> [GlobalId] -> [Export] -> Maybe Exp -> Module
    Module GlobalId
    m [GlobalId]
    is ([Export] -> [Export]
    reorder [Export]
    es) Maybe Exp
    callMain
      Bool -> Module -> TCMT IO ()
    writeModule (JSOptions -> Bool
    optJSMinify JSOptions
    opts) Module
    mod
      Module -> TCM Module
    forall (m :: * -> *) a. Monad m => a -> m a
    return Module
    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 -> TCM (Maybe Export)
    jsCompileDef JSOptions
    opts JSModuleEnv
    kit IsMain
    _isMain Definition
    def = EnvWithOpts -> (QName, Definition) -> TCM (Maybe Export)
    definition (JSOptions
    opts, JSModuleEnv
    kit) (Definition -> QName
    defName Definition
    def, Definition
    def)

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

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

    jsMod :: ModuleName -> GlobalId
    jsMod :: ModuleName -> GlobalId
    jsMod ModuleName
    m = [String] -> GlobalId
    GlobalId (String
    prefix String -> [String] -> [String]
    forall a. a -> [a] -> [a]
    : (Name -> String) -> [Name] -> [String]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> String
    forall a. Pretty a => a -> String
    prettyShow (ModuleName -> [Name]
    mnameToList ModuleName
    m))

    jsFileName :: GlobalId -> String
    jsFileName :: GlobalId -> String
    jsFileName (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
      ModuleName
    i <- Interface -> ModuleName
    iModuleName (Interface -> ModuleName)
    -> TCMT IO Interface -> TCMT IO ModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO Interface
    forall (m :: * -> *). ReadTCState m => m Interface
    curIF
      ModuleName
    modNm <- ModuleName -> TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => ModuleName -> m ModuleName
    topLevelModuleName (QName -> ModuleName
    qnameModule QName
    q)
      let
        -- Global module prefix
        qms :: [Name]
    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 :: [Name]
    localms = Int -> [Name] -> [Name]
    forall a. Int -> [a] -> [a]
    drop ([Name] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([Name] -> Int) -> [Name] -> Int
    forall a b. (a -> b) -> a -> b
    $ ModuleName -> [Name]
    mnameToList ModuleName
    modNm) [Name]
    qms
        nm :: JSQName
    nm = (Name -> MemberId) -> NonEmpty Name -> JSQName
    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 ModuleName
    modNm ModuleName -> ModuleName -> Bool
    forall a. Eq a => a -> a -> Bool
    == ModuleName
    i
        then (Exp, JSQName) -> TCM (Exp, JSQName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp
    Self, JSQName
    nm)
        else (Exp, JSQName) -> TCM (Exp, JSQName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (GlobalId -> Exp
    Global (ModuleName -> GlobalId
    jsMod ModuleName
    modNm), JSQName
    nm)

    global :: QName -> TCM (Exp, JSQName)
    global :: QName -> TCM (Exp, JSQName)
    global QName
    q = do
      Definition
    d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
      case Definition
    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 (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
              (Exp
    m,JSQName
    ls) <- QName -> TCM (Exp, JSQName)
    global' QName
    p
              (Exp, JSQName) -> TCM (Exp, JSQName)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp
    m, JSQName
    ls JSQName -> JSQName -> JSQName
    forall a. Semigroup a => a -> a -> a
    <> MemberId -> JSQName
    forall el coll. Singleton el coll => el -> coll
    singleton (String -> MemberId
    MemberId String
    "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) -> TCM (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
    prettyTCM QName
    q
      (Exp
    _,JSQName
    ls) <- QName -> TCM (Exp, JSQName)
    global QName
    q
      Definition
    d <- Definition -> TCMT IO Definition
    forall a (m :: * -> *).
    (InstantiateFull a, MonadReduce m) =>
    a -> m a
    instantiateFull Definition
    d

      EnvWithOpts
    -> QName -> Definition -> Type -> JSQName -> TCM (Maybe Export)
    definition' EnvWithOpts
    kit QName
    q Definition
    d (Definition -> Type
    defType Definition
    d) JSQName
    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 (String -> QName -> TCMT IO (Maybe CompilerPragma)
    getUniqueCompilerPragma String
    jsBackendName QName
    q) (() -> TCMT IO ()
    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) ->
      Range -> TCMT IO () -> TCMT IO ()
    forall (m :: * -> *) x a.
    (MonadTrace m, HasRange x) =>
    x -> m a -> m a
    setCurrentRange Range
    r (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ case String -> [String]
    words String
    s of
        String
    "=" : [String]
    _ -> () -> TCMT IO ()
    forall (m :: * -> *) a. Monad m => a -> m a
    return ()
        [String]
    _       -> Doc -> TCMT IO ()
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    forall (t :: * -> *). Foldable t => t Doc -> Doc
    P.sep [ Doc
    "Badly formed COMPILE JS pragma. Expected",
                                             Doc
    "{-# COMPILE JS <name> = <js> #-}" ]

    defJSDef :: Definition -> Maybe String
    defJSDef :: Definition -> Maybe String
    defJSDef Definition
    def =
      case String -> Definition -> [CompilerPragma]
    defCompilerPragmas String
    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 -> TCM (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 -> TCM (Maybe Export)
    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 -> TCM (Maybe Export)
    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 -> TCM (Maybe Export)
    ret (Exp -> TCM (Maybe Export)) -> Exp -> TCM (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{} -> TCM (Maybe Export)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

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

        GeneralizableVar{} -> Maybe Export -> TCM (Maybe Export)
    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 -> TCM (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
    prettyTCM QName
    q
          TCMT IO (Maybe TTerm)
    -> TCM (Maybe Export)
    -> (TTerm -> TCM (Maybe Export))
    -> TCM (Maybe Export)
    forall (m :: * -> *) a b.
    Monad m =>
    m (Maybe a) -> m b -> (a -> m b) -> m b
    caseMaybeM (EvaluationStrategy -> QName -> TCMT IO (Maybe TTerm)
    toTreeless EvaluationStrategy
    T.EagerEvaluation QName
    q) (Maybe Export -> TCM (Maybe Export)
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Maybe Export
    forall a. Maybe a
    Nothing) ((TTerm -> TCM (Maybe Export)) -> TCM (Maybe Export))
    -> (TTerm -> TCM (Maybe Export)) -> TCM (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ \ TTerm
    treeless -> do
            [ArgUsage]
    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
            TTerm
    funBody <- TTerm -> TCM TTerm
    eliminateCaseDefaults (TTerm -> TCM TTerm) -> TCM TTerm -> TCM TTerm
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<<
              TTerm -> TCM TTerm
    eliminateLiteralPatterns
              (TTerm -> TTerm
    convertGuards TTerm
    treeless)
            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.js" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    " compiled treeless fun:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> TTerm -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    pretty TTerm
    funBody
            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.js" Int
    40 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    " argument usage:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc)
    -> ([ArgUsage] -> String) -> [ArgUsage] -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [ArgUsage] -> String
    forall a. Show a => a -> String
    show) [ArgUsage]
    used

            let (TTerm
    body, Int
    given) = TTerm -> (TTerm, Int)
    lamView TTerm
    funBody
                  where
                    lamView :: T.TTerm -> (T.TTerm, Int)
                    lamView :: TTerm -> (TTerm, Int)
    lamView (T.TLam TTerm
    t) = (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    1) (Int -> Int) -> (TTerm, Int) -> (TTerm, Int)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TTerm -> (TTerm, Int)
    lamView TTerm
    t
                    lamView TTerm
    t = (TTerm
    t, Int
    0)

                -- number of eta expanded args
                etaN :: Int
    etaN = [ArgUsage] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([ArgUsage] -> Int) -> [ArgUsage] -> Int
    forall a b. (a -> b) -> a -> b
    $ (ArgUsage -> Bool) -> [ArgUsage] -> [ArgUsage]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhileEnd (ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUsed) ([ArgUsage] -> [ArgUsage]) -> [ArgUsage] -> [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ Int -> [ArgUsage] -> [ArgUsage]
    forall a. Int -> [a] -> [a]
    drop Int
    given [ArgUsage]
    used

                unusedN :: Int
    unusedN = [ArgUsage] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([ArgUsage] -> Int) -> [ArgUsage] -> Int
    forall a b. (a -> b) -> a -> b
    $ (ArgUsage -> Bool) -> [ArgUsage] -> [ArgUsage]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUnused) [ArgUsage]
    used

            Exp
    funBody' <- EnvWithOpts -> TTerm -> TCM Exp
    compileTerm EnvWithOpts
    kit
                      (TTerm -> TCM Exp) -> TTerm -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ Int -> (TTerm -> TTerm) -> TTerm -> TTerm
    forall i a. Integral i => i -> (a -> a) -> a -> a
    iterate' (Int
    given Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    etaN Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    unusedN) TTerm -> TTerm
    T.TLam
                      (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ [Bool] -> TTerm -> TTerm
    eraseLocalVars ((ArgUsage -> Bool) -> [ArgUsage] -> [Bool]
    forall a b. (a -> b) -> [a] -> [b]
    map (ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUnused) [ArgUsage]
    used)
                      (TTerm -> TTerm) -> TTerm -> TTerm
    forall a b. (a -> b) -> a -> b
    $ TTerm -> Args -> TTerm
    T.mkTApp (Int -> TTerm -> TTerm
    forall a. Subst a => Int -> a -> a
    raise Int
    etaN TTerm
    body) (Int -> TTerm
    T.TVar (Int -> TTerm) -> [Int] -> Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    etaN)

            String -> Int -> TCMT IO Doc -> TCMT IO ()
    forall (m :: * -> *).
    MonadDebug m =>
    String -> Int -> TCMT IO Doc -> m ()
    reportSDoc String
    "compile.js" Int
    30 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    " compiled JS fun:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> (String -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => String -> m Doc
    text (String -> TCMT IO Doc) -> (Exp -> String) -> Exp -> TCMT IO Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Exp -> String
    forall a. Show a => a -> String
    show) Exp
    funBody'
            Maybe Export -> TCM (Maybe Export)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Export -> TCM (Maybe Export))
    -> Maybe Export -> TCM (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $
              if Exp
    funBody' Exp -> Exp -> Bool
    forall a. Eq a => a -> a -> Bool
    == Exp
    Null then Maybe Export
    forall a. Maybe a
    Nothing
              else Export -> Maybe Export
    forall a. a -> Maybe a
    Just (Export -> Maybe Export) -> Export -> Maybe Export
    forall a b. (a -> b) -> a -> b
    $ JSQName -> Exp -> Export
    Export JSQName
    ls Exp
    funBody'

        Primitive{primName :: Defn -> String
    primName = String
    p}
          | String
    p String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    builtin_glueU ->
            -- The string prim^glueU is not a valid JS name.
            String -> TCM (Maybe Export)
    plainJS String
    "agdaRTS.prim_glueU"
          | String
    p String -> String -> Bool
    forall a. Eq a => a -> a -> Bool
    == String
    builtin_unglueU ->
            -- The string prim^unglueU is not a valid JS name.
            String -> TCM (Maybe Export)
    plainJS String
    "agdaRTS.prim_unglueU"
          | String
    p String -> Set String -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `Set.member` Set String
    primitives ->
            String -> TCM (Maybe Export)
    plainJS (String -> TCM (Maybe Export)) -> String -> TCM (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ String
    "agdaRTS." String -> String -> String
    forall a. [a] -> [a] -> [a]
    ++ String
    p
          | Just String
    e <- Definition -> Maybe String
    defJSDef Definition
    d ->
            String -> TCM (Maybe Export)
    plainJS String
    e
          | Bool
    otherwise ->
            Exp -> TCM (Maybe Export)
    ret Exp
    Undefined
        PrimitiveSort{} -> Maybe Export -> TCM (Maybe Export)
    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 -> TCM (Maybe Export)
    ret Exp
    emp
        Record{} -> do
            QName -> TCMT IO ()
    computeErasedConstructorArgs QName
    q
            Maybe Export -> TCM (Maybe Export)
    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 -> TCM (Maybe Export)
    plainJS String
    e
        Constructor{conData :: Defn -> QName
    conData = QName
    p, conPars :: Defn -> Int
    conPars = Int
    nc} -> do
          TelV Tele (Dom Type)
    tel Type
    _ <- Type -> TCMT IO (TelV Type)
    forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
    telViewPath Type
    t
          let np :: Int
    np = [Dom (String, Type)] -> 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
          [Bool]
    erased <- QName -> TCMT IO [Bool]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    q
          let nargs :: Int
    nargs = Int
    np Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Bool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ((Bool -> Bool) -> [Bool] -> [Bool]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Bool -> Bool
    forall a. a -> a
    id [Bool]
    erased)
              args :: [Exp]
    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] ]
          Definition
    d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    p
          let l :: MemberId
    l = JSQName -> MemberId
    forall a. NonEmpty a -> a
    List1.last JSQName
    ls
          case Definition -> Defn
    theDef Definition
    d of
            Record { recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    flds } -> Exp -> TCM (Maybe Export)
    ret (Exp -> TCM (Maybe Export)) -> Exp -> TCM (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ Int -> Exp -> Exp
    curriedLambda Int
    nargs (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $
              if JSOptions -> Bool
    optJSOptimize (EnvWithOpts -> JSOptions
    forall a b. (a, b) -> a
    fst EnvWithOpts
    kit)
                then Int -> Exp -> Exp
    Lambda Int
    1 (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    Apply (LocalId -> Exp
    Local (Int -> LocalId
    LocalId Int
    0)) [Exp]
    args
                else Map MemberId Exp -> Exp
    Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ MemberId -> Exp -> Map MemberId Exp
    forall k a. k -> a -> Map k a
    Map.singleton MemberId
    l (Exp -> Map MemberId Exp) -> Exp -> Map MemberId Exp
    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 (LocalId -> Exp
    Local (Int -> LocalId
    LocalId Int
    0)) MemberId
    l) [Exp]
    args
            Defn
    dt -> do
              MemberId
    i <- TCM MemberId
    index
              Exp -> TCM (Maybe Export)
    ret (Exp -> TCM (Maybe Export)) -> Exp -> TCM (Maybe Export)
    forall a b. (a -> b) -> a -> b
    $ Int -> Exp -> Exp
    curriedLambda (Int
    nargs Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1) (Exp -> Exp) -> Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp] -> Exp
    Apply (Exp -> MemberId -> Exp
    Lookup (LocalId -> Exp
    Local (Int -> LocalId
    LocalId Int
    0)) MemberId
    i) [Exp]
    args
              where
                index :: TCM MemberId
                index :: TCM MemberId
    index
                  | Datatype{} <- Defn
    dt
                  , JSOptions -> Bool
    optJSOptimize (EnvWithOpts -> JSOptions
    forall a b. (a, b) -> a
    fst EnvWithOpts
    kit) = do
                      QName
    q  <- QName -> TCMT IO QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName QName
    q
                      [QName]
    cs <- (QName -> TCMT IO QName) -> [QName] -> TCMT IO [QName]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM QName -> TCMT IO QName
    forall (m :: * -> *). HasConstInfo m => QName -> m QName
    canonicalName ([QName] -> TCMT IO [QName]) -> [QName] -> TCMT IO [QName]
    forall a b. (a -> b) -> a -> b
    $ Defn -> [QName]
    defConstructors Defn
    dt
                      case (QName -> Bool) -> [QName] -> Maybe Int
    forall a. (a -> Bool) -> [a] -> Maybe Int
    findIndex (QName
    q QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    ==) [QName]
    cs of
                        Just Int
    i  -> MemberId -> TCM MemberId
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MemberId -> TCM MemberId) -> MemberId -> TCM MemberId
    forall a b. (a -> b) -> a -> b
    $ Int -> Comment -> MemberId
    MemberIndex Int
    i (MemberId -> Comment
    mkComment MemberId
    l)
                        Maybe Int
    Nothing -> String -> TCM MemberId
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ (String -> TCM MemberId) -> String -> TCM MemberId
    forall a b. (a -> b) -> a -> b
    $ [String] -> String
    unwords [ String
    "Constructor", QName -> String
    forall a. Pretty a => a -> String
    prettyShow QName
    q, String
    "not found in", [QName] -> String
    forall a. Pretty a => a -> String
    prettyShow [QName]
    cs ]
                  | Bool
    otherwise = MemberId -> TCM MemberId
    forall (m :: * -> *) a. Monad m => a -> m a
    return MemberId
    l
                mkComment :: MemberId -> Comment
    mkComment (MemberId String
    s) = String -> Comment
    Comment String
    s
                mkComment MemberId
    _ = Comment
    forall a. Monoid a => a
    mempty

        AbstractDefn{} -> TCM (Maybe Export)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      where
        ret :: Exp -> TCM (Maybe Export)
    ret = Maybe Export -> TCM (Maybe Export)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Export -> TCM (Maybe Export))
    -> (Exp -> Maybe Export) -> Exp -> TCM (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 -> TCM (Maybe Export)
    plainJS = Maybe Export -> TCM (Maybe Export)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe Export -> TCM (Maybe Export))
    -> (String -> Maybe Export) -> String -> TCM (Maybe Export)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Export -> Maybe Export
    forall a. a -> Maybe a
    Just (Export -> Maybe Export)
    -> (String -> Export) -> String -> Maybe Export
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . JSQName -> Exp -> Export
    Export JSQName
    ls (Exp -> Export) -> (String -> Exp) -> String -> Export
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Exp
    PlainJS

    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 (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
            Definition
    d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
            case Definition -> Defn
    theDef Definition
    d of
              -- Datatypes and records are erased
              Datatype {} -> Exp -> TCM Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Text -> Exp
    String Text
    "*")
              Record {} -> Exp -> TCM Exp
    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
            Exp
    x <- TTerm -> TCM Exp
    go TTerm
    x
            let evalThunk :: String
    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
    "}"
                  ]
            Exp -> TCM Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Exp -> TCM Exp) -> Exp -> TCM Exp
    forall a b. (a -> b) -> a -> b
    $ 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
    flatName, String -> Exp
    PlainJS String
    evalThunk)
              ,(String -> MemberId
    MemberId String
    "__flat_helper", Int -> Exp -> Exp
    Lambda Int
    0 Exp
    x)]
          T.TApp TTerm
    t' Args
    xs | Just Either QName QName
    f <- TTerm -> Maybe (Either QName QName)
    getDef TTerm
    t' -> do
            [ArgUsage]
    used <- case Either QName QName
    f of
              Left  QName
    q -> [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
              Right QName
    c -> (Bool -> ArgUsage) -> [Bool] -> [ArgUsage]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Bool
    b -> if Bool
    b then ArgUsage
    ArgUnused else ArgUsage
    ArgUsed) ([Bool] -> [ArgUsage]) -> TCMT IO [Bool] -> TCMT IO [ArgUsage]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> TCMT IO [Bool]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    c
                -- Andreas, 2021-02-10 NB: could be @map (bool ArgUsed ArgUnused)@
                -- but I find it unintuitive that 'bool' takes the 'False'-branch first.
            let given :: Int
    given = Args -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length Args
    xs

                -- number of eta expanded args
                etaN :: Int
    etaN = [ArgUsage] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([ArgUsage] -> Int) -> [ArgUsage] -> Int
    forall a b. (a -> b) -> a -> b
    $ (ArgUsage -> Bool) -> [ArgUsage] -> [ArgUsage]
    forall a. (a -> Bool) -> [a] -> [a]
    dropWhile (ArgUsage -> ArgUsage -> Bool
    forall a. Eq a => a -> a -> Bool
    == ArgUsage
    ArgUsed) ([ArgUsage] -> [ArgUsage]) -> [ArgUsage] -> [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ [ArgUsage] -> [ArgUsage]
    forall a. [a] -> [a]
    reverse ([ArgUsage] -> [ArgUsage]) -> [ArgUsage] -> [ArgUsage]
    forall a b. (a -> b) -> a -> b
    $ Int -> [ArgUsage] -> [ArgUsage]
    forall a. Int -> [a] -> [a]
    drop Int
    given [ArgUsage]
    used

                args :: Args
    args = [ArgUsage] -> Args -> Args
    forall a. [ArgUsage] -> [a] -> [a]
    filterUsed [ArgUsage]
    used (Args -> Args) -> Args -> Args
    forall a b. (a -> b) -> a -> b
    $
                         Int -> Args -> Args
    forall a. Subst a => Int -> a -> a
    raise Int
    etaN Args
    xs Args -> Args -> Args
    forall a. [a] -> [a] -> [a]
    ++ (Int -> TTerm
    T.TVar (Int -> TTerm) -> [Int] -> Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom Int
    etaN)

            Int -> Exp -> Exp
    curriedLambda Int
    etaN (Exp -> Exp) -> TCM Exp -> TCM Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (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 (Int -> TTerm -> TTerm
    forall a. Subst a => Int -> a -> a
    raise Int
    etaN TTerm
    t') TCMT IO ([Exp] -> Exp) -> TCMT IO [Exp] -> TCM Exp
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM Exp) -> Args -> TCMT IO [Exp]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TTerm -> TCM Exp
    go Args
    args)

          T.TApp TTerm
    t Args
    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 (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM Exp) -> Args -> TCMT IO [Exp]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    mapM TTerm -> TCM Exp
    go Args
    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
          -- TODO This is not a lazy let, but it should be...
          T.TLet TTerm
    t TTerm
    e -> Exp -> [Exp] -> Exp
    apply (Exp -> [Exp] -> Exp) -> TCM Exp -> TCMT IO ([Exp] -> Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (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
    e) TCMT IO ([Exp] -> Exp) -> TCMT IO [Exp] -> TCM Exp
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> (TTerm -> TCM Exp) -> Args -> TCMT IO [Exp]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse TTerm -> TCM Exp
    go [TTerm
    t]
          T.TLit Literal
    l -> Exp -> TCM Exp
    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
          T.TCon QName
    q -> do
            Definition
    d <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    q
            QName -> TCM Exp
    qname QName
    q
          T.TCase Int
    sc CaseInfo
    ct TTerm
    def [TAlt]
    alts | T.CTData Quantity
    _ QName
    dt <- CaseInfo -> CaseType
    T.caseType CaseInfo
    ct -> do
            Definition
    dt <- QName -> TCMT IO Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    dt
            [((QName, MemberId), Exp)]
    alts' <- (TAlt -> TCMT IO ((QName, MemberId), Exp))
    -> [TAlt] -> TCMT IO [((QName, MemberId), Exp)]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    traverse (EnvWithOpts -> TAlt -> TCMT IO ((QName, MemberId), Exp)
    compileAlt EnvWithOpts
    kit) [TAlt]
    alts
            let cs :: [QName]
    cs  = Defn -> [QName]
    defConstructors (Defn -> [QName]) -> Defn -> [QName]
    forall a b. (a -> b) -> a -> b
    $ Definition -> Defn
    theDef Definition
    dt
                obj :: Exp
    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__ [((QName, MemberId) -> MemberId
    forall a b. (a, b) -> b
    snd (QName, MemberId)
    x, Exp
    y) | ((QName, MemberId)
    x, Exp
    y) <- [((QName, MemberId), Exp)]
    alts']
                arr :: Exp
    arr = [(Comment, Exp)] -> Exp
    mkArray [(Comment, Exp) -> [(Comment, Exp)] -> (Comment, Exp)
    forall a. a -> [a] -> a
    headWithDefault (Comment
    forall a. Monoid a => a
    mempty, Exp
    Null) [(String -> Comment
    Comment String
    s, Exp
    y) | ((QName
    c', MemberId String
    s), Exp
    y) <- [((QName, MemberId), Exp)]
    alts', QName
    c' QName -> QName -> Bool
    forall a. Eq a => a -> a -> Bool
    == QName
    c] | QName
    c <- [QName]
    cs]
            case (Definition -> Defn
    theDef Definition
    dt, Definition -> Maybe String
    defJSDef Definition
    dt) of
              (Defn
    _, Just String
    e) -> do
                Exp -> TCM Exp
    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
    _) | JSOptions -> Bool
    optJSOptimize (EnvWithOpts -> JSOptions
    forall a b. (a, b) -> a
    fst EnvWithOpts
    kit) -> do
                Exp -> TCM Exp
    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 (LocalId -> Exp
    Local (LocalId -> Exp) -> LocalId -> Exp
    forall a b. (a -> b) -> a -> b
    $ Int -> LocalId
    LocalId Int
    sc) [((QName, MemberId), Exp) -> Exp
    forall a b. (a, b) -> b
    snd (((QName, MemberId), Exp) -> Exp)
    -> ((QName, MemberId), Exp) -> Exp
    forall a b. (a -> b) -> a -> b
    $ ((QName, MemberId), Exp)
    -> [((QName, MemberId), Exp)] -> ((QName, MemberId), Exp)
    forall a. a -> [a] -> a
    headWithDefault ((QName, MemberId), Exp)
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [((QName, MemberId), Exp)]
    alts']
              (Record{}, Maybe String
    _) -> do
                MemberId
    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
                Exp -> TCM Exp
    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 (Exp -> MemberId -> Exp
    Lookup (LocalId -> Exp
    Local (LocalId -> Exp) -> LocalId -> Exp
    forall a b. (a -> b) -> a -> b
    $ Int -> LocalId
    LocalId Int
    sc) MemberId
    memId) [Exp
    obj]
              (Datatype{}, Maybe String
    _) | JSOptions -> Bool
    optJSOptimize (EnvWithOpts -> JSOptions
    forall a b. (a, b) -> a
    fst EnvWithOpts
    kit) -> do
                Exp -> TCM Exp
    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
    arr]
              (Datatype{}, Maybe String
    _) -> do
                Exp -> TCM Exp
    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 (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 (m :: * -> *) a. Monad m => a -> m a
    return Exp
    Undefined
          T.TError T.TMeta{}      -> Exp -> TCM Exp
    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 (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 (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 (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)

    compileAlt :: EnvWithOpts -> T.TAlt -> TCM ((QName, MemberId), Exp)
    compileAlt :: EnvWithOpts -> TAlt -> TCMT IO ((QName, MemberId), Exp)
    compileAlt EnvWithOpts
    kit = \case
      T.TACon QName
    con Int
    ar TTerm
    body -> do
        [Bool]
    erased <- QName -> TCMT IO [Bool]
    forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
    getErasedConArgs QName
    con
        let nargs :: Int
    nargs = Int
    ar Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - [Bool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ((Bool -> Bool) -> [Bool] -> [Bool]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Bool -> Bool
    forall a. a -> a
    id [Bool]
    erased)
        MemberId
    memId <- QName -> TCM MemberId
    visitorName QName
    con
        Exp
    body <- Int -> Exp -> Exp
    Lambda Int
    nargs (Exp -> Exp) -> TCM Exp -> TCM Exp
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> EnvWithOpts -> TTerm -> TCM Exp
    compileTerm EnvWithOpts
    kit ([Bool] -> TTerm -> TTerm
    eraseLocalVars [Bool]
    erased TTerm
    body)
        ((QName, MemberId), Exp) -> TCMT IO ((QName, MemberId), Exp)
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((QName
    con, MemberId
    memId), Exp
    body)
      TAlt
    _ -> TCMT IO ((QName, MemberId), Exp)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    eraseLocalVars :: [Bool] -> T.TTerm -> T.TTerm
    eraseLocalVars :: [Bool] -> TTerm -> TTerm
    eraseLocalVars [] TTerm
    x = TTerm
    x
    eraseLocalVars (Bool
    False: [Bool]
    es) TTerm
    x = [Bool] -> TTerm -> TTerm
    eraseLocalVars [Bool]
    es TTerm
    x
    eraseLocalVars (Bool
    True: [Bool]
    es) TTerm
    x = [Bool] -> TTerm -> TTerm
    eraseLocalVars [Bool]
    es (Int -> SubstArg TTerm -> TTerm -> TTerm
    forall a. Subst a => Int -> SubstArg a -> a -> a
    TC.subst ([Bool] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Bool]
    es) TTerm
    SubstArg TTerm
    T.TErased TTerm
    x)

    visitorName :: QName -> TCM MemberId
    visitorName :: QName -> TCM MemberId
    visitorName QName
    q = do (Exp
    m,JSQName
    ls) <- QName -> TCM (Exp, JSQName)
    global QName
    q; MemberId -> TCM MemberId
    forall (m :: * -> *) a. Monad m => a -> m a
    return (JSQName -> MemberId
    forall a. NonEmpty a -> a
    List1.last JSQName
    ls)

    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
      (Exp
    e,JSQName
    ls) <- QName -> TCM (Exp, JSQName)
    global QName
    q
      Exp -> TCM Exp
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Exp -> MemberId -> Exp) -> Exp -> JSQName -> Exp
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Exp -> MemberId -> Exp
    Lookup Exp
    e JSQName
    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{}     -> Exp
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    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

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

    writeModule :: Bool -> Module -> TCM ()
    writeModule :: Bool -> Module -> TCMT IO ()
    writeModule Bool
    minify Module
    m = do
      String
    out <- GlobalId -> TCMT IO String
    outFile (Module -> GlobalId
    modName Module
    m)
      IO () -> TCMT IO ()
    forall (m :: * -> *) a. MonadIO m => IO a -> m a
    liftIO (String -> String -> IO ()
    writeFile String
    out (Bool -> Module -> String
    forall a. Pretty a => Bool -> a -> String
    JSPretty.prettyShow Bool
    minify Module
    m))

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

    outFile_ :: TCM FilePath
    outFile_ :: TCMT IO String
    outFile_ = do
      ModuleName
    m <- TCMT IO ModuleName
    forall (m :: * -> *). ReadTCState m => m ModuleName
    curMName
      GlobalId -> TCMT IO String
    outFile (ModuleName -> GlobalId
    jsMod ModuleName
    m)

    -- | 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 String
    primitives :: Set String
    primitives = [String] -> Set String
    forall a. Ord a => [a] -> Set a
    Set.fromList
      [  String
    "primShowInteger"

      -- Natural number functions
      -- , "primNatPlus"                 -- missing
      , String
    "primNatMinus"
      -- , "primNatTimes"                -- missing
      -- , "primNatDivSucAux"            -- missing
      -- , "primNatModSucAux"            -- missing
      -- , "primNatEquality"             -- missing
      -- , "primNatLess"                 -- missing
      -- , "primShowNat"                 -- missing

      -- Machine words
      , String
    "primWord64ToNat"
      , String
    "primWord64FromNat"
      -- , "primWord64ToNatInjective"    -- missing

      -- Level functions
      -- , "primLevelZero"               -- missing
      -- , "primLevelSuc"                -- missing
      -- , "primLevelMax"                -- missing

      -- Sorts
      -- , "primSetOmega"                -- missing
      -- , "primStrictSetOmega"          -- missing

      -- Floating point functions
      , String
    "primFloatEquality"
      , String
    "primFloatInequality"
      , String
    "primFloatLess"
      , String
    "primFloatIsInfinite"
      , String
    "primFloatIsNaN"
      , String
    "primFloatIsNegativeZero"
      , String
    "primFloatIsSafeInteger"
      , String
    "primFloatToWord64"
      -- , "primFloatToWord64Injective"  -- missing
      , String
    "primNatToFloat"
      , String
    "primIntToFloat"
      -- , "primFloatRound"              -- in Agda.Builtin.Float
      -- , "primFloatFloor"              -- in Agda.Builtin.Float
      -- , "primFloatCeiling"            -- in Agda.Builtin.Float
      -- , "primFloatToRatio"            -- in Agda.Builtin.Float
      , String
    "primRatioToFloat"
      -- , "primFloatDecode"             -- in Agda.Builtin.Float
      -- , "primFloatEncode"             -- in Agda.Builtin.Float
      , String
    "primShowFloat"
      , String
    "primFloatPlus"
      , String
    "primFloatMinus"
      , String
    "primFloatTimes"
      , String
    "primFloatNegate"
      , String
    "primFloatDiv"
      , String
    "primFloatSqrt"
      , String
    "primFloatExp"
      , String
    "primFloatLog"
      , String
    "primFloatSin"
      , String
    "primFloatCos"
      , String
    "primFloatTan"
      , String
    "primFloatASin"
      , String
    "primFloatACos"
      , String
    "primFloatATan"
      , String
    "primFloatATan2"
      , String
    "primFloatSinh"
      , String
    "primFloatCosh"
      , String
    "primFloatTanh"
      , String
    "primFloatASinh"
      , String
    "primFloatACosh"
      , String
    "primFloatATanh"
      , String
    "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
      , String
    "primQNameEquality"
      , String
    "primQNameLess"
      , String
    "primShowQName"
      , String
    "primQNameFixity"
      -- , "primQNameToWord64s"          -- missing
      -- , "primQNameToWord64sInjective" -- missing
      -- , "primMetaEquality"            -- missing
      -- , "primMetaLess"                -- missing
      -- , "primShowMeta"                -- missing
      -- , "primMetaToNat"               -- missing
      -- , "primMetaToNatInjective"      -- missing
      , String
    builtinIMin
      , String
    builtinIMax
      , String
    builtinINeg
      , String
    "primPartial"
      , String
    "primPartialP"
      , String
    builtinPOr
      , String
    builtinComp
      , String
    builtinTrans
      , String
    builtinHComp
      , String
    builtinSubOut
      , String
    builtin_glueU
      , String
    builtin_unglueU
      , String
    builtinFaceForall
      , String
    "primDepIMin"
      , String
    "primIdFace"
      , String
    "primIdPath"
      , String
    "primIdJ"
      , String
    builtinIdElim
      -- , builtinGlue                   -- missing
      -- , builtin_glue                  -- missing
      -- , builtin_unglue                -- missing
      ]