-- | Main module for JS backend.

module Agda.Compiler.JS.Compiler where

import Prelude hiding ( null, writeFile )

import Control.DeepSeq
import Control.Monad.Trans

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

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

import GHC.Generics (Generic)

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

import Agda.Setup         ( getDataDir )

import Agda.Interaction.Options

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

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

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

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

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

import Agda.Utils.Impossible (__IMPOSSIBLE__)

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

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

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

--- Options ---

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

instance NFData JSModuleStyle

instance NFData JSOptions

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

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

--- Top-level compilation ---

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

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

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

  -- Copy RTE modules.

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

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

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

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

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

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

--- Module compilation ---

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

type EnvWithOpts = (JSOptions, JSModuleEnv)

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

  definition' kit q d (defType d) ls

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

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

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

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

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

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

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

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

        funBody' <- compileTerm kit funBody

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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


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

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

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

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

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

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

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

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

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

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

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