-- | Main module for JS backend.

module Agda.Compiler.JS.Compiler where

import Prelude hiding ( null, writeFile )

import Control.DeepSeq
import Control.Monad.Trans

import Data.Char     ( isSpace )
import Data.Foldable ( forM_ )
import Data.List     ( dropWhileEnd, findIndex, intercalate, partition )
import Data.Set      ( Set )

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

import GHC.Generics (Generic)

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

import Paths_Agda

import Agda.Interaction.Options

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

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

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

import Agda.Compiler.Common
import Agda.Compiler.ToTreeless
import Agda.Compiler.Treeless.EliminateDefaults
import Agda.Compiler.Treeless.EliminateLiteralPatterns
import Agda.Compiler.Treeless.GuardsToPrims
import Agda.Compiler.Treeless.Erase ( computeErasedConstructorArgs )
import Agda.Compiler.Treeless.Subst ()
import Agda.Compiler.Backend (Backend(..), Backend'(..), Recompile(..))

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

import Agda.Utils.Impossible (__IMPOSSIBLE__)

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

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

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

--- Options ---

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

instance NFData JSOptions

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

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

--- Top-level compilation ---

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

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

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

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

  -- Copy RTE modules.

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

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

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

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

    Map ModuleName Module -> (Module -> TCMT IO ()) -> TCMT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Map ModuleName Module
ms ((Module -> TCMT IO ()) -> TCMT IO ())
-> (Module -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ Module{ GlobalId
modName :: GlobalId
modName :: Module -> GlobalId
modName, Maybe Exp
callMain :: Maybe Exp
callMain :: Module -> Maybe Exp
callMain } -> do
      String
jsFile <- GlobalId -> TCMT IO String
outFile GlobalId
modName
      String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js.verify" Int
30 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"Considering JS module:" , String
jsFile ]

      -- Since we do not run a JS program for real, we skip all modules that could
      -- have a call to main.
      -- Atm, modules whose compilation was skipped are also skipped during verification
      -- (they appear here as main modules).
      Maybe Exp -> TCMT IO () -> TCMT IO ()
forall m a. Monoid m => Maybe a -> m -> m
whenNothing Maybe Exp
callMain (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ do
        let cmd :: String
cmd = [String] -> String
unwords [ String
"node", String
"-", String
"<", String
jsFile ]
        String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js.verify" Int
20 (String -> TCMT IO ()) -> String -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [ String
"calling:", String
cmd ]
        IO () -> TCMT IO ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCMT IO ()) -> IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
callCommand String
cmd


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

--- Module compilation ---

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

jsPreModule :: JSOptions -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module)
jsPreModule :: JSOptions
-> IsMain
-> ModuleName
-> Maybe String
-> TCM (Recompile JSModuleEnv Module)
jsPreModule JSOptions
_opts IsMain
_ ModuleName
m Maybe String
mifile = do
  Maybe Cubical
cubical <- PragmaOptions -> Maybe Cubical
optCubical (PragmaOptions -> Maybe Cubical)
-> TCMT IO PragmaOptions -> TCMT IO (Maybe Cubical)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO PragmaOptions
forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
  let compile :: Bool
compile = case Maybe Cubical
cubical of
        -- Code that uses --cubical is not compiled.
        Just Cubical
CFull   -> Bool
False
        Just Cubical
CErased -> Bool
True
        Maybe Cubical
Nothing      -> Bool
True
  TCM Bool
-> TCM (Recompile JSModuleEnv Module)
-> TCM (Recompile JSModuleEnv Module)
-> TCM (Recompile JSModuleEnv Module)
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCM Bool
uptodate TCM (Recompile JSModuleEnv Module)
noComp (Bool -> TCM (Recompile JSModuleEnv Module)
yesComp Bool
compile)
  where
    uptodate :: TCM Bool
uptodate = case Maybe String
mifile of
      Maybe String
Nothing -> Bool -> TCM Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      Just String
ifile -> IO Bool -> TCM Bool
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCM Bool) -> TCMT IO (IO Bool) -> TCM Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> String -> IO Bool
isNewerThan (String -> String -> IO Bool)
-> TCMT IO String -> TCMT IO (String -> IO Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO String
outFile_ TCMT IO (String -> IO Bool) -> TCMT IO String -> TCMT IO (IO Bool)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO String
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
ifile
    ifileDesc :: String
ifileDesc = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"(memory)" Maybe String
mifile

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

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

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

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


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

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

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

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

jsFileName :: GlobalId -> String
jsFileName :: GlobalId -> String
jsFileName (GlobalId [String]
ms) = String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
ms String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
".js"

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

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

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

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

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

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

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

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

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

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

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

type EnvWithOpts = (JSOptions, JSModuleEnv)

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

  EnvWithOpts
-> QName -> Definition -> Type -> JSQName -> TCM (Maybe Export)
definition' EnvWithOpts
kit QName
q Definition
d (Definition -> Type
defType Definition
d) JSQName
ls

-- | Ensure that there is at most one pragma for a name.
checkCompilerPragmas :: QName -> TCM ()
checkCompilerPragmas :: QName -> TCMT IO ()
checkCompilerPragmas QName
q =
  TCMT IO (Maybe CompilerPragma)
-> TCMT IO () -> (CompilerPragma -> TCMT IO ()) -> TCMT IO ()
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (String -> QName -> TCMT IO (Maybe CompilerPragma)
getUniqueCompilerPragma String
jsBackendName QName
q) (() -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((CompilerPragma -> TCMT IO ()) -> TCMT IO ())
-> (CompilerPragma -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (CompilerPragma Range
r String
s) ->
  Range -> TCMT IO () -> TCMT IO ()
forall (m :: * -> *) x a.
(MonadTrace m, HasRange x) =>
x -> m a -> m a
setCurrentRange Range
r (TCMT IO () -> TCMT IO ()) -> TCMT IO () -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ case String -> [String]
words String
s of
    String
"=" : [String]
_ -> () -> TCMT IO ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [String]
_       -> Doc -> TCMT IO ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError (Doc -> TCMT IO ()) -> Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
P.sep [ Doc
"Badly formed COMPILE JS pragma. Expected",
                                         Doc
"{-# COMPILE JS <name> = <js> #-}" ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

compileTerm :: EnvWithOpts -> T.TTerm -> TCM Exp
compileTerm :: EnvWithOpts -> TTerm -> TCM Exp
compileTerm EnvWithOpts
kit TTerm
t = TTerm -> TCM Exp
go TTerm
t
  where
    go :: T.TTerm -> TCM Exp
    go :: TTerm -> TCM Exp
go = \case
      T.TVar Int
x -> Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ LocalId -> Exp
Local (LocalId -> Exp) -> LocalId -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId Int
x
      T.TDef QName
q -> do
        Definition
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
        case Definition -> Defn
theDef Definition
d of
          -- Datatypes and records are erased
          Datatype {} -> Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Exp
String Text
"*")
          Record {} -> Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Exp
String Text
"*")
          Defn
_ -> QName -> TCM Exp
qname QName
q
      T.TApp (T.TCon QName
q) [TTerm
x]
        | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfSharp (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (EnvWithOpts -> JSModuleEnv
forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
        Exp
x <- TTerm -> TCM Exp
go TTerm
x
        let evalThunk :: String
evalThunk = [String] -> String
unlines
              [ String
"function() {"
              , String
"  delete this.flat;"
              , String
"  var result = this.__flat_helper();"
              , String
"  delete this.__flat_helper;"
              , String
"  this.flat = function() { return result; };"
              , String
"  return result;"
              , String
"}"
              ]
        Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
          [(MemberId
flatName, String -> Exp
PlainJS String
evalThunk)
          ,(String -> MemberId
MemberId String
"__flat_helper", Int -> Exp -> Exp
Lambda Int
0 Exp
x)]
      T.TApp TTerm
t' [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 -> [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
-> TCMT IO (Maybe [ArgUsage]) -> TCMT IO [ArgUsage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe [ArgUsage])
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
          Right QName
c -> (Bool -> ArgUsage) -> [Bool] -> [ArgUsage]
forall a b. (a -> b) -> [a] -> [b]
map (\ Bool
b -> if Bool
b then ArgUsage
ArgUnused else ArgUsage
ArgUsed) ([Bool] -> [ArgUsage]) -> TCMT IO [Bool] -> TCMT IO [ArgUsage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO [Bool]
forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
getErasedConArgs QName
c
            -- Andreas, 2021-02-10 NB: could be @map (bool ArgUsed ArgUnused)@
            -- but I find it unintuitive that 'bool' takes the 'False'-branch first.
        let given :: Int
given = [TTerm] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
xs

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

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

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

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

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

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

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

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

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


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

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

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

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

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

qname :: QName -> TCM Exp
qname :: QName -> TCM Exp
qname QName
q = do
  (Exp
e,JSQName
ls) <- QName -> TCM (Exp, JSQName)
global QName
q
  Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return ((Exp -> MemberId -> Exp) -> Exp -> JSQName -> Exp
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Exp -> MemberId -> Exp
Lookup Exp
e JSQName
ls)

literal :: Literal -> Exp
literal :: Literal -> Exp
literal = \case
  (LitNat    Integer
x) -> Integer -> Exp
Integer Integer
x
  (LitWord64 Word64
x) -> Integer -> Exp
Integer (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x)
  (LitFloat  Double
x) -> Double -> Exp
Double  Double
x
  (LitString Text
x) -> Text -> Exp
String  Text
x
  (LitChar   Char
x) -> Char -> Exp
Char    Char
x
  (LitQName  QName
x) -> QName -> Exp
litqname QName
x
  LitMeta{}     -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

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

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

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

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

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

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

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

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

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

  -- Floating point functions
  , String
"primFloatEquality"
  , String
"primFloatInequality"
  , String
"primFloatLess"
  , String
"primFloatIsInfinite"
  , String
"primFloatIsNaN"
  , String
"primFloatIsNegativeZero"
  , String
"primFloatIsSafeInteger"
  , String
"primFloatToWord64"
  -- , "primFloatToWord64Injective"  -- missing
  , String
"primNatToFloat"
  , String
"primIntToFloat"
  -- , "primFloatRound"              -- in Agda.Builtin.Float
  -- , "primFloatFloor"              -- in Agda.Builtin.Float
  -- , "primFloatCeiling"            -- in Agda.Builtin.Float
  -- , "primFloatToRatio"            -- in Agda.Builtin.Float
  , String
"primRatioToFloat"
  -- , "primFloatDecode"             -- in Agda.Builtin.Float
  -- , "primFloatEncode"             -- in Agda.Builtin.Float
  , String
"primShowFloat"
  , String
"primFloatPlus"
  , String
"primFloatMinus"
  , String
"primFloatTimes"
  , String
"primFloatNegate"
  , String
"primFloatDiv"
  , String
"primFloatSqrt"
  , String
"primFloatExp"
  , String
"primFloatLog"
  , String
"primFloatSin"
  , String
"primFloatCos"
  , String
"primFloatTan"
  , String
"primFloatASin"
  , String
"primFloatACos"
  , String
"primFloatATan"
  , String
"primFloatATan2"
  , String
"primFloatSinh"
  , String
"primFloatCosh"
  , String
"primFloatTanh"
  , String
"primFloatASinh"
  , String
"primFloatACosh"
  , String
"primFloatATanh"
  , String
"primFloatPow"

  -- Character functions
  -- , "primCharEquality"            -- missing
  -- , "primIsLower"                 -- missing
  -- , "primIsDigit"                 -- missing
  -- , "primIsAlpha"                 -- missing
  -- , "primIsSpace"                 -- missing
  -- , "primIsAscii"                 -- missing
  -- , "primIsLatin1"                -- missing
  -- , "primIsPrint"                 -- missing
  -- , "primIsHexDigit"              -- missing
  -- , "primToUpper"                 -- missing
  -- , "primToLower"                 -- missing
  -- , "primCharToNat"               -- missing
  -- , "primCharToNatInjective"      -- missing
  -- , "primNatToChar"               -- missing
  -- , "primShowChar"                -- in Agda.Builtin.String

  -- String functions
  -- , "primStringToList"            -- in Agda.Builtin.String
  -- , "primStringToListInjective"   -- missing
  -- , "primStringFromList"          -- in Agda.Builtin.String
  -- , "primStringFromListInjective" -- missing
  -- , "primStringAppend"            -- in Agda.Builtin.String
  -- , "primStringEquality"          -- in Agda.Builtin.String
  -- , "primShowString"              -- in Agda.Builtin.String
  -- , "primStringUncons"            -- in Agda.Builtin.String

  -- Other stuff
  -- , "primEraseEquality"           -- missing
  -- , "primForce"                   -- missing
  -- , "primForceLemma"              -- missing
  , String
"primQNameEquality"
  , String
"primQNameLess"
  , String
"primShowQName"
  , String
"primQNameFixity"
  -- , "primQNameToWord64s"          -- missing
  -- , "primQNameToWord64sInjective" -- missing
  -- , "primMetaEquality"            -- missing
  -- , "primMetaLess"                -- missing
  -- , "primShowMeta"                -- missing
  -- , "primMetaToNat"               -- missing
  -- , "primMetaToNatInjective"      -- missing
  , String
builtinIMin
  , String
builtinIMax
  , String
builtinINeg
  , String
"primPartial"
  , String
"primPartialP"
  , String
builtinPOr
  , String
builtinComp
  , String
builtinTrans
  , String
builtinHComp
  , String
builtinSubOut
  , String
builtin_glueU
  , String
builtin_unglueU
  , String
builtinFaceForall
  , String
"primDepIMin"
  , String
"primIdFace"
  , String
"primIdPath"
  , String
"primIdJ"
  , String
builtinIdElim
  -- , builtinGlue                   -- missing
  -- , builtin_glue                  -- missing
  -- , builtin_unglue                -- missing
  ]