1-- | Main module for JS backend. 2 3module Agda.Compiler.JS.Compiler where 4 5import Prelude hiding ( null, writeFile ) 6 7import Control.DeepSeq 8import Control.Monad.Trans 9 10import Data.Char ( isSpace ) 11import Data.Foldable ( forM_ ) 12import Data.List ( dropWhileEnd, findIndex, intercalate, partition ) 13import Data.Set ( Set ) 14 15import qualified Data.Set as Set 16import qualified Data.Map as Map 17import qualified Data.Text as T 18 19import GHC.Generics (Generic) 20 21import System.Directory ( createDirectoryIfMissing ) 22import System.Environment ( setEnv ) 23import System.FilePath ( splitFileName, (</>) ) 24import System.Process ( callCommand ) 25 26import Paths_Agda 27 28import Agda.Interaction.Options 29 30import Agda.Syntax.Common 31import Agda.Syntax.Concrete.Name ( isNoName ) 32import Agda.Syntax.Abstract.Name 33 ( ModuleName, QName, 34 mnameToList, qnameName, qnameModule, nameId ) 35import Agda.Syntax.Internal 36 ( Name, Type 37 , arity, nameFixity, unDom ) 38import Agda.Syntax.Literal ( Literal(..) ) 39import Agda.Syntax.Treeless ( ArgUsage(..), filterUsed ) 40import qualified Agda.Syntax.Treeless as T 41 42import Agda.TypeChecking.Monad 43import Agda.TypeChecking.Reduce ( instantiateFull ) 44import Agda.TypeChecking.Substitute as TC ( TelV(..), raise, subst ) 45import Agda.TypeChecking.Pretty 46 47import Agda.Utils.FileName ( isNewerThan ) 48import Agda.Utils.Function ( iterate' ) 49import Agda.Utils.List ( downFrom, headWithDefault ) 50import Agda.Utils.List1 ( List1, pattern (:|) ) 51import qualified Agda.Utils.List1 as List1 52import Agda.Utils.Maybe ( boolToMaybe, catMaybes, caseMaybeM, fromMaybe, whenNothing ) 53import Agda.Utils.Monad ( ifM, when ) 54import Agda.Utils.Null ( null ) 55import Agda.Utils.Pretty (prettyShow, render) 56import qualified Agda.Utils.Pretty as P 57import Agda.Utils.IO.Directory 58import Agda.Utils.IO.UTF8 ( writeFile ) 59import Agda.Utils.Singleton ( singleton ) 60 61import Agda.Compiler.Common 62import Agda.Compiler.ToTreeless 63import Agda.Compiler.Treeless.EliminateDefaults 64import Agda.Compiler.Treeless.EliminateLiteralPatterns 65import Agda.Compiler.Treeless.GuardsToPrims 66import Agda.Compiler.Treeless.Erase ( computeErasedConstructorArgs ) 67import Agda.Compiler.Treeless.Subst () 68import Agda.Compiler.Backend (Backend(..), Backend'(..), Recompile(..)) 69 70import Agda.Compiler.JS.Syntax 71 ( Exp(Self,Local,Global,Undefined,Null,String,Char,Integer,Double,Lambda,Object,Array,Apply,Lookup,If,BinOp,PlainJS), 72 LocalId(LocalId), GlobalId(GlobalId), MemberId(MemberId,MemberIndex), Export(Export), Module(Module, modName, callMain), Comment(Comment), 73 modName, expName, uses 74 , JSQName 75 ) 76import Agda.Compiler.JS.Substitution 77 ( curriedLambda, curriedApply, emp, apply ) 78import qualified Agda.Compiler.JS.Pretty as JSPretty 79 80import Agda.Utils.Impossible (__IMPOSSIBLE__) 81 82-------------------------------------------------- 83-- Entry point into the compiler 84-------------------------------------------------- 85 86jsBackend :: Backend 87jsBackend = Backend jsBackend' 88 89jsBackend' :: Backend' JSOptions JSOptions JSModuleEnv Module (Maybe Export) 90jsBackend' = Backend' 91 { backendName = jsBackendName 92 , backendVersion = Nothing 93 , options = defaultJSOptions 94 , commandLineFlags = jsCommandLineFlags 95 , isEnabled = optJSCompile 96 , preCompile = jsPreCompile 97 , postCompile = jsPostCompile 98 , preModule = jsPreModule 99 , postModule = jsPostModule 100 , compileDef = jsCompileDef 101 , scopeCheckingSuffices = False 102 , mayEraseType = const $ return True 103 -- Andreas, 2019-05-09, see issue #3732. 104 -- If you want to use JS data structures generated from Agda 105 -- @data@/@record@, you might want to tell the treeless compiler 106 -- not to erase these types even if they have no content, 107 -- to get a stable interface. 108 } 109 110--- Options --- 111 112data JSOptions = JSOptions 113 { optJSCompile :: Bool 114 , optJSOptimize :: Bool 115 , optJSMinify :: Bool 116 -- ^ Remove spaces etc. See https://en.wikipedia.org/wiki/Minification_(programming). 117 , optJSVerify :: Bool 118 -- ^ Run generated code through interpreter. 119 } 120 deriving Generic 121 122instance NFData JSOptions 123 124defaultJSOptions :: JSOptions 125defaultJSOptions = JSOptions 126 { optJSCompile = False 127 , optJSOptimize = False 128 , optJSMinify = False 129 , optJSVerify = False 130 } 131 132jsCommandLineFlags :: [OptDescr (Flag JSOptions)] 133jsCommandLineFlags = 134 [ Option [] ["js"] (NoArg enable) "compile program using the JS backend" 135 , Option [] ["js-optimize"] (NoArg enableOpt) "turn on optimizations during JS code generation" 136 -- Minification is described at https://en.wikipedia.org/wiki/Minification_(programming) 137 , Option [] ["js-minify"] (NoArg enableMin) "minify generated JS code" 138 , Option [] ["js-verify"] (NoArg enableVerify) "except for main module, run generated JS modules through `node` (needs to be in PATH)" 139 ] 140 where 141 enable o = pure o{ optJSCompile = True } 142 enableOpt o = pure o{ optJSOptimize = True } 143 enableMin o = pure o{ optJSMinify = True } 144 enableVerify o = pure o{ optJSVerify = True } 145 146--- Top-level compilation --- 147 148jsPreCompile :: JSOptions -> TCM JSOptions 149jsPreCompile opts = return opts 150 151-- | After all modules have been compiled, copy RTE modules and verify compiled modules. 152 153jsPostCompile :: JSOptions -> IsMain -> Map.Map ModuleName Module -> TCM () 154jsPostCompile opts _ ms = do 155 156 -- Copy RTE modules. 157 158 compDir <- compileDir 159 liftIO $ do 160 dataDir <- getDataDir 161 let srcDir = dataDir </> "JS" 162 copyDirContent srcDir compDir 163 164 -- Verify generated JS modules (except for main). 165 166 reportSLn "compile.js.verify" 10 $ "Considering to verify generated JS modules" 167 when (optJSVerify opts) $ do 168 169 reportSLn "compile.js.verify" 10 $ "Verifying generated JS modules" 170 liftIO $ setEnv "NODE_PATH" compDir 171 172 forM_ ms $ \ Module{ modName, callMain } -> do 173 jsFile <- outFile modName 174 reportSLn "compile.js.verify" 30 $ unwords [ "Considering JS module:" , jsFile ] 175 176 -- Since we do not run a JS program for real, we skip all modules that could 177 -- have a call to main. 178 -- Atm, modules whose compilation was skipped are also skipped during verification 179 -- (they appear here as main modules). 180 whenNothing callMain $ do 181 let cmd = unwords [ "node", "-", "<", jsFile ] 182 reportSLn "compile.js.verify" 20 $ unwords [ "calling:", cmd ] 183 liftIO $ callCommand cmd 184 185 186mergeModules :: Map.Map ModuleName Module -> [(GlobalId, Export)] 187mergeModules ms 188 = [ (jsMod n, e) 189 | (n, Module _ _ es _) <- Map.toList ms 190 , e <- es 191 ] 192 193--- Module compilation --- 194 195type JSModuleEnv = Maybe CoinductionKit 196 197jsPreModule :: JSOptions -> IsMain -> ModuleName -> Maybe FilePath -> TCM (Recompile JSModuleEnv Module) 198jsPreModule _opts _ m mifile = ifM uptodate noComp yesComp 199 where 200 uptodate = case mifile of 201 Nothing -> pure False 202 Just ifile -> liftIO =<< isNewerThan <$> outFile_ <*> pure ifile 203 ifileDesc = fromMaybe "(memory)" mifile 204 205 noComp = do 206 reportSLn "compile.js" 2 . (++ " : no compilation is needed.") . prettyShow =<< curMName 207 return $ Skip skippedModule 208 209 -- A skipped module acts as a fake main module, to be skipped by --js-verify as well. 210 skippedModule = Module (jsMod m) mempty mempty (Just __IMPOSSIBLE__) 211 212 yesComp = do 213 m <- prettyShow <$> curMName 214 out <- outFile_ 215 reportSLn "compile.js" 1 $ repl [m, ifileDesc, out] "Compiling <<0>> in <<1>> to <<2>>" 216 Recompile <$> coinductionKit 217 218jsPostModule :: JSOptions -> JSModuleEnv -> IsMain -> ModuleName -> [Maybe Export] -> TCM Module 219jsPostModule opts _ isMain _ defs = do 220 m <- jsMod <$> curMName 221 is <- map (jsMod . fst) . iImportedModules <$> curIF 222 let mod = Module m is (reorder es) callMain 223 writeModule (optJSMinify opts) mod 224 return mod 225 where 226 es = catMaybes defs 227 main = MemberId "main" 228 -- Andreas, 2020-10-27, only add invocation of "main" if such function is defined. 229 -- This allows loading of generated .js files into an interpreter 230 -- even if they do not define "main". 231 hasMain = isMain == IsMain && any ((singleton main ==) . expName) es 232 callMain :: Maybe Exp 233 callMain = boolToMaybe hasMain $ Apply (Lookup Self main) [Lambda 1 emp] 234 235 236jsCompileDef :: JSOptions -> JSModuleEnv -> IsMain -> Definition -> TCM (Maybe Export) 237jsCompileDef opts kit _isMain def = definition (opts, kit) (defName def, def) 238 239-------------------------------------------------- 240-- Naming 241-------------------------------------------------- 242 243prefix :: [Char] 244prefix = "jAgda" 245 246jsMod :: ModuleName -> GlobalId 247jsMod m = GlobalId (prefix : map prettyShow (mnameToList m)) 248 249jsFileName :: GlobalId -> String 250jsFileName (GlobalId ms) = intercalate "." ms ++ ".js" 251 252jsMember :: Name -> MemberId 253jsMember n 254 -- Anonymous fields are used for where clauses, 255 -- and they're all given the concrete name "_", 256 -- so we disambiguate them using their name id. 257 | isNoName n = MemberId ("_" ++ show (nameId n)) 258 | otherwise = MemberId $ prettyShow n 259 260global' :: QName -> TCM (Exp, JSQName) 261global' q = do 262 i <- iModuleName <$> curIF 263 modNm <- topLevelModuleName (qnameModule q) 264 let 265 -- Global module prefix 266 qms = mnameToList $ qnameModule q 267 -- File-local module prefix 268 localms = drop (length $ mnameToList modNm) qms 269 nm = fmap jsMember $ List1.snoc localms $ qnameName q 270 if modNm == i 271 then return (Self, nm) 272 else return (Global (jsMod modNm), nm) 273 274global :: QName -> TCM (Exp, JSQName) 275global q = do 276 d <- getConstInfo q 277 case d of 278 Defn { theDef = Constructor { conData = p } } -> do 279 getConstInfo p >>= \case 280 -- Andreas, 2020-10-27, comment quotes outdated fact. 281 -- anon. constructors are now M.R.constructor. 282 -- We could simplify/remove the workaround by switching "record" 283 -- to "constructor", but this changes the output of the JS compiler 284 -- maybe in ways that break user's developments 285 -- (if they link to Agda-generated JS). 286 -- -- Rather annoyingly, the anonymous constructor of a record R in module M 287 -- -- is given the name M.recCon, but a named constructor C 288 -- -- is given the name M.R.C, sigh. This causes a lot of hoop-jumping 289 -- -- in the map from Agda names to JS names, which we patch by renaming 290 -- -- anonymous constructors to M.R.record. 291 Defn { theDef = Record { recNamedCon = False } } -> do 292 (m,ls) <- global' p 293 return (m, ls <> singleton (MemberId "record")) 294 _ -> global' (defName d) 295 _ -> global' (defName d) 296 297-- Reorder a list of exports to ensure def-before-use. 298-- Note that this can diverge in the case when there is no such reordering. 299 300-- Only top-level values are evaluated before definitions are added to the 301-- module, so we put those last, ordered in dependency order. There can't be 302-- any recursion between top-level values (unless termination checking has been 303-- disabled and someone's written a non-sensical program), so reordering will 304-- terminate. 305 306reorder :: [Export] -> [Export] 307reorder es = datas ++ funs ++ reorder' (Set.fromList $ map expName $ datas ++ funs) vals 308 where 309 (vs, funs) = partition isTopLevelValue es 310 (datas, vals) = partition isEmptyObject vs 311 312reorder' :: Set JSQName -> [Export] -> [Export] 313reorder' defs [] = [] 314reorder' defs (e : es) = 315 let us = uses e `Set.difference` defs 316 in if null us 317 then e : (reorder' (Set.insert (expName e) defs) es) 318 else reorder' defs (insertAfter us e es) 319 320isTopLevelValue :: Export -> Bool 321isTopLevelValue (Export _ e) = case e of 322 Object m | flatName `Map.member` m -> False 323 Lambda{} -> False 324 _ -> True 325 326isEmptyObject :: Export -> Bool 327isEmptyObject (Export _ e) = case e of 328 Object m -> null m 329 Lambda{} -> True 330 _ -> False 331 332insertAfter :: Set JSQName -> Export -> [Export] -> [Export] 333insertAfter us e [] = [e] 334insertAfter us e (f : fs) | null us = e : f : fs 335insertAfter us e (f : fs) | otherwise = 336 f : insertAfter (Set.delete (expName f) us) e fs 337 338-------------------------------------------------- 339-- Main compiling clauses 340-------------------------------------------------- 341 342type EnvWithOpts = (JSOptions, JSModuleEnv) 343 344definition :: EnvWithOpts -> (QName,Definition) -> TCM (Maybe Export) 345definition kit (q,d) = do 346 reportSDoc "compile.js" 10 $ "compiling def:" <+> prettyTCM q 347 (_,ls) <- global q 348 d <- instantiateFull d 349 350 definition' kit q d (defType d) ls 351 352-- | Ensure that there is at most one pragma for a name. 353checkCompilerPragmas :: QName -> TCM () 354checkCompilerPragmas q = 355 caseMaybeM (getUniqueCompilerPragma jsBackendName q) (return ()) $ \ (CompilerPragma r s) -> 356 setCurrentRange r $ case words s of 357 "=" : _ -> return () 358 _ -> genericDocError $ P.sep [ "Badly formed COMPILE JS pragma. Expected", 359 "{-# COMPILE JS <name> = <js> #-}" ] 360 361defJSDef :: Definition -> Maybe String 362defJSDef def = 363 case defCompilerPragmas jsBackendName def of 364 [CompilerPragma _ s] -> Just (dropEquals s) 365 [] -> Nothing 366 _:_:_ -> __IMPOSSIBLE__ 367 where 368 dropEquals = dropWhile $ \ c -> isSpace c || c == '=' 369 370definition' :: EnvWithOpts -> QName -> Definition -> Type -> JSQName -> TCM (Maybe Export) 371definition' kit q d t ls = if not (usableModality d) then return Nothing else do 372 checkCompilerPragmas q 373 case theDef d of 374 -- coinduction 375 Constructor{} | Just q == (nameOfSharp <$> snd kit) -> do 376 return Nothing 377 Function{} | Just q == (nameOfFlat <$> snd kit) -> do 378 ret $ Lambda 1 $ Apply (Lookup (local 0) flatName) [] 379 380 DataOrRecSig{} -> __IMPOSSIBLE__ 381 382 Axiom{} | Just e <- defJSDef d -> plainJS e 383 Axiom{} | otherwise -> ret Undefined 384 385 GeneralizableVar{} -> return Nothing 386 387 Function{} | Just e <- defJSDef d -> plainJS e 388 Function{} | otherwise -> do 389 390 reportSDoc "compile.js" 5 $ "compiling fun:" <+> prettyTCM q 391 caseMaybeM (toTreeless T.EagerEvaluation q) (pure Nothing) $ \ treeless -> do 392 used <- fromMaybe [] <$> getCompiledArgUse q 393 funBody <- eliminateCaseDefaults =<< 394 eliminateLiteralPatterns 395 (convertGuards treeless) 396 reportSDoc "compile.js" 30 $ " compiled treeless fun:" <+> pretty funBody 397 reportSDoc "compile.js" 40 $ " argument usage:" <+> (text . show) used 398 399 let (body, given) = lamView funBody 400 where 401 lamView :: T.TTerm -> (T.TTerm, Int) 402 lamView (T.TLam t) = (+1) <$> lamView t 403 lamView t = (t, 0) 404 405 -- number of eta expanded args 406 etaN = length $ dropWhileEnd (== ArgUsed) $ drop given used 407 408 unusedN = length $ filter (== ArgUnused) used 409 410 funBody' <- compileTerm kit 411 $ iterate' (given + etaN - unusedN) T.TLam 412 $ eraseLocalVars (map (== ArgUnused) used) 413 $ T.mkTApp (raise etaN body) (T.TVar <$> downFrom etaN) 414 415 reportSDoc "compile.js" 30 $ " compiled JS fun:" <+> (text . show) funBody' 416 return $ 417 if funBody' == Null then Nothing 418 else Just $ Export ls funBody' 419 420 Primitive{primName = p} 421 | p `Set.member` cubicalPrimitives -> 422 typeError $ NotImplemented p 423 | p `Set.member` primitives -> 424 plainJS $ "agdaRTS." ++ p 425 | Just e <- defJSDef d -> 426 plainJS e 427 | otherwise -> 428 ret Undefined 429 PrimitiveSort{} -> return Nothing 430 431 Datatype{ dataPathCons = _ : _ } -> do 432 s <- render <$> prettyTCM q 433 typeError $ NotImplemented $ 434 "Higher inductive types (" ++ s ++ ")" 435 Datatype{} -> do 436 computeErasedConstructorArgs q 437 ret emp 438 Record{} -> do 439 computeErasedConstructorArgs q 440 return Nothing 441 442 Constructor{} | Just e <- defJSDef d -> plainJS e 443 Constructor{conData = p, conPars = nc} -> do 444 let np = arity t - nc 445 erased <- getErasedConArgs q 446 let nargs = np - length (filter id erased) 447 args = [ Local $ LocalId $ nargs - i | i <- [0 .. nargs-1] ] 448 d <- getConstInfo p 449 let l = List1.last ls 450 case theDef d of 451 Record { recFields = flds } -> ret $ curriedLambda nargs $ 452 if optJSOptimize (fst kit) 453 then Lambda 1 $ Apply (Local (LocalId 0)) args 454 else Object $ Map.fromList [ (l, Lambda 1 $ Apply (Lookup (Local (LocalId 0)) l) args) ] 455 dt -> do 456 i <- index 457 ret $ curriedLambda (nargs + 1) $ Apply (Lookup (Local (LocalId 0)) i) args 458 where 459 index :: TCM MemberId 460 index 461 | Datatype{} <- dt 462 , optJSOptimize (fst kit) = do 463 q <- canonicalName q 464 cs <- mapM canonicalName $ defConstructors dt 465 case findIndex (q ==) cs of 466 Just i -> return $ MemberIndex i (mkComment l) 467 Nothing -> __IMPOSSIBLE_VERBOSE__ $ unwords [ "Constructor", prettyShow q, "not found in", prettyShow cs ] 468 | otherwise = return l 469 mkComment (MemberId s) = Comment s 470 mkComment _ = mempty 471 472 AbstractDefn{} -> __IMPOSSIBLE__ 473 where 474 ret = return . Just . Export ls 475 plainJS = return . Just . Export ls . PlainJS 476 477compileTerm :: EnvWithOpts -> T.TTerm -> TCM Exp 478compileTerm kit t = go t 479 where 480 go :: T.TTerm -> TCM Exp 481 go = \case 482 T.TVar x -> return $ Local $ LocalId x 483 T.TDef q -> do 484 d <- getConstInfo q 485 case theDef d of 486 -- Datatypes and records are erased 487 Datatype {} -> return (String "*") 488 Record {} -> return (String "*") 489 _ -> qname q 490 T.TApp (T.TCon q) [x] | Just q == (nameOfSharp <$> snd kit) -> do 491 x <- go x 492 let evalThunk = unlines 493 [ "function() {" 494 , " delete this.flat;" 495 , " var result = this.__flat_helper();" 496 , " delete this.__flat_helper;" 497 , " this.flat = function() { return result; };" 498 , " return result;" 499 , "}" 500 ] 501 return $ Object $ Map.fromList 502 [(flatName, PlainJS evalThunk) 503 ,(MemberId "__flat_helper", Lambda 0 x)] 504 T.TApp t' xs | Just f <- getDef t' -> do 505 used <- case f of 506 Left q -> fromMaybe [] <$> getCompiledArgUse q 507 Right c -> map (\ b -> if b then ArgUnused else ArgUsed) <$> getErasedConArgs c 508 -- Andreas, 2021-02-10 NB: could be @map (bool ArgUsed ArgUnused)@ 509 -- but I find it unintuitive that 'bool' takes the 'False'-branch first. 510 let given = length xs 511 512 -- number of eta expanded args 513 etaN = length $ dropWhile (== ArgUsed) $ reverse $ drop given used 514 515 args = filterUsed used $ xs ++ (T.TVar <$> downFrom etaN) 516 517 curriedLambda etaN <$> (curriedApply <$> go (raise etaN t') <*> mapM go args) 518 519 T.TApp t xs -> do 520 curriedApply <$> go t <*> mapM go xs 521 T.TLam t -> Lambda 1 <$> go t 522 -- TODO This is not a lazy let, but it should be... 523 T.TLet t e -> apply <$> (Lambda 1 <$> go e) <*> traverse go [t] 524 T.TLit l -> return $ literal l 525 T.TCon q -> do 526 d <- getConstInfo q 527 qname q 528 T.TCase sc ct def alts | T.CTData _ dt <- T.caseType ct -> do 529 dt <- getConstInfo dt 530 alts' <- traverse (compileAlt kit) alts 531 let cs = defConstructors $ theDef dt 532 obj = Object $ Map.fromList [(snd x, y) | (x, y) <- alts'] 533 arr = mkArray [headWithDefault (mempty, Null) [(Comment s, y) | ((c', MemberId s), y) <- alts', c' == c] | c <- cs] 534 case (theDef dt, defJSDef dt) of 535 (_, Just e) -> do 536 return $ apply (PlainJS e) [Local (LocalId sc), obj] 537 (Record{}, _) | optJSOptimize (fst kit) -> do 538 return $ apply (Local $ LocalId sc) [snd $ headWithDefault __IMPOSSIBLE__ alts'] 539 (Record{}, _) -> do 540 memId <- visitorName $ recCon $ theDef dt 541 return $ apply (Lookup (Local $ LocalId sc) memId) [obj] 542 (Datatype{}, _) | optJSOptimize (fst kit) -> do 543 return $ curriedApply (Local (LocalId sc)) [arr] 544 (Datatype{}, _) -> do 545 return $ curriedApply (Local (LocalId sc)) [obj] 546 _ -> __IMPOSSIBLE__ 547 T.TCase _ _ _ _ -> __IMPOSSIBLE__ 548 549 T.TPrim p -> return $ compilePrim p 550 T.TUnit -> unit 551 T.TSort -> unit 552 T.TErased -> unit 553 T.TError T.TUnreachable -> return Undefined 554 T.TError T.TMeta{} -> return Undefined 555 T.TCoerce t -> go t 556 557 getDef (T.TDef f) = Just (Left f) 558 getDef (T.TCon c) = Just (Right c) 559 getDef (T.TCoerce x) = getDef x 560 getDef _ = Nothing 561 562 unit = return Null 563 564 mkArray xs 565 | 2 * length (filter ((==Null) . snd) xs) <= length xs = Array xs 566 | otherwise = Object $ Map.fromList [(MemberIndex i c, x) | (i, (c, x)) <- zip [0..] xs, x /= Null] 567 568compilePrim :: T.TPrim -> Exp 569compilePrim p = 570 case p of 571 T.PIf -> curriedLambda 3 $ If (local 2) (local 1) (local 0) 572 T.PEqI -> binOp "agdaRTS.uprimIntegerEqual" 573 T.PEqF -> binOp "agdaRTS.uprimFloatEquality" 574 T.PEqQ -> binOp "agdaRTS.uprimQNameEquality" 575 T.PEqS -> primEq 576 T.PEqC -> primEq 577 T.PGeq -> binOp "agdaRTS.uprimIntegerGreaterOrEqualThan" 578 T.PLt -> binOp "agdaRTS.uprimIntegerLessThan" 579 T.PAdd -> binOp "agdaRTS.uprimIntegerPlus" 580 T.PSub -> binOp "agdaRTS.uprimIntegerMinus" 581 T.PMul -> binOp "agdaRTS.uprimIntegerMultiply" 582 T.PRem -> binOp "agdaRTS.uprimIntegerRem" 583 T.PQuot -> binOp "agdaRTS.uprimIntegerQuot" 584 T.PAdd64 -> binOp "agdaRTS.uprimWord64Plus" 585 T.PSub64 -> binOp "agdaRTS.uprimWord64Minus" 586 T.PMul64 -> binOp "agdaRTS.uprimWord64Multiply" 587 T.PRem64 -> binOp "agdaRTS.uprimIntegerRem" -- -| 588 T.PQuot64 -> binOp "agdaRTS.uprimIntegerQuot" -- > These can use the integer functions 589 T.PEq64 -> binOp "agdaRTS.uprimIntegerEqual" -- | 590 T.PLt64 -> binOp "agdaRTS.uprimIntegerLessThan" -- -| 591 T.PITo64 -> unOp "agdaRTS.primWord64FromNat" 592 T.P64ToI -> unOp "agdaRTS.primWord64ToNat" 593 T.PSeq -> binOp "agdaRTS.primSeq" 594 where binOp js = curriedLambda 2 $ apply (PlainJS js) [local 1, local 0] 595 unOp js = curriedLambda 1 $ apply (PlainJS js) [local 0] 596 primEq = curriedLambda 2 $ BinOp (local 1) "===" (local 0) 597 598 599compileAlt :: EnvWithOpts -> T.TAlt -> TCM ((QName, MemberId), Exp) 600compileAlt kit = \case 601 T.TACon con ar body -> do 602 erased <- getErasedConArgs con 603 let nargs = ar - length (filter id erased) 604 memId <- visitorName con 605 body <- Lambda nargs <$> compileTerm kit (eraseLocalVars erased body) 606 return ((con, memId), body) 607 _ -> __IMPOSSIBLE__ 608 609eraseLocalVars :: [Bool] -> T.TTerm -> T.TTerm 610eraseLocalVars [] x = x 611eraseLocalVars (False: es) x = eraseLocalVars es x 612eraseLocalVars (True: es) x = eraseLocalVars es (TC.subst (length es) T.TErased x) 613 614visitorName :: QName -> TCM MemberId 615visitorName q = do (m,ls) <- global q; return (List1.last ls) 616 617flatName :: MemberId 618flatName = MemberId "flat" 619 620local :: Nat -> Exp 621local = Local . LocalId 622 623qname :: QName -> TCM Exp 624qname q = do 625 (e,ls) <- global q 626 return (foldl Lookup e ls) 627 628literal :: Literal -> Exp 629literal = \case 630 (LitNat x) -> Integer x 631 (LitWord64 x) -> Integer (fromIntegral x) 632 (LitFloat x) -> Double x 633 (LitString x) -> String x 634 (LitChar x) -> Char x 635 (LitQName x) -> litqname x 636 LitMeta{} -> __IMPOSSIBLE__ 637 638litqname :: QName -> Exp 639litqname q = 640 Object $ Map.fromList 641 [ (mem "id", Integer $ fromIntegral n) 642 , (mem "moduleId", Integer $ fromIntegral m) 643 , (mem "name", String $ T.pack $ prettyShow q) 644 , (mem "fixity", litfixity fx)] 645 where 646 mem = MemberId 647 NameId n (ModuleNameHash m) = nameId $ qnameName q 648 fx = theFixity $ nameFixity $ qnameName q 649 650 litfixity :: Fixity -> Exp 651 litfixity fx = Object $ Map.fromList 652 [ (mem "assoc", litAssoc $ fixityAssoc fx) 653 , (mem "prec", litPrec $ fixityLevel fx)] 654 655 -- TODO this will probably not work well together with the necessary FFI bindings 656 litAssoc NonAssoc = String "non-assoc" 657 litAssoc LeftAssoc = String "left-assoc" 658 litAssoc RightAssoc = String "right-assoc" 659 660 litPrec Unrelated = String "unrelated" 661 litPrec (Related l) = Double l 662 663-------------------------------------------------- 664-- Writing out an ECMAScript module 665-------------------------------------------------- 666 667writeModule :: Bool -> Module -> TCM () 668writeModule minify m = do 669 out <- outFile (modName m) 670 liftIO (writeFile out (JSPretty.prettyShow minify m)) 671 672outFile :: GlobalId -> TCM FilePath 673outFile m = do 674 mdir <- compileDir 675 let (fdir, fn) = splitFileName (jsFileName m) 676 let dir = mdir </> fdir 677 fp = dir </> fn 678 liftIO $ createDirectoryIfMissing True dir 679 return fp 680 681outFile_ :: TCM FilePath 682outFile_ = do 683 m <- curMName 684 outFile (jsMod m) 685 686-- | Cubical primitives that are (currently) not compiled. 687-- 688-- TODO: Primitives that are neither part of this set nor of 689-- 'primitives', and for which 'defJSDef' does not return anything, 690-- are silently compiled to 'Undefined'. Thus, if a cubical primitive 691-- is by accident omitted from 'cubicalPrimitives', then programs that 692-- should be rejected are compiled to something which might not work 693-- as intended. A better approach might be to list exactly those 694-- primitives which should be compiled to 'Undefined'. 695 696cubicalPrimitives :: Set String 697cubicalPrimitives = Set.fromList 698 [ "primIMin" 699 , "primIMax" 700 , "primINeg" 701 , "primPartial" 702 , "primPartialP" 703 , "primPFrom1" 704 , "primPOr" 705 , "primComp" 706 , "primTransp" 707 , "primHComp" 708 , "primSubOut" 709 ] 710 711-- | Primitives implemented in the JS Agda RTS. 712primitives :: Set String 713primitives = Set.fromList 714 [ "primShowInteger" 715 716 -- Natural number functions 717 -- , "primNatPlus" -- missing 718 , "primNatMinus" 719 -- , "primNatTimes" -- missing 720 -- , "primNatDivSucAux" -- missing 721 -- , "primNatModSucAux" -- missing 722 -- , "primNatEquality" -- missing 723 -- , "primNatLess" -- missing 724 -- , "primShowNat" -- missing 725 726 -- Machine words 727 , "primWord64ToNat" 728 , "primWord64FromNat" 729 -- , "primWord64ToNatInjective" -- missing 730 731 -- Level functions 732 -- , "primLevelZero" -- missing 733 -- , "primLevelSuc" -- missing 734 -- , "primLevelMax" -- missing 735 736 -- Sorts 737 -- , "primSetOmega" -- missing 738 -- , "primStrictSetOmega" -- missing 739 740 -- Floating point functions 741 , "primFloatEquality" 742 , "primFloatInequality" 743 , "primFloatLess" 744 , "primFloatIsInfinite" 745 , "primFloatIsNaN" 746 , "primFloatIsNegativeZero" 747 , "primFloatIsSafeInteger" 748 , "primFloatToWord64" 749 -- , "primFloatToWord64Injective" -- missing 750 , "primNatToFloat" 751 , "primIntToFloat" 752 -- , "primFloatRound" -- in Agda.Builtin.Float 753 -- , "primFloatFloor" -- in Agda.Builtin.Float 754 -- , "primFloatCeiling" -- in Agda.Builtin.Float 755 -- , "primFloatToRatio" -- in Agda.Builtin.Float 756 , "primRatioToFloat" 757 -- , "primFloatDecode" -- in Agda.Builtin.Float 758 -- , "primFloatEncode" -- in Agda.Builtin.Float 759 , "primShowFloat" 760 , "primFloatPlus" 761 , "primFloatMinus" 762 , "primFloatTimes" 763 , "primFloatNegate" 764 , "primFloatDiv" 765 , "primFloatSqrt" 766 , "primFloatExp" 767 , "primFloatLog" 768 , "primFloatSin" 769 , "primFloatCos" 770 , "primFloatTan" 771 , "primFloatASin" 772 , "primFloatACos" 773 , "primFloatATan" 774 , "primFloatATan2" 775 , "primFloatSinh" 776 , "primFloatCosh" 777 , "primFloatTanh" 778 , "primFloatASinh" 779 , "primFloatACosh" 780 , "primFloatATanh" 781 , "primFloatPow" 782 783 -- Character functions 784 -- , "primCharEquality" -- missing 785 -- , "primIsLower" -- missing 786 -- , "primIsDigit" -- missing 787 -- , "primIsAlpha" -- missing 788 -- , "primIsSpace" -- missing 789 -- , "primIsAscii" -- missing 790 -- , "primIsLatin1" -- missing 791 -- , "primIsPrint" -- missing 792 -- , "primIsHexDigit" -- missing 793 -- , "primToUpper" -- missing 794 -- , "primToLower" -- missing 795 -- , "primCharToNat" -- missing 796 -- , "primCharToNatInjective" -- missing 797 -- , "primNatToChar" -- missing 798 -- , "primShowChar" -- in Agda.Builtin.String 799 800 -- String functions 801 -- , "primStringToList" -- in Agda.Builtin.String 802 -- , "primStringToListInjective" -- missing 803 -- , "primStringFromList" -- in Agda.Builtin.String 804 -- , "primStringFromListInjective" -- missing 805 -- , "primStringAppend" -- in Agda.Builtin.String 806 -- , "primStringEquality" -- in Agda.Builtin.String 807 -- , "primShowString" -- in Agda.Builtin.String 808 -- , "primStringUncons" -- in Agda.Builtin.String 809 810 -- Other stuff 811 -- , "primEraseEquality" -- missing 812 -- , "primForce" -- missing 813 -- , "primForceLemma" -- missing 814 , "primQNameEquality" 815 , "primQNameLess" 816 , "primShowQName" 817 , "primQNameFixity" 818 -- , "primQNameToWord64s" -- missing 819 -- , "primQNameToWord64sInjective" -- missing 820 -- , "primMetaEquality" -- missing 821 -- , "primMetaLess" -- missing 822 -- , "primShowMeta" -- missing 823 -- , "primMetaToNat" -- missing 824 -- , "primMetaToNatInjective" -- missing 825 -- , "primIMin" -- missing 826 -- , "primIMax" -- missing 827 -- , "primINeg" -- missing 828 -- , "primPOr" -- missing 829 -- , "primComp" -- missing 830 -- , builtinTrans -- missing 831 -- , builtinHComp -- missing 832 -- , "primIdJ" -- missing 833 -- , "primPartial" -- missing 834 -- , "primPartialP" -- missing 835 -- , builtinGlue -- missing 836 -- , builtin_glue -- missing 837 -- , builtin_unglue -- missing 838 -- , builtinFaceForall -- missing 839 -- , "primDepIMin" -- missing 840 -- , "primIdFace" -- missing 841 -- , "primIdPath" -- missing 842 -- , builtinIdElim -- missing 843 -- , builtinSubOut -- missing 844 -- , builtin_glueU -- missing 845 -- , builtin_unglueU -- missing 846 ] 847