-- | 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, elemIndex, 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
  ( QName,
    mnameToList, qnameName, qnameModule, nameId )
import Agda.Syntax.Internal
  ( Name, Type
  , nameFixity, unDom, telToList )
import Agda.Syntax.Literal       ( Literal(..) )
import Agda.Syntax.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.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.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 )
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 = 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'
  { backendName :: String
backendName           = String
jsBackendName
  , backendVersion :: Maybe String
backendVersion        = 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 TopLevelModuleName Module -> TCMT IO ()
postCompile           = JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
jsPostCompile
  , preModule :: JSOptions
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile JSModuleEnv Module)
preModule             = JSOptions
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCM (Recompile JSModuleEnv Module)
jsPreModule
  , postModule :: JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [Maybe Export]
-> TCM Module
postModule            = JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [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          = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ 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. 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
  { 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 =
    [ forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js"] (forall a. a -> ArgDescr a
NoArg forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enable) String
"compile program using the JS backend"
    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-optimize"] (forall a. a -> ArgDescr a
NoArg 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)
    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-minify"] (forall a. a -> ArgDescr a
NoArg forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enableMin) String
"minify generated JS code"
    , forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-verify"] (forall a. a -> ArgDescr a
NoArg 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSCompile :: Bool
optJSCompile  = Bool
True }
    enableOpt :: JSOptions -> f JSOptions
enableOpt    JSOptions
o = forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSOptimize :: Bool
optJSOptimize = Bool
True }
    enableMin :: JSOptions -> f JSOptions
enableMin    JSOptions
o = forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSMinify :: Bool
optJSMinify   = Bool
True }
    enableVerify :: JSOptions -> f JSOptions
enableVerify JSOptions
o = 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let notSupported :: String -> m a
notSupported String
s =
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
          String
"Compilation of code that uses " forall a. [a] -> [a] -> [a]
++ String
s forall a. [a] -> [a] -> [a]
++ String
" is not supported."
  case Maybe Cubical
cubical of
    Maybe Cubical
Nothing      -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CErased -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    Just Cubical
CFull   -> forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
notSupported String
"--cubical"

  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 TopLevelModuleName Module -> TCM ()
jsPostCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
jsPostCompile JSOptions
opts IsMain
_ Map TopLevelModuleName Module
ms = do

  -- Copy RTE modules.

  String
compDir  <- forall (m :: * -> *). HasOptions m => m String
compileDir
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO 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).

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

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

    forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Map TopLevelModuleName Module
ms 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 -> TCM String
outFile GlobalId
modName
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js.verify" Int
30 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).
      forall m a. Monoid m => Maybe a -> m -> m
whenNothing Maybe Exp
callMain forall a b. (a -> b) -> a -> b
$ do
        let cmd :: String
cmd = [String] -> String
unwords [ String
"node", String
"-", String
"<", String
jsFile ]
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js.verify" Int
20 forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"calling:", String
cmd ]
        forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ String -> IO ()
callCommand String
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
-> TCM (Recompile JSModuleEnv Module)
jsPreModule JSOptions
_opts IsMain
_ TopLevelModuleName
m Maybe String
mifile = do
  Maybe Cubical
cubical <- PragmaOptions -> Maybe Cubical
optCubical forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  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 -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      Just String
ifile -> forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> String -> IO Bool
isNewerThan forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM String
outFile_ forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure String
ifile
    ifileDesc :: String
ifileDesc = forall a. a -> Maybe a -> a
fromMaybe String
"(memory)" Maybe String
mifile

    noComp :: TCM (Recompile JSModuleEnv Module)
noComp = do
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js" Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. [a] -> [a] -> [a]
++ String
" : no compilation is needed.") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Pretty a => a -> String
prettyShow forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty (forall a. a -> Maybe a
Just forall a. HasCallStack => a
__IMPOSSIBLE__)

    yesComp :: Bool -> TCM (Recompile JSModuleEnv Module)
yesComp Bool
compile = do
      String
m   <- forall a. Pretty a => a -> String
prettyShow forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
      String
out <- TCM String
outFile_
      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js" Int
1 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
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall menv mod. menv -> Recompile menv mod
Recompile forall a b. (a -> b) -> a -> b
$ JSModuleEnv
        { jsCoinductionKit :: Maybe CoinductionKit
jsCoinductionKit = Maybe CoinductionKit
kit
        , jsCompile :: Bool
jsCompile        = Bool
compile
        }

jsPostModule ::
  JSOptions -> JSModuleEnv -> IsMain -> TopLevelModuleName ->
  [Maybe Export] -> TCM Module
jsPostModule :: JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [Maybe Export]
-> TCM Module
jsPostModule JSOptions
opts JSModuleEnv
_ IsMain
isMain TopLevelModuleName
_ [Maybe Export]
defs = do
  GlobalId
m  <- TopLevelModuleName -> GlobalId
jsMod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
  [GlobalId]
is <- forall a b. (a -> b) -> [a] -> [b]
map (TopLevelModuleName -> GlobalId
jsMod forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> [(TopLevelModuleName, Word64)]
iImportedModules forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  forall (m :: * -> *) a. Monad m => a -> m a
return Module
mod
  where
  es :: [Export]
es       = 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 forall a. Eq a => a -> a -> Bool
== IsMain
IsMain Bool -> Bool -> Bool
&& forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((forall el coll. Singleton el coll => el -> coll
singleton MemberId
main forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. Export -> JSQName
expName) [Export]
es
  callMain :: Maybe Exp
  callMain :: Maybe Exp
callMain = forall a. Bool -> a -> Maybe a
boolToMaybe Bool
hasMain 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 :: TopLevelModuleName -> GlobalId
jsMod :: TopLevelModuleName -> GlobalId
jsMod TopLevelModuleName
m =
  [String] -> GlobalId
GlobalId (String
prefix forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack (forall l. IsList l => l -> [Item l]
List1.toList (TopLevelModuleName -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m)))

jsFileName :: GlobalId -> String
jsFileName :: GlobalId -> String
jsFileName (GlobalId [String]
ms) = forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
ms 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.
  | forall a. IsNoName a => a -> Bool
isNoName Name
n = String -> MemberId
MemberId (String
"_" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (Name -> NameId
nameId Name
n))
  | Bool
otherwise  = String -> MemberId
MemberId forall a b. (a -> b) -> a -> b
$ forall a. Pretty a => a -> String
prettyShow Name
n

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

global :: QName -> TCM (Exp, JSQName)
global :: QName -> TCM (Exp, JSQName)
global QName
q = do
  Definition
d <- 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
      forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p 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
          forall (m :: * -> *) a. Monad m => a -> m a
return (Exp
m, JSQName
ls forall a. Semigroup a => a -> a -> a
<> 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 forall a. [a] -> [a] -> [a]
++ [Export]
funs forall a. [a] -> [a] -> [a]
++ Set JSQName -> [Export] -> [Export]
reorder' (forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Export -> JSQName
expName forall a b. (a -> b) -> a -> b
$ [Export]
datas forall a. [a] -> [a] -> [a]
++ [Export]
funs) [Export]
vals
  where
    ([Export]
vs, [Export]
funs)    = forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Export -> Bool
isTopLevelValue [Export]
es
    ([Export]
datas, [Export]
vals) = 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 = forall a. Uses a => a -> Set JSQName
uses Export
e forall a. Ord a => Set a -> Set a -> Set a
`Set.difference` Set JSQName
defs
  in  if forall a. Null a => a -> Bool
null Set JSQName
us
        then Export
e forall a. a -> [a] -> [a]
: (Set JSQName -> [Export] -> [Export]
reorder' (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 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 -> 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) | forall a. Null a => a -> Bool
null Set JSQName
us   = Export
e forall a. a -> [a] -> [a]
: Export
f forall a. a -> [a] -> [a]
: [Export]
fs
insertAfter Set JSQName
us Export
e (Export
f : [Export]
fs) | Bool
otherwise =
  Export
f forall a. a -> [a] -> [a]
: Set JSQName -> Export -> [Export] -> [Export]
insertAfter (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
  forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
10 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compiling def:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m 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 <- 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 =
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (String -> QName -> TCM (Maybe CompilerPragma)
getUniqueCompilerPragma String
jsBackendName QName
q) (forall (m :: * -> *) a. Monad m => a -> m a
return ()) forall a b. (a -> b) -> a -> b
$ \ (CompilerPragma Range
r String
s) ->
  forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r forall a b. (a -> b) -> a -> b
$ case String -> [String]
words String
s of
    String
"=" : [String]
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [String]
_       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall a b. (a -> b) -> a -> b
$ 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] -> forall a. a -> Maybe a
Just (String -> String
dropEquals String
s)
    []                   -> forall a. Maybe a
Nothing
    CompilerPragma
_:CompilerPragma
_:[CompilerPragma]
_                -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    dropEquals :: String -> String
dropEquals = forall a. (a -> Bool) -> [a] -> [a]
dropWhile forall a b. (a -> b) -> a -> b
$ \ Char
c -> Char -> Bool
isSpace Char
c Bool -> Bool -> Bool
|| Char
c 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 (forall a b. (a, b) -> b
snd EnvWithOpts
kit)) Bool -> Bool -> Bool
|| Bool -> Bool
not (forall a. LensModality a => a -> Bool
usableModality Definition
d)
  then forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
  else do
  QName -> TCMT IO ()
checkCompilerPragmas QName
q
  case Definition -> Defn
theDef Definition
d of
    -- coinduction
    Constructor{}
      | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfSharp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
    Function{}
      | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfFlat forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
      Exp -> TCM (Maybe Export)
ret forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
Lambda Int
1 forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup (Int -> Exp
local Int
0) MemberId
flatName) []

    DataOrRecSig{} -> 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return 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

      forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
5 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compiling fun:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM QName
q
      forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (EvaluationStrategy -> QName -> TCM (Maybe TTerm)
toTreeless EvaluationStrategy
T.EagerEvaluation QName
q) (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. Maybe a
Nothing) forall a b. (a -> b) -> a -> b
$ \ TTerm
treeless -> do
        [ArgUsage]
used <- forall a. a -> Maybe a -> a
fromMaybe [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
        TTerm
funBody <- TTerm -> TCMT IO TTerm
eliminateCaseDefaults forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<
          TTerm -> TCMT IO TTerm
eliminateLiteralPatterns
          (TTerm -> TTerm
convertGuards TTerm
treeless)
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
30 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" compiled treeless fun:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
pretty TTerm
funBody
        forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
40 forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
" argument usage:" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (forall (m :: * -> *). Applicative m => String -> m Doc
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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) = (forall a. Num a => a -> a -> a
+Int
1) 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
dropWhileEnd (forall a. Eq a => a -> a -> Bool
== ArgUsage
ArgUsed) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
given [ArgUsage]
used

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

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

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

    Primitive{primName :: Defn -> String
primName = String
p}
      | String
p 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 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 forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
primitives ->
        String -> TCM (Maybe Export)
plainJS forall a b. (a -> b) -> a -> b
$ String
"agdaRTS." 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return 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
        forall (m :: * -> *) a. Monad m => a -> m a
return 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
_ <- forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
      let np :: Int
np = forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel) forall a. Num a => a -> a -> a
- Int
nc
      [Bool]
erased <- forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
getErasedConArgs QName
q
      let nargs :: Int
nargs = Int
np forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. a -> a
id [Bool]
erased)
          args :: [Exp]
args = [ LocalId -> Exp
Local forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId forall a b. (a -> b) -> a -> b
$ Int
nargs forall a. Num a => a -> a -> a
- Int
i | Int
i <- [Int
0 .. Int
nargsforall a. Num a => a -> a -> a
-Int
1] ]
      Definition
d <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p
      let l :: MemberId
l = 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 forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
curriedLambda Int
nargs forall a b. (a -> b) -> a -> b
$
          if JSOptions -> Bool
optJSOptimize (forall a b. (a, b) -> a
fst EnvWithOpts
kit)
            then Int -> Exp -> Exp
Lambda Int
1 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 forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton MemberId
l forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
Lambda Int
1 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 forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
curriedLambda (Int
nargs forall a. Num a => a -> a -> a
+ Int
1) 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 (forall a b. (a, b) -> a
fst EnvWithOpts
kit) = do
                  QName
q  <- forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
q
                  [QName]
cs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName forall a b. (a -> b) -> a -> b
$ Defn -> [QName]
defConstructors Defn
dt
                  case QName
q forall a. Eq a => a -> [a] -> Maybe Int
`elemIndex` [QName]
cs of
                    Just Int
i  -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Int -> Comment -> MemberId
MemberIndex Int
i (MemberId -> Comment
mkComment MemberId
l)
                    Maybe Int
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadDebug m) =>
String -> m a
__IMPOSSIBLE_VERBOSE__ forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"Constructor", forall a. Pretty a => a -> String
prettyShow QName
q, String
"not found in", forall a. Pretty a => a -> String
prettyShow [QName]
cs ]
              | Bool
otherwise = 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
_ = forall a. Monoid a => a
mempty

    AbstractDefn{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
  where
    ret :: Exp -> TCM (Maybe Export)
ret = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. JSQName -> Exp -> Export
Export JSQName
ls
    plainJS :: String -> TCM (Maybe Export)
plainJS = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. JSQName -> Exp -> Export
Export JSQName
ls 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ LocalId -> Exp
Local forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId Int
x
      T.TDef QName
q -> do
        Definition
d <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
        case Definition -> Defn
theDef Definition
d of
          -- Datatypes and records are erased
          Datatype {} -> forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Exp
String Text
"*")
          Record {} -> 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]
        | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfSharp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (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
"}"
              ]
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Map MemberId Exp -> Exp
Object forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith 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' [TTerm]
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 -> forall a. a -> Maybe a -> a
fromMaybe [] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
          Right QName
c -> forall a b. (a -> b) -> [a] -> [b]
map (\ Bool
b -> if Bool
b then ArgUsage
ArgUnused else ArgUsage
ArgUsed) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
xs

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

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

        Int -> Exp -> Exp
curriedLambda Int
etaN forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Exp -> [Exp] -> Exp
curriedApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM Exp
go (forall a. Subst a => Int -> a -> a
raise Int
etaN TTerm
t') forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TTerm -> TCM Exp
go [TTerm]
args)

      T.TApp TTerm
t [TTerm]
xs -> do
            Exp -> [Exp] -> Exp
curriedApply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM Exp
go TTerm
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM TTerm -> TCM Exp
go [TTerm]
xs
      T.TLam TTerm
t -> Int -> Exp -> Exp
Lambda Int
1 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int -> Exp -> Exp
Lambda Int
1 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM Exp
go TTerm
e) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Literal -> Exp
literal Literal
l
      T.TCon QName
q -> do
        Definition
d <- 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
dt
        [((QName, MemberId), Exp)]
alts' <- forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse (EnvWithOpts -> TAlt -> TCM ((QName, MemberId), Exp)
compileAlt EnvWithOpts
kit) [TAlt]
alts
        let cs :: [QName]
cs  = Defn -> [QName]
defConstructors forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
dt
            obj :: Exp
obj = Map MemberId Exp -> Exp
Object forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__ [(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 [forall a. a -> [a] -> a
headWithDefault (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' 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
            forall (m :: * -> *) a. Monad m => a -> m a
return 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 (forall a b. (a, b) -> a
fst EnvWithOpts
kit) -> do
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (LocalId -> Exp
Local forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId Int
sc) [forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> a
headWithDefault forall a. HasCallStack => a
__IMPOSSIBLE__ [((QName, MemberId), Exp)]
alts']
          (Record{}, Maybe String
_) -> do
            MemberId
memId <- QName -> TCM MemberId
visitorName forall a b. (a -> b) -> a -> b
$ Defn -> QName
recCon forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
dt
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (Exp -> MemberId -> Exp
Lookup (LocalId -> Exp
Local forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId Int
sc) MemberId
memId) [Exp
obj]
          (Datatype{}, Maybe String
_) | JSOptions -> Bool
optJSOptimize (forall a b. (a, b) -> a
fst EnvWithOpts
kit) -> do
            forall (m :: * -> *) a. Monad m => a -> m a
return 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
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
curriedApply (LocalId -> Exp
Local (Int -> LocalId
LocalId Int
sc)) [Exp
obj]
          (Defn, Maybe String)
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
      T.TCase Int
_ CaseInfo
_ TTerm
_ [TAlt]
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__

      T.TPrim TPrim
p -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Exp
Undefined
      T.TError T.TMeta{}      -> 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) = forall a. a -> Maybe a
Just (forall a b. a -> Either a b
Left QName
f)
    getDef (T.TCon QName
c) = forall a. a -> Maybe a
Just (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
_ = forall a. Maybe a
Nothing

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

    mkArray :: [(Comment, Exp)] -> Exp
mkArray [(Comment, Exp)]
xs
        | Int
2 forall a. Num a => a -> a -> a
* forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Eq a => a -> a -> Bool
==Exp
Null) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Comment, Exp)]
xs) forall a. Ord a => a -> a -> Bool
<= 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 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__
            [ (Int -> Comment -> MemberId
MemberIndex Int
i Comment
c, Exp
x) | (Int
i, (Comment
c, Exp
x)) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(Comment, Exp)]
xs, Exp
x 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 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 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 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 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 -> TCM ((QName, MemberId), Exp)
compileAlt EnvWithOpts
kit = \case
  T.TACon QName
con Int
ar TTerm
body -> do
    [Bool]
erased <- forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
getErasedConArgs QName
con
    let nargs :: Int
nargs = Int
ar forall a. Num a => a -> a -> a
- forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall a. (a -> Bool) -> [a] -> [a]
filter forall a. a -> a
id [Bool]
erased)
    MemberId
memId <- QName -> TCM MemberId
visitorName QName
con
    Exp
body <- Int -> Exp -> Exp
Lambda Int
nargs 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)
    forall (m :: * -> *) a. Monad m => a -> m a
return ((QName
con, MemberId
memId), Exp
body)
  TAlt
_ -> 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 (forall a. Subst a => Int -> SubstArg a -> a -> a
TC.subst (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Bool]
es) 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; forall (m :: * -> *) a. Monad m => a -> m a
return (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 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
  forall (m :: * -> *) a. Monad m => a -> m a
return (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 (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{}     -> forall a. HasCallStack => a
__IMPOSSIBLE__

litqname :: QName -> Exp
litqname :: QName -> Exp
litqname QName
q =
  Map MemberId Exp -> Exp
Object forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__
    [ (String -> MemberId
mem String
"id", Integer -> Exp
Integer forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n)
    , (String -> MemberId
mem String
"moduleId", Integer -> Exp
Integer forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
m)
    , (String -> MemberId
mem String
"name", Text -> Exp
String forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ 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 forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
    fx :: Fixity
fx = Fixity' -> Fixity
theFixity forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
nameFixity 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 forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. HasCallStack => a
__IMPOSSIBLE__
      [ (String -> MemberId
mem String
"assoc", Associativity -> Exp
litAssoc forall a b. (a -> b) -> a -> b
$ Fixity -> Associativity
fixityAssoc Fixity
fx)
      , (String -> MemberId
mem String
"prec", FixityLevel -> Exp
litPrec 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 -> TCM String
outFile (Module -> GlobalId
modName Module
m)
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (String -> String -> IO ()
writeFile String
out (forall a. Pretty a => Bool -> a -> String
JSPretty.prettyShow Bool
minify Module
m))

outFile :: GlobalId -> TCM FilePath
outFile :: GlobalId -> TCM String
outFile GlobalId
m = do
  String
mdir <- 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
  forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO forall a b. (a -> b) -> a -> b
$ Bool -> String -> IO ()
createDirectoryIfMissing Bool
True String
dir
  forall (m :: * -> *) a. Monad m => a -> m a
return String
fp

outFile_ :: TCM FilePath
outFile_ :: TCM String
outFile_ = do
  TopLevelModuleName
m <- forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
  GlobalId -> TCM String
outFile (TopLevelModuleName -> GlobalId
jsMod TopLevelModuleName
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 = 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
builtinIdElim
  , String
builtinConId
  -- , builtinGlue                   -- missing
  -- , builtin_glue                  -- missing
  -- , builtin_unglue                -- missing
  ]