module Agda.Compiler.JS.Compiler where

import Prelude hiding ( null, writeFile )

import Control.Monad.Reader ( liftIO )
import Control.Monad.Trans

import Data.Char ( isSpace )
import Data.List ( intercalate, partition )
import Data.Set ( Set, null, insert, difference, delete )
import Data.Traversable (traverse)
import Data.Map ( fromList )
import qualified Data.Set as Set
import qualified Data.Map as Map

import System.Directory ( createDirectoryIfMissing )
import System.FilePath ( splitFileName, (</>) )

import Paths_Agda

import Agda.Interaction.Options
import Agda.Interaction.Imports ( isNewerThan )

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
  , arity, nameFixity, unDom )
import Agda.Syntax.Literal ( Literal(..) )
import qualified Agda.Syntax.Treeless as T

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Debug ( reportSLn )
import Agda.TypeChecking.Reduce ( instantiateFull )
import Agda.TypeChecking.Pretty

import Agda.Utils.Maybe
import Agda.Utils.Monad ( (<$>), (<*>), ifM )
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
import Agda.Utils.IO.Directory
import Agda.Utils.IO.UTF8 ( writeFile )

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.Backend (Backend(..), Backend'(..), Recompile(..))

import Agda.Compiler.JS.Syntax
  ( Exp(Self,Local,Global,Undefined,String,Char,Integer,Double,Lambda,Object,Apply,Lookup,If,BinOp,PlainJS),
    LocalId(LocalId), GlobalId(GlobalId), MemberId(MemberId), Export(Export), Module(Module),
    modName, expName, uses )
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 () (Maybe Export)
-> Backend
forall opts env menv mod def.
Backend' opts env menv mod def -> Backend
Backend Backend' JSOptions JSOptions JSModuleEnv () (Maybe Export)
jsBackend'

jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv () (Maybe Export)
jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv () (Maybe Export)
jsBackend' = Backend' :: forall opts env menv mod def.
String
-> Maybe String
-> opts
-> [OptDescr (Flag opts)]
-> (opts -> Bool)
-> (opts -> TCM env)
-> (env -> IsMain -> Map ModuleName mod -> TCM ())
-> (env
    -> IsMain -> ModuleName -> String -> TCM (Recompile menv mod))
-> (env -> menv -> IsMain -> ModuleName -> [def] -> TCM mod)
-> (env -> menv -> IsMain -> Definition -> TCM def)
-> Bool
-> (QName -> TCM Bool)
-> Backend' opts env menv mod def
Backend'
  { backendName :: String
backendName           = String
jsBackendName
  , backendVersion :: Maybe String
backendVersion        = Maybe String
forall a. Maybe a
Nothing
  , options :: JSOptions
options               = JSOptions
defaultJSOptions
  , commandLineFlags :: [OptDescr (Flag JSOptions)]
commandLineFlags      = [OptDescr (Flag JSOptions)]
jsCommandLineFlags
  , isEnabled :: JSOptions -> Bool
isEnabled             = JSOptions -> Bool
optJSCompile
  , preCompile :: JSOptions -> TCM JSOptions
preCompile            = JSOptions -> TCM JSOptions
jsPreCompile
  , postCompile :: JSOptions -> IsMain -> Map ModuleName () -> TCM ()
postCompile           = JSOptions -> IsMain -> Map ModuleName () -> TCM ()
forall a. JSOptions -> IsMain -> a -> TCM ()
jsPostCompile
  , preModule :: JSOptions
-> IsMain -> ModuleName -> String -> TCM (Recompile JSModuleEnv ())
preModule             = JSOptions
-> IsMain -> ModuleName -> String -> TCM (Recompile JSModuleEnv ())
jsPreModule
  , postModule :: JSOptions
-> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM ()
postModule            = JSOptions
-> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM ()
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 }

defaultJSOptions :: JSOptions
defaultJSOptions :: JSOptions
defaultJSOptions = JSOptions :: Bool -> JSOptions
JSOptions
  { optJSCompile :: Bool
optJSCompile = 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"
    ]
  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 }

--- Top-level compilation ---

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

jsPostCompile :: JSOptions -> IsMain -> a -> TCM ()
jsPostCompile :: JSOptions -> IsMain -> a -> TCM ()
jsPostCompile JSOptions
_ IsMain
_ a
_ = TCM ()
copyRTEModules

--- Module compilation ---

type JSModuleEnv = Maybe CoinductionKit

jsPreModule :: JSOptions -> IsMain -> ModuleName -> FilePath -> TCM (Recompile JSModuleEnv ())
jsPreModule :: JSOptions
-> IsMain -> ModuleName -> String -> TCM (Recompile JSModuleEnv ())
jsPreModule JSOptions
_ IsMain
_ ModuleName
m String
ifile = TCM Bool
-> TCM (Recompile JSModuleEnv ())
-> TCM (Recompile JSModuleEnv ())
-> TCM (Recompile JSModuleEnv ())
forall (m :: * -> *) a. Monad m => m Bool -> m a -> m a -> m a
ifM TCM Bool
uptodate TCM (Recompile JSModuleEnv ())
forall menv. TCMT IO (Recompile menv ())
noComp TCM (Recompile JSModuleEnv ())
forall mod. TCMT IO (Recompile JSModuleEnv mod)
yesComp
  where
    uptodate :: TCM Bool
uptodate = 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

    noComp :: TCMT IO (Recompile menv ())
noComp = do
      String -> VerboseLevel -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"compile.js" VerboseLevel
2 (String -> TCM ())
-> (ModuleName -> String) -> ModuleName -> TCM ()
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 -> TCM ()) -> TCMT IO ModuleName -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO ModuleName
curMName
      Recompile menv () -> TCMT IO (Recompile menv ())
forall (m :: * -> *) a. Monad m => a -> m a
return (Recompile menv () -> TCMT IO (Recompile menv ()))
-> Recompile menv () -> TCMT IO (Recompile menv ())
forall a b. (a -> b) -> a -> b
$ () -> Recompile menv ()
forall menv mod. mod -> Recompile menv mod
Skip ()

    yesComp :: TCMT IO (Recompile JSModuleEnv mod)
yesComp = 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
curMName
      String
out <- TCMT IO String
outFile_
      String -> VerboseLevel -> String -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> String -> m ()
reportSLn String
"compile.js" VerboseLevel
1 (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ [String] -> String -> String
repl [String
m, String
ifile, String
out] String
"Compiling <<0>> in <<1>> to <<2>>"
      JSModuleEnv -> Recompile JSModuleEnv mod
forall menv mod. menv -> Recompile menv mod
Recompile (JSModuleEnv -> Recompile JSModuleEnv mod)
-> TCMT IO JSModuleEnv -> TCMT IO (Recompile JSModuleEnv mod)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO JSModuleEnv
coinductionKit

jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM ()
jsPostModule :: JSOptions
-> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM ()
jsPostModule JSOptions
_ 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
curMName
  [GlobalId]
is            <- ((ModuleName, Hash) -> GlobalId)
-> [(ModuleName, Hash)] -> [GlobalId]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName -> GlobalId
jsMod (ModuleName -> GlobalId)
-> ((ModuleName, Hash) -> ModuleName)
-> (ModuleName, Hash)
-> GlobalId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst) ([(ModuleName, Hash)] -> [GlobalId])
-> (Interface -> [(ModuleName, Hash)]) -> Interface -> [GlobalId]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> [(ModuleName, Hash)]
iImportedModules (Interface -> [GlobalId])
-> TCMT IO Interface -> TCMT IO [GlobalId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
curIF
  let es :: [Export]
es = [Maybe Export] -> [Export]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Export]
defs
  Module -> TCM ()
writeModule (Module -> TCM ()) -> Module -> TCM ()
forall a b. (a -> b) -> a -> b
$ GlobalId -> [Export] -> Maybe Exp -> Module
Module GlobalId
m ([Export] -> [Export]
reorder [Export]
es) Maybe Exp
main
  where
    main :: Maybe Exp
main = case IsMain
isMain of
      IsMain
IsMain  -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> Maybe Exp) -> Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup Exp
Self (MemberId -> Exp) -> MemberId -> Exp
forall a b. (a -> b) -> a -> b
$ String -> MemberId
MemberId String
"main") [VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
1 Exp
emp]
      IsMain
NotMain -> Maybe Exp
forall a. Maybe a
Nothing

jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
jsCompileDef :: JSOptions
-> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
jsCompileDef JSOptions
_ JSModuleEnv
kit IsMain
_isMain Definition
def = JSModuleEnv -> (QName, Definition) -> TCM (Maybe Export)
definition 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

-- Rather annoyingly, the anonymous construtor 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.

global' :: QName -> TCM (Exp,[MemberId])
global' :: QName -> TCM (Exp, [MemberId])
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
curIF
  ModuleName
modNm <- ModuleName -> TCMT IO ModuleName
topLevelModuleName (QName -> ModuleName
qnameModule QName
q)
  let
    qms :: [Name]
qms = ModuleName -> [Name]
mnameToList (ModuleName -> [Name]) -> ModuleName -> [Name]
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
    nm :: [MemberId]
nm = (Name -> MemberId) -> [Name] -> [MemberId]
forall a b. (a -> b) -> [a] -> [b]
map Name -> MemberId
jsMember (VerboseLevel -> [Name] -> [Name]
forall a. VerboseLevel -> [a] -> [a]
drop ([Name] -> VerboseLevel
forall (t :: * -> *) a. Foldable t => t a -> VerboseLevel
length ([Name] -> VerboseLevel) -> [Name] -> VerboseLevel
forall a b. (a -> b) -> a -> b
$ ModuleName -> [Name]
mnameToList ModuleName
modNm) [Name]
qms [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ [QName -> Name
qnameName QName
q])
  if ModuleName
modNm ModuleName -> ModuleName -> Bool
forall a. Eq a => a -> a -> Bool
== ModuleName
i
    then (Exp, [MemberId]) -> TCM (Exp, [MemberId])
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp
Self, [MemberId]
nm)
    else (Exp, [MemberId]) -> TCM (Exp, [MemberId])
forall (m :: * -> *) a. Monad m => a -> m a
return (GlobalId -> Exp
Global (ModuleName -> GlobalId
jsMod ModuleName
modNm), [MemberId]
nm)

global :: QName -> TCM (Exp,[MemberId])
global :: QName -> TCM (Exp, [MemberId])
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
      Definition
e <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p
      case Definition
e of
        Defn { theDef :: Definition -> Defn
theDef = Record { recNamedCon :: Defn -> Bool
recNamedCon = Bool
False } } -> do
          (Exp
m,[MemberId]
ls) <- QName -> TCM (Exp, [MemberId])
global' QName
p
          (Exp, [MemberId]) -> TCM (Exp, [MemberId])
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp
m, [MemberId]
ls [MemberId] -> [MemberId] -> [MemberId]
forall a. [a] -> [a] -> [a]
++ [String -> MemberId
MemberId String
"record"])
        Definition
_ -> QName -> TCM (Exp, [MemberId])
global' (Definition -> QName
defName Definition
d)
    Definition
_ -> QName -> TCM (Exp, [MemberId])
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 [MemberId] -> [Export] -> [Export]
reorder' ([[MemberId]] -> Set [MemberId]
forall a. Ord a => [a] -> Set a
Set.fromList ([[MemberId]] -> Set [MemberId]) -> [[MemberId]] -> Set [MemberId]
forall a b. (a -> b) -> a -> b
$ (Export -> [MemberId]) -> [Export] -> [[MemberId]]
forall a b. (a -> b) -> [a] -> [b]
map Export -> [MemberId]
expName ([Export] -> [[MemberId]]) -> [Export] -> [[MemberId]]
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 [MemberId] -> [Export] -> [Export]
reorder' :: Set [MemberId] -> [Export] -> [Export]
reorder' Set [MemberId]
defs [] = []
reorder' Set [MemberId]
defs (Export
e : [Export]
es) =
  let us :: Set [MemberId]
us = Export -> Set [MemberId]
forall a. Uses a => a -> Set [MemberId]
uses Export
e Set [MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => Set a -> Set a -> Set a
`difference` Set [MemberId]
defs in
  case Set [MemberId] -> Bool
forall a. Set a -> Bool
null Set [MemberId]
us of
    Bool
True -> Export
e Export -> [Export] -> [Export]
forall a. a -> [a] -> [a]
: (Set [MemberId] -> [Export] -> [Export]
reorder' ([MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => a -> Set a -> Set a
insert (Export -> [MemberId]
expName Export
e) Set [MemberId]
defs) [Export]
es)
    Bool
False -> Set [MemberId] -> [Export] -> [Export]
reorder' Set [MemberId]
defs (Set [MemberId] -> Export -> [Export] -> [Export]
insertAfter Set [MemberId]
us Export
e [Export]
es)

isTopLevelValue :: Export -> Bool
isTopLevelValue :: Export -> Bool
isTopLevelValue (Export [MemberId]
_ 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 [MemberId]
_ Exp
e) = case Exp
e of
  Object Map MemberId Exp
m -> Map MemberId Exp -> Bool
forall k a. Map k a -> Bool
Map.null Map MemberId Exp
m
  Lambda{} -> Bool
True
  Exp
_        -> Bool
False

insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export]
insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export]
insertAfter Set [MemberId]
us Export
e []                 = [Export
e]
insertAfter Set [MemberId]
us Export
e (Export
f:[Export]
fs) | Set [MemberId] -> Bool
forall a. Set a -> Bool
null Set [MemberId]
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 [MemberId]
us Export
e (Export
f:[Export]
fs) | Bool
otherwise = Export
f Export -> [Export] -> [Export]
forall a. a -> [a] -> [a]
: Set [MemberId] -> Export -> [Export] -> [Export]
insertAfter ([MemberId] -> Set [MemberId] -> Set [MemberId]
forall a. Ord a => a -> Set a -> Set a
delete (Export -> [MemberId]
expName Export
f) Set [MemberId]
us) Export
e [Export]
fs

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

curModule :: IsMain -> TCM Module
curModule :: IsMain -> TCM Module
curModule IsMain
isMain = do
  JSModuleEnv
kit <- TCMT IO JSModuleEnv
coinductionKit
  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
curMName)
  [GlobalId]
is <- (ModuleName -> GlobalId) -> [ModuleName] -> [GlobalId]
forall a b. (a -> b) -> [a] -> [b]
map ModuleName -> GlobalId
jsMod ([ModuleName] -> [GlobalId])
-> TCMT IO [ModuleName] -> TCMT IO [GlobalId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((ModuleName, Hash) -> ModuleName)
-> [(ModuleName, Hash)] -> [ModuleName]
forall a b. (a -> b) -> [a] -> [b]
map (ModuleName, Hash) -> ModuleName
forall a b. (a, b) -> a
fst ([(ModuleName, Hash)] -> [ModuleName])
-> (Interface -> [(ModuleName, Hash)]) -> Interface -> [ModuleName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Interface -> [(ModuleName, Hash)]
iImportedModules (Interface -> [ModuleName])
-> TCMT IO Interface -> TCMT IO [ModuleName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
curIF)
  [Export]
es <- [Maybe Export] -> [Export]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe Export] -> [Export])
-> TCMT IO [Maybe Export] -> TCMT IO [Export]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (((QName, Definition) -> TCM (Maybe Export))
-> [(QName, Definition)] -> TCMT IO [Maybe Export]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (JSModuleEnv -> (QName, Definition) -> TCM (Maybe Export)
definition JSModuleEnv
kit) ([(QName, Definition)] -> TCMT IO [Maybe Export])
-> TCMT IO [(QName, Definition)] -> TCMT IO [Maybe Export]
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (Definitions -> [(QName, Definition)]
sortDefs (Definitions -> [(QName, Definition)])
-> TCMT IO Definitions -> TCMT IO [(QName, Definition)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Definitions
curDefs))
  Module -> TCM Module
forall (m :: * -> *) a. Monad m => a -> m a
return (Module -> TCM Module) -> Module -> TCM Module
forall a b. (a -> b) -> a -> b
$ GlobalId -> [Export] -> Maybe Exp -> Module
Module GlobalId
m ([Export] -> [Export]
reorder [Export]
es) Maybe Exp
main
  where
    main :: Maybe Exp
main = case IsMain
isMain of
      IsMain
IsMain -> Exp -> Maybe Exp
forall a. a -> Maybe a
Just (Exp -> Maybe Exp) -> Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup Exp
Self (MemberId -> Exp) -> MemberId -> Exp
forall a b. (a -> b) -> a -> b
$ String -> MemberId
MemberId String
"main") [VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
1 Exp
emp]
      IsMain
NotMain -> Maybe Exp
forall a. Maybe a
Nothing

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

  JSModuleEnv
-> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)
definition' JSModuleEnv
kit QName
q Definition
d (Definition -> Type
defType Definition
d) [MemberId]
ls

-- | Ensure that there is at most one pragma for a name.
checkCompilerPragmas :: QName -> TCM ()
checkCompilerPragmas :: QName -> TCM ()
checkCompilerPragmas QName
q =
  TCMT IO (Maybe CompilerPragma)
-> TCM () -> (CompilerPragma -> TCM ()) -> TCM ()
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) (() -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((CompilerPragma -> TCM ()) -> TCM ())
-> (CompilerPragma -> TCM ()) -> TCM ()
forall a b. (a -> b) -> a -> b
$ \ (CompilerPragma Range
r String
s) ->
  Range -> TCM () -> TCM ()
forall (tcm :: * -> *) x a.
(MonadTCM tcm, ReadTCState tcm, MonadDebug tcm, HasRange x) =>
x -> tcm a -> tcm a
setCurrentRange Range
r (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ case String -> [String]
words String
s of
    String
"=" : [String]
_ -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
    [String]
_       -> Doc -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
Doc -> m a
genericDocError (Doc -> TCM ()) -> Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ [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' :: Maybe CoinductionKit -> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)
definition' :: JSModuleEnv
-> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)
definition' JSModuleEnv
kit QName
q Definition
d Type
t [MemberId]
ls = do
  QName -> TCM ()
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) -> JSModuleEnv -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv
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) -> JSModuleEnv -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv
kit) -> do
      Exp -> TCM (Maybe Export)
ret (Exp -> TCM (Maybe Export)) -> Exp -> TCM (Maybe Export)
forall a b. (a -> b) -> a -> b
$ VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
1 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup (VerboseLevel -> Exp
local VerboseLevel
0) MemberId
flatName) []

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

    Defn
Axiom | Just String
e <- Definition -> Maybe String
defJSDef Definition
d -> String -> TCM (Maybe Export)
plainJS String
e
    Defn
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 -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"compile.js" VerboseLevel
5 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
"compiling fun:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCM 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
        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 -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"compile.js" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
" compiled treeless fun:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> TTerm -> TCM Doc
forall (m :: * -> *) a. (Monad m, Pretty a) => a -> m Doc
pretty TTerm
funBody
        Exp
funBody' <- TTerm -> TCM Exp
compileTerm TTerm
funBody
        String -> VerboseLevel -> TCM Doc -> TCM ()
forall (m :: * -> *).
MonadDebug m =>
String -> VerboseLevel -> TCM Doc -> m ()
reportSDoc String
"compile.js" VerboseLevel
30 (TCM Doc -> TCM ()) -> TCM Doc -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM Doc
" compiled JS fun:" TCM Doc -> TCM Doc -> TCM Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> (String -> TCM Doc
forall (m :: * -> *). Monad m => String -> m Doc
text (String -> TCM Doc) -> (Exp -> String) -> Exp -> TCM 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
$ Export -> Maybe Export
forall a. a -> Maybe a
Just (Export -> Maybe Export) -> Export -> Maybe Export
forall a b. (a -> b) -> a -> b
$ [MemberId] -> Exp -> Export
Export [MemberId]
ls Exp
funBody'

    Primitive{primName :: Defn -> String
primName = String
p} | 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
    Primitive{} | Just String
e <- Definition -> Maybe String
defJSDef Definition
d -> String -> TCM (Maybe Export)
plainJS String
e
    Primitive{} | Bool
otherwise -> Exp -> TCM (Maybe Export)
ret Exp
Undefined

    Datatype{} -> Exp -> TCM (Maybe Export)
ret Exp
emp
    Record{} -> 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 -> VerboseLevel
conPars = VerboseLevel
nc} | Bool
otherwise -> do
      VerboseLevel
np <- VerboseLevel -> TCMT IO VerboseLevel
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> VerboseLevel
arity Type
t VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
nc)
      Definition
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p
      case Definition -> Defn
theDef Definition
d of
        Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
flds } ->
          Exp -> TCM (Maybe Export)
ret (VerboseLevel -> Exp -> Exp
curriedLambda VerboseLevel
np (Map MemberId Exp -> Exp
Object ([(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => [(k, a)] -> Map k a
fromList
            ( ([MemberId] -> MemberId
forall a. [a] -> a
last [MemberId]
ls , VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
1
                 (Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup (LocalId -> Exp
Local (VerboseLevel -> LocalId
LocalId VerboseLevel
0)) ([MemberId] -> MemberId
forall a. [a] -> a
last [MemberId]
ls))
                   [ LocalId -> Exp
Local (VerboseLevel -> LocalId
LocalId (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
i)) | VerboseLevel
i <- [VerboseLevel
0 .. VerboseLevel
npVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1] ]))
            (MemberId, Exp) -> [(MemberId, Exp)] -> [(MemberId, Exp)]
forall a. a -> [a] -> [a]
: ([MemberId] -> [Exp] -> [(MemberId, Exp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ Name -> MemberId
jsMember (QName -> Name
qnameName (Dom QName -> QName
forall t e. Dom' t e -> e
unDom Dom QName
fld)) | Dom QName
fld <- [Dom QName]
flds ]
                 [ LocalId -> Exp
Local (VerboseLevel -> LocalId
LocalId (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
i)) | VerboseLevel
i <- [VerboseLevel
1 .. VerboseLevel
np] ])))))
        Defn
_ ->
          Exp -> TCM (Maybe Export)
ret (VerboseLevel -> Exp -> Exp
curriedLambda (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
+ VerboseLevel
1)
            (Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup (LocalId -> Exp
Local (VerboseLevel -> LocalId
LocalId VerboseLevel
0)) ([MemberId] -> MemberId
forall a. [a] -> a
last [MemberId]
ls))
              [ LocalId -> Exp
Local (VerboseLevel -> LocalId
LocalId (VerboseLevel
np VerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
- VerboseLevel
i)) | VerboseLevel
i <- [VerboseLevel
0 .. VerboseLevel
npVerboseLevel -> VerboseLevel -> VerboseLevel
forall a. Num a => a -> a -> a
-VerboseLevel
1] ]))

    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
. [MemberId] -> Exp -> Export
Export [MemberId]
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
. [MemberId] -> Exp -> Export
Export [MemberId]
ls (Exp -> Export) -> (String -> Exp) -> String -> Export
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Exp
PlainJS

compileTerm :: T.TTerm -> TCM Exp
compileTerm :: TTerm -> TCM Exp
compileTerm TTerm
t = do
  JSModuleEnv
kit <- TCMT IO JSModuleEnv
coinductionKit
  JSModuleEnv -> TTerm -> TCM Exp
compileTerm' JSModuleEnv
kit TTerm
t

compileTerm' :: Maybe CoinductionKit -> T.TTerm -> TCM Exp
compileTerm' :: JSModuleEnv -> TTerm -> TCM Exp
compileTerm' JSModuleEnv
kit TTerm
t = TTerm -> TCM Exp
go TTerm
t
  where
    go :: T.TTerm -> TCM Exp
    go :: TTerm -> TCM Exp
go TTerm
t = case TTerm
t of
      T.TVar VerboseLevel
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
$ VerboseLevel -> LocalId
LocalId VerboseLevel
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 (String -> Exp
String String
"*")
          Record {} -> Exp -> TCM Exp
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Exp
String String
"*")
          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) -> JSModuleEnv -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv
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
$ [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
          [(MemberId
flatName, String -> Exp
PlainJS String
evalThunk)
          ,(String -> MemberId
MemberId String
"__flat_helper", VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
0 Exp
x)]
      T.TApp TTerm
t [TTerm]
xs -> 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 -> VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
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
<$> (VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
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 VerboseLevel
sc CaseInfo
ct TTerm
def [TAlt]
alts | T.CTData 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
        [(MemberId, Exp)]
alts' <- (TAlt -> TCMT IO (MemberId, Exp))
-> [TAlt] -> TCMT IO [(MemberId, Exp)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse TAlt -> TCMT IO (MemberId, Exp)
compileAlt [TAlt]
alts
        let obj :: Exp
obj = 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. Ord k => [(k, a)] -> Map k a
Map.fromList [(MemberId, Exp)]
alts'
        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 (VerboseLevel -> LocalId
LocalId VerboseLevel
sc), Exp
obj]
          (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
$ VerboseLevel -> LocalId
LocalId VerboseLevel
sc) MemberId
memId) [Exp
obj]
          (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 (VerboseLevel -> LocalId
LocalId VerboseLevel
sc)) [Exp
obj]
          (Defn, Maybe String)
_ -> TCM Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
      T.TCase VerboseLevel
_ 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.TCoerce TTerm
t -> TTerm -> TCM Exp
go TTerm
t

    unit :: TCM Exp
unit = 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
$ Integer -> Exp
Integer Integer
0

compilePrim :: T.TPrim -> Exp
compilePrim :: TPrim -> Exp
compilePrim TPrim
p =
  case TPrim
p of
    TPrim
T.PIf -> VerboseLevel -> Exp -> Exp
curriedLambda VerboseLevel
3 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp -> Exp
If (VerboseLevel -> Exp
local VerboseLevel
2) (VerboseLevel -> Exp
local VerboseLevel
1) (VerboseLevel -> Exp
local VerboseLevel
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 = VerboseLevel -> Exp -> Exp
curriedLambda VerboseLevel
2 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (String -> Exp
PlainJS String
js) [VerboseLevel -> Exp
local VerboseLevel
1, VerboseLevel -> Exp
local VerboseLevel
0]
        unOp :: String -> Exp
unOp String
js  = VerboseLevel -> Exp -> Exp
curriedLambda VerboseLevel
1 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (String -> Exp
PlainJS String
js) [VerboseLevel -> Exp
local VerboseLevel
0]
        primEq :: Exp
primEq   = VerboseLevel -> Exp -> Exp
curriedLambda VerboseLevel
2 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> String -> Exp -> Exp
BinOp (VerboseLevel -> Exp
local VerboseLevel
1) String
"===" (VerboseLevel -> Exp
local VerboseLevel
0)


compileAlt :: T.TAlt -> TCM (MemberId, Exp)
compileAlt :: TAlt -> TCMT IO (MemberId, Exp)
compileAlt TAlt
a = case TAlt
a of
  T.TACon QName
con VerboseLevel
ar TTerm
body -> do
    MemberId
memId <- QName -> TCM MemberId
visitorName QName
con
    Exp
body <- VerboseLevel -> Exp -> Exp
Lambda VerboseLevel
ar (Exp -> Exp) -> TCM Exp -> TCM Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM Exp
compileTerm TTerm
body
    (MemberId, Exp) -> TCMT IO (MemberId, Exp)
forall (m :: * -> *) a. Monad m => a -> m a
return (MemberId
memId, Exp
body)
  TAlt
_ -> TCMT IO (MemberId, Exp)
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

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

literal :: Literal -> Exp
literal :: Literal -> Exp
literal Literal
l = case Literal
l of
  (LitNat    Range
_ Integer
x) -> Integer -> Exp
Integer Integer
x
  (LitWord64 Range
_ Hash
x) -> Integer -> Exp
Integer (Hash -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Hash
x)
  (LitFloat  Range
_ Double
x) -> Double -> Exp
Double  Double
x
  (LitString Range
_ String
x) -> String -> Exp
String  String
x
  (LitChar   Range
_ Char
x) -> Char -> Exp
Char    Char
x
  (LitQName  Range
_ 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
$ [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (String -> MemberId
mem String
"id", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Hash -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Hash
n)
    , (String -> MemberId
mem String
"moduleId", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Hash -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Hash
m)
    , (String -> MemberId
mem String
"name", String -> Exp
String (String -> Exp) -> String -> Exp
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 Hash
n Hash
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
$ [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
      [ (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   = String -> Exp
String String
"non-assoc"
    litAssoc Associativity
LeftAssoc  = String -> Exp
String String
"left-assoc"
    litAssoc Associativity
RightAssoc = String -> Exp
String String
"right-assoc"

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

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

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

outFile :: GlobalId -> TCM FilePath
outFile :: GlobalId -> TCMT IO String
outFile GlobalId
m = do
  String
mdir <- TCMT IO 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 () -> TCM ()
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO () -> TCM ()) -> IO () -> TCM ()
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
curMName
  GlobalId -> TCMT IO String
outFile (ModuleName -> GlobalId
jsMod ModuleName
m)

copyRTEModules :: TCM ()
copyRTEModules :: TCM ()
copyRTEModules = do
  String
dataDir <- IO String -> TCMT IO String
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift IO String
getDataDir
  let srcDir :: String
srcDir = String
dataDir String -> String -> String
</> String
"JS"
  (IO () -> TCM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO () -> TCM ()) -> (String -> IO ()) -> String -> TCM ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> IO ()
copyDirContent String
srcDir) (String -> TCM ()) -> TCMT IO String -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO String
compileDir

-- | Primitives implemented in the JS Agda RTS.
primitives :: Set String
primitives :: Set String
primitives = [String] -> Set String
forall a. Ord a => [a] -> Set a
Set.fromList
  [ String
"primExp"
  , String
"primFloatDiv"
  , String
"primFloatEquality"
  , String
"primFloatLess"
  , String
"primFloatNumericalEquality"
  , String
"primFloatNumericalLess"
  , String
"primFloatNegate"
  , String
"primFloatMinus"
  , String
"primFloatPlus"
  , String
"primFloatSqrt"
  , String
"primFloatTimes"
  , String
"primNatMinus"
  , String
"primShowFloat"
  , String
"primShowInteger"
  , String
"primSin"
  , String
"primCos"
  , String
"primTan"
  , String
"primASin"
  , String
"primACos"
  , String
"primATan"
  , String
"primATan2"
  , String
"primShowQName"
  , String
"primQNameEquality"
  , String
"primQNameLess"
  , String
"primQNameFixity"
  , String
"primWord64ToNat"
  , String
"primWord64FromNat"
  ]