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)

-- Pretty-print a lambda-calculus expression as ECMAScript.

-- Since ECMAScript is C-like rather than Haskell-like, it's easier to
-- do the pretty-printing directly than use the Pretty library, which
-- assumes Haskell-like indentation.

br :: Int -> String
br :: Int -> String
br Int
i = String
"\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String -> String
forall a. Int -> [a] -> [a]
take (Int
2Int -> Int -> Int
forall a. Num a => a -> a -> a
*Int
i) (Char -> String
forall a. a -> [a]
repeat Char
' ')

unescape :: Char -> String
unescape :: Char -> String
unescape Char
'"'      = String
"\\\""
unescape Char
'\\'     = String
"\\\\"
unescape Char
'\n'     = String
"\\n"
unescape Char
'\r'     = String
"\\r"
unescape Char
'\x2028' = String
"\\u2028"
unescape Char
'\x2029' = String
"\\u2029"
unescape Char
c        = [Char
c]

unescapes :: String -> String
unescapes :: String -> String
unescapes 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)

-- pretty n i e pretty-prints e, under n levels of de Bruijn binding,
-- with i levels of indentation.

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 Int
n Int
i (a
x,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 -> 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
+Int
1) b
y

-- Pretty-print collections

class Pretties a where
    pretties :: Nat -> Int -> a -> [String]

instance Pretty a => Pretties [a] where
  pretties :: Int -> Int -> [a] -> [String]
pretties Int
n 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 Int
n Int
i 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)

-- Pretty print identifiers

instance Pretty LocalId where
  pretty :: Int -> Int -> LocalId -> String
pretty Int
n Int
i (LocalId Int
x) = String
"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
- Int
1)

instance Pretty GlobalId where
  pretty :: Int -> Int -> GlobalId -> String
pretty Int
n Int
i (GlobalId [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
"_" [String]
m

instance Pretty MemberId where
  pretty :: Int -> Int -> MemberId -> String
pretty Int
n Int
i (MemberId String
s) = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
unescapes String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""

-- Pretty print expressions

instance Pretty Exp where
  pretty :: Int -> Int -> Exp -> String
pretty Int
n Int
i (Exp
Self)                 = String
"exports"
  pretty Int
n Int
i (Local LocalId
x)              = Int -> Int -> LocalId -> String
forall a. Pretty a => Int -> Int -> a -> String
pretty Int
n Int
i LocalId
x
  pretty Int
n Int
i (Global GlobalId
m)             = Int -> Int -> GlobalId -> String
forall a. Pretty a => Int -> Int -> a -> String
pretty Int
n Int
i GlobalId
m
  pretty Int
n Int
i (Exp
Undefined)            = String
"undefined"
  pretty Int
n Int
i (String String
s)             = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> String
unescapes String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  pretty Int
n Int
i (Char Char
c)               = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char -> String
unescape Char
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""
  pretty Int
n Int
i (Integer Integer
x)            = String
"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]
++ String
"\")"
  pretty Int
n Int
i (Double Double
x)             = Double -> String
forall a. Show a => a -> String
show Double
x
  pretty Int
n Int
i (Lambda Int
x Exp
e)           =
    String
"function (" String -> String -> String
forall a. [a] -> [a] -> [a]
++
      String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (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
-Int
1, Int
xInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2 .. Int
0])) String -> String -> String
forall a. [a] -> [a] -> [a]
++
    String
") " 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 Int
n Int
i (Object Map MemberId Exp
o) | Map MemberId Exp -> Bool
forall k a. Map k a -> Bool
null Map MemberId Exp
o    = String
"{}"
  pretty Int
n Int
i (Object Map MemberId Exp
o) | Bool
otherwise =
    String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
br (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate (String
"," String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
br (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
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]
++ String
"}"
  pretty Int
n Int
i (Apply Exp
f [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 -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
", " (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]
++ String
")"
  pretty Int
n Int
i (Lookup Exp
e 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 -> 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]
++ String
"]"
  pretty Int
n Int
i (If Exp
e Exp
f Exp
g)             =
    String
"(" 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 -> 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 -> 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]
++ String
")"
  pretty Int
n Int
i (PreOp String
op Exp
e)           = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " 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
")"
  pretty Int
n Int
i (BinOp Exp
e String
op Exp
f)         = String
"(" 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 -> String
forall a. [a] -> [a] -> [a]
++ String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" " 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
")"
  pretty Int
n Int
i (Const String
c)              = String
c
  pretty Int
n Int
i (PlainJS String
js)           = String
"(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
js String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

block :: Nat -> Int -> Exp -> String
block :: Int -> Int -> Exp -> String
block Int
n Int
i (If Exp
e Exp
f Exp
g) = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
br (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
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
+Int
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]
++ String
"}"
block Int
n Int
i Exp
e          = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
br (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"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
+Int
1) Exp
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
";" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
br Int
i String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"

block' :: Nat -> Int -> Exp -> String
block' :: Int -> Int -> Exp -> String
block' Int
n Int
i (If Exp
e Exp
f Exp
g) = String
"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 -> 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]
++ String
" else " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Int -> Exp -> String
block' Int
n Int
i Exp
g
block' Int
n Int
i Exp
e          = Int -> Int -> Exp -> String
block Int
n Int
i Exp
e

modname :: GlobalId -> String
modname :: GlobalId -> String
modname (GlobalId [String]
ms) = String
"\"" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"." [String]
ms String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\""


exports :: Nat -> Int -> Set [MemberId] -> [Export] -> String
exports :: Int -> Int -> Set [MemberId] -> [Export] -> String
exports Int
n Int
i Set [MemberId]
lss [] = String
""
exports Int
n Int
i Set [MemberId]
lss (Export [MemberId]
ls Exp
e : [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 =
  String
"exports[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"][" (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 -> 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
+Int
1) Exp
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
";" 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 Int
n Int
i Set [MemberId]
lss (Export [MemberId]
ls Exp
e : [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 Int
n Int
i (Module GlobalId
m [Export]
es 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 String
"" (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
$
            [String
"var agdaRTS = require(\"agda-rts\");"] [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++
            [String
"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
+Int
1) GlobalId
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" = require(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ GlobalId -> String
modname GlobalId
e String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
");"
            | GlobalId
e <- [GlobalId]
js]

variableName :: String -> String
variableName :: String -> String
variableName String
s = if String -> Bool
isValidJSIdent String
s then String
"z_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s else String
"h_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show (String -> Word64
hashString String
s)

-- | Check if a string is a valid JS identifier. The check ignores keywords
-- as we prepend z_ to our identifiers. The check
-- is conservative and may not admit all valid JS identifiers.

isValidJSIdent :: String -> Bool
isValidJSIdent :: String -> Bool
isValidJSIdent []     = Bool
False
isValidJSIdent (Char
c: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 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
== Char
'_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'$'

  validOther :: Char -> Bool
  validOther :: Char -> Bool
validOther Char
c = Char -> Bool
validFirst Char
c Bool -> Bool -> Bool
|| Char -> Bool
isDigit Char
c