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 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)

-- 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 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

-- Pretty-print collections

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)

-- Pretty print identifiers

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]
++ "\""

-- Pretty print expressions

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)

-- | 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 (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