Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Compiler.JS.Pretty

Synopsis

Documentation

data JSModuleStyle Source #

Constructors

JSCJS 
JSAMD 

Instances

Instances details
Generic JSModuleStyle Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Associated Types

type Rep JSModuleStyle :: Type -> Type

NFData JSModuleStyle 
Instance details

Defined in Agda.Compiler.JS.Compiler

Methods

rnf :: JSModuleStyle -> ()

type Rep JSModuleStyle Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

type Rep JSModuleStyle = D1 ('MetaData "JSModuleStyle" "Agda.Compiler.JS.Pretty" "Agda-2.6.3.20230930-inplace" 'False) (C1 ('MetaCons "JSCJS" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "JSAMD" 'PrefixI 'False) (U1 :: Type -> Type))

data Doc Source #

Constructors

Doc String 
Indent Int Doc 
Group Doc 
Beside Doc Doc 
Above Doc Doc 
Enclose Doc Doc Doc 
Space 
Empty 

Instances

Instances details
IsString Doc Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

fromString :: String -> Doc

Monoid Doc Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

mempty :: Doc

mappend :: Doc -> Doc -> Doc

mconcat :: [Doc] -> Doc

Semigroup Doc Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

(<>) :: Doc -> Doc -> Doc #

sconcat :: NonEmpty Doc -> Doc

stimes :: Integral b => b -> Doc -> Doc

render :: Bool -> Doc -> String Source #

($+$) :: Doc -> Doc -> Doc infixr 5 Source #

($++$) :: Doc -> Doc -> Doc infixr 5 Source #

Separate by blank line.

(<+>) :: Doc -> Doc -> Doc infixr 6 Source #

Separate by space that will be removed by minify.

For non-removable space, use d <> " " <> d'.

text :: String -> Doc Source #

indentBy :: Int -> Doc -> Doc Source #

enclose :: Doc -> Doc -> Doc -> Doc Source #

hcat :: [Doc] -> Doc Source #

vcat :: [Doc] -> Doc Source #

vsep :: [Doc] -> Doc Source #

Concatenate vertically, separated by blank lines.

mparens :: Bool -> Doc -> Doc Source #

Apply parens to Doc if boolean is true.

unescape :: Char -> String Source #

unescapes :: String -> Doc Source #

class Pretty a where Source #

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> a -> Doc Source #

Instances

Instances details
Pretty Comment Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Comment -> Doc Source #

Pretty Exp Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Exp -> Doc Source #

Pretty GlobalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> GlobalId -> Doc Source #

Pretty LocalId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> LocalId -> Doc Source #

Pretty MemberId Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> MemberId -> Doc Source #

Pretty Module Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Module -> Doc Source #

Pretty a => Pretty (Maybe a) Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> Maybe a -> Doc Source #

Pretty [(GlobalId, Export)] Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> [(GlobalId, Export)] -> Doc Source #

(Pretty a, Pretty b) => Pretty (a, b) Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretty :: (Nat, Bool, JSModuleStyle) -> (a, b) -> Doc Source #

prettyShow :: Pretty a => Bool -> JSModuleStyle -> a -> String Source #

class Pretties a where Source #

Methods

pretties :: (Nat, Bool, JSModuleStyle) -> a -> [Doc] Source #

Instances

Instances details
Pretty a => Pretties (List1 a) Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretties :: (Nat, Bool, JSModuleStyle) -> List1 a -> [Doc] Source #

Pretty a => Pretties [a] Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretties :: (Nat, Bool, JSModuleStyle) -> [a] -> [Doc] Source #

(Pretty a, Pretty b) => Pretties (Map a b) Source # 
Instance details

Defined in Agda.Compiler.JS.Pretty

Methods

pretties :: (Nat, Bool, JSModuleStyle) -> Map a b -> [Doc] Source #

block :: (Nat, Bool, JSModuleStyle) -> Exp -> Doc Source #

exports :: (Nat, Bool, JSModuleStyle) -> Set JSQName -> [Export] -> Doc Source #

variableName :: String -> String Source #

isValidJSIdent :: String -> Bool Source #

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.