{-# LANGUAGE CPP #-}
{-# 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 (Ranged a) where
  render :: Ranged a -> Inlines
render = a -> Inlines
forall a. Render a => a -> Inlines
render (a -> Inlines) -> (Ranged a -> a) -> Ranged a -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged a -> a
forall a. Ranged a -> a
rangedThing

instance Render a => Render (WithHiding a) where
  render :: WithHiding a -> Inlines
render WithHiding a
w = WithHiding a -> (Inlines -> Inlines) -> Inlines -> Inlines
forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding WithHiding a
w Inlines -> Inlines
forall a. a -> a
id (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ a -> Inlines
forall a. Render a => a -> Inlines
render (a -> Inlines) -> a -> Inlines
forall a b. (a -> b) -> a -> b
$ WithHiding a -> a
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
    [ Relevance -> Inlines
forall a. Render a => a -> Inlines
render (Modality -> Relevance
forall a. LensRelevance a => a -> Relevance
getRelevance Modality
mod)
    , Quantity -> Inlines
forall a. Render a => a -> Inlines
render (Modality -> Quantity
forall a. LensQuantity a => a -> Quantity
getQuantity Modality
mod)
    , Cohesion -> Inlines
forall a. Render a => a -> Inlines
render (Modality -> Cohesion
forall a. LensCohesion a => a -> Cohesion
getCohesion Modality
mod)
    ]

-- | OpApp
instance Render (OpApp Expr) where
  render :: OpApp Expr -> Inlines
render (Ordinary Expr
e) = Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
  render (SyntaxBindingLambda Range
r List1 LamBinding
bs Expr
e) = Expr -> Inlines
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) = a -> Inlines
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 -> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
qname
    Lit Range
range Literal
lit -> Literal -> Inlines
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 (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> (String -> Inlines) -> Maybe String -> Inlines
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 ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e1 Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (NamedArg Expr -> Inlines) -> [NamedArg Expr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NamedArg Expr -> Inlines
forall a. Render a => a -> Inlines
render [NamedArg Expr]
args
    RawApp Range
_ List2 Expr
es -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Expr -> Inlines) -> [Expr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Inlines
forall a. Render a => a -> Inlines
render (List2 Expr -> [Item (List2 Expr)]
forall l. IsList l => l -> [Item l]
List2.toList List2 Expr
es)
    OpApp Range
_ QName
q Set Name
_ OpAppArgs
es -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ QName -> OpAppArgs -> [Inlines]
forall a.
Render a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
renderOpApp QName
q OpAppArgs
es
    WithApp Range
_ Expr
e [Expr]
es -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (Expr -> Inlines) -> [Expr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ClassNames -> String -> Inlines
text' [String
"delimiter"] String
"|" Inlines -> Inlines -> Inlines
<+>) (Inlines -> Inlines) -> (Expr -> Inlines) -> Expr -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Inlines
forall a. Render a => a -> Inlines
render) [Expr]
es
    HiddenArg Range
_ Named_ Expr
e -> Inlines -> Inlines
braces' (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Inlines
forall a. Render a => a -> Inlines
render Named_ Expr
e
    InstanceArg Range
_ Named_ Expr
e -> Inlines -> Inlines
dbraces (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Named_ Expr -> Inlines
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 ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render (List1 LamBinding -> [Item (List1 LamBinding)]
forall l. IsList l => l -> [Item l]
toList List1 LamBinding
bs)) Inlines -> Inlines -> Inlines
<+> Hiding -> 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 ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render (List1 LamBinding -> [Item (List1 LamBinding)]
forall l. IsList l => l -> [Item l]
toList List1 LamBinding
bs)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow, Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e]
    AbsurdLam Range
_ Hiding
h -> Inlines
lambda Inlines -> Inlines -> Inlines
<+> Hiding -> 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 ((LamClause -> Inlines) -> [LamClause] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamClause -> Inlines
forall a. Render a => a -> Inlines
render (List1 LamClause -> [Item (List1 LamClause)]
forall l. IsList l => l -> [Item l]
toList List1 LamClause
pes))
    Fun Range
_ Arg Expr
e1 Expr
e2 ->
      [Inlines] -> Inlines
sep
        [ Arg Expr -> Inlines -> Inlines
forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion Arg Expr
e1 (Arg Expr -> Inlines -> Inlines
forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity Arg Expr
e1 (Arg Expr -> Inlines
forall a. Render a => a -> Inlines
render Arg Expr
e1)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow,
          Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e2
        ]
    Pi Telescope1
tel Expr
e ->
      [Inlines] -> Inlines
sep
        [ Tel -> Inlines
forall a. Render a => a -> Inlines
render (Telescope -> Tel
Tel (Telescope -> Tel) -> Telescope -> Tel
forall a b. (a -> b) -> a -> b
$ Telescope -> Telescope
smashTel (Telescope1 -> [Item Telescope1]
forall l. IsList l => l -> [Item l]
toList Telescope1
tel)) Inlines -> Inlines -> Inlines
<+> Inlines
arrow,
          Expr -> Inlines
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 ((Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render (List1 Declaration -> [Item (List1 Declaration)]
forall l. IsList l => l -> [Item l]
toList List1 Declaration
ds)),
          Inlines -> (Expr -> Inlines) -> Maybe Expr -> Inlines
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Inlines
forall a. Monoid a => a
mempty (\Expr
e -> Inlines
"in" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e) Maybe Expr
me
        ]
    Paren Range
_ Expr
e -> Inlines -> Inlines
parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Expr -> Inlines
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
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> Inlines
rightIdiomBrkt
        Expr
e : [Expr]
es -> Inlines
leftIdiomBrkt Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep ((Expr -> Inlines) -> [Expr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Inlines
"|" Inlines -> Inlines -> Inlines
<+>) (Inlines -> Inlines) -> (Expr -> Inlines) -> Expr -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Inlines
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 ((DoStmt -> Inlines) -> [DoStmt] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap DoStmt -> Inlines
forall a. Render a => a -> Inlines
render (List1 DoStmt -> [Item (List1 DoStmt)]
forall l. IsList l => l -> [Item l]
toList List1 DoStmt
ss))
    As Range
_ Name
x Expr
e -> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"@" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
    Dot Range
_ Expr
e -> Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
    DoubleDot Range
_ Expr
e -> Inlines
".." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
    Absurd Range
_ -> Inlines
"()"
    Rec Range
_ RecordAssignments
xs -> [Inlines] -> Inlines
sep [Inlines
"record", [Inlines] -> Inlines
bracesAndSemicolons ((RecordAssignment -> Inlines) -> RecordAssignments -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RecordAssignment -> Inlines
forall a. Render a => a -> Inlines
render RecordAssignments
xs)]
    RecUpdate Range
_ Expr
e [FieldAssignment]
xs ->
      [Inlines] -> Inlines
sep [Inlines
"record" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e, [Inlines] -> Inlines
bracesAndSemicolons ((FieldAssignment -> Inlines) -> [FieldAssignment] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FieldAssignment -> Inlines
forall a. Render a => a -> Inlines
render [FieldAssignment]
xs)]
#if !MIN_VERSION_Agda(2,6,3)
    ETel [] -> "()"
    ETel tel -> fsep $ fmap render tel
#endif
    Quote Range
_ -> Inlines
"quote"
    QuoteTerm Range
_ -> Inlines
"quoteTerm"
    Unquote Range
_ -> Inlines
"unquote"
    Tactic Range
_ Expr
t -> Inlines
"tactic" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
t
    -- Andreas, 2011-10-03 print irrelevant things as .(e)
    DontCare Expr
e -> Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines -> Inlines
parens (Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e)
    Equal Range
_ Expr
a Expr
b -> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
a Inlines -> Inlines -> Inlines
<+> Inlines
"=" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
b
    Ellipsis Range
_ -> Inlines
"..."
    Generalized Expr
e -> Expr -> Inlines
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 = (a -> Inlines) -> (b -> Inlines) -> Either a b -> Inlines
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either a -> Inlines
forall a. Render a => a -> Inlines
render b -> Inlines
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 [Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> Inlines
"=", a -> 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 (QName -> Inlines
forall a. Render a => a -> Inlines
render QName
m Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (Expr -> Inlines) -> [Expr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Inlines
forall a. Render a => a -> Inlines
render [Expr]
es) Inlines -> Inlines -> Inlines
<+> ImportDirective -> 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
      [ [Pattern] -> Inlines
forall a. Render a => a -> Inlines
render [Pattern]
lhs,
        RHS -> Inlines
forall {a}. Render a => RHS' a -> Inlines
render' RHS
rhs
      ]
    where
      render' :: RHS' a -> Inlines
render' (RHS a
e) = Inlines
arrow Inlines -> Inlines -> Inlines
<+> a -> Inlines
forall a. Render a => a -> Inlines
render a
e
      render' RHS' a
AbsurdRHS = Inlines
forall a. Monoid a => a
mempty

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

renderTactic :: BoundName -> Inlines -> Inlines
renderTactic :: BoundName -> Inlines -> Inlines
renderTactic = Maybe Expr -> Inlines -> Inlines
renderTactic' (Maybe Expr -> Inlines -> Inlines)
-> (BoundName -> Maybe Expr) -> BoundName -> Inlines -> Inlines
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
"@" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> (Inlines -> Inlines
parens (Inlines
"tactic " Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Expr -> Inlines
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) = NamedBinding -> Inlines
forall a. Render a => a -> Inlines
render (Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
True NamedArg Binder
x)
  render (DomainFull TypedBinding
b) = TypedBinding -> Inlines
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 (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"let" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat ((Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render (List1 Declaration -> [Item (List1 Declaration)]
forall l. IsList l => l -> [Item l]
toList List1 Declaration
ds))
  render (TBind Range
_ List1 (NamedArg Binder)
xs (Underscore Range
_ Maybe String
Nothing)) =
    [Inlines] -> Inlines
fsep ((NamedArg Binder -> Inlines) -> [NamedArg Binder] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NamedBinding -> Inlines
forall a. Render a => a -> Inlines
render (NamedBinding -> Inlines)
-> (NamedArg Binder -> NamedBinding) -> NamedArg Binder -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
True) (List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
toList List1 (NamedArg Binder)
xs))
  render (TBind Range
_ List1 (NamedArg Binder)
binders Expr
e) =
    [Inlines] -> Inlines
fsep
      [ NamedArg Binder -> Inlines -> Inlines
forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance NamedArg Binder
y (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          NamedArg Binder -> (Inlines -> Inlines) -> Inlines -> Inlines
forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding NamedArg Binder
y Inlines -> Inlines
parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
            NamedArg Binder -> Inlines -> Inlines
forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion NamedArg Binder
y (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
              NamedArg Binder -> Inlines -> Inlines
forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity NamedArg Binder
y (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
                BoundName -> Inlines -> Inlines
renderTactic (Binder -> BoundName
forall a. Binder' a -> a
binderName (Binder -> BoundName) -> Binder -> BoundName
forall a b. (a -> b) -> a -> b
$ NamedArg Binder -> Binder
forall a. NamedArg a -> a
namedArg NamedArg Binder
y) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
                  [Inlines] -> Inlines
sep
                    [ [Inlines] -> Inlines
fsep ((NamedArg Binder -> Inlines) -> [NamedArg Binder] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (NamedBinding -> Inlines
forall a. Render a => a -> Inlines
render (NamedBinding -> Inlines)
-> (NamedArg Binder -> NamedBinding) -> NamedArg Binder -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Bool -> NamedArg Binder -> NamedBinding
NamedBinding Bool
False) [NamedArg Binder]
ys),
                      Inlines
":" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
                    ]
        | ys :: [NamedArg Binder]
ys@(NamedArg Binder
y : [NamedArg Binder]
_) <- [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds (List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
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] [NamedArg Binder] -> [[NamedArg Binder]] -> [[NamedArg Binder]]
forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
xs
        | Bool
otherwise = (NamedArg Binder
x NamedArg Binder -> [NamedArg Binder] -> [NamedArg Binder]
forall a. a -> [a] -> [a]
: [NamedArg Binder]
ys) [NamedArg Binder] -> [[NamedArg Binder]] -> [[NamedArg Binder]]
forall a. a -> [a] -> [a]
: [NamedArg Binder] -> [[NamedArg Binder]]
groupBinds [NamedArg Binder]
zs
        where
          ([NamedArg Binder]
ys, [NamedArg Binder]
zs) = (NamedArg Binder -> Bool)
-> [NamedArg Binder] -> ([NamedArg Binder], [NamedArg Binder])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (NamedArg Binder -> NamedArg Binder -> Bool
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 = a -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo a
a ArgInfo -> ArgInfo -> Bool
forall a. Eq a => a -> a -> Bool
== NamedArg Binder -> ArgInfo
forall a. LensArgInfo a => a -> ArgInfo
getArgInfo NamedArg Binder
b Bool -> Bool -> Bool
&& Maybe String -> 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)
    | (TypedBinding -> Bool) -> Telescope -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any TypedBinding -> Bool
isMeta Telescope
tel = Inlines
forallQ Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep ((TypedBinding -> Inlines) -> Telescope -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedBinding -> Inlines
forall a. Render a => a -> Inlines
render Telescope
tel)
    | Bool
otherwise = [Inlines] -> Inlines
fsep ((TypedBinding -> Inlines) -> Telescope -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedBinding -> Inlines
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
    )
    | Expr -> String
forall a. Show a => a -> String
show Expr
e String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== Expr -> String
forall a. Show a => a -> String
show Expr
e' = Telescope -> Telescope
smashTel (Range -> List1 (NamedArg Binder) -> Expr -> TypedBinding
forall e. Range -> List1 (NamedArg Binder) -> e -> TypedBinding' e
TBind Range
r ([Item (List1 (NamedArg Binder))] -> List1 (NamedArg Binder)
forall l. IsList l => [Item l] -> l
fromList (List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
toList List1 (NamedArg Binder)
xs [NamedArg Binder] -> [NamedArg Binder] -> [NamedArg Binder]
forall a. [a] -> [a] -> [a]
++ List1 (NamedArg Binder) -> [Item (List1 (NamedArg Binder))]
forall l. IsList l => l -> [Item l]
toList List1 (NamedArg Binder)
ys)) Expr
e TypedBinding -> Telescope -> Telescope
forall a. a -> [a] -> [a]
: Telescope
tel)
smashTel (TypedBinding
b : Telescope
tel) = TypedBinding
b TypedBinding -> Telescope -> Telescope
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
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
  render RHS
AbsurdRHS = Inlines
forall a. Monoid a => a
mempty

instance Render WhereClause where
  render :: WhereClause -> Inlines
render WhereClause
NoWhere = Inlines
forall a. Monoid a => a
mempty
  render (AnyWhere Range
_range [Module Range
_ QName
x [] [Declaration]
ds])
    | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName (QName -> Name
unqualify QName
x) =
      [Inlines] -> Inlines
vcat [Inlines
"where", [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render [Declaration]
ds]
  render (AnyWhere Range
_range [Declaration]
ds) = [Inlines] -> Inlines
vcat [Inlines
"where", [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
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 ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$
          Bool -> ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a. Bool -> (a -> a) -> a -> a
applyWhen
            (Access
a Access -> Access -> Bool
forall a. Eq a => a -> a -> Bool
== Origin -> Access
PrivateAccess Origin
UserWritten)
            (Inlines
"private" Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
:)
            [Inlines
"module", Name -> Inlines
forall a. Render a => a -> Inlines
render Name
m, Inlines
"where"],
        [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
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
      [ Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p,
        if [RewriteEqn] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RewriteEqn]
eqs then Inlines
forall a. Monoid a => a
mempty else [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (RewriteEqn -> Inlines) -> [RewriteEqn] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap RewriteEqn -> Inlines
forall a. Render a => a -> Inlines
render [RewriteEqn]
eqs,
        Inlines -> [Inlines] -> Inlines
prefixedThings Inlines
"with" ((WithExpr -> Inlines) -> [WithExpr] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
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 = Arg Expr -> Inlines
forall a. Render a => a -> Inlines
render Arg Expr
wh in
        case Maybe Name
nm of
          Maybe Name
Nothing -> Inlines
e
          Just Name
n  -> Name -> Inlines
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 ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ QName -> Inlines
forall a. Render a => a -> Inlines
render QName
f Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (NamedArg Pattern -> Inlines) -> [NamedArg Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens (Inlines -> Inlines)
-> (NamedArg Pattern -> Inlines) -> NamedArg Pattern -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Inlines
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 ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$
      QName -> Inlines
forall a. Render a => a -> Inlines
render QName
d Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
:
      (NamedArg Pattern -> Inlines) -> [NamedArg Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens (Inlines -> Inlines)
-> (NamedArg Pattern -> Inlines) -> NamedArg Pattern -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Inlines
forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps
        [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ Inlines -> Inlines
parens (NamedArg LHSCore -> Inlines
forall a. Render a => a -> Inlines
render NamedArg LHSCore
lhscore) Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
:
      (NamedArg Pattern -> Inlines) -> [NamedArg Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens (Inlines -> Inlines)
-> (NamedArg Pattern -> Inlines) -> NamedArg Pattern -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Inlines
forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps'
  render (LHSWith LHSCore
h [Pattern]
wps [NamedArg Pattern]
ps) =
    if [NamedArg Pattern] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NamedArg Pattern]
ps
      then Inlines
doc
      else [Inlines] -> Inlines
sep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> Inlines
parens Inlines
doc Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (NamedArg Pattern -> Inlines) -> [NamedArg Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines -> Inlines
parens (Inlines -> Inlines)
-> (NamedArg Pattern -> Inlines) -> NamedArg Pattern -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NamedArg Pattern -> Inlines
forall a. Render a => a -> Inlines
render) [NamedArg Pattern]
ps
    where
      doc :: Inlines
doc = [Inlines] -> Inlines
sep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ LHSCore -> Inlines
forall a. Render a => a -> Inlines
render LHSCore
h Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (Pattern -> Inlines) -> [Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Inlines
"|" Inlines -> Inlines -> Inlines
<+>) (Inlines -> Inlines) -> (Pattern -> Inlines) -> Pattern -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Pattern -> Inlines
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 ((TypedBinding -> Inlines) -> Telescope -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedBinding -> Inlines
forall a. Render a => a -> Inlines
render Telescope
bs) Inlines -> Inlines -> Inlines
<+> Inlines
"=" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
  render (RecordModuleInstance Range
_ QName
rec) = Inlines
"=" Inlines -> Inlines -> Inlines
<+> QName -> 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 [Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p Inlines -> Inlines -> Inlines
<+> Inlines
"←", Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e, [LamClause] -> Inlines
forall {a}. Render a => [a] -> Inlines
prCs [LamClause]
cs]
    where
      prCs :: [a] -> Inlines
prCs [] = Inlines
forall a. Monoid a => a
mempty
      prCs [a]
cs' = [Inlines] -> Inlines
fsep [Inlines
"where", [Inlines] -> Inlines
vcat ((a -> Inlines) -> [a] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inlines
forall a. Render a => a -> Inlines
render [a]
cs')]
  render (DoThen Expr
e) = Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e
  render (DoLet Range
_ List1 Declaration
ds) = Inlines
"let" Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
vcat ((Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render ([Declaration] -> [Inlines]) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ List1 Declaration -> [Item (List1 Declaration)]
forall l. IsList l => l -> [Item l]
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 (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Inlines -> Inlines
forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Inlines -> Inlines
forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Inlines -> Inlines
forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> Inlines
":",
            Expr -> 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 (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
          ArgInfo -> Inlines -> Inlines
forall {a}. LensHiding a => a -> Inlines -> Inlines
mkOverlap ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
            ArgInfo -> Inlines -> Inlines
forall a. LensRelevance a => a -> Inlines -> Inlines
renderRelevance ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
              ArgInfo -> (Inlines -> Inlines) -> Inlines -> Inlines
forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
i Inlines -> Inlines
forall a. a -> a
id (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
                ArgInfo -> Inlines -> Inlines
forall a. LensCohesion a => a -> Inlines -> Inlines
renderCohesion ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
                  ArgInfo -> Inlines -> Inlines
forall a. LensQuantity a => a -> Inlines -> Inlines
renderQuantity ArgInfo
i (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$
                    Declaration -> Inlines
forall a. Render a => a -> Inlines
render (Declaration -> Inlines) -> Declaration -> Inlines
forall a b. (a -> b) -> a -> b
$ ArgInfo -> Maybe Expr -> Name -> Expr -> Declaration
TypeSig (Relevance -> ArgInfo -> ArgInfo
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
            | a -> Bool
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 ((Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render [Declaration]
fs)
          ]
      FunClause LHS
lhs RHS
rhs WhereClause
wh Bool
_ ->
        [Inlines] -> Inlines
sep
          [ LHS -> Inlines
forall a. Render a => a -> Inlines
render LHS
lhs,
            RHS -> Inlines
forall a. Render a => a -> Inlines
render RHS
rhs,
            WhereClause -> Inlines
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",
                Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                Expr -> 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",
                Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e,
                Inlines
"where"
              ],
            [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
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",
                Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            Inlines
"where",
            [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
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",
                Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
                [Inlines] -> Inlines
fcat ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render [LamBinding]
tel)
              ],
            [Inlines] -> Inlines
hsep
              [ Inlines
":",
                Expr -> 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 (Expr -> Maybe Expr
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 Maybe Expr
forall a. Maybe a
Nothing [Declaration]
cs
      RecordDirective RecordDirective
r -> RecordDirective -> Inlines
pRecordDirective RecordDirective
r
      Infix Fixity
f List1 Name
xs -> Fixity -> Inlines
forall a. Render a => a -> Inlines
render Fixity
f Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep (Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"," ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (Name -> Inlines) -> [Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Inlines
forall a. Render a => a -> Inlines
render (List1 Name -> [Item (List1 Name)]
forall l. IsList l => l -> [Item l]
toList List1 Name
xs))
      Syntax Name
n Notation
_ -> Inlines
"syntax" Inlines -> Inlines -> Inlines
<+> Name -> 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
<+> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
n Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fsep ((Arg Name -> Inlines) -> [Arg Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Arg Name -> Inlines
forall a. Render a => a -> Inlines
render [Arg Name]
as)
          Inlines -> Inlines -> Inlines
<+> Inlines
"="
          Inlines -> Inlines -> Inlines
<+> Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p
      Mutual Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"mutual" [Declaration]
ds
      InterleavedMutual Range
_ [Declaration]
ds  -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"interleaved mutual" [Declaration]
ds
      LoneConstructor Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"constructor" [Declaration]
ds
      Abstract Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"abstract" [Declaration]
ds
      Private Range
_ Origin
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"private" [Declaration]
ds
      InstanceB Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"instance" [Declaration]
ds
      Macro Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"macro" [Declaration]
ds
      Postulate Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"postulate" [Declaration]
ds
      Primitive Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
forall {a}. Render a => String -> [a] -> Inlines
namedBlock String
"primitive" [Declaration]
ds
      Generalize Range
_ [Declaration]
ds -> String -> [Declaration] -> Inlines
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",
                QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x,
                [Inlines] -> Inlines
fcat ((TypedBinding -> Inlines) -> Telescope -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedBinding -> Inlines
forall a. Render a => a -> Inlines
render Telescope
tel),
                Inlines
"where"
              ],
            [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render [Declaration]
ds
          ]
      ModuleMacro Range
_ Name
x (SectionApp Range
_ [] Expr
e) OpenShortHand
DoOpen ImportDirective
i
        | Name -> Bool
forall a. IsNoName a => a -> Bool
isNoName Name
x ->
          [Inlines] -> Inlines
fsep
            [ OpenShortHand -> Inlines
forall a. Render a => a -> Inlines
render OpenShortHand
DoOpen,
              Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e,
              ImportDirective -> Inlines
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
          [ OpenShortHand -> Inlines
forall a. Render a => a -> Inlines
render OpenShortHand
open Inlines -> Inlines -> Inlines
<+> Inlines
"module" Inlines -> Inlines -> Inlines
<+> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
fcat ((TypedBinding -> Inlines) -> Telescope -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypedBinding -> Inlines
forall a. Render a => a -> Inlines
render Telescope
tel),
            Inlines
"=" Inlines -> Inlines -> Inlines
<+> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e Inlines -> Inlines -> Inlines
<+> ImportDirective -> Inlines
forall a. Render a => a -> Inlines
render ImportDirective
i
          ]
      ModuleMacro Range
_ Name
x (RecordModuleInstance Range
_ QName
rec) OpenShortHand
open ImportDirective
_ ->
        [Inlines] -> Inlines
fsep
          [ OpenShortHand -> Inlines
forall a. Render a => a -> Inlines
render OpenShortHand
open Inlines -> Inlines -> Inlines
<+> Inlines
"module" Inlines -> Inlines -> Inlines
<+> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
            Inlines
"=" Inlines -> Inlines -> Inlines
<+> QName -> 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", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x, ImportDirective -> Inlines
forall a. Render a => a -> Inlines
render ImportDirective
i]
      Import Range
_ QName
x Maybe AsName
rn OpenShortHand
open ImportDirective
i ->
        [Inlines] -> Inlines
hsep [OpenShortHand -> Inlines
forall a. Render a => a -> Inlines
render OpenShortHand
open, Inlines
"import", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x, Maybe AsName -> Inlines
forall {a}. Render a => Maybe (AsName' a) -> Inlines
as Maybe AsName
rn, ImportDirective -> Inlines
forall a. Render a => a -> Inlines
render ImportDirective
i]
        where
          as :: Maybe (AsName' a) -> Inlines
as Maybe (AsName' a)
Nothing = Inlines
forall a. Monoid a => a
mempty
          as (Just AsName' a
y) = Inlines
"as" Inlines -> Inlines -> Inlines
<+> a -> Inlines
forall a. Render a => a -> Inlines
render (AsName' a -> a
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 ((Name -> Inlines) -> [Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Inlines
forall a. Render a => a -> Inlines
render [Name]
xs) Inlines -> Inlines -> Inlines
<+> Inlines
"=", Expr -> 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 ((Name -> Inlines) -> [Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Inlines
forall a. Render a => a -> Inlines
render [Name]
xs) Inlines -> Inlines -> Inlines
<+> Inlines
"=", Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
t]
      Pragma Pragma
pr -> [Inlines] -> Inlines
sep [Inlines
"{-#" Inlines -> Inlines -> Inlines
<+> Pragma -> Inlines
forall a. Render a => a -> Inlines
render Pragma
pr, Inlines
"#-}"]
#if MIN_VERSION_Agda(2,6,3)
      UnquoteData Range
_ Name
x [Name]
xs Expr
e ->
        [Inlines] -> Inlines
fsep [ [Inlines] -> Inlines
hsep [ Inlines
"unquoteData", Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x, [Inlines] -> Inlines
fsep ((Name -> Inlines) -> [Name] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Name -> Inlines
forall a. Render a => a -> Inlines
render [Name]
xs), Inlines
"=" ], Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e ]
#endif
    where
      namedBlock :: String -> [a] -> Inlines
namedBlock String
s [a]
ds =
        [Inlines] -> Inlines
fsep
          [ String -> Inlines
text String
s,
            [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (a -> Inlines) -> [a] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inlines
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 -> Ranged Induction -> Inlines
forall a. Render a => a -> Inlines
render Ranged Induction
ind
  Constructor Name
n IsInstance
inst -> [Inlines] -> Inlines
hsep [ Inlines
pInst, Inlines
"constructor", Name -> Inlines
forall a. Render a => a -> Inlines
render Name
n ] where
    pInst :: Inlines
pInst = case IsInstance
inst of
      InstanceDef{} -> Inlines
"instance"
      NotInstanceDef{} -> Inlines
forall a. Monoid a => a
mempty
  Eta Ranged HasEta0
eta -> HasEta0 -> Inlines
pHasEta0 (Ranged HasEta0 -> HasEta0
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",
          Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x,
          [Inlines] -> Inlines
fcat ((LamBinding -> Inlines) -> [LamBinding] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap LamBinding -> Inlines
forall a. Render a => a -> Inlines
render [LamBinding]
tel)
        ],
      Maybe Expr -> Inlines
forall {a}. Render a => Maybe a -> Inlines
pType Maybe Expr
me,
      [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$
        [Inlines]
pInd
          [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ [Inlines]
pEta
          [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ [Inlines]
pCon
          [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ (Declaration -> Inlines) -> [Declaration] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Declaration -> Inlines
forall a. Render a => a -> Inlines
render [Declaration]
cs
    ]
  where
    pType :: Maybe a -> Inlines
pType (Just a
e) =
      [Inlines] -> Inlines
hsep
        [ Inlines
":",
          a -> Inlines
forall a. Render a => a -> Inlines
render a
e,
          Inlines
"where"
        ]
    pType Maybe a
Nothing =
      Inlines
"where"
    pInd :: [Inlines]
pInd = Maybe Inlines -> [Inlines]
forall a. Maybe a -> [a]
maybeToList (Maybe Inlines -> [Inlines]) -> Maybe Inlines -> [Inlines]
forall a b. (a -> b) -> a -> b
$ String -> Inlines
text (String -> Inlines)
-> (Ranged Induction -> String) -> Ranged Induction -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Induction -> String
forall a. Show a => a -> String
show (Induction -> String)
-> (Ranged Induction -> Induction) -> Ranged Induction -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged Induction -> Induction
forall a. Ranged a -> a
rangedThing (Ranged Induction -> Inlines)
-> Maybe (Ranged Induction) -> Maybe Inlines
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe (Ranged Induction)
ind
    pEta :: [Inlines]
pEta =
      Maybe Inlines -> [Inlines]
forall a. Maybe a -> [a]
maybeToList (Maybe Inlines -> [Inlines]) -> Maybe Inlines -> [Inlines]
forall a b. (a -> b) -> a -> b
$
        Maybe HasEta0
eta Maybe HasEta0 -> (HasEta0 -> Inlines) -> Maybe Inlines
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 = Maybe Inlines -> [Inlines]
forall a. Maybe a -> [a]
maybeToList (Maybe Inlines -> [Inlines]) -> Maybe Inlines -> [Inlines]
forall a b. (a -> b) -> a -> b
$ ((Inlines
"constructor" Inlines -> Inlines -> Inlines
<+>) (Inlines -> Inlines) -> (Name -> Inlines) -> Name -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Inlines
forall a. Render a => a -> Inlines
render) (Name -> Inlines)
-> ((Name, IsInstance) -> Name) -> (Name, IsInstance) -> Inlines
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name, IsInstance) -> Name
forall a b. (a, b) -> a
fst ((Name, IsInstance) -> Inlines)
-> Maybe (Name, IsInstance) -> Maybe Inlines
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 = Inlines
forall a. Monoid a => a
mempty

instance Render Pragma where
  render :: Pragma -> Inlines
render (OptionsPragma Range
_ ClassNames
opts) = [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (String -> Inlines) -> ClassNames -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap String -> Inlines
text (ClassNames -> [Inlines]) -> ClassNames -> [Inlines]
forall a b. (a -> b) -> a -> b
$ String
"OPTIONS" String -> ClassNames -> ClassNames
forall a. a -> [a] -> [a]
: ClassNames
opts
  render (BuiltinPragma Range
_ RString
b QName
x) = [Inlines] -> Inlines
hsep [Inlines
"BUILTIN", String -> Inlines
text (RString -> String
forall a. Ranged a -> a
rangedThing RString
b), QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x]
  render (RewritePragma Range
_ Range
_ [QName]
xs) =
    [Inlines] -> Inlines
hsep [Inlines
"REWRITE", [Inlines] -> Inlines
hsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (QName -> Inlines) -> [QName] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap QName -> Inlines
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 (RString -> String
forall a. Ranged a -> a
rangedThing RString
b), QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x, String -> Inlines
text String
e]
  render (ForeignPragma Range
_ RString
b String
s) =
    [Inlines] -> Inlines
vcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ String -> Inlines
text (String
"FOREIGN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RString -> String
forall a. Ranged a -> a
rangedThing RString
b) Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (String -> Inlines) -> ClassNames -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
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", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
i]
  render (InjectivePragma Range
_ QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"INJECTIVE", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
i]
  render (InlinePragma Range
_ Bool
True QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"INLINE", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
i]
  render (InlinePragma Range
_ Bool
False QName
i) =
    [Inlines] -> Inlines
hsep [Inlines
"NOINLINE", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
i]
  render (ImpossiblePragma Range
_ ClassNames
strs) =
    [Inlines] -> Inlines
hsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines
"IMPOSSIBLE" Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (String -> Inlines) -> ClassNames -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
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", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x]
  render (TerminationCheckPragma Range
_ TerminationCheck Name
tc) =
    case TerminationCheck Name
tc of
      TerminationCheck Name
TerminationCheck -> Inlines
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", Name -> Inlines
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", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
nm, String -> Inlines
text (String -> Inlines) -> String -> Inlines
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 (String -> Inlines) -> String -> Inlines
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 [Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
lhs Inlines -> Inlines -> Inlines
<+> Inlines
"=", Expr -> 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" Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: Name -> Inlines
forall a. Render a => a -> Inlines
render Name
q Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: (Occurrence -> Inlines) -> [Occurrence] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Occurrence -> Inlines
forall a. Render a => a -> Inlines
render [Occurrence]
occs)
  render (NoUniverseCheckPragma Range
_) = Inlines
"NO_UNIVERSE_CHECK"
#if MIN_VERSION_Agda(2,6,3)
  render (NotProjectionLikePragma Range
_ QName
q) =
    [Inlines] -> Inlines
hsep [ Inlines
"NOT_PROJECTION_LIKE", QName -> Inlines
forall a. Render a => a -> Inlines
render QName
q ]
#endif

instance Render Fixity where
  render :: Fixity -> Inlines
render (Fixity Range
_ FixityLevel
Unrelated Associativity
_) = Inlines
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"

#if MIN_VERSION_Agda(2,6,3)
instance Render NotationPart where
  render :: NotationPart -> Inlines
render = \case
    IdPart  RString
x  -> String -> Inlines
text (String -> Inlines) -> String -> Inlines
forall a b. (a -> b) -> a -> b
$ RString -> String
forall a. Ranged a -> a
rangedThing RString
x
    HolePart{} -> Inlines
"_"
    VarPart {} -> Inlines
"_"
    WildPart{} -> Inlines
"_"
#else
instance Render GenPart where
  render (IdPart x) = text $ rangedThing x
  render BindHole {} = "_"
  render NormalHole {} = "_"
  render WildHole {} = "_"
#endif

instance Render Fixity' where
  render :: Fixity' -> Inlines
render (Fixity' Fixity
fix Notation
nota Range
_)
    | Notation
nota Notation -> Notation -> Bool
forall a. Eq a => a -> a -> Bool
== Notation
noNotation = Fixity -> Inlines
forall a. Render a => a -> Inlines
render Fixity
fix
    | Bool
otherwise = Inlines
"syntax" Inlines -> Inlines -> Inlines
<+> Notation -> 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) = ArgInfo -> (Inlines -> Inlines) -> Inlines -> Inlines
forall a.
LensHiding a =>
a -> (Inlines -> Inlines) -> Inlines -> Inlines
renderHiding ArgInfo
ai Inlines -> Inlines
localParens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Int -> a -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p' a
e
    where
      p' :: Int
p'
        | ArgInfo -> Bool
forall a. LensHiding a => a -> Bool
visible ArgInfo
ai = Int
p
        | Bool
otherwise = Int
0
      localParens :: Inlines -> Inlines
localParens
        | ArgInfo -> Origin
forall a. LensOrigin a => a -> Origin
getOrigin ArgInfo
ai Origin -> Origin -> Bool
forall a. Eq a => a -> a -> Bool
== Origin
Substitution = Inlines -> Inlines
parens
        | Bool
otherwise = Inlines -> Inlines
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 <- Maybe NamedName -> Maybe String
forall a. (LensNamed a, NameOf a ~ NamedName) => a -> Maybe String
bareNameOf Maybe NamedName
nm = Bool -> Inlines -> Inlines
mparens (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0) (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
sep [String -> Inlines
text String
s Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
" =", e -> Inlines
forall a. Render a => a -> Inlines
render e
e]
    | Bool
otherwise = Int -> e -> Inlines
forall a. Render a => Int -> a -> Inlines
renderPrec Int
p e
e

instance Render Pattern where
  render :: Pattern -> Inlines
render = \case
    IdentP QName
x -> QName -> Inlines
forall a. Render a => a -> Inlines
render QName
x
    AppP Pattern
p1 NamedArg Pattern
p2 -> [Inlines] -> Inlines
fsep [Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p1, NamedArg Pattern -> Inlines
forall a. Render a => a -> Inlines
render NamedArg Pattern
p2]
    RawAppP Range
_ List2 Pattern
ps -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ (Pattern -> Inlines) -> [Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Pattern -> Inlines
forall a. Render a => a -> Inlines
render (List2 Pattern -> [Item (List2 Pattern)]
forall l. IsList l => l -> [Item l]
List2.toList List2 Pattern
ps)
    OpAppP Range
_ QName
q Set Name
_ [NamedArg Pattern]
ps -> [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ QName -> [NamedArg (MaybePlaceholder Pattern)] -> [Inlines]
forall a.
Render a =>
QName -> [NamedArg (MaybePlaceholder a)] -> [Inlines]
renderOpApp QName
q ((NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern))
-> [NamedArg Pattern] -> [NamedArg (MaybePlaceholder Pattern)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Named NamedName Pattern -> Named_ (MaybePlaceholder Pattern))
-> NamedArg Pattern -> NamedArg (MaybePlaceholder Pattern)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Pattern -> MaybePlaceholder Pattern)
-> Named NamedName Pattern -> Named_ (MaybePlaceholder Pattern)
forall a b. (a -> b) -> Named NamedName a -> Named NamedName b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe PositionInName -> Pattern -> MaybePlaceholder Pattern
forall e. Maybe PositionInName -> e -> MaybePlaceholder e
NoPlaceholder Maybe PositionInName
forall a. Maybe a
Strict.Nothing))) [NamedArg Pattern]
ps)
    HiddenP Range
_ Named NamedName Pattern
p -> Inlines -> Inlines
braces' (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Named NamedName Pattern -> Inlines
forall a. Render a => a -> Inlines
render Named NamedName Pattern
p
    InstanceP Range
_ Named NamedName Pattern
p -> Inlines -> Inlines
dbraces (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Named NamedName Pattern -> Inlines
forall a. Render a => a -> Inlines
render Named NamedName Pattern
p
    ParenP Range
_ Pattern
p -> Inlines -> Inlines
parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p
    WildP Range
_ -> Inlines
"_"
    AsP Range
_ Name
x Pattern
p -> Name -> Inlines
forall a. Render a => a -> Inlines
render Name
x Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
"@" Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Pattern -> Inlines
forall a. Render a => a -> Inlines
render Pattern
p
    DotP Range
_ Expr
p -> Inlines
"." Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
p
    AbsurdP Range
_ -> Inlines
"()"
    LitP Range
_ Literal
l -> Literal -> Inlines
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 ((FieldAssignment' Pattern -> Inlines)
-> [FieldAssignment' Pattern] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap FieldAssignment' Pattern -> Inlines
forall a. Render a => a -> Inlines
render [FieldAssignment' Pattern]
fs)]
    EqualP Range
_ [(Expr, Expr)]
es -> [Inlines] -> Inlines
sep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines -> Inlines
parens ([Inlines] -> Inlines
sep [Expr -> Inlines
forall a. Render a => a -> Inlines
render Expr
e1, Inlines
"=", Expr -> 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
<+> Pattern -> 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] [Inlines] -> [Inlines] -> [Inlines]
forall a. [a] -> [a] -> [a]
++ (Inlines -> Inlines) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Inlines
";" Inlines -> Inlines -> Inlines
<+>) [Inlines]
ds [Inlines] -> [Inlines] -> [Inlines]
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 [] ([(Inlines, Maybe PositionInName)] -> [Inlines])
-> [(Inlines, Maybe PositionInName)] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
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 = List1 Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (QName -> List1 Name
qnameParts QName
q)
    -- xs: the concrete name (alternation of @Id@ and @Hole@)
    concreteNames :: [Item NameParts]
concreteNames = case QName -> Name
unqualify QName
q of
      Name Range
_ NameInScope
_ NameParts
xs -> NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
List1.toList NameParts
xs
      NoName {} -> [Item NameParts]
[NamePart]
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 NamedArg (MaybePlaceholder a) -> MaybePlaceholder a
forall a. NamedArg a -> a
namedArg NamedArg (MaybePlaceholder a)
e of
        Placeholder PositionInName
p -> ([Name] -> Inlines -> Inlines
forall {a}. Render a => [a] -> Inlines -> Inlines
qual [Name]
ms (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ NamedArg (MaybePlaceholder a) -> Inlines
forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, PositionInName -> Maybe PositionInName
forall a. a -> Maybe a
Just PositionInName
p) (Inlines, Maybe PositionInName)
-> [(Inlines, Maybe PositionInName)]
-> [(Inlines, Maybe PositionInName)]
forall a. a -> [a] -> [a]
: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
forall a.
Render a =>
[Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
prOp [] [NamePart]
xs [NamedArg (MaybePlaceholder a)]
es
        NoPlaceholder {} -> (NamedArg (MaybePlaceholder a) -> Inlines
forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, Maybe PositionInName
forall a. Maybe a
Nothing) (Inlines, Maybe PositionInName)
-> [(Inlines, Maybe PositionInName)]
-> [(Inlines, Maybe PositionInName)]
forall a. a -> [a] -> [a]
: [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
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]
_) [] = [(Inlines, Maybe PositionInName)]
forall a. HasCallStack => a
__IMPOSSIBLE__
    prOp [Name]
ms (Id String
x : [NamePart]
xs) [NamedArg (MaybePlaceholder a)]
es =
      ( [Name] -> Inlines -> Inlines
forall {a}. Render a => [a] -> Inlines -> Inlines
qual [Name]
ms (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ Name -> Inlines
forall a. Render a => a -> Inlines
render (Name -> Inlines) -> Name -> Inlines
forall a b. (a -> b) -> a -> b
$ String -> Name
simpleName String
x,
        Maybe PositionInName
forall a. Maybe a
Nothing
      ) (Inlines, Maybe PositionInName)
-> [(Inlines, Maybe PositionInName)]
-> [(Inlines, Maybe PositionInName)]
forall a. a -> [a] -> [a]
:
      [Name]
-> [NamePart]
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
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 = (NamedArg (MaybePlaceholder a) -> (Inlines, Maybe PositionInName))
-> [NamedArg (MaybePlaceholder a)]
-> [(Inlines, Maybe PositionInName)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\NamedArg (MaybePlaceholder a)
e -> (NamedArg (MaybePlaceholder a) -> Inlines
forall a. Render a => a -> Inlines
render NamedArg (MaybePlaceholder a)
e, Maybe PositionInName
forall a. Maybe a
Nothing)) [NamedArg (MaybePlaceholder a)]
es

    qual :: [a] -> Inlines -> Inlines
qual [a]
ms' Inlines
doc = [Inlines] -> Inlines
hcat ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
"." ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (a -> Inlines) -> [a] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inlines
forall a. Render a => a -> Inlines
render [a]
ms' [Inlines] -> [Inlines] -> [Inlines]
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 [] = [Inlines] -> [Inlines]
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 Inlines -> [Inlines] -> [Inlines]
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 Inlines -> [Inlines] -> (Inlines, [Inlines])
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' Inlines -> [Inlines] -> [Inlines]
forall a. a -> [a] -> [a]
: [Inlines]
bs) [(Inlines, Maybe PositionInName)]
after
    merge [Inlines]
before ((Inlines
d, Just PositionInName
Middle) : [(Inlines, Maybe PositionInName)]
after) = case Inlines -> [Inlines] -> (Inlines, [Inlines])
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 =
      [Inlines] -> [Inlines]
forall a. [a] -> [a]
reverse [Inlines]
before
        [Inlines] -> [Inlines] -> [Inlines]
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 Inlines -> Inlines -> Inlines
forall a. Semigroup a => a -> a -> a
<> Inlines
a) Inlines -> [Inlines] -> [Inlines]
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 a -> a -> a
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
      [ Maybe Range -> Inlines
forall {a} {a}. (IsString a, Monoid a) => Maybe a -> a
public (ImportDirective' a b -> Maybe Range
forall n m. ImportDirective' n m -> Maybe Range
publicOpen ImportDirective' a b
i),
        Using' a b -> Inlines
forall a. Render a => a -> Inlines
render (Using' a b -> Inlines) -> Using' a b -> Inlines
forall a b. (a -> b) -> a -> b
$ ImportDirective' a b -> Using' a b
forall n m. ImportDirective' n m -> Using' n m
using ImportDirective' a b
i,
        [ImportedName' a b] -> Inlines
forall {a}. Render a => [a] -> Inlines
renderHiding' ([ImportedName' a b] -> Inlines) -> [ImportedName' a b] -> Inlines
forall a b. (a -> b) -> a -> b
$ ImportDirective' a b -> [ImportedName' a b]
forall n m. ImportDirective' n m -> HidingDirective' n m
hiding ImportDirective' a b
i,
        [Renaming' a b] -> Inlines
forall {a}. Render a => [a] -> Inlines
rename ([Renaming' a b] -> Inlines) -> [Renaming' a b] -> Inlines
forall a b. (a -> b) -> a -> b
$ ImportDirective' a b -> [Renaming' 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 = a
forall a. Monoid a => a
mempty

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

      rename :: [a] -> Inlines
rename [] = Inlines
forall a. Monoid a => a
mempty
      rename [a]
xs =
        [Inlines] -> Inlines
hsep
          [ Inlines
"renaming",
            Inlines -> Inlines
parens (Inlines -> Inlines) -> Inlines -> Inlines
forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
";" ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (a -> Inlines) -> [a] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Inlines
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 = Inlines
forall a. Monoid a => a
mempty
  render (Using [ImportedName' a b]
xs) =
    Inlines
"using" Inlines -> Inlines -> Inlines
<+> Inlines -> Inlines
parens ([Inlines] -> Inlines
fsep ([Inlines] -> Inlines) -> [Inlines] -> Inlines
forall a b. (a -> b) -> a -> b
$ Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
";" ([Inlines] -> [Inlines]) -> [Inlines] -> [Inlines]
forall a b. (a -> b) -> a -> b
$ (ImportedName' a b -> Inlines) -> [ImportedName' a b] -> [Inlines]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ImportedName' a b -> Inlines
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
      [ ImportedName' a b -> Inlines
forall a. Render a => a -> Inlines
render ImportedName' a b
from,
        Inlines
"to",
        Inlines -> (Fixity -> Inlines) -> Maybe Fixity -> Inlines
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Inlines
forall a. Monoid a => a
mempty Fixity -> Inlines
forall a. Render a => a -> Inlines
render Maybe Fixity
mfx,
        case ImportedName' a b
to of
          ImportedName a
a -> a -> Inlines
forall a. Render a => a -> Inlines
render a
a
          ImportedModule b
b -> b -> Inlines
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) = a -> Inlines
forall a. Render a => a -> Inlines
render a
a
  render (ImportedModule b
b) = Inlines
"module" Inlines -> Inlines -> Inlines
<+> b -> Inlines
forall a. Render a => a -> Inlines
render b
b