module Agda.Compiler.JS.Compiler where
import Prelude hiding ( null, writeFile )
import Control.DeepSeq
import Control.Monad.Trans
import Data.Char ( isSpace )
import Data.Foldable ( forM_ )
import Data.List ( dropWhileEnd, elemIndex, intercalate, partition )
import Data.Set ( Set )
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.Text as T
import GHC.Generics (Generic)
import System.Directory ( createDirectoryIfMissing )
import System.Environment ( setEnv )
import System.FilePath ( splitFileName, (</>) )
import System.Process ( callCommand )
import Paths_Agda
import Agda.Interaction.Options
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name ( isNoName )
import Agda.Syntax.Abstract.Name
( QName,
mnameToList, qnameName, qnameModule, nameId )
import Agda.Syntax.Internal
( Name, Type
, nameFixity, unDom, telToList )
import Agda.Syntax.Literal ( Literal(..) )
import Agda.Syntax.TopLevelModuleName (TopLevelModuleName, TopLevelModuleName'(..))
import Agda.Syntax.Treeless ( ArgUsage(..), filterUsed )
import qualified Agda.Syntax.Treeless as T
import Agda.TypeChecking.Monad
import Agda.TypeChecking.Reduce ( instantiateFull )
import Agda.TypeChecking.Substitute as TC ( TelV(..), raise, subst )
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Telescope ( telViewPath )
import Agda.Utils.FileName ( isNewerThan )
import Agda.Utils.Function ( iterate' )
import Agda.Utils.List ( downFrom, headWithDefault )
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Maybe ( boolToMaybe, catMaybes, caseMaybeM, fromMaybe, whenNothing )
import Agda.Utils.Monad ( ifM, when )
import Agda.Utils.Null ( null )
import Agda.Syntax.Common.Pretty (prettyShow, render)
import qualified Agda.Syntax.Common.Pretty as P
import Agda.Utils.IO.Directory
import Agda.Utils.IO.UTF8 ( writeFile )
import Agda.Utils.Singleton ( singleton )
import Agda.Utils.Size (size)
import Agda.Compiler.Common as CC
import Agda.Compiler.ToTreeless
import Agda.Compiler.Treeless.EliminateDefaults
import Agda.Compiler.Treeless.EliminateLiteralPatterns
import Agda.Compiler.Treeless.GuardsToPrims
import Agda.Compiler.Treeless.Erase ( computeErasedConstructorArgs )
import Agda.Compiler.Treeless.Subst ()
import Agda.Compiler.Backend (Backend,Backend_boot(..), Backend',Backend'_boot(..), Recompile(..))
import Agda.Compiler.JS.Syntax
( Exp(Self,Local,Global,Undefined,Null,String,Char,Integer,Double,Lambda,Object,Array,Apply,Lookup,If,BinOp,PlainJS),
LocalId(LocalId), GlobalId(GlobalId), MemberId(MemberId,MemberIndex), Export(Export), Module(Module, modName, callMain), Comment(Comment),
modName, expName, uses
, JSQName
)
import Agda.Compiler.JS.Substitution
( curriedLambda, curriedApply, emp, apply )
import qualified Agda.Compiler.JS.Pretty as JSPretty
import Agda.Compiler.JS.Pretty (JSModuleStyle(..))
import Agda.Utils.Impossible (__IMPOSSIBLE__)
jsBackend :: Backend
jsBackend :: Backend
jsBackend = Backend'_boot
(TCMT IO) JSOptions JSOptions JSModuleEnv Module (Maybe Export)
-> Backend
forall opts (tcm :: * -> *) env menv mod def.
NFData opts =>
Backend'_boot tcm opts env menv mod def -> Backend_boot tcm
Backend Backend'_boot
(TCMT IO) JSOptions JSOptions JSModuleEnv Module (Maybe Export)
jsBackend'
jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export)
jsBackend' :: Backend'_boot
(TCMT IO) 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 -> TCMT IO JSOptions
preCompile = JSOptions -> TCMT IO JSOptions
jsPreCompile
, postCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
postCompile = JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
jsPostCompile
, preModule :: JSOptions
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCMT IO (Recompile JSModuleEnv Module)
preModule = JSOptions
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCMT IO (Recompile JSModuleEnv Module)
jsPreModule
, postModule :: JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [Maybe Export]
-> TCMT IO Module
postModule = JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [Maybe Export]
-> TCMT IO Module
jsPostModule
, compileDef :: JSOptions
-> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
compileDef = JSOptions
-> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
jsCompileDef
, scopeCheckingSuffices :: Bool
scopeCheckingSuffices = Bool
False
, mayEraseType :: QName -> TCMT IO Bool
mayEraseType = TCMT IO Bool -> QName -> TCMT IO Bool
forall a b. a -> b -> a
const (TCMT IO Bool -> QName -> TCMT IO Bool)
-> TCMT IO Bool -> QName -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
}
data JSOptions = JSOptions
{ JSOptions -> Bool
optJSCompile :: Bool
, JSOptions -> Bool
optJSOptimize :: Bool
, JSOptions -> Bool
optJSMinify :: Bool
, JSOptions -> Bool
optJSVerify :: Bool
, JSOptions -> JSModuleStyle
optJSModuleStyle :: JSModuleStyle
}
deriving (forall x. JSOptions -> Rep JSOptions x)
-> (forall x. Rep JSOptions x -> JSOptions) -> Generic JSOptions
forall x. Rep JSOptions x -> JSOptions
forall x. JSOptions -> Rep JSOptions x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. JSOptions -> Rep JSOptions x
from :: forall x. JSOptions -> Rep JSOptions x
$cto :: forall x. Rep JSOptions x -> JSOptions
to :: forall x. Rep JSOptions x -> JSOptions
Generic
instance NFData JSModuleStyle
instance NFData JSOptions
defaultJSOptions :: JSOptions
defaultJSOptions :: JSOptions
defaultJSOptions = JSOptions
{ optJSCompile :: Bool
optJSCompile = Bool
False
, optJSOptimize :: Bool
optJSOptimize = Bool
False
, optJSMinify :: Bool
optJSMinify = Bool
False
, optJSVerify :: Bool
optJSVerify = Bool
False
, optJSModuleStyle :: JSModuleStyle
optJSModuleStyle = JSModuleStyle
JSCJS
}
jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
jsCommandLineFlags :: [OptDescr (Flag JSOptions)]
jsCommandLineFlags =
[ String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enable) String
"compile program using the JS backend"
, String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-optimize"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enableOpt) String
"turn on optimizations during JS code generation"
, String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-minify"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enableMin) String
"minify generated JS code"
, String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-verify"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
enableVerify) String
"except for main module, run generated JS modules through `node` (needs to be in PATH)"
, String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-cjs"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
setCJS) String
"use CommonJS module style (default)"
, String
-> [String]
-> ArgDescr (Flag JSOptions)
-> String
-> OptDescr (Flag JSOptions)
forall a. String -> [String] -> ArgDescr a -> String -> OptDescr a
Option [] [String
"js-amd"] (Flag JSOptions -> ArgDescr (Flag JSOptions)
forall a. a -> ArgDescr a
NoArg Flag JSOptions
forall {f :: * -> *}. Applicative f => JSOptions -> f JSOptions
setAMD) String
"use AMD module style for JS"
]
where
enable :: JSOptions -> f JSOptions
enable JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSCompile = True }
enableOpt :: JSOptions -> f JSOptions
enableOpt JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSOptimize = True }
enableMin :: JSOptions -> f JSOptions
enableMin JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSMinify = True }
enableVerify :: JSOptions -> f JSOptions
enableVerify JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSVerify = True }
setCJS :: JSOptions -> f JSOptions
setCJS JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSModuleStyle = JSCJS }
setAMD :: JSOptions -> f JSOptions
setAMD JSOptions
o = JSOptions -> f JSOptions
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure JSOptions
o{ optJSModuleStyle = JSAMD }
jsPreCompile :: JSOptions -> TCM JSOptions
jsPreCompile :: JSOptions -> TCMT IO JSOptions
jsPreCompile JSOptions
opts = do
cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
let 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 cubical of
Maybe Cubical
Nothing -> () -> TCMT IO ()
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Just Cubical
CErased -> String -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
notSupported String
"--erased-cubical"
Just Cubical
CFull -> String -> TCMT IO ()
forall {m :: * -> *} {a}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
notSupported String
"--cubical"
return opts
jsPostCompile ::
JSOptions -> IsMain -> Map.Map TopLevelModuleName Module -> TCM ()
jsPostCompile :: JSOptions -> IsMain -> Map TopLevelModuleName Module -> TCMT IO ()
jsPostCompile JSOptions
opts IsMain
_ Map TopLevelModuleName Module
ms = do
compDir <- TCMT IO String
forall (m :: * -> *). HasOptions m => m String
compileDir
liftIO $ do
dataDir <- getDataDir
let fname = case JSOptions -> JSModuleStyle
optJSModuleStyle JSOptions
opts of
JSModuleStyle
JSCJS -> String
"agda-rts.js"
JSModuleStyle
JSAMD -> String
"agda-rts.amd.js"
srcPath = String
dataDir String -> String -> String
</> String
"JS" String -> String -> String
</> String
fname
compPath = String
compDir String -> String -> String
</> String
fname
copyIfChanged srcPath compPath
reportSLn "compile.js.verify" 10 $ "Considering to verify generated JS modules"
when (optJSVerify opts) $ do
reportSLn "compile.js.verify" 10 $ "Verifying generated JS modules"
liftIO $ setEnv "NODE_PATH" compDir
forM_ ms $ \ Module{ GlobalId
modName :: Module -> GlobalId
modName :: GlobalId
modName, Maybe Exp
callMain :: Module -> Maybe Exp
callMain :: Maybe Exp
callMain } -> do
jsFile <- GlobalId -> TCMT IO String
outFile GlobalId
modName
reportSLn "compile.js.verify" 30 $ unwords [ "Considering JS module:" , jsFile ]
whenNothing callMain $ do
let cmd = [String] -> String
unwords [ String
"node", String
"-", String
"<", String
jsFile ]
reportSLn "compile.js.verify" 20 $ unwords [ "calling:", cmd ]
liftIO $ callCommand cmd
data JSModuleEnv = JSModuleEnv
{ JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit :: Maybe CoinductionKit
, JSModuleEnv -> Bool
jsCompile :: Bool
}
jsPreModule ::
JSOptions -> IsMain -> TopLevelModuleName -> Maybe FilePath ->
TCM (Recompile JSModuleEnv Module)
jsPreModule :: JSOptions
-> IsMain
-> TopLevelModuleName
-> Maybe String
-> TCMT IO (Recompile JSModuleEnv Module)
jsPreModule JSOptions
_opts IsMain
_ TopLevelModuleName
m Maybe String
mifile = do
cubical <- TCMT IO (Maybe Cubical)
forall (m :: * -> *). HasOptions m => m (Maybe Cubical)
cubicalOption
let compile = case Maybe Cubical
cubical of
Just Cubical
CFull -> Bool
False
Just Cubical
CErased -> Bool
True
Maybe Cubical
Nothing -> Bool
True
ifM uptodate noComp (yesComp compile)
where
uptodate :: TCMT IO Bool
uptodate = case Maybe String
mifile of
Maybe String
Nothing -> Bool -> TCMT IO Bool
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
Just String
ifile -> IO Bool -> TCMT IO Bool
forall a. IO a -> TCMT IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Bool -> TCMT IO Bool) -> TCMT IO (IO Bool) -> TCMT IO Bool
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< String -> String -> IO Bool
isNewerThan (String -> String -> IO Bool)
-> TCMT IO String -> TCMT IO (String -> IO Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO String
outFile_ TCMT IO (String -> IO Bool) -> TCMT IO String -> TCMT IO (IO Bool)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> String -> TCMT IO String
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
ifile
ifileDesc :: String
ifileDesc = String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe String
"(memory)" Maybe String
mifile
noComp :: TCMT IO (Recompile JSModuleEnv Module)
noComp = do
String -> Int -> String -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> String -> m ()
reportSLn String
"compile.js" Int
2 (String -> TCMT IO ())
-> (TopLevelModuleName -> String)
-> TopLevelModuleName
-> TCMT IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" : no compilation is needed.") (String -> String)
-> (TopLevelModuleName -> String) -> TopLevelModuleName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow (TopLevelModuleName -> TCMT IO ())
-> TCMT IO TopLevelModuleName -> TCMT IO ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
Recompile JSModuleEnv Module
-> TCMT IO (Recompile JSModuleEnv Module)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Recompile JSModuleEnv Module
-> TCMT IO (Recompile JSModuleEnv Module))
-> Recompile JSModuleEnv Module
-> TCMT IO (Recompile JSModuleEnv Module)
forall a b. (a -> b) -> a -> b
$ Module -> Recompile JSModuleEnv Module
forall menv mod. mod -> Recompile menv mod
Skip Module
skippedModule
skippedModule :: Module
skippedModule = GlobalId -> [GlobalId] -> [Export] -> Maybe Exp -> Module
Module (TopLevelModuleName -> GlobalId
jsMod TopLevelModuleName
m) [GlobalId]
forall a. Monoid a => a
mempty [Export]
forall a. Monoid a => a
mempty (Exp -> Maybe Exp
forall a. a -> Maybe a
Just Exp
forall a. HasCallStack => a
__IMPOSSIBLE__)
yesComp :: Bool -> TCMT IO (Recompile JSModuleEnv Module)
yesComp Bool
compile = do
m <- TopLevelModuleName -> String
forall a. Pretty a => a -> String
prettyShow (TopLevelModuleName -> String)
-> TCMT IO TopLevelModuleName -> TCMT IO String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
out <- outFile_
alwaysReportSLn "compile.js" 1 $ repl [m, ifileDesc, out] "Compiling <<0>> in <<1>> to <<2>>"
kit <- coinductionKit
return $ Recompile $ JSModuleEnv
{ jsCoinductionKit = kit
, jsCompile = compile
}
jsPostModule ::
JSOptions -> JSModuleEnv -> IsMain -> TopLevelModuleName ->
[Maybe Export] -> TCM Module
jsPostModule :: JSOptions
-> JSModuleEnv
-> IsMain
-> TopLevelModuleName
-> [Maybe Export]
-> TCMT IO Module
jsPostModule JSOptions
opts JSModuleEnv
_ IsMain
isMain TopLevelModuleName
_ [Maybe Export]
defs = do
m <- TopLevelModuleName -> GlobalId
jsMod (TopLevelModuleName -> GlobalId)
-> TCMT IO TopLevelModuleName -> TCMT IO GlobalId
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
is <- map (jsMod . fst) . iImportedModules <$> curIF
let mod = GlobalId -> [GlobalId] -> [Export] -> Maybe Exp -> Module
Module GlobalId
m [GlobalId]
is ([Export] -> [Export]
reorder [Export]
es) Maybe Exp
callMain
writeModule (optJSMinify opts) (optJSModuleStyle opts) mod
return mod
where
es :: [Export]
es = [Maybe Export] -> [Export]
forall a. [Maybe a] -> [a]
catMaybes [Maybe Export]
defs
main :: MemberId
main = String -> MemberId
MemberId String
"main"
hasMain :: Bool
hasMain = IsMain
isMain IsMain -> IsMain -> Bool
forall a. Eq a => a -> a -> Bool
== IsMain
IsMain Bool -> Bool -> Bool
&& (Export -> Bool) -> [Export] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((MemberId -> JSQName
forall el coll. Singleton el coll => el -> coll
singleton MemberId
main JSQName -> JSQName -> Bool
forall a. Eq a => a -> a -> Bool
==) (JSQName -> Bool) -> (Export -> JSQName) -> Export -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Export -> JSQName
expName) [Export]
es
callMain :: Maybe Exp
callMain :: Maybe Exp
callMain = Bool -> Exp -> Maybe Exp
forall a. Bool -> a -> Maybe a
boolToMaybe Bool
hasMain (Exp -> Maybe Exp) -> Exp -> Maybe Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup Exp
Self MemberId
main) [Int -> Exp -> Exp
Lambda Int
1 Exp
emp]
jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export)
jsCompileDef :: JSOptions
-> JSModuleEnv -> IsMain -> Definition -> TCMT IO (Maybe Export)
jsCompileDef JSOptions
opts JSModuleEnv
kit IsMain
_isMain Definition
def = EnvWithOpts -> (QName, Definition) -> TCMT IO (Maybe Export)
definition (JSOptions
opts, JSModuleEnv
kit) (Definition -> QName
defName Definition
def, Definition
def)
prefix :: [Char]
prefix :: String
prefix = String
"jAgda"
jsMod :: TopLevelModuleName -> GlobalId
jsMod :: TopLevelModuleName -> GlobalId
jsMod TopLevelModuleName
m =
[String] -> GlobalId
GlobalId (String
prefix String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
T.unpack (TopLevelModuleNameParts -> [Item TopLevelModuleNameParts]
forall l. IsList l => l -> [Item l]
List1.toList (TopLevelModuleName -> TopLevelModuleNameParts
forall range. TopLevelModuleName' range -> TopLevelModuleNameParts
moduleNameParts TopLevelModuleName
m)))
jsFileName :: 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
| Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
n = String -> MemberId
MemberId (String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NameId -> String
forall a. Show a => a -> String
show (Name -> NameId
nameId Name
n))
| Bool
otherwise = String -> MemberId
MemberId (String -> MemberId) -> String -> MemberId
forall a b. (a -> b) -> a -> b
$ Name -> String
forall a. Pretty a => a -> String
prettyShow Name
n
global' :: QName -> TCM (Exp, JSQName)
global' :: QName -> TCM (Exp, JSQName)
global' QName
q = do
i <- Interface -> TopLevelModuleName
iTopLevelModuleName (Interface -> TopLevelModuleName)
-> TCMT IO Interface -> TCMT IO TopLevelModuleName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Interface
forall (m :: * -> *). ReadTCState m => m Interface
curIF
top <- CC.topLevelModuleName (qnameModule q)
let
qms = ModuleName -> [Name]
mnameToList (ModuleName -> [Name]) -> ModuleName -> [Name]
forall a b. (a -> b) -> a -> b
$ QName -> ModuleName
qnameModule QName
q
localms = Int -> [Name] -> [Name]
forall a. Int -> [a] -> [a]
drop (TopLevelModuleName -> Int
forall a. Sized a => a -> Int
size TopLevelModuleName
top) [Name]
qms
nm = (Name -> MemberId) -> NonEmpty Name -> JSQName
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> MemberId
jsMember (NonEmpty Name -> JSQName) -> NonEmpty Name -> JSQName
forall a b. (a -> b) -> a -> b
$ [Name] -> Name -> NonEmpty Name
forall a. [a] -> a -> List1 a
List1.snoc [Name]
localms (Name -> NonEmpty Name) -> Name -> NonEmpty Name
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
if top == i
then return (Self, nm)
else return (Global (jsMod top), nm)
global :: QName -> TCM (Exp, JSQName)
global :: QName -> TCM (Exp, JSQName)
global QName
q = do
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case d of
Defn { theDef :: Definition -> Defn
theDef = Constructor { conData :: Defn -> QName
conData = QName
p } } -> do
QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
p TCMT IO Definition
-> (Definition -> TCM (Exp, JSQName)) -> TCM (Exp, JSQName)
forall a b. TCMT IO a -> (a -> TCMT IO b) -> TCMT IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Defn { theDef :: Definition -> Defn
theDef = Record { recNamedCon :: Defn -> Bool
recNamedCon = Bool
False } } -> do
(m,ls) <- QName -> TCM (Exp, JSQName)
global' QName
p
return (m, ls <> singleton (MemberId "record"))
Definition
_ -> QName -> TCM (Exp, JSQName)
global' (Definition -> QName
defName Definition
d)
Definition
_ -> QName -> TCM (Exp, JSQName)
global' (Definition -> QName
defName Definition
d)
reorder :: [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
type EnvWithOpts = (JSOptions, JSModuleEnv)
definition :: EnvWithOpts -> (QName,Definition) -> TCM (Maybe Export)
definition :: EnvWithOpts -> (QName, Definition) -> TCMT IO (Maybe Export)
definition EnvWithOpts
kit (QName
q,Definition
d) = do
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
10 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compiling def:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
(_,ls) <- QName -> TCM (Exp, JSQName)
global QName
q
d <- instantiateFull d
definition' kit q d (defType d) ls
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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) ((CompilerPragma -> TCMT IO ()) -> TCMT IO ())
-> (CompilerPragma -> TCMT IO ()) -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ \ (CompilerPragma Range
r String
s) ->
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 a. a -> TCMT IO a
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 -> TCMT IO (Maybe Export)
definition' EnvWithOpts
kit QName
q Definition
d Type
t JSQName
ls =
if Bool -> Bool
not (JSModuleEnv -> Bool
jsCompile (EnvWithOpts -> JSModuleEnv
forall a b. (a, b) -> b
snd EnvWithOpts
kit)) Bool -> Bool -> Bool
|| Bool -> Bool
not (Definition -> Bool
forall a. LensModality a => a -> Bool
usableModality Definition
d)
then Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Export
forall a. Maybe a
Nothing
else do
QName -> TCMT IO ()
checkCompilerPragmas QName
q
case Definition -> Defn
theDef Definition
d of
Constructor{}
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfSharp (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (EnvWithOpts -> JSModuleEnv
forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Export
forall a. Maybe a
Nothing
Function{}
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfFlat (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (EnvWithOpts -> JSModuleEnv
forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
Exp -> TCMT IO (Maybe Export)
ret (Exp -> TCMT IO (Maybe Export)) -> Exp -> TCMT IO (Maybe Export)
forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
Lambda Int
1 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
Apply (Exp -> MemberId -> Exp
Lookup (Int -> Exp
local Int
0) MemberId
flatName) []
DataOrRecSig{} -> TCMT IO (Maybe Export)
forall a. HasCallStack => a
__IMPOSSIBLE__
Axiom{} | Just String
e <- Definition -> Maybe String
defJSDef Definition
d -> String -> TCMT IO (Maybe Export)
plainJS String
e
Axiom{} | Bool
otherwise -> Exp -> TCMT IO (Maybe Export)
ret Exp
Undefined
GeneralizableVar{} -> Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Export
forall a. Maybe a
Nothing
Function{} | Just String
e <- Definition -> Maybe String
defJSDef Definition
d -> String -> TCMT IO (Maybe Export)
plainJS String
e
Function{} | Bool
otherwise -> do
String -> Int -> TCMT IO Doc -> TCMT IO ()
forall (m :: * -> *).
MonadDebug m =>
String -> Int -> TCMT IO Doc -> m ()
reportSDoc String
"compile.js" Int
5 (TCMT IO Doc -> TCMT IO ()) -> TCMT IO Doc -> TCMT IO ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Doc
"compiling fun:" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> QName -> TCMT IO Doc
forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
forall (m :: * -> *). MonadPretty m => QName -> m Doc
prettyTCM QName
q
TCMT IO (Maybe TTerm)
-> TCMT IO (Maybe Export)
-> (TTerm -> TCMT IO (Maybe Export))
-> TCMT IO (Maybe Export)
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (EvaluationStrategy -> QName -> TCMT IO (Maybe TTerm)
toTreeless EvaluationStrategy
T.EagerEvaluation QName
q) (Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe Export
forall a. Maybe a
Nothing) ((TTerm -> TCMT IO (Maybe Export)) -> TCMT IO (Maybe Export))
-> (TTerm -> TCMT IO (Maybe Export)) -> TCMT IO (Maybe Export)
forall a b. (a -> b) -> a -> b
$ \ TTerm
treeless -> do
used <- [ArgUsage] -> Maybe [ArgUsage] -> [ArgUsage]
forall a. a -> Maybe a -> a
fromMaybe [] (Maybe [ArgUsage] -> [ArgUsage])
-> TCMT IO (Maybe [ArgUsage]) -> TCMT IO [ArgUsage]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO (Maybe [ArgUsage])
forall (m :: * -> *).
HasConstInfo m =>
QName -> m (Maybe [ArgUsage])
getCompiledArgUse QName
q
funBody <- eliminateCaseDefaults =<<
eliminateLiteralPatterns
(convertGuards treeless)
reportSDoc "compile.js" 30 $ " compiled treeless fun:" <+> pretty funBody
reportSDoc "compile.js" 40 $ " argument usage:" <+> (text . show) used
let (body, given) = lamView funBody
where
lamView :: T.TTerm -> (T.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)
etaN = [ArgUsage] -> Int
forall a. [a] -> 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 = [ArgUsage] -> Int
forall a. [a] -> 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
funBody' <- compileTerm kit
$ iterate' (given + etaN - unusedN) T.TLam
$ eraseLocalVars (map (== ArgUnused) used)
$ T.mkTApp (raise etaN body) (T.TVar <$> downFrom etaN)
reportSDoc "compile.js" 30 $ " compiled JS fun:" <+> (text . show) funBody'
return $
if funBody' == Null then Nothing
else Just $ Export ls funBody'
Primitive{primName :: Defn -> PrimitiveId
primName = PrimitiveId
p}
| PrimitiveId
p PrimitiveId -> PrimitiveId -> Bool
forall a. Eq a => a -> a -> Bool
== PrimitiveId
builtin_glueU ->
String -> TCMT IO (Maybe Export)
plainJS String
"agdaRTS.prim_glueU"
| PrimitiveId
p PrimitiveId -> PrimitiveId -> Bool
forall a. Eq a => a -> a -> Bool
== PrimitiveId
builtin_unglueU ->
String -> TCMT IO (Maybe Export)
plainJS String
"agdaRTS.prim_unglueU"
| PrimitiveId
p PrimitiveId -> Set PrimitiveId -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set PrimitiveId
primitives ->
String -> TCMT IO (Maybe Export)
plainJS (String -> TCMT IO (Maybe Export))
-> String -> TCMT IO (Maybe Export)
forall a b. (a -> b) -> a -> b
$ String
"agdaRTS." String -> String -> String
forall a. [a] -> [a] -> [a]
++ PrimitiveId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
p
| Just String
e <- Definition -> Maybe String
defJSDef Definition
d ->
String -> TCMT IO (Maybe Export)
plainJS String
e
| Bool
otherwise ->
Exp -> TCMT IO (Maybe Export)
ret Exp
Undefined
PrimitiveSort{} -> Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Export
forall a. Maybe a
Nothing
Datatype{} -> do
QName -> TCMT IO ()
computeErasedConstructorArgs QName
q
Exp -> TCMT IO (Maybe Export)
ret Exp
emp
Record{} -> do
QName -> TCMT IO ()
computeErasedConstructorArgs QName
q
Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Export
forall a. Maybe a
Nothing
Constructor{} | Just String
e <- Definition -> Maybe String
defJSDef Definition
d -> String -> TCMT IO (Maybe Export)
plainJS String
e
Constructor{conData :: Defn -> QName
conData = QName
p, conPars :: Defn -> Int
conPars = Int
nc} -> do
TelV tel _ <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *). PureTCM m => Type -> m (TelV Type)
telViewPath Type
t
let np = [Dom (String, Type)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
tel) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nc
erased <- getErasedConArgs q
let nargs = Int
np Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Bool] -> Int
forall a. [a] -> 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 = [ LocalId -> Exp
Local (LocalId -> Exp) -> LocalId -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId (Int -> LocalId) -> Int -> LocalId
forall a b. (a -> b) -> a -> b
$ Int
nargs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
i | Int
i <- [Int
0 .. Int
nargsInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]
d <- getConstInfo p
let l = JSQName -> MemberId
forall a. NonEmpty a -> a
List1.last JSQName
ls
case theDef d of
Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName]
flds } -> Exp -> TCMT IO (Maybe Export)
ret (Exp -> TCMT IO (Maybe Export)) -> Exp -> TCMT IO (Maybe Export)
forall a b. (a -> b) -> a -> b
$ Int -> Exp -> Exp
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
i <- TCM MemberId
index
ret $ curriedLambda (nargs + 1) $ Apply (Lookup (Local (LocalId 0)) i) 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
q <- QName -> TCMT IO QName
forall (m :: * -> *). HasConstInfo m => QName -> m QName
canonicalName QName
q
cs <- mapM canonicalName $ defConstructors dt
case q `elemIndex` cs of
Just Int
i -> MemberId -> TCM MemberId
forall a. a -> TCMT IO a
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 a. a -> TCMT IO a
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{} -> TCMT IO (Maybe Export)
forall a. HasCallStack => a
__IMPOSSIBLE__
where
ret :: Exp -> TCMT IO (Maybe Export)
ret = Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Export -> TCMT IO (Maybe Export))
-> (Exp -> Maybe Export) -> Exp -> TCMT IO (Maybe Export)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Export -> Maybe Export
forall a. a -> Maybe a
Just (Export -> Maybe Export) -> (Exp -> Export) -> Exp -> Maybe Export
forall b c a. (b -> c) -> (a -> b) -> a -> c
. JSQName -> Exp -> Export
Export JSQName
ls
plainJS :: String -> TCMT IO (Maybe Export)
plainJS = Maybe Export -> TCMT IO (Maybe Export)
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe Export -> TCMT IO (Maybe Export))
-> (String -> Maybe Export) -> String -> TCMT IO (Maybe Export)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Export -> Maybe Export
forall a. a -> Maybe a
Just (Export -> Maybe Export)
-> (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 a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ LocalId -> Exp
Local (LocalId -> Exp) -> LocalId -> Exp
forall a b. (a -> b) -> a -> b
$ Int -> LocalId
LocalId Int
x
T.TDef QName
q -> do
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case theDef d of
Datatype {} -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Exp
String Text
"*")
Record {} -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Text -> Exp
String Text
"*")
Defn
_ -> QName -> TCM Exp
qname QName
q
T.TApp (T.TCon QName
q) [TTerm
x]
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== (CoinductionKit -> QName
nameOfSharp (CoinductionKit -> QName) -> Maybe CoinductionKit -> Maybe QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> JSModuleEnv -> Maybe CoinductionKit
jsCoinductionKit (EnvWithOpts -> JSModuleEnv
forall a b. (a, b) -> b
snd EnvWithOpts
kit)) -> do
x <- TTerm -> TCM Exp
go TTerm
x
let evalThunk = [String] -> String
unlines
[ String
"function() {"
, String
" delete this.flat;"
, String
" var result = this.__flat_helper();"
, String
" delete this.__flat_helper;"
, String
" this.flat = function() { return result; };"
, String
" return result;"
, String
"}"
]
return $ Object $ Map.fromListWith __IMPOSSIBLE__
[(flatName, PlainJS evalThunk)
,(MemberId "__flat_helper", Lambda 0 x)]
T.TApp TTerm
t' [TTerm]
xs | Just Either QName QName
f <- TTerm -> Maybe (Either QName QName)
getDef TTerm
t' -> do
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
let given = [TTerm] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TTerm]
xs
etaN = [ArgUsage] -> Int
forall a. [a] -> 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 = [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)
curriedLambda etaN <$> (curriedApply <$> go (raise etaN t') <*> mapM go 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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> TCM Exp) -> [TTerm] -> TCMT IO [Exp]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TTerm -> TCM Exp
go [TTerm]
xs
T.TLam TTerm
t -> Int -> Exp -> Exp
Lambda Int
1 (Exp -> Exp) -> TCM Exp -> TCM Exp
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> TCM Exp
go TTerm
t
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 a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> TCM Exp) -> [TTerm] -> TCMT IO [Exp]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse TTerm -> TCM Exp
go [TTerm
t]
T.TLit Literal
l -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Literal -> Exp
literal Literal
l
T.TCon QName
q -> do
d <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
qname q
T.TCase Int
sc CaseInfo
ct TTerm
def [TAlt]
alts | T.CTData QName
dt <- CaseInfo -> CaseType
T.caseType CaseInfo
ct -> do
dt <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
dt
alts' <- traverse (compileAlt kit) alts
let cs = Defn -> [QName]
defConstructors (Defn -> [QName]) -> Defn -> [QName]
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
dt
obj = Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__ [((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 = [(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 (theDef dt, defJSDef dt) of
(Defn
_, Just String
e) -> do
Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (String -> Exp
PlainJS String
e) [LocalId -> Exp
Local (Int -> LocalId
LocalId Int
sc), Exp
obj]
(Record{}, Maybe String
_) | JSOptions -> Bool
optJSOptimize (EnvWithOpts -> JSOptions
forall a b. (a, b) -> a
fst EnvWithOpts
kit) -> do
Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
apply (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
memId <- QName -> TCM MemberId
visitorName (QName -> TCM MemberId) -> QName -> TCM MemberId
forall a b. (a -> b) -> a -> b
$ Defn -> QName
recCon (Defn -> QName) -> Defn -> QName
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
dt
return $ apply (Lookup (Local $ LocalId sc) memId) [obj]
(Datatype{}, Maybe String
_) | JSOptions -> Bool
optJSOptimize (EnvWithOpts -> JSOptions
forall a b. (a, b) -> a
fst EnvWithOpts
kit) -> do
Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
curriedApply (LocalId -> Exp
Local (Int -> LocalId
LocalId Int
sc)) [Exp
arr]
(Datatype{}, Maybe String
_) -> do
Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ Exp -> [Exp] -> Exp
curriedApply (LocalId -> Exp
Local (Int -> LocalId
LocalId Int
sc)) [Exp
obj]
(Defn, Maybe String)
_ -> TCM Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
T.TCase Int
_ CaseInfo
_ TTerm
_ [TAlt]
_ -> TCM Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
T.TPrim TPrim
p -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Exp -> TCM Exp) -> Exp -> TCM Exp
forall a b. (a -> b) -> a -> b
$ TPrim -> Exp
compilePrim TPrim
p
TTerm
T.TUnit -> TCM Exp
unit
TTerm
T.TSort -> TCM Exp
unit
TTerm
T.TErased -> TCM Exp
unit
T.TError TError
T.TUnreachable -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
Undefined
T.TError T.TMeta{} -> Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
Undefined
T.TCoerce TTerm
t -> TTerm -> TCM Exp
go TTerm
t
getDef :: TTerm -> Maybe (Either QName QName)
getDef (T.TDef QName
f) = Either QName QName -> Maybe (Either QName QName)
forall a. a -> Maybe a
Just (QName -> Either QName QName
forall a b. a -> Either a b
Left QName
f)
getDef (T.TCon QName
c) = Either QName QName -> Maybe (Either QName QName)
forall a. a -> Maybe a
Just (QName -> Either QName QName
forall a b. b -> Either a b
Right QName
c)
getDef (T.TCoerce TTerm
x) = TTerm -> Maybe (Either QName QName)
getDef TTerm
x
getDef TTerm
_ = Maybe (Either QName QName)
forall a. Maybe a
Nothing
unit :: TCM Exp
unit = Exp -> TCM Exp
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Exp
Null
mkArray :: [(Comment, Exp)] -> Exp
mkArray [(Comment, Exp)]
xs
| Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* [(Comment, Exp)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (((Comment, Exp) -> Bool) -> [(Comment, Exp)] -> [(Comment, Exp)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
== Exp
Null) (Exp -> Bool) -> ((Comment, Exp) -> Exp) -> (Comment, Exp) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Comment, Exp) -> Exp
forall a b. (a, b) -> b
snd) [(Comment, Exp)]
xs) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= [(Comment, Exp)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Comment, Exp)]
xs = [(Comment, Exp)] -> Exp
Array [(Comment, Exp)]
xs
| Bool
otherwise = Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
[ (Int -> Comment -> MemberId
MemberIndex Int
i Comment
c, Exp
x) | (Int
i, (Comment
c, Exp
x)) <- [Int] -> [(Comment, Exp)] -> [(Int, (Comment, Exp))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] [(Comment, Exp)]
xs, Exp
x Exp -> Exp -> Bool
forall a. Eq a => a -> a -> Bool
/= Exp
Null ]
compilePrim :: T.TPrim -> Exp
compilePrim :: TPrim -> Exp
compilePrim TPrim
p =
case TPrim
p of
TPrim
T.PIf -> Int -> Exp -> Exp
curriedLambda Int
3 (Exp -> Exp) -> Exp -> Exp
forall a b. (a -> b) -> a -> b
$ Exp -> Exp -> Exp -> Exp
If (Int -> Exp
local Int
2) (Int -> Exp
local Int
1) (Int -> Exp
local Int
0)
TPrim
T.PEqI -> String -> Exp
binOp String
"agdaRTS.uprimIntegerEqual"
TPrim
T.PEqF -> String -> Exp
binOp String
"agdaRTS.uprimFloatEquality"
TPrim
T.PEqQ -> String -> Exp
binOp String
"agdaRTS.uprimQNameEquality"
TPrim
T.PEqS -> Exp
primEq
TPrim
T.PEqC -> Exp
primEq
TPrim
T.PGeq -> String -> Exp
binOp String
"agdaRTS.uprimIntegerGreaterOrEqualThan"
TPrim
T.PLt -> String -> Exp
binOp String
"agdaRTS.uprimIntegerLessThan"
TPrim
T.PAdd -> String -> Exp
binOp String
"agdaRTS.uprimIntegerPlus"
TPrim
T.PSub -> String -> Exp
binOp String
"agdaRTS.uprimIntegerMinus"
TPrim
T.PMul -> String -> Exp
binOp String
"agdaRTS.uprimIntegerMultiply"
TPrim
T.PRem -> String -> Exp
binOp String
"agdaRTS.uprimIntegerRem"
TPrim
T.PQuot -> String -> Exp
binOp String
"agdaRTS.uprimIntegerQuot"
TPrim
T.PAdd64 -> String -> Exp
binOp String
"agdaRTS.uprimWord64Plus"
TPrim
T.PSub64 -> String -> Exp
binOp String
"agdaRTS.uprimWord64Minus"
TPrim
T.PMul64 -> String -> Exp
binOp String
"agdaRTS.uprimWord64Multiply"
TPrim
T.PRem64 -> String -> Exp
binOp String
"agdaRTS.uprimIntegerRem"
TPrim
T.PQuot64 -> String -> Exp
binOp String
"agdaRTS.uprimIntegerQuot"
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
erased <- QName -> TCMT IO [Bool]
forall (m :: * -> *). HasConstInfo m => QName -> m [Bool]
getErasedConArgs QName
con
let nargs = Int
ar Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Bool] -> Int
forall a. [a] -> 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)
memId <- visitorName con
body <- Lambda nargs <$> compileTerm kit (eraseLocalVars erased body)
return ((con, memId), 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 a. [a] -> 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 (m,ls) <- QName -> TCM (Exp, JSQName)
global QName
q; return (List1.last 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
(e,ls) <- QName -> TCM (Exp, JSQName)
global QName
q
return (foldl Lookup e ls)
literal :: Literal -> Exp
literal :: Literal -> Exp
literal = \case
(LitNat Integer
x) -> Integer -> Exp
Integer Integer
x
(LitWord64 Word64
x) -> Integer -> Exp
Integer (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
x)
(LitFloat Double
x) -> Double -> Exp
Double Double
x
(LitString Text
x) -> Text -> Exp
String Text
x
(LitChar Char
x) -> Char -> Exp
Char Char
x
(LitQName QName
x) -> QName -> Exp
litqname QName
x
(LitMeta TopLevelModuleName
_ MetaId
m) -> MetaId -> Exp
litmeta MetaId
m
litqname :: QName -> Exp
litqname :: QName -> Exp
litqname QName
q =
Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
[ (String -> MemberId
mem String
"id", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n)
, (String -> MemberId
mem String
"moduleId", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
m)
, (String -> MemberId
mem String
"name", Text -> Exp
String (Text -> Exp) -> Text -> Exp
forall a b. (a -> b) -> a -> b
$ String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ QName -> String
forall a. Pretty a => a -> String
prettyShow QName
q)
, (String -> MemberId
mem String
"fixity", Fixity -> Exp
litfixity Fixity
fx)]
where
mem :: String -> MemberId
mem = String -> MemberId
MemberId
NameId Word64
n (ModuleNameHash Word64
m) = Name -> NameId
nameId (Name -> NameId) -> Name -> NameId
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
fx :: Fixity
fx = Fixity' -> Fixity
theFixity (Fixity' -> Fixity) -> Fixity' -> Fixity
forall a b. (a -> b) -> a -> b
$ Name -> Fixity'
nameFixity (Name -> Fixity') -> Name -> Fixity'
forall a b. (a -> b) -> a -> b
$ QName -> Name
qnameName QName
q
litfixity :: Fixity -> Exp
litfixity :: Fixity -> Exp
litfixity Fixity
fx = Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
[ (String -> MemberId
mem String
"assoc", Associativity -> Exp
litAssoc (Associativity -> Exp) -> Associativity -> Exp
forall a b. (a -> b) -> a -> b
$ Fixity -> Associativity
fixityAssoc Fixity
fx)
, (String -> MemberId
mem String
"prec", FixityLevel -> Exp
litPrec (FixityLevel -> Exp) -> FixityLevel -> Exp
forall a b. (a -> b) -> a -> b
$ Fixity -> FixityLevel
fixityLevel Fixity
fx)]
litAssoc :: Associativity -> Exp
litAssoc Associativity
NonAssoc = Text -> Exp
String Text
"non-assoc"
litAssoc Associativity
LeftAssoc = Text -> Exp
String Text
"left-assoc"
litAssoc Associativity
RightAssoc = Text -> Exp
String Text
"right-assoc"
litPrec :: FixityLevel -> Exp
litPrec FixityLevel
Unrelated = Text -> Exp
String Text
"unrelated"
litPrec (Related Double
l) = Double -> Exp
Double Double
l
litmeta :: MetaId -> Exp
litmeta :: MetaId -> Exp
litmeta (MetaId Word64
m ModuleNameHash
h) =
Map MemberId Exp -> Exp
Object (Map MemberId Exp -> Exp) -> Map MemberId Exp -> Exp
forall a b. (a -> b) -> a -> b
$ (Exp -> Exp -> Exp) -> [(MemberId, Exp)] -> Map MemberId Exp
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Exp -> Exp -> Exp
forall a. HasCallStack => a
__IMPOSSIBLE__
[ (String -> MemberId
MemberId String
"id", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
m)
, (String -> MemberId
MemberId String
"module", Integer -> Exp
Integer (Integer -> Exp) -> Integer -> Exp
forall a b. (a -> b) -> a -> b
$ Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> Integer) -> Word64 -> Integer
forall a b. (a -> b) -> a -> b
$ ModuleNameHash -> Word64
moduleNameHash ModuleNameHash
h) ]
writeModule :: Bool -> JSModuleStyle -> Module -> TCM ()
writeModule :: Bool -> JSModuleStyle -> Module -> TCMT IO ()
writeModule Bool
minify JSModuleStyle
ms Module
m = do
out <- GlobalId -> TCMT IO String
outFile (Module -> GlobalId
modName Module
m)
liftIO (writeFile out (JSPretty.prettyShow minify ms m))
outFile :: GlobalId -> TCM FilePath
outFile :: GlobalId -> TCMT IO String
outFile GlobalId
m = do
mdir <- TCMT IO String
forall (m :: * -> *). HasOptions m => m String
compileDir
let (fdir, fn) = splitFileName (jsFileName m)
let dir = String
mdir String -> String -> String
</> String
fdir
fp = String
dir String -> String -> String
</> String
fn
liftIO $ createDirectoryIfMissing True dir
return fp
outFile_ :: TCM FilePath
outFile_ :: TCMT IO String
outFile_ = do
m <- TCMT IO TopLevelModuleName
forall (m :: * -> *). ReadTCState m => m TopLevelModuleName
curMName
outFile (jsMod m)
primitives :: Set PrimitiveId
primitives :: Set PrimitiveId
primitives = [PrimitiveId] -> Set PrimitiveId
forall a. Ord a => [a] -> Set a
Set.fromList
[ PrimitiveId
PrimShowInteger
, PrimitiveId
PrimNatMinus
, PrimitiveId
PrimWord64ToNat
, PrimitiveId
PrimWord64FromNat
, PrimitiveId
PrimFloatEquality
, PrimitiveId
PrimFloatInequality
, PrimitiveId
PrimFloatLess
, PrimitiveId
PrimFloatIsInfinite
, PrimitiveId
PrimFloatIsNaN
, PrimitiveId
PrimFloatIsNegativeZero
, PrimitiveId
PrimFloatIsSafeInteger
, PrimitiveId
PrimFloatToWord64
, PrimitiveId
PrimNatToFloat
, PrimitiveId
PrimIntToFloat
, PrimitiveId
PrimRatioToFloat
, PrimitiveId
PrimShowFloat
, PrimitiveId
PrimFloatPlus
, PrimitiveId
PrimFloatMinus
, PrimitiveId
PrimFloatTimes
, PrimitiveId
PrimFloatNegate
, PrimitiveId
PrimFloatDiv
, PrimitiveId
PrimFloatSqrt
, PrimitiveId
PrimFloatExp
, PrimitiveId
PrimFloatLog
, PrimitiveId
PrimFloatSin
, PrimitiveId
PrimFloatCos
, PrimitiveId
PrimFloatTan
, PrimitiveId
PrimFloatASin
, PrimitiveId
PrimFloatACos
, PrimitiveId
PrimFloatATan
, PrimitiveId
PrimFloatATan2
, PrimitiveId
PrimFloatSinh
, PrimitiveId
PrimFloatCosh
, PrimitiveId
PrimFloatTanh
, PrimitiveId
PrimFloatASinh
, PrimitiveId
PrimFloatACosh
, PrimitiveId
PrimFloatATanh
, PrimitiveId
PrimFloatPow
, PrimitiveId
PrimQNameEquality
, PrimitiveId
PrimQNameLess
, PrimitiveId
PrimShowQName
, PrimitiveId
PrimQNameFixity
, PrimitiveId
PrimMetaEquality
, PrimitiveId
PrimMetaLess
, PrimitiveId
PrimShowMeta
, PrimitiveId
PrimMetaToNat
, PrimitiveId
builtinIMin
, PrimitiveId
builtinIMax
, PrimitiveId
builtinINeg
, PrimitiveId
PrimPartial
, PrimitiveId
PrimPartialP
, PrimitiveId
builtinPOr
, PrimitiveId
builtinComp
, PrimitiveId
builtinTrans
, PrimitiveId
builtinHComp
, PrimitiveId
builtinSubOut
, PrimitiveId
builtin_glueU
, PrimitiveId
builtin_unglueU
, PrimitiveId
builtinFaceForall
, PrimitiveId
PrimDepIMin
, PrimitiveId
PrimIdFace
, PrimitiveId
PrimIdPath
, PrimitiveId
builtinIdElim
, PrimitiveId
builtinConId
]