{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE RankNTypes #-}

module Render.Concrete where

import qualified Data.Text     as T
import Data.Maybe (isNothing, maybeToList)
import qualified Data.Strict.Maybe as Strict

import Agda.Syntax.Common
import           Agda.Syntax.Concrete
import           Agda.Syntax.Concrete.Pretty (NamedBinding (..), Tel (..), isLabeled)
--import           Agda.Syntax.Position (noRange)
import           Agda.Utils.List1 as List1 (toList, fromList) 
import qualified Agda.Utils.List1 as List1
import qualified Agda.Utils.List2 as List2
import Agda.Utils.Float (toStringWithoutDotZero)
import Agda.Utils.Function (applyWhen)
import Agda.Utils.Functor (dget, (<&>))
import Agda.Utils.Impossible (__IMPOSSIBLE__)

import Render.Class
import Render.Common
import Render.Literal ()
import Render.Name ()
import Render.RichText
import Render.TypeChecking ()

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

instance Render a => Render (WithHiding a) where
  render :: WithHiding a -> Inlines
render WithHiding a
w = forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding WithHiding a
w forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Decoration t => t a -> a
dget WithHiding a
w

instance Render Modality where
  render :: Modality -> Inlines
render Modality
mod = [Inlines] -> Inlines
hsep
    [ forall a. Render a => a -> Inlines
render (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod)
    , forall a. Render a => a -> Inlines
render (forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod)
    , forall a. Render a => a -> Inlines
render (forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
mod)
    ]

-- | OpApp
instance Render (OpApp Expr) where
  render :: OpApp Expr -> Inlines
render (Ordinary Expr
e) = forall a. Render a => a -> Inlines
render Expr
e
  render (SyntaxBindingLambda Range
r List1 LamBinding
bs Expr
e) = forall a. Render a => a -> Inlines
render (Range -> List1 LamBinding -> Expr -> Expr
Lam Range
r List1 LamBinding
bs Expr
e)

-- | MaybePlaceholder
instance Render a => Render (MaybePlaceholder a) where
  render :: MaybePlaceholder a -> Inlines
render Placeholder {} = Inlines
"_"
  render (NoPlaceholder Maybe PositionInName
_ a
e) = forall a. Render a => a -> Inlines
render a
e

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

-- | InteractionId
instance Render InteractionId where
  render :: InteractionId -> Inlines
render (InteractionId Int
i) = Int -> Inlines
linkHole Int
i

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

-- | Expression
instance Render Expr where
  render :: Expr -> Inlines
render Expr
expr = case Expr
expr of
    Ident QName
qname -> forall a. Render a => a -> Inlines
render QName
qname
    Lit Range
range Literal
lit -> forall a. Render a => a -> Inlines
render Literal
lit
    -- no hole index, use LinkRange instead
    QuestionMark Range
range Maybe Int
Nothing -> Range -> Inlines -> Inlines
linkRange Range
range Inlines
"?"
    QuestionMark Range
_range (Just Int
n) -> Int -> Inlines
linkHole Int
n
    Underscore Range
range Maybe String
n -> Range -> Inlines -> Inlines
linkRange Range
range forall a b. (a -> b) -> a -> b
$ forall b a. b -> (a -> b) -> Maybe a -> b
maybe Inlines
"_" String -> Inlines
text Maybe String
n
    -- '_range' is almost always 'NoRange' :(
    App Range
_range Expr
_ NamedArg Expr
_ ->
      case Expr -> AppView
appView Expr
expr of
        AppView Expr
e1 [NamedArg Expr]
args -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Expr
e1 forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [NamedArg Expr]
args
    RawApp Range
_ List2 Expr
es -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall l. IsList l => l -> [Item l]
List2.toList List2 Expr
es)
    OpApp Range
_ QName
q Set Name
_ OpAppArgs
es -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall a.
Render a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
renderOpApp QName
q OpAppArgs
es
    WithApp Range
_ Expr
e [Expr]
es -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Expr
e forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ClassNames -> String -> Inlines
text' [String
"delimiter"] String
"|" Inlines -> Inlines -> Inlines
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [Expr]
es
    HiddenArg Range
_ Named_ Expr
e -> Inlines -> Inlines
braces' forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Named_ Expr
e
    InstanceArg Range
_ Named_ Expr
e -> Inlines -> Inlines
dbraces forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Named_ Expr
e
    Lam Range
_ List1 LamBinding
bs (AbsurdLam Range
_ Hiding
h) -> Inlines
lambda Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 LamBinding
bs)) Inlines -> Inlines -> Inlines
<+> forall {a}. IsString a => Hiding -> a
absurd Hiding
h
    Lam Range
_ List1 LamBinding
bs Expr
e -> [Inlines] -> Inlines
sep [Inlines
lambda Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 LamBinding
bs)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow, forall a. Render a => a -> Inlines
render Expr
e]
    AbsurdLam Range
_ Hiding
h -> Inlines
lambda Inlines -> Inlines -> Inlines
<+> forall {a}. IsString a => Hiding -> a
absurd Hiding
h
    ExtendedLam Range
range Erased
_ List1 LamClause
pes -> Inlines
lambda Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
bracesAndSemicolons (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 LamClause
pes))
    Fun Range
_ Arg Expr
e1 Expr
e2 ->
      [Inlines] -> Inlines
sep
        [ forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion Arg Expr
e1 (forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity Arg Expr
e1 (forall a. Render a => a -> Inlines
render Arg Expr
e1)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow,
          forall a. Render a => a -> Inlines
render Expr
e2
        ]
    Pi Telescope1
tel Expr
e ->
      [Inlines] -> Inlines
sep
        [ forall a. Render a => a -> Inlines
render (Telescope -> Tel
Tel forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope
smashTel (forall a. NonEmpty a -> [a]
toList Telescope1
tel)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow,
          forall a. Render a => a -> Inlines
render Expr
e
        ]
    Let Range
_ List1 Declaration
ds Maybe Expr
me ->
      [Inlines] -> Inlines
sep
        [ Inlines
"let" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 Declaration
ds)),
          forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty (\Expr
e -> Inlines
"in" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e) Maybe Expr
me
        ]
    Paren Range
_ Expr
e -> Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Expr
e
    IdiomBrackets Range
_ [Expr]
exprs ->
      case [Expr]
exprs of
        [] -> Inlines
emptyIdiomBrkt
        [Expr
e] -> Inlines
leftIdiomBrkt Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> Inlines
rightIdiomBrkt
        Expr
e : [Expr]
es -> Inlines
leftIdiomBrkt Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Inlines
"|" Inlines -> Inlines -> Inlines
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [Expr]
es) Inlines -> Inlines -> Inlines
<+> Inlines
rightIdiomBrkt
    DoBlock Range
_ List1 DoStmt
ss -> Inlines
"do" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 DoStmt
ss))
    As Range
_ Name
x Expr
e -> forall a. Render a => a -> Inlines
render Name
x forall a. Semigroup a => a -> a -> a
<> Inlines
"@" forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Expr
e
    Dot Range
_ Expr
e -> Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Expr
e
    DoubleDot Range
_ Expr
e -> Inlines
".." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Expr
e
    Absurd Range
_ -> Inlines
"()"
    Rec Range
_ RecordAssignments
xs -> [Inlines] -> Inlines
sep [Inlines
"record", [Inlines] -> Inlines
bracesAndSemicolons (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render RecordAssignments
xs)]
    RecUpdate Range
_ Expr
e [FieldAssignment]
xs ->
      [Inlines] -> Inlines
sep [Inlines
"record" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e, [Inlines] -> Inlines
bracesAndSemicolons (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [FieldAssignment]
xs)]
    ETel [] -> Inlines
"()"
    ETel Telescope
tel -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
tel
    Quote Range
_ -> Inlines
"quote"
    QuoteTerm Range
_ -> Inlines
"quoteTerm"
    Unquote Range
_ -> Inlines
"unquote"
    Tactic Range
_ Expr
t -> Inlines
"tactic" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
t
    -- Andreas, 2011-10-03 print irrelevant things as .(e)
    DontCare Expr
e -> Inlines
"." forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens (forall a. Render a => a -> Inlines
render Expr
e)
    Equal Range
_ Expr
a Expr
b -> forall a. Render a => a -> Inlines
render Expr
a Inlines -> Inlines -> Inlines
<+> Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
b
    Ellipsis Range
_ -> Inlines
"..."
    Generalized Expr
e -> forall a. Render a => a -> Inlines
render Expr
e
    where
      absurd :: Hiding -> a
absurd Hiding
NotHidden = a
"()"
      absurd Instance {} = a
"{{}}"
      absurd Hiding
Hidden = a
"{}"

-- instance RenderTCM Expr where
--   renderTCM = render

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

instance (Render a, Render b) => Render (Either a b) where
  render :: Either a b -> Inlines
render = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. Render a => a -> Inlines
render forall a. Render a => a -> Inlines
render

instance Render a => Render (FieldAssignment' a) where
  render :: FieldAssignment' a -> Inlines
render (FieldAssignment Name
x a
e) = [Inlines] -> Inlines
sep [forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> Inlines
"=", forall a. Render a => a -> Inlines
render a
e]

instance Render ModuleAssignment where
  render :: ModuleAssignment -> Inlines
render (ModuleAssignment QName
m [Expr]
es ImportDirective
i) = [Inlines] -> Inlines
fsep (forall a. Render a => a -> Inlines
render QName
m forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Expr]
es) Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render ImportDirective
i

instance Render LamClause where
  render :: LamClause -> Inlines
render (LamClause [Pattern]
lhs RHS
rhs Bool
_) =
    [Inlines] -> Inlines
sep
      [ forall a. Render a => a -> Inlines
render [Pattern]
lhs,
        forall {a}. Render a => RHS' a -> Inlines
render' RHS
rhs
      ]
    where
      render' :: RHS' a -> Inlines
render' (RHS a
e) = Inlines
arrow Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render a
e
      render' RHS' a
AbsurdRHS = forall a. Monoid a => a
mempty

instance Render BoundName where
  render :: BoundName -> Inlines
render BName {boundName :: BoundName -> Name
boundName = Name
x} = forall a. Render a => a -> Inlines
render Name
x

instance Render a => Render (Binder' a) where
  render :: Binder' a -> Inlines
render (Binder Maybe Pattern
mpat a
n) =
    let d :: Inlines
d = forall a. Render a => a -> Inlines
render a
n
     in case Maybe Pattern
mpat of
          Maybe Pattern
Nothing -> Inlines
d
          Just Pattern
pat -> Inlines
d Inlines -> Inlines -> Inlines
<+> Inlines
"@" Inlines -> Inlines -> Inlines
<+> Inlines -> Inlines
parens (forall a. Render a => a -> Inlines
render Pattern
pat)

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

-- | NamedBinding
instance Render NamedBinding where
  render :: NamedBinding -> Inlines
render (NamedBinding Bool
withH NamedArg Binder
x) =
    Inlines -> Inlines
prH forall a b. (a -> b) -> a -> b
$
      if
          | Just String
l <- NamedArg Binder -> Maybe String
isLabeled NamedArg Binder
x -> String -> Inlines
text String
l forall a. Semigroup a => a -> a -> a
<> Inlines
" = " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Binder
xb
          | Bool
otherwise -> forall a. Render a => a -> Inlines
render Binder
xb
    where
      xb :: Binder
xb = forall a. NamedArg a -> a
namedArg NamedArg Binder
x
      bn :: BoundName
bn = forall a. Binder' a -> a
binderName Binder
xb
      prH :: Inlines -> Inlines
prH
        | Bool
withH =
          forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance NamedArg Binder
x
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding NamedArg Binder
x Inlines -> Inlines
mparens'
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion NamedArg Binder
x
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity NamedArg Binder
x
            forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundName -> Inlines -> Inlines
renderTactic BoundName
bn
        | Bool
otherwise = forall a. a -> a
id
      -- Parentheses are needed when an attribute @... is present
      mparens' :: Inlines -> Inlines
mparens'
        | forall a. LensQuantity a => a -> Bool
noUserQuantity NamedArg Binder
x, Maybe Expr
Nothing <- BoundName -> Maybe Expr
bnameTactic BoundName
bn = forall a. a -> a
id
        | Bool
otherwise = Inlines -> Inlines
parens

renderTactic :: BoundName -> Inlines -> Inlines
renderTactic :: BoundName -> Inlines -> Inlines
renderTactic = Maybe Expr -> Inlines -> Inlines
renderTactic' forall b c a. (b -> c) -> (a -> b) -> a -> c
. BoundName -> Maybe Expr
bnameTactic

renderTactic' :: TacticAttribute -> Inlines -> Inlines
renderTactic' :: Maybe Expr -> Inlines -> Inlines
renderTactic' Maybe Expr
Nothing Inlines
d = Inlines
d
renderTactic' (Just Expr
t) Inlines
d = Inlines
"@" forall a. Semigroup a => a -> a -> a
<> (Inlines -> Inlines
parens (Inlines
"tactic " forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Expr
t) Inlines -> Inlines -> Inlines
<+> Inlines
d)

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

-- | LamBinding
instance Render LamBinding where
  render :: LamBinding -> Inlines
render (DomainFree NamedArg Binder
x) = forall a. Render a => a -> Inlines
render (Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
True NamedArg Binder
x)
  render (DomainFull TypedBinding
b) = forall a. Render a => a -> Inlines
render TypedBinding
b

-- | TypedBinding
instance Render TypedBinding where
  render :: TypedBinding -> Inlines
render (TLet Range
_ List1 Declaration
ds) = Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ Inlines
"let" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 Declaration
ds))
  render (TBind Range
_ List1 (NamedArg Binder)
xs (Underscore Range
_ Maybe String
Nothing)) =
    [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
True) (forall a. NonEmpty a -> [a]
toList List1 (NamedArg Binder)
xs))
  render (TBind Range
_ List1 (NamedArg Binder)
binders Expr
e) =
    [Inlines] -> Inlines
fsep
      [ forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance NamedArg Binder
y forall a b. (a -> b) -> a -> b
$
          forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding NamedArg Binder
y Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$
            forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion NamedArg Binder
y forall a b. (a -> b) -> a -> b
$
              forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity NamedArg Binder
y forall a b. (a -> b) -> a -> b
$
                BoundName -> Inlines -> Inlines
renderTactic (forall a. Binder' a -> a
binderName forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg Binder
y) forall a b. (a -> b) -> a -> b
$
                  [Inlines] -> Inlines
sep
                    [ [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a. Render a => a -> Inlines
render forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
False) [NamedArg Binder]
ys),
                      Inlines
":" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e
                    ]
        | ys :: [NamedArg Binder]
ys@(NamedArg Binder
y : [NamedArg Binder]
_) <- [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds (forall a. NonEmpty a -> [a]
toList List1 (NamedArg Binder)
binders)
      ]
    where
      groupBinds :: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [] = []
      groupBinds (NamedArg Binder
x : [NamedArg Binder]
xs)
        | Just {} <- NamedArg Binder -> Maybe String
isLabeled NamedArg Binder
x = [NamedArg Binder
x] forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
xs
        | Bool
otherwise = (NamedArg Binder
x forall a. a -> [a] -> [a]
: [NamedArg Binder]
ys) forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
zs
        where
          ([NamedArg Binder]
ys, [NamedArg Binder]
zs) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (forall {a}. LensArgInfo a => a -> NamedArg Binder -> Bool
same NamedArg Binder
x) [NamedArg Binder]
xs
          same :: a -> NamedArg Binder -> Bool
same a
a NamedArg Binder
b = forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
a forall a. Eq a => a -> a -> Bool
== forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Binder
b Bool -> Bool -> Bool
&& forall a. Maybe a -> Bool
isNothing (NamedArg Binder -> Maybe String
isLabeled NamedArg Binder
b)

instance Render Tel where
  render :: Tel -> Inlines
render (Tel Telescope
tel)
    | forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypedBinding -> Bool
isMeta Telescope
tel = Inlines
forallQ Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
tel)
    | Bool
otherwise = [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
tel)
    where
      isMeta :: TypedBinding -> Bool
isMeta (TBind Range
_ List1 (NamedArg Binder)
_ (Underscore Range
_ Maybe String
Nothing)) = Bool
True
      isMeta TypedBinding
_ = Bool
False

smashTel :: Telescope -> Telescope
smashTel :: Telescope -> Telescope
smashTel
  ( TBind Range
r List1 (NamedArg Binder)
xs Expr
e
      : TBind Range
_ List1 (NamedArg Binder)
ys Expr
e'
      : Telescope
tel
    )
    | forall a. Show a => a -> String
show Expr
e forall a. Eq a => a -> a -> Bool
== forall a. Show a => a -> String
show Expr
e' = Telescope -> Telescope
smashTel (forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r (forall a. [a] -> NonEmpty a
fromList (forall a. NonEmpty a -> [a]
toList List1 (NamedArg Binder)
xs forall a. [a] -> [a] -> [a]
++ forall a. NonEmpty a -> [a]
toList List1 (NamedArg Binder)
ys)) Expr
e forall a. a -> [a] -> [a]
: Telescope
tel)
smashTel (TypedBinding
b : Telescope
tel) = TypedBinding
b forall a. a -> [a] -> [a]
: Telescope -> Telescope
smashTel Telescope
tel
smashTel [] = []

instance Render RHS where
  render :: RHS -> Inlines
render (RHS Expr
e) = Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e
  render RHS
AbsurdRHS = forall a. Monoid a => a
mempty

instance Render WhereClause where
  render :: WhereClause -> Inlines
render WhereClause
NoWhere = forall a. Monoid a => a
mempty
  render (AnyWhere Range
_range [Module Range
_ QName
x [] [Declaration]
ds])
    | forall a. IsNoName a => a -> Bool
isNoName (QName -> Name
unqualify QName
x) =
      [Inlines] -> Inlines
vcat [Inlines
"where", [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
ds]
  render (AnyWhere Range
_range [Declaration]
ds) = [Inlines] -> Inlines
vcat [Inlines
"where", [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
ds]
  render (SomeWhere Range
_range Name
m Access
a [Declaration]
ds) =
    [Inlines] -> Inlines
vcat
      [ [Inlines] -> Inlines
hsep forall a b. (a -> b) -> a -> b
$
          forall a. Bool -> (a -> a) -> a -> a
applyWhen
            (Access
a forall a. Eq a => a -> a -> Bool
== Origin -> Access
PrivateAccess Origin
UserWritten)
            (Inlines
"private" forall a. a -> [a] -> [a]
:)
            [Inlines
"module", forall a. Render a => a -> Inlines
render Name
m, Inlines
"where"],
        [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
ds
      ]

instance Render LHS where
  render :: LHS -> Inlines
render (LHS Pattern
p [RewriteEqn]
eqs [WithExpr]
es) =
    [Inlines] -> Inlines
sep
      [ forall a. Render a => a -> Inlines
render Pattern
p,
        if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewriteEqn]
eqs then forall a. Monoid a => a
mempty else [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [RewriteEqn]
eqs,
        Inlines -> [Inlines] -> Inlines
prefixedThings Inlines
"with" (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap WithExpr -> Inlines
renderWithd [WithExpr]
es)
      ]
    where
      renderWithd :: WithExpr -> Inlines
      renderWithd :: WithExpr -> Inlines
renderWithd (Named Maybe Name
nm Arg Expr
wh) =
        let e :: Inlines
e = forall a. Render a => a -> Inlines
render Arg Expr
wh in
        case Maybe Name
nm of
          Maybe Name
Nothing -> Inlines
e
          Just Name
n  -> forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
<+> Inlines
":" Inlines -> Inlines -> Inlines
<+> Inlines
e

instance Render LHSCore where
  render :: LHSCore -> Inlines
render (LHSHead QName
f [NamedArg Pattern]
ps) = [Inlines] -> Inlines
sep forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render QName
f forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps
  render (LHSProj QName
d [NamedArg Pattern]
ps NamedArg LHSCore
lhscore [NamedArg Pattern]
ps') =
    [Inlines] -> Inlines
sep forall a b. (a -> b) -> a -> b
$
      forall a. Render a => a -> Inlines
render QName
d forall a. a -> [a] -> [a]
:
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps
        forall a. [a] -> [a] -> [a]
++ Inlines -> Inlines
parens (forall a. Render a => a -> Inlines
render NamedArg LHSCore
lhscore) forall a. a -> [a] -> [a]
:
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps'
  render (LHSWith LHSCore
h [Pattern]
wps [NamedArg Pattern]
ps) =
    if forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
ps
      then Inlines
doc
      else [Inlines] -> Inlines
sep forall a b. (a -> b) -> a -> b
$ Inlines -> Inlines
parens Inlines
doc forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps
    where
      doc :: Inlines
doc = [Inlines] -> Inlines
sep forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render LHSCore
h forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Inlines
"|" Inlines -> Inlines -> Inlines
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) [Pattern]
wps
  render (LHSEllipsis Range
r LHSCore
p) = Inlines
"..."

instance Render ModuleApplication where
  render :: ModuleApplication -> Inlines
render (SectionApp Range
_ Telescope
bs Expr
e) = [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
bs) Inlines -> Inlines -> Inlines
<+> Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e
  render (RecordModuleInstance Range
_ QName
rec) = Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render QName
rec Inlines -> Inlines -> Inlines
<+> Inlines
"{{...}}"

instance Render DoStmt where
  render :: DoStmt -> Inlines
render (DoBind Range
_ Pattern
p Expr
e [LamClause]
cs) =
    [Inlines] -> Inlines
fsep [forall a. Render a => a -> Inlines
render Pattern
p Inlines -> Inlines -> Inlines
<+> Inlines
"←", forall a. Render a => a -> Inlines
render Expr
e, forall {a}. Render a => [a] -> Inlines
prCs [LamClause]
cs]
    where
      prCs :: [a] -> Inlines
prCs [] = forall a. Monoid a => a
mempty
      prCs [a]
cs' = [Inlines] -> Inlines
fsep [Inlines
"where", [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
cs')]
  render (DoThen Expr
e) = forall a. Render a => a -> Inlines
render Expr
e
  render (DoLet Range
_ List1 Declaration
ds) = Inlines
"let" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
toList List1 Declaration
ds)

instance Render Declaration where
  render :: Declaration -> Inlines
render Declaration
d =
    case Declaration
d of
      TypeSig ArgInfo
i Maybe Expr
tac Name
x Expr
e ->
        [Inlines] -> Inlines
sep
          [ Maybe Expr -> Inlines -> Inlines
renderTactic' Maybe Expr
tac forall a b. (a -> b) -> a -> b
$ forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity ArgInfo
i forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> Inlines
":",
            forall a. Render a => a -> Inlines
render Expr
e
          ]
      FieldSig IsInstance
inst Maybe Expr
tac Name
x (Arg ArgInfo
i Expr
e) ->
        IsInstance -> Inlines -> Inlines
mkInst IsInstance
inst forall a b. (a -> b) -> a -> b
$
          forall {a}. LensHiding a => a -> Inlines -> Inlines
mkOverlap ArgInfo
i forall a b. (a -> b) -> a -> b
$
            forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance ArgInfo
i forall a b. (a -> b) -> a -> b
$
              forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
i forall a. a -> a
id forall a b. (a -> b) -> a -> b
$
                forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion ArgInfo
i forall a b. (a -> b) -> a -> b
$
                  forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity ArgInfo
i forall a b. (a -> b) -> a -> b
$
                    forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
TypeSig (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Relevant ArgInfo
i) Maybe Expr
tac Name
x Expr
e
        where
          mkInst :: IsInstance -> Inlines -> Inlines
mkInst (InstanceDef Range
_) Inlines
f = [Inlines] -> Inlines
sep [Inlines
"instance", Inlines
f]
          mkInst IsInstance
NotInstanceDef Inlines
f = Inlines
f

          mkOverlap :: a -> Inlines -> Inlines
mkOverlap a
j Inlines
f
            | forall a. LensHiding a => a -> Bool
isOverlappable a
j = Inlines
"overlap" Inlines -> Inlines -> Inlines
<+> Inlines
f
            | Bool
otherwise = Inlines
f
      Field Range
_ [Declaration]
fs ->
        [Inlines] -> Inlines
sep
          [ Inlines
"field",
            [Inlines] -> Inlines
vcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
fs)
          ]
      FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
_ ->
        [Inlines] -> Inlines
sep
          [ forall a. Render a => a -> Inlines
render LHS
lhs,
            forall a. Render a => a -> Inlines
render RHS
rhs,
            forall a. Render a => a -> Inlines
render WhereClause
wh
          ]
      DataSig Range
_ Name
x [LamBinding]
tel Expr
e ->
        [Inlines] -> Inlines
fsep
          [ [Inlines] -> Inlines
hsep
              [ Inlines
"data",
                forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                forall a. Render a => a -> Inlines
render Expr
e
              ]
          ]
      Data Range
_ Name
x [LamBinding]
tel Expr
e [Declaration]
cs ->
        [Inlines] -> Inlines
fsep
          [ [Inlines] -> Inlines
hsep
              [ Inlines
"data",
                forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                forall a. Render a => a -> Inlines
render Expr
e,
                Inlines
"where"
              ],
            [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
cs
          ]
      DataDef Range
_ Name
x [LamBinding]
tel [Declaration]
cs ->
        [Inlines] -> Inlines
sep
          [ [Inlines] -> Inlines
hsep
              [ Inlines
"data",
                forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            Inlines
"where",
            [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
cs
          ]
      RecordSig Range
_ Name
x [LamBinding]
tel Expr
e ->
        [Inlines] -> Inlines
sep
          [ [Inlines] -> Inlines
hsep
              [ Inlines
"record",
                forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                forall a. Render a => a -> Inlines
render Expr
e
              ]
          ]
      Record Range
_ Name
x RecordDirectives
dir [LamBinding]
tel Expr
e [Declaration]
cs ->
        Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Inlines
pRecord Name
x RecordDirectives
dir [LamBinding]
tel (forall a. a -> Maybe a
Just Expr
e) [Declaration]
cs
      RecordDef Range
_ Name
x RecordDirectives
dir [LamBinding]
tel [Declaration]
cs ->
        Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Inlines
pRecord Name
x RecordDirectives
dir [LamBinding]
tel forall a. Maybe a
Nothing [Declaration]
cs
      RecordDirective RecordDirective
r -> RecordDirective -> Inlines
pRecordDirective RecordDirective
r
      Infix Fixity
f List1 Name
xs -> forall a. Render a => a -> Inlines
render Fixity
f Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall a. NonEmpty a -> [a]
toList List1 Name
xs))
      Syntax Name
n Notation
_ -> Inlines
"syntax" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
<+> Inlines
"..."
      PatternSyn Range
_ Name
n [Arg Name]
as Pattern
p ->
        Inlines
"pattern" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Arg Name]
as)
          Inlines -> Inlines -> Inlines
<+> Inlines
"="
          Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Pattern
p
      Mutual Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"mutual" [Declaration]
ds
      InterleavedMutual Range
_ [Declaration]
ds  -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"interleaved mutual" [Declaration]
ds
      LoneConstructor Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"constructor" [Declaration]
ds
      Abstract Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"abstract" [Declaration]
ds
      Private Range
_ Origin
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"private" [Declaration]
ds
      InstanceB Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"instance" [Declaration]
ds
      Macro Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"macro" [Declaration]
ds
      Postulate Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"postulate" [Declaration]
ds
      Primitive Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"primitive" [Declaration]
ds
      Generalize Range
_ [Declaration]
ds -> forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"variable" [Declaration]
ds
      Module Range
_ QName
x Telescope
tel [Declaration]
ds ->
        [Inlines] -> Inlines
fsep
          [ [Inlines] -> Inlines
hsep
              [ Inlines
"module",
                forall a. Render a => a -> Inlines
render QName
x,
                [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
tel),
                Inlines
"where"
              ],
            [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
ds
          ]
      ModuleMacro Range
_ Name
x (SectionApp Range
_ [] Expr
e) OpenShortHand
DoOpen ImportDirective
i
        | forall a. IsNoName a => a -> Bool
isNoName Name
x ->
          [Inlines] -> Inlines
fsep
            [ forall a. Render a => a -> Inlines
render OpenShortHand
DoOpen,
              forall a. Render a => a -> Inlines
render Expr
e,
              forall a. Render a => a -> Inlines
render ImportDirective
i
            ]
      ModuleMacro Range
_ Name
x (SectionApp Range
_ Telescope
tel Expr
e) OpenShortHand
open ImportDirective
i ->
        [Inlines] -> Inlines
fsep
          [ forall a. Render a => a -> Inlines
render OpenShortHand
open Inlines -> Inlines -> Inlines
<+> Inlines
"module" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render Telescope
tel),
            Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render ImportDirective
i
          ]
      ModuleMacro Range
_ Name
x (RecordModuleInstance Range
_ QName
rec) OpenShortHand
open ImportDirective
_ ->
        [Inlines] -> Inlines
fsep
          [ forall a. Render a => a -> Inlines
render OpenShortHand
open Inlines -> Inlines -> Inlines
<+> Inlines
"module" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Name
x,
            Inlines
"=" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render QName
rec Inlines -> Inlines -> Inlines
<+> Inlines
"{{...}}"
          ]
      Open Range
_ QName
x ImportDirective
i -> [Inlines] -> Inlines
hsep [Inlines
"open", forall a. Render a => a -> Inlines
render QName
x, forall a. Render a => a -> Inlines
render ImportDirective
i]
      Import Range
_ QName
x Maybe AsName
rn OpenShortHand
open ImportDirective
i ->
        [Inlines] -> Inlines
hsep [forall a. Render a => a -> Inlines
render OpenShortHand
open, Inlines
"import", forall a. Render a => a -> Inlines
render QName
x, forall {a}. Render a => Maybe (AsName' a) -> Inlines
as Maybe AsName
rn, forall a. Render a => a -> Inlines
render ImportDirective
i]
        where
          as :: Maybe (AsName' a) -> Inlines
as Maybe (AsName' a)
Nothing = forall a. Monoid a => a
mempty
          as (Just AsName' a
y) = Inlines
"as" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render (forall a. AsName' a -> a
asName AsName' a
y)
      UnquoteDecl Range
_ [Name]
xs Expr
t ->
        [Inlines] -> Inlines
fsep [Inlines
"unquoteDecl" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Name]
xs) Inlines -> Inlines -> Inlines
<+> Inlines
"=", forall a. Render a => a -> Inlines
render Expr
t]
      UnquoteDef Range
_ [Name]
xs Expr
t ->
        [Inlines] -> Inlines
fsep [Inlines
"unquoteDef" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Name]
xs) Inlines -> Inlines -> Inlines
<+> Inlines
"=", forall a. Render a => a -> Inlines
render Expr
t]
      Pragma Pragma
pr -> [Inlines] -> Inlines
sep [Inlines
"{-#" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Pragma
pr, Inlines
"#-}"]
    where
      namedBlock :: String -> [a] -> Inlines
namedBlock String
s [a]
ds =
        [Inlines] -> Inlines
fsep
          [ String -> Inlines
text String
s,
            [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
ds
          ]

pHasEta0 :: HasEta0 -> Inlines
pHasEta0 :: HasEta0 -> Inlines
pHasEta0 = \case
  HasEta0
YesEta   -> Inlines
"eta-equality"
  NoEta () -> Inlines
"no-eta-equality"

pRecordDirective :: 
  RecordDirective ->
  Inlines
pRecordDirective :: RecordDirective -> Inlines
pRecordDirective = \case
  Induction Ranged Induction
ind -> forall a. Render a => a -> Inlines
render (forall a. Ranged a -> a
rangedThing Ranged Induction
ind)
  Constructor Name
n IsInstance
inst -> [Inlines] -> Inlines
hsep [ Inlines
pInst, Inlines
"constructor", forall a. Render a => a -> Inlines
render Name
n ] where
    pInst :: Inlines
pInst = case IsInstance
inst of
      InstanceDef{} -> Inlines
"instance"
      NotInstanceDef{} -> forall a. Monoid a => a
mempty
  Eta Ranged HasEta0
eta -> HasEta0 -> Inlines
pHasEta0 (forall a. Ranged a -> a
rangedThing Ranged HasEta0
eta)
  PatternOrCopattern{} -> Inlines
"pattern"


pRecord ::
  Name ->
  RecordDirectives ->
  [LamBinding] ->
  Maybe Expr ->
  [Declaration] ->
  Inlines
pRecord :: Name
-> RecordDirectives
-> [LamBinding]
-> Maybe Expr
-> [Declaration]
-> Inlines
pRecord Name
x (RecordDirectives Maybe (Ranged Induction)
ind Maybe HasEta0
eta Maybe Range
pat Maybe (Name, IsInstance)
con) [LamBinding]
tel Maybe Expr
me [Declaration]
cs =
  [Inlines] -> Inlines
sep
    [ [Inlines] -> Inlines
hsep
        [ Inlines
"record",
          forall a. Render a => a -> Inlines
render Name
x,
          [Inlines] -> Inlines
fcat (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [LamBinding]
tel)
        ],
      forall {a}. Render a => Maybe a -> Inlines
pType Maybe Expr
me,
      [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$
        [Inlines]
pInd
          forall a. [a] -> [a] -> [a]
++ [Inlines]
pEta
          forall a. [a] -> [a] -> [a]
++ [Inlines]
pCon
          forall a. [a] -> [a] -> [a]
++ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Declaration]
cs
    ]
  where
    pType :: Maybe a -> Inlines
pType (Just a
e) =
      [Inlines] -> Inlines
hsep
        [ Inlines
":",
          forall a. Render a => a -> Inlines
render a
e,
          Inlines
"where"
        ]
    pType Maybe a
Nothing =
      Inlines
"where"
    pInd :: [Inlines]
pInd = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ String -> Inlines
text forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ranged a -> a
rangedThing forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
    pEta :: [Inlines]
pEta =
      forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$
        Maybe HasEta0
eta forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \case
          HasEta0
YesEta -> Inlines
"eta-equality"
          NoEta ()
_ -> Inlines
"no-eta-equality"
    pCon :: [Inlines]
pCon = forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$ ((Inlines
"constructor" Inlines -> Inlines -> Inlines
<+>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Render a => a -> Inlines
render) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Name, IsInstance)
con

instance Render OpenShortHand where
  render :: OpenShortHand -> Inlines
render OpenShortHand
DoOpen = Inlines
"open"
  render OpenShortHand
DontOpen = forall a. Monoid a => a
mempty

instance Render Pragma where
  render :: Pragma -> Inlines
render (OptionsPragma Range
_ ClassNames
opts) = [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Inlines
text forall a b. (a -> b) -> a -> b
$ String
"OPTIONS" forall a. a -> [a] -> [a]
: ClassNames
opts
  render (BuiltinPragma Range
_ RString
b QName
x) = [Inlines] -> Inlines
hsep [Inlines
"BUILTIN", String -> Inlines
text (forall a. Ranged a -> a
rangedThing RString
b), forall a. Render a => a -> Inlines
render QName
x]
  render (RewritePragma Range
_ Range
_ [QName]
xs) =
    [Inlines] -> Inlines
hsep [Inlines
"REWRITE", [Inlines] -> Inlines
hsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [QName]
xs]
  render (CompilePragma Range
_ RString
b QName
x String
e) =
    [Inlines] -> Inlines
hsep [Inlines
"COMPILE", String -> Inlines
text (forall a. Ranged a -> a
rangedThing RString
b), forall a. Render a => a -> Inlines
render QName
x, String -> Inlines
text String
e]
  render (ForeignPragma Range
_ RString
b String
s) =
    [Inlines] -> Inlines
vcat forall a b. (a -> b) -> a -> b
$ String -> Inlines
text (String
"FOREIGN " forall a. [a] -> [a] -> [a]
++ forall a. Ranged a -> a
rangedThing RString
b) forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Inlines
text (String -> ClassNames
lines String
s)
  render (StaticPragma Range
_ QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"STATIC", forall a. Render a => a -> Inlines
render QName
i]
  render (InjectivePragma Range
_ QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"INJECTIVE", forall a. Render a => a -> Inlines
render QName
i]
  render (InlinePragma Range
_ Bool
True QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"INLINE", forall a. Render a => a -> Inlines
render QName
i]
  render (InlinePragma Range
_ Bool
False QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"NOINLINE", forall a. Render a => a -> Inlines
render QName
i]
  render (ImpossiblePragma Range
_ ClassNames
strs) =
    [Inlines] -> Inlines
hsep forall a b. (a -> b) -> a -> b
$ Inlines
"IMPOSSIBLE" forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Inlines
text ClassNames
strs
  render (EtaPragma Range
_ QName
x) =
    [Inlines] -> Inlines
hsep [Inlines
"ETA", forall a. Render a => a -> Inlines
render QName
x]
  render (TerminationCheckPragma Range
_ TerminationCheck Name
tc) =
    case TerminationCheck Name
tc of
      TerminationCheck Name
TerminationCheck -> forall a. HasCallStack => a
__IMPOSSIBLE__
      TerminationCheck Name
NoTerminationCheck -> Inlines
"NO_TERMINATION_CHECK"
      TerminationCheck Name
NonTerminating -> Inlines
"NON_TERMINATING"
      TerminationCheck Name
Terminating -> Inlines
"TERMINATING"
      TerminationMeasure Range
_ Name
x -> [Inlines] -> Inlines
hsep [Inlines
"MEASURE", forall a. Render a => a -> Inlines
render Name
x]
  render (NoCoverageCheckPragma Range
_) = Inlines
"NON_COVERING"
  render (WarningOnUsage Range
_ QName
nm Text
str) = [Inlines] -> Inlines
hsep [Inlines
"WARNING_ON_USAGE", forall a. Render a => a -> Inlines
render QName
nm, String -> Inlines
text forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
str]
  render (WarningOnImport Range
_ Text
str) = [Inlines] -> Inlines
hsep [Inlines
"WARNING_ON_IMPORT", String -> Inlines
text forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack Text
str]
  render (CatchallPragma Range
_) = Inlines
"CATCHALL"
  render (DisplayPragma Range
_ Pattern
lhs Expr
rhs) = Inlines
"DISPLAY" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep [forall a. Render a => a -> Inlines
render Pattern
lhs Inlines -> Inlines -> Inlines
<+> Inlines
"=", forall a. Render a => a -> Inlines
render Expr
rhs]
  render (NoPositivityCheckPragma Range
_) = Inlines
"NO_POSITIVITY_CHECK"
  render (PolarityPragma Range
_ Name
q [Occurrence]
occs) =
    [Inlines] -> Inlines
hsep (Inlines
"POLARITY" forall a. a -> [a] -> [a]
: forall a. Render a => a -> Inlines
render Name
q forall a. a -> [a] -> [a]
: forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [Occurrence]
occs)
  render (NoUniverseCheckPragma Range
_) = Inlines
"NO_UNIVERSE_CHECK"

instance Render Fixity where
  render :: Fixity -> Inlines
render (Fixity Range
_ FixityLevel
Unrelated Associativity
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
  render (Fixity Range
_ (Related PrecedenceLevel
d) Associativity
ass) = Inlines
s Inlines -> Inlines -> Inlines
<+> String -> Inlines
text (PrecedenceLevel -> String
toStringWithoutDotZero PrecedenceLevel
d)
    where
      s :: Inlines
s = case Associativity
ass of
        Associativity
LeftAssoc -> Inlines
"infixl"
        Associativity
RightAssoc -> Inlines
"infixr"
        Associativity
NonAssoc -> Inlines
"infix"

instance Render GenPart where
  render :: GenPart -> Inlines
render (IdPart RString
x) = String -> Inlines
text forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing RString
x
  render BindHole {} = Inlines
"_"
  render NormalHole {} = Inlines
"_"
  render WildHole {} = Inlines
"_"

instance Render Fixity' where
  render :: Fixity' -> Inlines
render (Fixity' Fixity
fix Notation
nota Range
_)
    | Notation
nota forall a. Eq a => a -> a -> Bool
== Notation
noNotation = forall a. Render a => a -> Inlines
render Fixity
fix
    | Bool
otherwise = Inlines
"syntax" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Notation
nota

-- | Arg
instance Render a => Render (Arg a) where
  renderPrec :: Int -> Arg a -> Inlines
renderPrec Int
p (Arg ArgInfo
ai a
e) = forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
ai Inlines -> Inlines
localParens forall a b. (a -> b) -> a -> b
$ forall a. Render a => Int -> a -> Inlines
renderPrec Int
p' a
e
    where
      p' :: Int
p'
        | forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Int
p
        | Bool
otherwise = Int
0
      localParens :: Inlines -> Inlines
localParens
        | forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai forall a. Eq a => a -> a -> Bool
== Origin
Substitution = Inlines -> Inlines
parens
        | Bool
otherwise = forall a. a -> a
id

-- | Named NamedName (Named_)
instance Render e => Render (Named NamedName e) where
  renderPrec :: Int -> Named NamedName e -> Inlines
renderPrec Int
p (Named Maybe NamedName
nm e
e)
    | Just String
s <- forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf Maybe NamedName
nm = Bool -> Inlines -> Inlines
mparens (Int
p forall a. Ord a => a -> a -> Bool
> Int
0) forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
sep [String -> Inlines
text String
s forall a. Semigroup a => a -> a -> a
<> Inlines
" =", forall a. Render a => a -> Inlines
render e
e]
    | Bool
otherwise = forall a. Render a => Int -> a -> Inlines
renderPrec Int
p e
e

instance Render Pattern where
  render :: Pattern -> Inlines
render = \case
    IdentP QName
x -> forall a. Render a => a -> Inlines
render QName
x
    AppP Pattern
p1 NamedArg Pattern
p2 -> [Inlines] -> Inlines
fsep [forall a. Render a => a -> Inlines
render Pattern
p1, forall a. Render a => a -> Inlines
render NamedArg Pattern
p2]
    RawAppP Range
_ List2 Pattern
ps -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render (forall l. IsList l => l -> [Item l]
List2.toList List2 Pattern
ps)
    OpAppP Range
_ QName
q Set Name
_ [NamedArg Pattern]
ps -> [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ forall a.
Render a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
renderOpApp QName
q (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall e. Maybe PositionInName -> e -> MaybePlaceholder e
NoPlaceholder forall a. Maybe a
Strict.Nothing))) [NamedArg Pattern]
ps)
    HiddenP Range
_ Named NamedName Pattern
p -> Inlines -> Inlines
braces' forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Named NamedName Pattern
p
    InstanceP Range
_ Named NamedName Pattern
p -> Inlines -> Inlines
dbraces forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Named NamedName Pattern
p
    ParenP Range
_ Pattern
p -> Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render Pattern
p
    WildP Range
_ -> Inlines
"_"
    AsP Range
_ Name
x Pattern
p -> forall a. Render a => a -> Inlines
render Name
x forall a. Semigroup a => a -> a -> a
<> Inlines
"@" forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Pattern
p
    DotP Range
_ Expr
p -> Inlines
"." forall a. Semigroup a => a -> a -> a
<> forall a. Render a => a -> Inlines
render Expr
p
    AbsurdP Range
_ -> Inlines
"()"
    LitP Range
_ Literal
l -> forall a. Render a => a -> Inlines
render Literal
l
    QuoteP Range
_ -> Inlines
"quote"
    RecP Range
_ [FieldAssignment' Pattern]
fs -> [Inlines] -> Inlines
sep [Inlines
"record", [Inlines] -> Inlines
bracesAndSemicolons (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [FieldAssignment' Pattern]
fs)]
    EqualP Range
_ [(Expr, Expr)]
es -> [Inlines] -> Inlines
sep forall a b. (a -> b) -> a -> b
$ [Inlines -> Inlines
parens ([Inlines] -> Inlines
sep [forall a. Render a => a -> Inlines
render Expr
e1, Inlines
"=", forall a. Render a => a -> Inlines
render Expr
e2]) | (Expr
e1, Expr
e2) <- [(Expr, Expr)]
es]
    EllipsisP Range
_ Maybe Pattern
mp -> Inlines
"..."
    WithP Range
_ Pattern
p -> Inlines
"|" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render Pattern
p

bracesAndSemicolons :: [Inlines] -> Inlines
bracesAndSemicolons :: [Inlines] -> Inlines
bracesAndSemicolons [] = Inlines
"{}"
bracesAndSemicolons (Inlines
d : [Inlines]
ds) = [Inlines] -> Inlines
sep ([Inlines
"{" Inlines -> Inlines -> Inlines
<+> Inlines
d] forall a. [a] -> [a] -> [a]
++ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines
";" Inlines -> Inlines -> Inlines
<+>) [Inlines]
ds forall a. [a] -> [a] -> [a]
++ [Inlines
"}"])

renderOpApp ::
  forall a.
  Render a =>
  QName ->
  [NamedArg (MaybePlaceholder a)] ->
  [Inlines]
renderOpApp :: forall a.
Render a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
renderOpApp QName
q [NamedArg (MaybePlaceholder a)]
args = [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge [] forall a b. (a -> b) -> a -> b
$ forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [Name]
moduleNames [NamePart]
concreteNames [NamedArg (MaybePlaceholder a)]
args
  where
    -- ms: the module part of the name.
    moduleNames :: [Name]
moduleNames = forall a. NonEmpty a -> [a]
List1.init (QName -> List1 Name
qnameParts QName
q)
    -- xs: the concrete name (alternation of @Id@ and @Hole@)
    concreteNames :: [NamePart]
concreteNames = case QName -> Name
unqualify QName
q of
      Name Range
_ NameInScope
_ NameParts
xs -> forall a. NonEmpty a -> [a]
List1.toList NameParts
xs
      NoName {} -> forall a. HasCallStack => a
__IMPOSSIBLE__

    prOp :: Render a => [Name] -> [NamePart] -> [NamedArg (MaybePlaceholder a)] -> [(Inlines, Maybe PositionInName)]
    prOp :: forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [Name]
ms (NamePart
Hole : [NamePart]
xs) (NamedArg (MaybePlaceholder a)
e : [NamedArg (MaybePlaceholder a)]
es) =
      case forall a. NamedArg a -> a
namedArg NamedArg (MaybePlaceholder a)
e of
        Placeholder PositionInName
p -> (forall {a}. Render a => [a] -> Inlines -> Inlines
qual [Name]
ms forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, forall a. a -> Maybe a
Just PositionInName
p) forall a. a -> [a] -> [a]
: forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [] [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
        NoPlaceholder {} -> (forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, forall a. Maybe a
Nothing) forall a. a -> [a] -> [a]
: forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [Name]
ms [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
    -- Module qualifier needs to go on section holes (#3072)
    prOp [Name]
_ (NamePart
Hole : [NamePart]
_) [] = forall a. HasCallStack => a
__IMPOSSIBLE__
    prOp [Name]
ms (Id String
x : [NamePart]
xs) [NamedArg (MaybePlaceholder a)]
es =
      ( forall {a}. Render a => [a] -> Inlines -> Inlines
qual [Name]
ms forall a b. (a -> b) -> a -> b
$ forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ String -> Name
simpleName String
x,
        forall a. Maybe a
Nothing
      ) forall a. a -> [a] -> [a]
:
      forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [] [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
    -- Qualify the name part with the module.
    -- We then clear @ms@ such that the following name parts will not be qualified.

    prOp [Name]
_ [] [NamedArg (MaybePlaceholder a)]
es = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedArg (MaybePlaceholder a)
e -> (forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, forall a. Maybe a
Nothing)) [NamedArg (MaybePlaceholder a)]
es

    qual :: [a] -> Inlines -> Inlines
qual [a]
ms' Inlines
doc = [Inlines] -> Inlines
hcat forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"." forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
ms' forall a. [a] -> [a] -> [a]
++ [Inlines
doc]

    -- Section underscores should be printed without surrounding
    -- whitespace. This function takes care of that.
    merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
    merge :: [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge [Inlines]
before [] = forall a. [a] -> [a]
reverse [Inlines]
before
    merge [Inlines]
before ((Inlines
d, Maybe PositionInName
Nothing) : [(Inlines, Maybe PositionInName)]
after) = [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge (Inlines
d forall a. a -> [a] -> [a]
: [Inlines]
before) [(Inlines, Maybe PositionInName)]
after
    merge [Inlines]
before ((Inlines
d, Just PositionInName
Beginning) : [(Inlines, Maybe PositionInName)]
after) = [Inlines]
-> Inlines -> [(Inlines, Maybe PositionInName)] -> [Inlines]
mergeRight [Inlines]
before Inlines
d [(Inlines, Maybe PositionInName)]
after
    merge [Inlines]
before ((Inlines
d, Just PositionInName
End) : [(Inlines, Maybe PositionInName)]
after) = case forall {a}. Semigroup a => a -> [a] -> (a, [a])
mergeLeft Inlines
d [Inlines]
before of
      (Inlines
d', [Inlines]
bs) -> [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge (Inlines
d' forall a. a -> [a] -> [a]
: [Inlines]
bs) [(Inlines, Maybe PositionInName)]
after
    merge [Inlines]
before ((Inlines
d, Just PositionInName
Middle) : [(Inlines, Maybe PositionInName)]
after) = case forall {a}. Semigroup a => a -> [a] -> (a, [a])
mergeLeft Inlines
d [Inlines]
before of
      (Inlines
d', [Inlines]
bs) -> [Inlines]
-> Inlines -> [(Inlines, Maybe PositionInName)] -> [Inlines]
mergeRight [Inlines]
bs Inlines
d' [(Inlines, Maybe PositionInName)]
after

    mergeRight :: [Inlines]
-> Inlines -> [(Inlines, Maybe PositionInName)] -> [Inlines]
mergeRight [Inlines]
before Inlines
d [(Inlines, Maybe PositionInName)]
after =
      forall a. [a] -> [a]
reverse [Inlines]
before
        forall a. [a] -> [a] -> [a]
++ case [Inlines] -> [(Inlines, Maybe PositionInName)] -> [Inlines]
merge [] [(Inlines, Maybe PositionInName)]
after of
          [] -> [Inlines
d]
          Inlines
a : [Inlines]
as -> (Inlines
d forall a. Semigroup a => a -> a -> a
<> Inlines
a) forall a. a -> [a] -> [a]
: [Inlines]
as

    mergeLeft :: a -> [a] -> (a, [a])
mergeLeft a
d [a]
before = case [a]
before of
      [] -> (a
d, [])
      a
b : [a]
bs -> (a
b forall a. Semigroup a => a -> a -> a
<> a
d, [a]
bs)

instance (Render a, Render b) => Render (ImportDirective' a b) where
  render :: ImportDirective' a b -> Inlines
render ImportDirective' a b
i =
    [Inlines] -> Inlines
sep
      [ forall {a} {a}. (IsString a, Monoid a) => Maybe a -> a
public (forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective' a b
i),
        forall a. Render a => a -> Inlines
render forall a b. (a -> b) -> a -> b
$ forall n m. ImportDirective' n m -> Using' n m
using ImportDirective' a b
i,
        forall {a}. Render a => [a] -> Inlines
renderHiding' forall a b. (a -> b) -> a -> b
$ forall n m. ImportDirective' n m -> HidingDirective' n m
hiding ImportDirective' a b
i,
        forall {a}. Render a => [a] -> Inlines
rename forall a b. (a -> b) -> a -> b
$ forall n m. ImportDirective' n m -> RenamingDirective' n m
impRenaming ImportDirective' a b
i
      ]
    where
      public :: Maybe a -> a
public Just {} = a
"public"
      public Maybe a
Nothing = forall a. Monoid a => a
mempty

      renderHiding' :: [a] -> Inlines
renderHiding' [] = forall a. Monoid a => a
mempty
      renderHiding' [a]
xs = Inlines
"hiding" Inlines -> Inlines -> Inlines
<+> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
";" forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
xs)

      rename :: [a] -> Inlines
rename [] = forall a. Monoid a => a
mempty
      rename [a]
xs =
        [Inlines] -> Inlines
hsep
          [ Inlines
"renaming",
            Inlines -> Inlines
parens forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
";" forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [a]
xs
          ]

instance (Render a, Render b) => Render (Using' a b) where
  render :: Using' a b -> Inlines
render Using' a b
UseEverything = forall a. Monoid a => a
mempty
  render (Using [ImportedName' a b]
xs) =
    Inlines
"using" Inlines -> Inlines -> Inlines
<+> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
";" forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Render a => a -> Inlines
render [ImportedName' a b]
xs)

instance (Render a, Render b) => Render (Renaming' a b) where
  render :: Renaming' a b -> Inlines
render (Renaming ImportedName' a b
from ImportedName' a b
to Maybe Fixity
mfx Range
_r) =
    [Inlines] -> Inlines
hsep
      [ forall a. Render a => a -> Inlines
render ImportedName' a b
from,
        Inlines
"to",
        forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Monoid a => a
mempty forall a. Render a => a -> Inlines
render Maybe Fixity
mfx,
        case ImportedName' a b
to of
          ImportedName a
a -> forall a. Render a => a -> Inlines
render a
a
          ImportedModule b
b -> forall a. Render a => a -> Inlines
render b
b -- don't print "module" here
      ]

instance (Render a, Render b) => Render (ImportedName' a b) where
  render :: ImportedName' a b -> Inlines
render (ImportedName a
a) = forall a. Render a => a -> Inlines
render a
a
  render (ImportedModule b
b) = Inlines
"module" Inlines -> Inlines -> Inlines
<+> forall a. Render a => a -> Inlines
render b
b