    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)

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

    -- 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 n i (x,y) = pretty n i x ++ ": " ++ pretty n (i+1) y

    -- Pretty-print collections

    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)

    -- Pretty print identifiers

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

    -- Pretty print expressions

    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)

    -- | 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 s = matchTest regex s
      where
        regex :: Regex
        regex = makeRegex ("^[a-zA-Z_$][0-9a-zA-Z_$]*$" :: String)