module Agda.Compiler.JS.Pretty where
import Prelude hiding ( null )
import Data.List ( intercalate )
import Data.Set ( Set, toList, singleton, insert, member )
import Data.Map ( Map, toAscList, empty, null )
import Text.Regex.TDFA (makeRegex, matchTest, Regex)
import Agda.Syntax.Common ( Nat )
import Agda.Utils.Hash
import Agda.Compiler.JS.Syntax hiding (exports)
br :: Int -> String
br i = "\n" ++ take (2*i) (repeat ' ')
unescape :: Char -> String
unescape '"' = "\\\""
unescape '\\' = "\\\\"
unescape '\n' = "\\n"
unescape '\r' = "\\r"
unescape '\x2028' = "\\u2028"
unescape '\x2029' = "\\u2029"
unescape c = [c]
unescapes :: String -> String
unescapes s = concat (map unescape s)
class Pretty a where
pretty :: Nat -> Int -> a -> String
instance (Pretty a, Pretty b) => Pretty (a,b) where
pretty n i (x,y) = pretty n i x ++ ": " ++ pretty n (i+1) y
class Pretties a where
pretties :: Nat -> Int -> a -> [String]
instance Pretty a => Pretties [a] where
pretties n i = map (pretty n i)
instance (Pretty a, Pretty b) => Pretties (Map a b) where
pretties n i o = pretties n i (toAscList o)
instance Pretty LocalId where
pretty n i (LocalId x) = "x" ++ show (n - x - 1)
instance Pretty GlobalId where
pretty n i (GlobalId m) = variableName $ intercalate "_" m
instance Pretty MemberId where
pretty n i (MemberId s) = "\"" ++ unescapes s ++ "\""
instance Pretty Exp where
pretty n i (Self) = "exports"
pretty n i (Local x) = pretty n i x
pretty n i (Global m) = pretty n i m
pretty n i (Undefined) = "undefined"
pretty n i (String s) = "\"" ++ unescapes s ++ "\""
pretty n i (Char c) = "\"" ++ unescape c ++ "\""
pretty n i (Integer x) = "agdaRTS.primIntegerFromString(\"" ++ show x ++ "\")"
pretty n i (Double x) = show x
pretty n i (Lambda x e) =
"function (" ++
intercalate ", " (pretties (n+x) i (map LocalId [x-1, x-2 .. 0])) ++
") " ++ block (n+x) i e
pretty n i (Object o) | null o = "{}"
pretty n i (Object o) | otherwise =
"{" ++ br (i+1) ++ intercalate ("," ++ br (i+1)) (pretties n i o) ++ br i ++ "}"
pretty n i (Apply f es) = pretty n i f ++ "(" ++ intercalate ", " (pretties n i es) ++ ")"
pretty n i (Lookup e l) = pretty n i e ++ "[" ++ pretty n i l ++ "]"
pretty n i (If e f g) =
"(" ++ pretty n i e ++ "? " ++ pretty n i f ++ ": " ++ pretty n i g ++ ")"
pretty n i (PreOp op e) = "(" ++ op ++ " " ++ pretty n i e ++ ")"
pretty n i (BinOp e op f) = "(" ++ pretty n i e ++ " " ++ op ++ " " ++ pretty n i f ++ ")"
pretty n i (Const c) = c
pretty n i (PlainJS js) = "(" ++ js ++ ")"
block :: Nat -> Int -> Exp -> String
block n i (If e f g) = "{" ++ br (i+1) ++ block' n (i+1) (If e f g) ++ br i ++ "}"
block n i e = "{" ++ br (i+1) ++ "return " ++ pretty n (i+1) e ++ ";" ++ br i ++ "}"
block' :: Nat -> Int -> Exp -> String
block' n i (If e f g) = "if (" ++ pretty n i e ++ ") " ++ block n i f ++ " else " ++ block' n i g
block' n i e = block n i e
modname :: GlobalId -> String
modname (GlobalId ms) = "\"" ++ intercalate "." ms ++ "\""
exports :: Nat -> Int -> Set [MemberId] -> [Export] -> String
exports n i lss [] = ""
exports n i lss (Export ls e : es) | member (init ls) lss =
"exports[" ++ intercalate "][" (pretties n i ls) ++ "] = " ++ pretty n (i+1) e ++ ";" ++ br i ++
exports n i (insert ls lss) es
exports n i lss (Export ls e : es) | otherwise =
exports n i lss (Export (init ls) (Object empty) : Export ls e : es)
instance Pretty Module where
pretty n i (Module m es ex) =
imports ++ br i
++ exports n i (singleton []) es ++ br i
++ maybe "" (pretty n i) ex
where
js = toList (globals es)
imports = unlines $
["var agdaRTS = require(\"agda-rts\");"] ++
["var " ++ pretty n (i+1) e ++ " = require(" ++ modname e ++ ");"
| e <- js]
variableName :: String -> String
variableName s = if isValidJSIdent s then "z_" ++ s else "h_" ++ show (hashString s)
isValidJSIdent :: String -> Bool
isValidJSIdent s = matchTest regex s
where
regex :: Regex
regex = makeRegex "^[a-zA-Z_$][0-9a-zA-Z_$]*$"