    module Agda.Compiler.JS.Pretty where

    import Data.Char ( isAsciiLower, isAsciiUpper, isDigit )
    import Data.List ( intercalate )
    import Data.String ( IsString (fromString) )
    import Data.Semigroup ( Semigroup, (<>) )
    import Data.Set ( Set, toList, singleton, insert, member )
    import qualified Data.Set as Set
    import Data.Map ( Map, toAscList, empty, null )
    import qualified Data.Text as T

    import Agda.Syntax.Common ( Nat )

    import Agda.Utils.Hash
    import Agda.Utils.List ( indexWithDefault )
    import Agda.Utils.List1 ( List1, pattern (:|), (<|) )
    import qualified Agda.Utils.List1 as List1

    import Agda.Utils.Impossible

    import Agda.Compiler.JS.Syntax hiding (exports)

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

    --- The indentation combinators of the pretty library does not fit C-like languages
    --- like ECMAScript.
    --- A simple pretty printer is implemented with a better `indent` and punctuation compaction.
    ---
    --- More explanation:
    ---
    --- I have struggled with different pretty printers, and at the end it was much easier
    --- to implement and use this ~100 SLOC code pretty printer library.
    --- It produces really better quality indentation than I could achieve with the
    --  standard pretty printers.
    --- This library code is only used in this module, and it is specialized to pretty
    --- print JavaScript code for the Agda backend, so I think its best place is in this module.
    data Doc
        = Doc String
        | Indent Int Doc
        | Group Doc
        | Beside Doc Doc
        | Above Doc Doc
        | Enclose Doc Doc Doc
        | Space
        | Empty

    minifiedCodeLinesLength :: Int
    minifiedCodeLinesLength :: Int
    minifiedCodeLinesLength = Int
    500

    render :: Bool -> Doc -> String
    render :: Bool -> Doc -> [Char]
    render Bool
    minify = [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "\n" ([[Char]] -> [Char]) -> (Doc -> [[Char]]) -> Doc -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [[Char]] -> [[Char]]
    joinLines ([[Char]] -> [[Char]]) -> (Doc -> [[Char]]) -> Doc -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((Int, [Char]) -> [Char]) -> [(Int, [Char])] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int -> [Char] -> [Char]) -> (Int, [Char]) -> [Char]
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Int -> [Char] -> [Char]
    mkIndent) ([(Int, [Char])] -> [[Char]])
    -> (Doc -> [(Int, [Char])]) -> Doc -> [[Char]]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Doc -> [(Int, [Char])]
    go Int
    0
      where
        joinLines :: [String] -> [String]
        joinLines :: [[Char]] -> [[Char]]
    joinLines = if Bool
    minify then Int -> [[Char]] -> [[Char]] -> [[Char]]
    forall {a}. Int -> [[a]] -> [[a]] -> [[a]]
    chunks Int
    0 [] else [[Char]] -> [[Char]]
    forall a. a -> a
    id
          where
            chunks :: Int -> [[a]] -> [[a]] -> [[a]]
    chunks Int
    len [[a]]
    acc [] = [[[a]] -> [a]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[a]] -> [[a]]
    forall a. [a] -> [a]
    reverse [[a]]
    acc)]
            chunks Int
    len [[a]]
    acc ([a]
    s: [[a]]
    ss)
                | Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    minifiedCodeLinesLength = Int -> [[a]] -> [[a]] -> [[a]]
    chunks (Int
    len Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    n) ([a]
    s[a] -> [[a]] -> [[a]]
    forall a. a -> [a] -> [a]
    : [[a]]
    acc) [[a]]
    ss
                | Bool
    otherwise = [[a]] -> [a]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[a]] -> [[a]]
    forall a. [a] -> [a]
    reverse [[a]]
    acc)[a] -> [[a]] -> [[a]]
    forall a. a -> [a] -> [a]
    : Int -> [[a]] -> [[a]] -> [[a]]
    chunks Int
    n [[a]
    s] [[a]]
    ss
              where
                n :: Int
    n = [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [a]
    s

        joinBy :: (a -> a -> [a]) -> [a] -> [a] -> [a]
    joinBy a -> a -> [a]
    f [a
    x] (a
    y: [a]
    ys) = a -> a -> [a]
    f a
    x a
    y [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a]
    ys
        joinBy a -> a -> [a]
    f (a
    x:[a]
    xs) [a]
    ys = a
    xa -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : (a -> a -> [a]) -> [a] -> [a] -> [a]
    joinBy a -> a -> [a]
    f [a]
    xs [a]
    ys
        joinBy a -> a -> [a]
    f [a]
    xs [a]
    ys = [a]
    xs [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    ++ [a]
    ys

        mkIndent :: Int -> [Char] -> [Char]
    mkIndent Int
    n [Char]
    s | Bool
    minify = [Char]
    s
        mkIndent Int
    n [Char]
    "" = [Char]
    ""
        mkIndent Int
    n [Char]
    s = Int -> Char -> [Char]
    forall a. Int -> a -> [a]
    replicate Int
    n Char
    ' ' [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s

        overlay :: (Int, [Char]) -> (Int, [Char]) -> [(Int, [Char])]
    overlay (Int
    i, [Char]
    s) (Int
    j, [Char]
    s') | (Char -> Bool) -> [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    punctuation ([Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s') Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 = [(Int
    i, [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char] -> [Char]
    mkIndent Int
    n [Char]
    s')]
          where n :: Int
    n = Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    s)
        overlay (Int
    j, [Char]
    s') (Int
    i, [Char]
    s) | (Char -> Bool) -> [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    punctuation ([Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s') Bool -> Bool -> Bool
    && Int
    n Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    0 = [(Int
    i, [Char]
    s' [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Int -> [Char] -> [Char]
    mkIndent Int
    n [Char]
    s)]
          where n :: Int
    n = Int
    j Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + [Char] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [Char]
    s)
        overlay (Int, [Char])
    a (Int, [Char])
    b = [(Int, [Char])
    a, (Int, [Char])
    b]

        punctuation :: Char -> Bool
    punctuation = (Char -> [Char] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` ([Char]
    "(){}[];:, " :: String))

        go :: Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    Space = if Bool
    minify then [] else [(Int
    i, [Char]
    " ")]
        go Int
    i Doc
    Empty = []
        go Int
    i (Doc [Char]
    s) = [(Int
    i, [Char]
    s)]
        go Int
    i (Beside Doc
    d Doc
    d') = ((Int, [Char]) -> (Int, [Char]) -> [(Int, [Char])])
    -> [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall {a}. (a -> a -> [a]) -> [a] -> [a] -> [a]
    joinBy (\(Int
    i, [Char]
    s) (Int
    _, [Char]
    s') -> [(Int
    i, [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s')]) (Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    d) (Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    d')
        go Int
    i (Above Doc
    d Doc
    d') = ((Int, [Char]) -> (Int, [Char]) -> [(Int, [Char])])
    -> [(Int, [Char])] -> [(Int, [Char])] -> [(Int, [Char])]
    forall {a}. (a -> a -> [a]) -> [a] -> [a] -> [a]
    joinBy (Int, [Char]) -> (Int, [Char]) -> [(Int, [Char])]
    overlay (Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    d) (Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    d')
        go Int
    i (Indent Int
    j Doc
    d) = Int -> Doc -> [(Int, [Char])]
    go (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    j) Doc
    d
        go Int
    i (Enclose Doc
    open Doc
    close Doc
    d) = Int -> Doc -> [(Int, [Char])]
    go Int
    i (Doc -> [(Int, [Char])]) -> Doc -> [(Int, [Char])]
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc
    Group (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc -> Doc
    Above Doc
    open (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> Doc -> Doc
    Above Doc
    d Doc
    close
        go Int
    i (Group Doc
    d)
            | [(Int, [Char])] -> Int
    forall {a} {a}. [(a, [a])] -> Int
    size [(Int, [Char])]
    ss Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    40 = [(Int, [Char])] -> [(Int, [Char])]
    forall {a} {b}. [(a, [b])] -> [(a, [b])]
    compact [(Int, [Char])]
    ss
            | Bool
    otherwise    = [(Int, [Char])]
    ss
          where
            ss :: [(Int, [Char])]
    ss = Int -> Doc -> [(Int, [Char])]
    go Int
    i Doc
    d
            size :: [(a, [a])] -> Int
    size = [Int] -> Int
    forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
    sum ([Int] -> Int) -> ([(a, [a])] -> [Int]) -> [(a, [a])] -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ((a, [a]) -> Int) -> [(a, [a])] -> [Int]
    forall a b. (a -> b) -> [a] -> [b]
    map ([a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length ([a] -> Int) -> ((a, [a]) -> [a]) -> (a, [a]) -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a, [a]) -> [a]
    forall a b. (a, b) -> b
    snd)
            compact :: [(a, [b])] -> [(a, [b])]
    compact [] = []
            compact ((a
    i, [b]
    x): [(a, [b])]
    xs) = [(a
    i, [b]
    x [b] -> [b] -> [b]
    forall a. [a] -> [a] -> [a]
    ++ ((a, [b]) -> [b]) -> [(a, [b])] -> [b]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap (a, [b]) -> [b]
    forall a b. (a, b) -> b
    snd [(a, [b])]
    xs)]

    instance IsString Doc where
        fromString :: [Char] -> Doc
    fromString = [Char] -> Doc
    Doc

    instance Semigroup Doc where
        Doc
    Empty <> :: Doc -> Doc -> Doc
    <> Doc
    d = Doc
    d
        Doc
    d <> Doc
    Empty = Doc
    d
        Doc
    d <> Doc
    d' = Doc -> Doc -> Doc
    Beside Doc
    d Doc
    d'

    instance Monoid Doc where
        mempty :: Doc
    mempty = Doc
    Empty
        mappend :: Doc -> Doc -> Doc
    mappend = Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    (<>)

    infixr 5 $+$
    infixr 5 $++$
    infixr 6 <+>  -- fixity has to match the one of Semigroup.(<>)

    ($+$) :: Doc -> Doc -> Doc
    Doc
    Empty $+$ :: Doc -> Doc -> Doc
    $+$ Doc
    d = Doc
    d
    Doc
    d $+$ Doc
    Empty = Doc
    d
    Doc
    d $+$ Doc
    d' = Doc -> Doc -> Doc
    Above Doc
    d Doc
    d'

    -- | Separate by blank line.

    ($++$) :: Doc -> Doc -> Doc
    Doc
    Empty $++$ :: Doc -> Doc -> Doc
    $++$ Doc
    d = Doc
    d
    Doc
    d $++$ Doc
    Empty = Doc
    d
    Doc
    d $++$ Doc
    d' = Doc
    d Doc -> Doc -> Doc
    `Above` Doc
    "" Doc -> Doc -> Doc
    `Above` Doc
    d'

    -- | Separate by space that will be removed by minify.
    --
    -- For non-removable space, use @d <> " " <> d'@.

    (<+>) :: Doc -> Doc -> Doc
    Doc
    Empty <+> :: Doc -> Doc -> Doc
    <+> Doc
    d = Doc
    d
    Doc
    d <+> Doc
    Empty = Doc
    d
    Doc
    d <+> Doc
    d' = Doc
    d Doc -> Doc -> Doc
    `Beside` Doc
    Space Doc -> Doc -> Doc
    `Beside` Doc
    d'

    text :: String -> Doc
    text :: [Char] -> Doc
    text = [Char] -> Doc
    Doc

    group :: Doc -> Doc
    group :: Doc -> Doc
    group = Doc -> Doc
    Group

    indentBy :: Int -> Doc -> Doc
    indentBy :: Int -> Doc -> Doc
    indentBy Int
    i Doc
    Empty = Doc
    Empty
    indentBy Int
    i (Indent Int
    j Doc
    d) = Int -> Doc -> Doc
    Indent (Int
    iInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    j) Doc
    d
    indentBy Int
    i Doc
    d = Int -> Doc -> Doc
    Indent Int
    i Doc
    d

    enclose :: Doc -> Doc -> Doc -> Doc
    enclose :: Doc -> Doc -> Doc -> Doc
    enclose Doc
    open Doc
    close (Enclose Doc
    o Doc
    c Doc
    d) = Doc -> Doc -> Doc -> Doc
    Enclose (Doc
    open Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    o) (Doc
    c Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    close) Doc
    d
    enclose Doc
    open Doc
    close (Indent Int
    _ (Enclose Doc
    o Doc
    c Doc
    d)) = Doc -> Doc -> Doc -> Doc
    Enclose (Doc
    open Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    o) (Doc
    c Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    close) Doc
    d
    enclose Doc
    open Doc
    close Doc
    d = Doc -> Doc -> Doc -> Doc
    Enclose Doc
    open Doc
    close Doc
    d

    ----------------------------------------------------------------------------------------------

    space :: Doc
    space :: Doc
    space = Doc
    Space

    indent :: Doc -> Doc
    indent :: Doc -> Doc
    indent = Int -> Doc -> Doc
    indentBy Int
    2

    hcat :: [Doc] -> Doc
    hcat :: [Doc] -> Doc
    hcat = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    (<>) Doc
    forall a. Monoid a => a
    mempty

    vcat :: [Doc] -> Doc
    vcat :: [Doc] -> Doc
    vcat = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Doc -> Doc -> Doc
    ($+$) Doc
    forall a. Monoid a => a
    mempty

    -- | Concatenate vertically, separated by blank lines.

    vsep :: [Doc] -> Doc
    vsep :: [Doc] -> Doc
    vsep = (Doc -> Doc -> Doc) -> Doc -> [Doc] -> Doc
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr Doc -> Doc -> Doc
    ($++$) Doc
    forall a. Monoid a => a
    mempty

    punctuate :: Doc -> [Doc] -> Doc
    punctuate :: Doc -> [Doc] -> Doc
    punctuate Doc
    _ []     = Doc
    forall a. Monoid a => a
    mempty
    punctuate Doc
    p (Doc
    x:[Doc]
    xs) = Doc -> Doc
    indent (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Doc] -> Doc
    vcat ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> [Doc]
    go Doc
    x [Doc]
    xs
                       where go :: Doc -> [Doc] -> [Doc]
    go Doc
    y []     = [Doc
    y]
                             go Doc
    y (Doc
    z:[Doc]
    zs) = (Doc
    y Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    p) Doc -> [Doc] -> [Doc]
    forall a. a -> [a] -> [a]
    : Doc -> [Doc] -> [Doc]
    go Doc
    z [Doc]
    zs

    parens, brackets, braces :: Doc -> Doc
    parens :: Doc -> Doc
    parens   = Doc -> Doc -> Doc -> Doc
    enclose Doc
    "(" Doc
    ")"
    brackets :: Doc -> Doc
    brackets = Doc -> Doc -> Doc -> Doc
    enclose Doc
    "[" Doc
    "]"
    braces :: Doc -> Doc
    braces   = Doc -> Doc -> Doc -> Doc
    enclose Doc
    "{" Doc
    "}"

    -- | Apply 'parens' to 'Doc' if boolean is true.
    mparens :: Bool -> Doc -> Doc
    mparens :: Bool -> Doc -> Doc
    mparens Bool
    True  Doc
    d = Doc -> Doc
    parens Doc
    d
    mparens Bool
    False Doc
    d = Doc
    d

    ----------------------------------------------------------------------------------------------

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

    unescapes :: String -> Doc
    unescapes :: [Char] -> Doc
    unescapes [Char]
    s = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Char -> [Char]) -> [Char] -> [Char]
    forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
    concatMap Char -> [Char]
    unescape [Char]
    s

    -- pretty (n,b) i e pretty-prints e, under n levels of de Bruijn binding
    --   if b is true then the output is minified

    class Pretty a where
        pretty :: (Nat, Bool) -> a -> Doc

    prettyShow :: Pretty a => Bool -> a -> String
    prettyShow :: forall a. Pretty a => Bool -> a -> [Char]
    prettyShow Bool
    minify = Bool -> Doc -> [Char]
    render Bool
    minify (Doc -> [Char]) -> (a -> Doc) -> a -> [Char]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int, Bool) -> a -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int
    0, Bool
    minify)

    instance Pretty a => Pretty (Maybe a) where
      pretty :: (Int, Bool) -> Maybe a -> Doc
    pretty (Int, Bool)
    n = Doc -> (a -> Doc) -> Maybe a -> Doc
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc
    forall a. Monoid a => a
    mempty ((Int, Bool) -> a -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n)

    instance (Pretty a, Pretty b) => Pretty (a,b) where
      pretty :: (Int, Bool) -> (a, b) -> Doc
    pretty (Int, Bool)
    n (a
    x,b
    y) = (Int, Bool) -> a -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n a
    x Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ":" Doc -> Doc -> Doc
    <+> (Int, Bool) -> b -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n b
    y

    -- Pretty-print collections

    class Pretties a where
        pretties :: (Nat, Bool) -> a -> [Doc]

    instance Pretty a => Pretties [a] where
      pretties :: (Int, Bool) -> [a] -> [Doc]
    pretties (Int, Bool)
    n = (a -> Doc) -> [a] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Int, Bool) -> a -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n)

    instance Pretty a => Pretties (List1 a) where
      pretties :: (Int, Bool) -> List1 a -> [Doc]
    pretties (Int, Bool)
    n = (Int, Bool) -> [a] -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n ([a] -> [Doc]) -> (List1 a -> [a]) -> List1 a -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . List1 a -> [a]
    forall a. NonEmpty a -> [a]
    List1.toList

    instance (Pretty a, Pretty b) => Pretties (Map a b) where
      pretties :: (Int, Bool) -> Map a b -> [Doc]
    pretties (Int, Bool)
    n = (Int, Bool) -> [(a, b)] -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n ([(a, b)] -> [Doc]) -> (Map a b -> [(a, b)]) -> Map a b -> [Doc]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Map a b -> [(a, b)]
    forall k a. Map k a -> [(k, a)]
    toAscList

    -- Pretty print identifiers

    instance Pretty LocalId where
      pretty :: (Int, Bool) -> LocalId -> Doc
    pretty (Int
    n, Bool
    _) (LocalId Int
    x) = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> Int -> [Char]
    forall a. a -> [a] -> Int -> a
    indexWithDefault [Char]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ [[Char]]
    vars (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)
        where
          vars :: [[Char]]
    vars = ([Char]
    ""[Char] -> [[Char]] -> [[Char]]
    forall a. a -> [a] -> [a]
    : (Integer -> [Char]) -> [Integer] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map Integer -> [Char]
    forall a. Show a => a -> [Char]
    show [Integer
    0..]) [[Char]] -> ([Char] -> [[Char]]) -> [[Char]]
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= \[Char]
    s -> (Char -> [Char]) -> [Char] -> [[Char]]
    forall a b. (a -> b) -> [a] -> [b]
    map (Char -> [Char] -> [Char]
    forall a. a -> [a] -> [a]
    :[Char]
    s) [Char
    'a'..Char
    'z']

    instance Pretty GlobalId where
      pretty :: (Int, Bool) -> GlobalId -> Doc
    pretty (Int, Bool)
    n (GlobalId [[Char]]
    m) = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [Char]
    variableName ([Char] -> [Char]) -> [Char] -> [Char]
    forall a b. (a -> b) -> a -> b
    $ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "_" [[Char]]
    m

    instance Pretty MemberId where
      pretty :: (Int, Bool) -> MemberId -> Doc
    pretty (Int, Bool)
    _ (MemberId [Char]
    s) = Doc
    "\"" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    unescapes [Char]
    s Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "\""
      pretty (Int, Bool)
    n (MemberIndex Int
    i Comment
    comment) = [Char] -> Doc
    text (Int -> [Char]
    forall a. Show a => a -> [Char]
    show Int
    i) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Int, Bool) -> Comment -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Comment
    comment

    instance Pretty Comment where
      pretty :: (Int, Bool) -> Comment -> Doc
    pretty (Int, Bool)
    _ (Comment [Char]
    "") = Doc
    forall a. Monoid a => a
    mempty
      pretty (Int
    _, Bool
    True) Comment
    _ = Doc
    forall a. Monoid a => a
    mempty
      pretty (Int, Bool)
    _ (Comment [Char]
    s) = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "/* " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    " */"

    -- Pretty print expressions

    instance Pretty Exp where
      pretty :: (Int, Bool) -> Exp -> Doc
    pretty (Int, Bool)
    n (Exp
    Self)            = Doc
    "exports"
      pretty (Int, Bool)
    n (Local LocalId
    x)         = (Int, Bool) -> LocalId -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n LocalId
    x
      pretty (Int, Bool)
    n (Global GlobalId
    m)        = (Int, Bool) -> GlobalId -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n GlobalId
    m
      pretty (Int, Bool)
    n (Exp
    Undefined)       = Doc
    "undefined"
      pretty (Int, Bool)
    n (Exp
    Null)            = Doc
    "null"
      pretty (Int, Bool)
    n (String Text
    s)        = Doc
    "\"" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    unescapes (Text -> [Char]
    T.unpack Text
    s) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "\""
      pretty (Int, Bool)
    n (Char Char
    c)          = Doc
    "\"" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    unescapes [Char
    c] Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "\""
      pretty (Int, Bool)
    n (Integer Integer
    x)       = Doc
    "agdaRTS.primIntegerFromString(\"" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    text (Integer -> [Char]
    forall a. Show a => a -> [Char]
    show Integer
    x) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "\")"
      pretty (Int, Bool)
    n (Double Double
    x)        = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ Double -> [Char]
    forall a. Show a => a -> [Char]
    show Double
    x
      pretty (Int
    n, Bool
    min) (Lambda Int
    x Exp
    e) =
        Bool -> Doc -> Doc
    mparens (Int
    x Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Int
    1) (Doc -> [Doc] -> Doc
    punctuate Doc
    "," ((Int, Bool) -> [LocalId] -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    x, Bool
    min) ((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])))
        Doc -> Doc -> Doc
    <+> Doc
    "=>" Doc -> Doc -> Doc
    <+> (Int, Bool) -> Exp -> Doc
    block (Int
    nInt -> Int -> Int
    forall a. Num a => a -> a -> a
    +Int
    x, Bool
    min) Exp
    e
      pretty (Int, Bool)
    n (Object Map MemberId Exp
    o)        = Doc -> Doc
    braces (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> Doc
    punctuate Doc
    "," ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Int, Bool) -> Map MemberId Exp -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n Map MemberId Exp
    o
      pretty (Int, Bool)
    n (Array [(Comment, Exp)]
    es)        = Doc -> Doc
    brackets (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ Doc -> [Doc] -> Doc
    punctuate Doc
    "," [(Int, Bool) -> Comment -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Comment
    c Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e | (Comment
    c, Exp
    e) <- [(Comment, Exp)]
    es]
      pretty (Int, Bool)
    n (Apply Exp
    f [Exp]
    es)      = (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    f Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    parens (Doc -> [Doc] -> Doc
    punctuate Doc
    "," ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Int, Bool) -> [Exp] -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n [Exp]
    es)
      pretty (Int, Bool)
    n (Lookup Exp
    e MemberId
    l)      = (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    brackets ((Int, Bool) -> MemberId -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n MemberId
    l)
      pretty (Int, Bool)
    n (If Exp
    e Exp
    f Exp
    g)        = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    "?" Doc -> Doc -> Doc
    <+> (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    f Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ":" Doc -> Doc -> Doc
    <+> (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    g
      pretty (Int, Bool)
    n (PreOp [Char]
    op Exp
    e)      = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char] -> Doc
    text [Char]
    op Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    " " Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e
      pretty (Int, Bool)
    n (BinOp Exp
    e [Char]
    op Exp
    f)    = Doc -> Doc
    parens (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    " " Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Char] -> Doc
    text [Char]
    op Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    " " Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    f
      pretty (Int, Bool)
    n (Const [Char]
    c)         = [Char] -> Doc
    text [Char]
    c
      pretty (Int, Bool)
    n (PlainJS [Char]
    js)      = [Char] -> Doc
    text [Char]
    js

    block :: (Nat, Bool) -> Exp -> Doc
    block :: (Int, Bool) -> Exp -> Doc
    block (Int, Bool)
    n Exp
    e = Bool -> Doc -> Doc
    mparens (Exp -> Bool
    doNest Exp
    e) (Doc -> Doc) -> Doc -> Doc
    forall a b. (a -> b) -> a -> b
    $ (Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e
      where
        doNest :: Exp -> Bool
    doNest Object{} = Bool
    True
        doNest Exp
    _ = Bool
    False

    modname :: GlobalId -> Doc
    modname :: GlobalId -> Doc
    modname (GlobalId [[Char]]
    ms) = [Char] -> Doc
    text ([Char] -> Doc) -> [Char] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "\"" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char] -> [[Char]] -> [Char]
    forall a. [a] -> [[a]] -> [a]
    intercalate [Char]
    "." [[Char]]
    ms [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    "\""

    exports :: (Nat, Bool) -> Set JSQName -> [Export] -> Doc
    exports :: (Int, Bool) -> Set JSQName -> [Export] -> Doc
    exports (Int, Bool)
    n Set JSQName
    lss [] = Doc
    Empty
    exports (Int, Bool)
    n Set JSQName
    lss es0 :: [Export]
    es0@(Export JSQName
    ls Exp
    e : [Export]
    es)
      -- If the parent of @ls@ is already defined (or no parent exists), @ls@ can be defined
      | Bool -> (JSQName -> Bool) -> Maybe JSQName -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (JSQName -> Set JSQName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `member` Set JSQName
    lss) Maybe JSQName
    parent =
          Doc
    "exports" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Doc] -> Doc
    hcat ((Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> Doc
    brackets ((Int, Bool) -> JSQName -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n JSQName
    ls)) Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Doc -> Doc
    indent ((Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ";" Doc -> Doc -> Doc
    $+$
          (Int, Bool) -> Set JSQName -> [Export] -> Doc
    exports (Int, Bool)
    n (JSQName -> Set JSQName -> Set JSQName
    forall a. Ord a => a -> Set a -> Set a
    insert JSQName
    ls Set JSQName
    lss) [Export]
    es
      -- If the parent is not yet defined, first define it as empty object, and then continue with @ls@.
      | Bool
    otherwise =
          (Int, Bool) -> Set JSQName -> [Export] -> Doc
    exports (Int, Bool)
    n Set JSQName
    lss ([Export] -> Doc) -> [Export] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [Export] -> (JSQName -> [Export]) -> Maybe JSQName -> [Export]
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe [Export]
    es0 (\ JSQName
    ls' -> JSQName -> Exp -> Export
    Export JSQName
    ls' (Map MemberId Exp -> Exp
    Object Map MemberId Exp
    forall a. Monoid a => a
    mempty) Export -> [Export] -> [Export]
    forall a. a -> [a] -> [a]
    : [Export]
    es0) Maybe JSQName
    parent
      where
      parent :: Maybe JSQName
    parent = [MemberId] -> Maybe JSQName
    forall a. [a] -> Maybe (NonEmpty a)
    List1.nonEmpty ([MemberId] -> Maybe JSQName) -> [MemberId] -> Maybe JSQName
    forall a b. (a -> b) -> a -> b
    $ JSQName -> [MemberId]
    forall a. NonEmpty a -> [a]
    List1.init JSQName
    ls

    instance Pretty [(GlobalId, Export)] where
      pretty :: (Int, Bool) -> [(GlobalId, Export)] -> Doc
    pretty (Int, Bool)
    n [(GlobalId, Export)]
    es
        = [Doc] -> Doc
    vcat [ (Int, Bool) -> GlobalId -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n GlobalId
    g Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> [Doc] -> Doc
    hcat ((Doc -> Doc) -> [Doc] -> [Doc]
    forall a b. (a -> b) -> [a] -> [b]
    map Doc -> Doc
    brackets ((Int, Bool) -> JSQName -> [Doc]
    forall a. Pretties a => (Int, Bool) -> a -> [Doc]
    pretties (Int, Bool)
    n JSQName
    ls)) Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Doc -> Doc
    indent ((Int, Bool) -> Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Exp
    e) Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ";"
               | (GlobalId
    g, Export JSQName
    ls Exp
    e) <- [(GlobalId, Export)]
    es ]

    instance Pretty Module where
      pretty :: (Int, Bool) -> Module -> Doc
    pretty (Int, Bool)
    n (Module GlobalId
    m [GlobalId]
    is [Export]
    es Maybe Exp
    callMain) = [Doc] -> Doc
    vsep
        [ Doc
    importRTS
        , Doc
    imports
        , (Int, Bool) -> Set JSQName -> [Export] -> Doc
    exports (Int, Bool)
    n Set JSQName
    forall a. Set a
    Set.empty [Export]
    es
        , (Int, Bool) -> Maybe Exp -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n Maybe Exp
    callMain
        ]
        Doc -> Doc -> Doc
    $+$ Doc
    "" -- Final newline
        where
          importRTS :: Doc
    importRTS = Doc
    "var agdaRTS" Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Doc
    "require(\"agda-rts\");"
          imports :: Doc
    imports   = [Doc] -> Doc
    vcat
            [ Doc
    "var " Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc -> Doc
    indent ((Int, Bool) -> GlobalId -> Doc
    forall a. Pretty a => (Int, Bool) -> a -> Doc
    pretty (Int, Bool)
    n GlobalId
    e) Doc -> Doc -> Doc
    <+> Doc
    "=" Doc -> Doc -> Doc
    <+> Doc
    "require(" Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> GlobalId -> Doc
    modname GlobalId
    e Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Doc
    ");"
            | GlobalId
    e <- Set GlobalId -> [GlobalId]
    forall a. Set a -> [a]
    toList ([Export] -> Set GlobalId
    forall a. Globals a => a -> Set GlobalId
    globals [Export]
    es Set GlobalId -> Set GlobalId -> Set GlobalId
    forall a. Semigroup a => a -> a -> a
    <> [GlobalId] -> Set GlobalId
    forall a. Ord a => [a] -> Set a
    Set.fromList [GlobalId]
    is)
            ]

    variableName :: String -> String
    variableName :: [Char] -> [Char]
    variableName [Char]
    s = if [Char] -> Bool
    isValidJSIdent [Char]
    s then [Char]
    "z_" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ [Char]
    s else [Char]
    "h_" [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Word64 -> [Char]
    forall a. Show a => a -> [Char]
    show ([Char] -> Word64
    hashString [Char]
    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 :: [Char] -> Bool
    isValidJSIdent []     = Bool
    False
    isValidJSIdent (Char
    c:[Char]
    cs) = Char -> Bool
    validFirst Char
    c Bool -> Bool -> Bool
    && (Char -> Bool) -> [Char] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Char -> Bool
    validOther [Char]
    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