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