summaryrefslogtreecommitdiff
path: root/src/full/Agda/Compiler/JS/Compiler.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Compiler/JS/Compiler.hs')
-rw-r--r--src/full/Agda/Compiler/JS/Compiler.hs533
1 files changed, 245 insertions, 288 deletions
diff --git a/src/full/Agda/Compiler/JS/Compiler.hs b/src/full/Agda/Compiler/JS/Compiler.hs
index 658966f..0d0a938 100644
--- a/src/full/Agda/Compiler/JS/Compiler.hs
+++ b/src/full/Agda/Compiler/JS/Compiler.hs
@@ -1,13 +1,15 @@
{-# LANGUAGE CPP #-}
-{-# LANGUAGE NamedFieldPuns #-}
module Agda.Compiler.JS.Compiler where
import Prelude hiding ( null, writeFile )
+import Control.Applicative
import Control.Monad.Reader ( liftIO )
+import Control.Monad.Trans
import Data.List ( intercalate, genericLength, partition )
import Data.Maybe ( isJust )
import Data.Set ( Set, null, insert, difference, delete )
+import Data.Traversable (traverse)
import Data.Map ( fromList, elems )
import qualified Data.Set as Set
import qualified Data.Map as Map
@@ -17,7 +19,7 @@ import System.FilePath ( splitFileName, (</>) )
import Agda.Interaction.FindFile ( findFile, findInterfaceFile )
import Agda.Interaction.Imports ( isNewerThan )
import Agda.Interaction.Options ( optCompileDir )
-import Agda.Syntax.Common ( Nat, unArg, namedArg )
+import Agda.Syntax.Common ( Nat, unArg, namedArg, NameId(..) )
import Agda.Syntax.Concrete.Name ( projectRoot )
import Agda.Syntax.Abstract.Name
( ModuleName(MName), QName,
@@ -25,50 +27,45 @@ import Agda.Syntax.Abstract.Name
mnameToList, qnameName, qnameModule, isInModule, nameId )
import Agda.Syntax.Internal
( Name, Args, Type,
- Clause, Pattern, Pattern'(VarP,DotP,LitP,ConP,ProjP),
- ClauseBodyF(Body,NoBody,Bind),ClauseBody,
- Term(Var,Lam,Lit,Level,Def,Con,Pi,Sort,MetaV,DontCare,Shared),
- unSpine, allApplyElims,
conName,
- derefPtr,
- toTopLevelModuleName, clausePats, clauseBody, arity, unEl, unAbs )
-import Agda.Syntax.Internal.Pattern ( unnumberPatVars )
-import Agda.TypeChecking.Substitute ( absBody )
+ toTopLevelModuleName, arity, unEl, unAbs, nameFixity )
import Agda.Syntax.Literal ( Literal(LitNat,LitFloat,LitString,LitChar,LitQName,LitMeta) )
+import Agda.Syntax.Fixity
+import qualified Agda.Syntax.Treeless as T
+import Agda.TypeChecking.Substitute ( absBody )
import Agda.TypeChecking.Level ( reallyUnLevelView )
-import Agda.TypeChecking.Monad
- ( TCM, Definition(Defn), Interface,
- JSCode, Defn(Record,Datatype,Constructor,Primitive,Function,Axiom),
- Projection(Projection), projProper, projFromType, projIndex,
- iModuleName, iImportedModules, theDef, getConstInfo,
- ignoreAbstractMode, miInterface, getVisitedModules,
- defName, defType, funClauses, funProjection, projectionArgs,
- dataPars, dataCons,
- conPars, conData,
- recConHead, recFields, recNamedCon,
- localTCState,
- typeError, TypeError(NotImplemented),
- defJSDef )
+import Agda.TypeChecking.Monad hiding (Global, Local)
+import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.Options ( setCommandLineOptions, commandLineOptions, reportSLn )
import Agda.TypeChecking.Reduce ( instantiateFull, normalise )
+import Agda.TypeChecking.Substitute (TelV(..))
+import Agda.TypeChecking.Telescope
+import Agda.TypeChecking.Pretty
import Agda.Utils.FileName ( filePath )
import Agda.Utils.Function ( iterate' )
+import Agda.Utils.Maybe
import Agda.Utils.Monad ( (<$>), (<*>), ifM )
import Agda.Utils.Pretty (prettyShow)
+import qualified Agda.Utils.Pretty as P
+import Agda.Utils.IO.Directory
import Agda.Utils.IO.UTF8 ( writeFile )
import qualified Agda.Utils.HashMap as HMap
+
import Agda.Compiler.Common
- ( curDefs, curIF, curMName, setInterface, repl, inCompilerEnv,
- IsMain (..), doCompile )
+import Agda.Compiler.ToTreeless
+import Agda.Compiler.Treeless.DelayCoinduction
+import Agda.Compiler.Treeless.EliminateLiteralPatterns
+import Agda.Compiler.Treeless.GuardsToPrims
import Agda.Compiler.JS.Syntax
- ( Exp(Self,Local,Global,Undefined,String,Char,Integer,Double,Lambda,Object,Apply,Lookup),
+ ( Exp(Self,Local,Global,Undefined,String,Char,Integer,Double,Lambda,Object,Apply,Lookup,If,BinOp,PlainJS),
LocalId(LocalId), GlobalId(GlobalId), MemberId(MemberId), Export(Export), Module(Module),
modName, expName, uses )
import Agda.Compiler.JS.Substitution
( curriedLambda, curriedApply, emp, subst, apply )
-import Agda.Compiler.JS.Case ( Tag(Tag), Case(Case), Patt(VarPatt,Tagged), lambda )
-import Agda.Compiler.JS.Pretty ( pretty )
+import qualified Agda.Compiler.JS.Pretty as JSPretty
+
+import Paths_Agda
#include "undefined.h"
import Agda.Utils.Impossible ( Impossible(Impossible), throwImpossible )
@@ -79,19 +76,21 @@ import Agda.Utils.Impossible ( Impossible(Impossible), throwImpossible )
compilerMain :: Interface -> TCM ()
compilerMain mainI = inCompilerEnv mainI $ do
- doCompile IsMain mainI $ \_ -> compile
+ doCompile IsMain mainI $ do
+ compile
+ copyRTEModules
-compile :: Interface -> TCM ()
-compile i = do
+compile :: IsMain -> Interface -> TCM ()
+compile isMain i = do
ifM uptodate noComp $ do
yesComp
- writeModule =<< curModule
+ writeModule =<< curModule isMain
where
uptodate = liftIO =<< (isNewerThan <$> outFile_ <*> ifile)
ifile = maybe __IMPOSSIBLE__ filePath <$>
(findInterfaceFile . toTopLevelModuleName =<< curMName)
- noComp = reportSLn "" 1 . (++ " : no compilation is needed.") . prettyShow =<< curMName
- yesComp = reportSLn "" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
+ noComp = reportSLn "compile.js" 2 . (++ " : no compilation is needed.") . prettyShow =<< curMName
+ yesComp = reportSLn "compile.js" 1 . (`repl` "Compiling <<0>> in <<1>> to <<2>>") =<<
sequence [prettyShow <$> curMName, ifile, outFile_] :: TCM ()
--------------------------------------------------
@@ -125,17 +124,13 @@ jsMember n =
global' :: QName -> TCM (Exp,[MemberId])
global' q = do
i <- iModuleName <$> curIF
- is <- filter (isInModule q) <$> map (iModuleName . miInterface) <$> elems <$> getVisitedModules
- case is of
- [] -> __IMPOSSIBLE__
- _ -> let
- seg = maximum (map (length . mnameToList) is)
- ms = mnameToList (qnameModule q)
- m = MName (take seg ms)
- ls = map jsMember (drop seg ms ++ [qnameName q])
- in case (m == i) of
- True -> return (Self, ls)
- False -> return (Global (jsMod m), ls)
+ modNm <- topLevelModuleName (qnameModule q)
+ let
+ qms = mnameToList $ qnameModule q
+ nm = map jsMember (drop (length $ mnameToList modNm) qms ++ [qnameName q])
+ if modNm == i
+ then return (Self, nm)
+ else return (Global (jsMod modNm), nm)
global :: QName -> TCM (Exp,[MemberId])
global q = do
@@ -174,13 +169,15 @@ reorder' defs (e : es) =
False -> reorder' defs (insertAfter us e es)
isTopLevelValue :: Export -> Bool
-isTopLevelValue (Export _ e) = case e of
+isTopLevelValue (Export _ isCoind e) = case e of
+ _ | isCoind -> False
Lambda{} -> False
_ -> True
isEmptyObject :: Export -> Bool
-isEmptyObject (Export _ e) = case e of
+isEmptyObject (Export _ _ e) = case e of
Object m -> Map.null m
+ Lambda{} -> True
_ -> False
insertAfter :: Set [MemberId] -> Export -> [Export] -> [Export]
@@ -192,246 +189,156 @@ insertAfter us e (f:fs) | otherwise = f : insertAfter (delete (expName f) us) e
-- Main compiling clauses
--------------------------------------------------
-curModule :: TCM Module
-curModule = do
+curModule :: IsMain -> TCM Module
+curModule isMain = do
+ kit <- coinductionKit
m <- (jsMod <$> curMName)
is <- map jsMod <$> (map fst . iImportedModules <$> curIF)
- es <- mapM definition =<< (HMap.toList <$> curDefs)
- return (Module m (reorder es))
+ es <- catMaybes <$> (mapM (definition kit) =<< (sortDefs <$> curDefs))
+ return $ Module m (reorder es) main
+ where
+ main = case isMain of
+ IsMain -> Just $ Apply (Lookup Self $ MemberId "main") [Lambda 1 emp]
+ NotMain -> Nothing
-definition :: (QName,Definition) -> TCM Export
-definition (q,d) = do
+definition :: Maybe CoinductionKit -> (QName,Definition) -> TCM (Maybe Export)
+definition kit (q,d) = do
+ reportSDoc "compile.js" 10 $ text "compiling def:" <+> prettyTCM q
(_,ls) <- global q
d <- instantiateFull d
- e <- defn q ls (defType d) (defJSDef d) (theDef d)
- return (Export ls e)
-
-defn :: QName -> [MemberId] -> Type -> Maybe JSCode -> Defn -> TCM Exp
-defn q ls t (Just e) Axiom =
- return e
-defn q ls t Nothing Axiom = do
- t <- normalise t
- s <- isSingleton t
- case s of
- -- Inline and eta-expand postulates of singleton type
- Just e ->
- return (curriedLambda (arity t) e)
- -- Everything else we leave undefined
- Nothing ->
- return Undefined
-defn q ls t (Just e) (Function {}) =
- return e
-defn q ls t Nothing (Function { funProjection = proj, funClauses = cls }) = do
- t <- normalise t
- s <- isSingleton t
- cs <- mapM clause cls
- case s of
- -- Inline and eta-expand expressions of singleton type
- Just e ->
- return (curriedLambda (arity t) e)
- Nothing -> case proj of
- Just Projection{ projProper, projFromType = p, projIndex = i } -> do
- -- Andreas, 2013-05-20: whether a projection is proper is now stored.
- if isJust projProper then
- -- For projections from records we use a field lookup
- return (curriedLambda (numPars cls)
- (Lookup (Local (LocalId 0)) (last ls)))
- else
- -- For anything else we generate code, after adding (i-1) dummy lambdas
- return (dummyLambda (i-1) (lambda cs))
-{- OLD way of finding out whether a projection is proper (ie. from record)
- d <- getConstInfo p
- case theDef d of
- -- For projections from records we use a field lookup
- Record { recFields = flds } | q `elem` map unArg flds ->
- return (curriedLambda (numPars cls)
- (Lookup (Local (LocalId 0)) (last ls)))
- _ ->
- -- For anything else we generate code, after adding (i-1) dummy lambdas
- return (dummyLambda (i-1) (lambda cs))
--}
- Nothing ->
- return (lambda cs)
-defn q ls t (Just e) (Primitive {}) =
- return e
-defn q ls t _ (Primitive {}) =
- return Undefined
-defn q ls t _ (Datatype {}) =
- return emp
-defn q ls t (Just e) (Constructor {}) =
- return e
-defn q ls t _ (Constructor { conData = p, conPars = nc }) = do
- np <- return (arity t - nc)
- d <- getConstInfo p
+
+ definition' kit q d (defType d) ls
+
+definition' :: Maybe CoinductionKit -> QName -> Definition -> Type -> [MemberId] -> TCM (Maybe Export)
+definition' kit q d t ls =
case theDef d of
- Record { recFields = flds } ->
- return (curriedLambda np (Object (fromList
- ( (last ls , Lambda 1
- (Apply (Lookup (Local (LocalId 0)) (last ls))
- [ Local (LocalId (np - i)) | i <- [0 .. np-1] ]))
- : (zip [ jsMember (qnameName (unArg fld)) | fld <- flds ]
- [ Local (LocalId (np - i)) | i <- [1 .. np] ])))))
- _ ->
- return (curriedLambda (np + 1)
- (Apply (Lookup (Local (LocalId 0)) (last ls))
- [ Local (LocalId (np - i)) | i <- [0 .. np-1] ]))
-defn q ls t _ (Record {}) =
- return emp
-
--- Number of params in a function declaration
-
-numPars :: [Clause] -> Nat
-numPars [] = 0
-numPars (c : _) = genericLength (clausePats c)
-
--- One clause in a function definition
-
-clause :: Clause -> TCM Case
-clause c = do
- let pats = unnumberPatVars $ clausePats c
- ps <- mapM (pattern . unArg) pats
- (av,bv,es) <- return (mapping (map unArg pats))
- e <- body (clauseBody c)
- return (Case ps (subst av es e))
-
--- Mapping from Agda variables to JS variables in a pattern.
--- If mapping ps = (av,bv,es) then av is the number of Agda variables,
--- bv is the number of JS variables, and es is a list of expressions,
--- where es[i] is the JS variable corresponding to Agda variable i.
-
-mapping :: [Pattern] -> (Nat,Nat,[Exp])
-mapping = foldr mapping' (0,0,[])
-
-mapping' :: Pattern -> (Nat,Nat,[Exp]) -> (Nat,Nat,[Exp])
-mapping' (ProjP _) (av,bv,es) =
- __IMPOSSIBLE__
-mapping' (VarP _) (av,bv,es) = (av+1, bv+1, Local (LocalId bv) : es)
-mapping' (DotP _) (av,bv,es) = (av+1, bv+1, Local (LocalId bv) : es)
-mapping' (ConP _ _ ps) (av,bv,es) = (av',bv'+1,es') where
- (av',bv',es') = foldr mapping' (av,bv,es) (map namedArg ps)
-mapping' (LitP _) (av,bv,es) = (av, bv+1, es)
-
--- Not doing literal patterns yet
-
-pattern :: Pattern -> TCM Patt
-pattern (ProjP _) = typeError $ NotImplemented $ "Compilation of copatterns"
-pattern (ConP c _ ps) = do
- l <- tag $ conName c
- ps <- mapM (pattern . namedArg) ps
- return (Tagged l ps)
-pattern _ = return VarPatt
-
-tag :: QName -> TCM Tag
-tag q = do
- l <- visitorName q
- c <- getConstInfo q
- case theDef c of
- (Constructor { conData = p }) -> do
+ -- coinduction
+ Constructor{} | Just q == (nameOfSharp <$> kit) -> do
+ ret $ Lambda 1 $ local 0
+ Function{} | Just q == (nameOfFlat <$> kit) -> do
+ ret $ Lambda 1 $ Apply (local 0) [Integer 0]
+
+ Axiom | Just e <- defJSDef d -> plainJS e
+ Axiom | otherwise -> ret Undefined
+
+ Function{} | Just e <- defJSDef d -> plainJS e
+ Function{} | otherwise -> do
+ isInfVal <- outputIsInf kit t
+
+ reportSDoc "compile.js" 5 $ text "compiling fun:" <+> prettyTCM q
+ caseMaybeM (toTreeless q) (pure Nothing) $ \ treeless -> do
+ funBody <- eliminateLiteralPatterns $ convertGuards $ treeless
+ funBody' <- delayCoinduction funBody t
+ reportSDoc "compile.js" 30 $ text " compiled treeless fun:" <+> pretty funBody'
+ funBody'' <- compileTerm funBody'
+ reportSDoc "compile.js" 30 $ text " compiled JS fun:" <+> (text . show) funBody''
+ return $ Just $ Export ls isInfVal funBody''
+
+ Primitive{primName = p} | p `Set.member` primitives ->
+ plainJS $ "agdaRTS." ++ p
+ Primitive{} | Just e <- defJSDef d -> plainJS e
+ Primitive{} | otherwise -> ret Undefined
+
+ Datatype{} -> ret emp
+ Record{} -> return Nothing
+
+ Constructor{} | Just e <- defJSDef d -> plainJS e
+ Constructor{conData = p, conPars = nc} | otherwise -> do
+ np <- return (arity t - nc)
d <- getConstInfo p
- case (defJSDef d, theDef d) of
- (Just e, Datatype { dataCons = qs }) -> do
- ls <- mapM visitorName qs
- return (Tag l ls (\ x xs -> apply e (x:xs)))
- (Nothing, Datatype { dataCons = qs }) -> do
- ls <- mapM visitorName qs
- return (Tag l ls Apply)
- (Just e, Record {}) -> do
- return (Tag l [l] (\ x xs -> apply e (x:xs)))
- (Nothing, Record {}) -> do
- return (Tag l [l] Apply)
- _ -> __IMPOSSIBLE__
- _ -> __IMPOSSIBLE__
+ case theDef d of
+ Record { recFields = flds } ->
+ ret (curriedLambda np (Object (fromList
+ ( (last ls , Lambda 1
+ (Apply (Lookup (Local (LocalId 0)) (last ls))
+ [ Local (LocalId (np - i)) | i <- [0 .. np-1] ]))
+ : (zip [ jsMember (qnameName (unArg fld)) | fld <- flds ]
+ [ Local (LocalId (np - i)) | i <- [1 .. np] ])))))
+ _ ->
+ ret (curriedLambda (np + 1)
+ (Apply (Lookup (Local (LocalId 0)) (last ls))
+ [ Local (LocalId (np - i)) | i <- [0 .. np-1] ]))
+
+ AbstractDefn -> __IMPOSSIBLE__
+ where
+ ret = return . Just . Export ls False
+ plainJS = return . Just . Export ls False . PlainJS
-visitorName :: QName -> TCM MemberId
-visitorName q = do (m,ls) <- global q; return (last ls)
-body :: ClauseBody -> TCM Exp
-body (Body e) = term e
-body (Bind b) = body (unAbs b)
-body (NoBody) = return Undefined
-
-term :: Term -> TCM Exp
-term v = do
- case unSpine v of
- (Var i es) -> do
- let Just as = allApplyElims es
- e <- return (Local (LocalId i))
- es <- args 0 as
- return (curriedApply e es)
- (Lam _ at) -> Lambda 1 <$> term (absBody at)
- (Lit l) -> return (literal l)
- (Level l) -> term =<< reallyUnLevelView l
- (Shared p) -> term $ derefPtr p
- (Def q es) -> do
- let Just as = allApplyElims es
+compileTerm :: T.TTerm -> TCM Exp
+compileTerm term = do
+ case term of
+ T.TVar x -> return $ Local $ LocalId x
+ T.TDef q -> do
d <- getConstInfo q
case theDef d of
-- Datatypes and records are erased
Datatype {} -> return (String "*")
Record {} -> return (String "*")
- _ -> case defJSDef d of
- -- Inline functions with an FFI definition
- Just e -> do
- es <- args (projectionArgs $ theDef d) as
- return (curriedApply e es)
- Nothing -> do
- t <- normalise (defType d)
- s <- isSingleton t
- case s of
- -- Inline and eta-expand singleton types
- Just e ->
- return (curriedLambda (arity t) e)
- -- Everything else we leave non-inline
- Nothing -> do
- e <- qname q
- es <- args (projectionArgs $ theDef d) as
- return (curriedApply e es)
- (Con con as) -> do
- let q = conName con
+ _ -> qname q
+ T.TApp t xs -> curriedApply <$> compileTerm t <*> mapM compileTerm xs
+ T.TLam t -> Lambda 1 <$> compileTerm t
+ -- TODO This is not a lazy let, but it should be...
+ T.TLet t e -> apply <$> (Lambda 1 <$> compileTerm e) <*> traverse compileTerm [t]
+ T.TLit l -> return $ literal l
+ T.TCon q -> do
d <- getConstInfo q
- case defJSDef d of
- -- Inline functions with an FFI definition
- Just e -> do
- es <- args 0 as
- return (curriedApply e es)
- -- Everything else we leave non-inline
- Nothing -> do
- e <- qname q
- es <- args 0 as
- return (curriedApply e es)
- (Pi _ _) -> return (String "*")
- (Sort _) -> return (String "*")
- (MetaV _ _) -> return (Undefined)
- (DontCare _) -> return (Undefined)
-
--- Check to see if a type is a singleton, and if so, return its only
--- member. Singleton types are of the form T1 -> ... -> Tn -> T where
--- T is either a record with no fields, a datatype with one
--- no-argument constructor, a datatype with no constructors,
--- or (since this is a type-erasing translation) Set.
-
-isSingleton :: Type -> TCM (Maybe Exp)
-isSingleton t = case unEl t of
- Pi _ b -> isSingleton (unAbs b)
- Sort _ -> return (Just (String "*"))
- Def q as -> do
- d <- getConstInfo q
- case (theDef d) of
- Datatype { dataPars = np, dataCons = [] } ->
- return (Just Undefined)
- Datatype { dataPars = np, dataCons = [p] } -> do
- c <- getConstInfo p
- case (arity (defType c) == np) of
- True -> Just <$> qname p
- False -> return (Nothing)
- Record { recConHead = con, recFields = [] } ->
- Just <$> qname (conName con)
- _ -> return (Nothing)
- _ -> return (Nothing)
-
-args :: Int -> Args -> TCM [Exp]
-args n as = (replicate n Undefined ++) <$>
- mapM (term . unArg) as
+ qname q
+ T.TCase sc (T.CTData dt) def alts -> do
+ dt <- getConstInfo dt
+ alts' <- traverse compileAlt alts
+ let obj = Object $ Map.fromList alts'
+ case (theDef dt, defJSDef dt) of
+ (_, Just e) -> do
+ return $ apply (PlainJS e) [Local (LocalId sc), obj]
+ (Record{}, _) -> do
+ memId <- visitorName $ recCon $ theDef dt
+ return $ apply (Lookup (Local $ LocalId sc) memId) [obj]
+ (Datatype{}, _) -> do
+ return $ curriedApply (Local (LocalId sc)) [obj]
+ _ -> __IMPOSSIBLE__
+ T.TCase _ _ _ _ -> __IMPOSSIBLE__
+
+ T.TPrim p -> return $ compilePrim p
+ T.TUnit -> unit
+ T.TSort -> unit
+ T.TErased -> unit
+ T.TError T.TUnreachable -> return Undefined
+
+ where
+ unit = return $ Integer 0
+
+compilePrim :: T.TPrim -> Exp
+compilePrim p =
+ case p of
+ T.PIf -> curriedLambda 3 $ If (local 2) (local 1) (local 0)
+ T.PEqI -> binOp "agdaRTS.uprimIntegerEqual"
+ T.PEqF -> binOp "agdaRTS.uprimFloatEquality"
+ T.PEqQ -> binOp "agdaRTS.uprimQNameEquality"
+ p | T.isPrimEq p -> curriedLambda 2 $ BinOp (local 1) "===" (local 0)
+ T.PGeq -> binOp "agdaRTS.uprimIntegerGreaterOrEqualThan"
+ T.PLt -> binOp "agdaRTS.uprimIntegerLessThan"
+ T.PAdd -> binOp "agdaRTS.uprimIntegerPlus"
+ T.PSub -> binOp "agdaRTS.uprimIntegerMinus"
+ T.PMul -> binOp "agdaRTS.uprimIntegerMultiply"
+ T.PSeq -> binOp "agdaRTS.primSeq"
+ _ -> __IMPOSSIBLE__
+ where binOp js = curriedLambda 2 $ apply (PlainJS js) [local 1, local 0]
+
+
+compileAlt :: T.TAlt -> TCM (MemberId, Exp)
+compileAlt a = case a of
+ T.TACon con ar body -> do
+ memId <- visitorName con
+ body <- Lambda ar <$> compileTerm body
+ return (memId, body)
+ _ -> __IMPOSSIBLE__
+
+visitorName :: QName -> TCM MemberId
+visitorName q = do (m,ls) <- global q; return (last ls)
+
+local :: Nat -> Exp
+local = Local . LocalId
qname :: QName -> TCM Exp
qname q = do
@@ -439,15 +346,38 @@ qname q = do
return (foldl Lookup e ls)
literal :: Literal -> Exp
-literal (LitNat _ x) = Integer x
-literal (LitFloat _ x) = Double x
-literal (LitString _ x) = String x
-literal (LitChar _ x) = Char x
-literal (LitQName _ x) = String (show x)
-literal LitMeta{} = __IMPOSSIBLE__
+literal l = case l of
+ (LitNat _ x) -> Integer x
+ (LitFloat _ x) -> Double x
+ (LitString _ x) -> String x
+ (LitChar _ x) -> Char x
+ (LitQName _ x) -> litqname x
+ LitMeta{} -> __IMPOSSIBLE__
+
+litqname :: QName -> Exp
+litqname q =
+ Object $ Map.fromList
+ [ (mem "id", Integer $ fromIntegral n)
+ , (mem "moduleId", Integer $ fromIntegral m)
+ , (mem "name", String $ show q)
+ , (mem "fixity", litfixity fx)]
+ where
+ mem = MemberId
+ NameId n m = nameId $ qnameName q
+ fx = theFixity $ nameFixity $ qnameName q
+
+ litfixity :: Fixity -> Exp
+ litfixity fx = Object $ Map.fromList
+ [ (mem "assoc", litAssoc $ fixityAssoc fx)
+ , (mem "prec", litPrec $ fixityLevel fx)]
+
+ -- TODO this will probably not work well together with the necessary FFI bindings
+ litAssoc NonAssoc = String "NonAssoc"
+ litAssoc LeftAssoc = String "LeftAssoc"
+ litAssoc RightAssoc = String "RightAssoc"
-dummyLambda :: Int -> Exp -> Exp
-dummyLambda n = iterate' n (Lambda 0)
+ litPrec Unrelated = String "Unrelated"
+ litPrec (Related l) = Integer l
--------------------------------------------------
-- Writing out an ECMAScript module
@@ -456,14 +386,7 @@ dummyLambda n = iterate' n (Lambda 0)
writeModule :: Module -> TCM ()
writeModule m = do
out <- outFile (modName m)
- liftIO (writeFile out (pretty 0 0 m))
-
-compileDir :: TCM FilePath
-compileDir = do
- mdir <- optCompileDir <$> commandLineOptions
- case mdir of
- Just dir -> return dir
- Nothing -> __IMPOSSIBLE__
+ liftIO (writeFile out (JSPretty.pretty 0 0 m))
outFile :: GlobalId -> TCM FilePath
outFile m = do
@@ -478,3 +401,37 @@ outFile_ :: TCM FilePath
outFile_ = do
m <- curMName
outFile (jsMod m)
+
+
+copyRTEModules :: TCM ()
+copyRTEModules = do
+ dataDir <- lift getDataDir
+ let srcDir = dataDir </> "JS"
+ (lift . copyDirContent srcDir) =<< compileDir
+
+-- | Primitives implemented in the JS Agda RTS.
+primitives :: Set String
+primitives = Set.fromList
+ [ "primExp"
+ , "primFloatDiv"
+ , "primFloatEquality"
+ , "primFloatNumericalEquality"
+ , "primFloatNumericalLess"
+ , "primFloatNegate"
+ , "primFloatMinus"
+ , "primFloatPlus"
+ , "primFloatSqrt"
+ , "primFloatTimes"
+ , "primNatMinus"
+ , "primShowFloat"
+ , "primShowInteger"
+ , "primSin"
+ , "primCos"
+ , "primTan"
+ , "primASin"
+ , "primACos"
+ , "primATan"
+ , "primATan2"
+ , "primShowQName"
+ , "primQNameEquality"
+ ]