{-# 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 w = renderHiding w id $ render $ dget w

instance Render Modality where
  render mod = hsep
    [ render (getRelevance mod)
    , render (getQuantity mod)
    , render (getCohesion mod)
    ]

-- | OpApp
instance Render (OpApp Expr) where
  render (Ordinary e) = render e
  render (SyntaxBindingLambda r bs e) = render (Lam r bs e)

-- | MaybePlaceholder
instance Render a => Render (MaybePlaceholder a) where
  render Placeholder {} = "_"
  render (NoPlaceholder _ e) = render e

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

-- | InteractionId
instance Render InteractionId where
  render (InteractionId i) = linkHole i

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

-- | Expression
instance Render Expr where
  render expr = case expr of
    Ident qname -> render qname
    Lit range lit -> render lit
    -- no hole index, use LinkRange instead
    QuestionMark range Nothing -> linkRange range "?"
    QuestionMark _range (Just n) -> linkHole n
    Underscore range n -> linkRange range $ maybe "_" text n
    -- '_range' is almost always 'NoRange' :(
    App _range _ _ ->
      case appView expr of
        AppView e1 args -> fsep $ render e1 : fmap render args
    RawApp _ es -> fsep $ fmap render (List2.toList es)
    OpApp _ q _ es -> fsep $ renderOpApp q es
    WithApp _ e es -> fsep $ render e : fmap ((text' ["delimiter"] "|" <+>) . render) es
    HiddenArg _ e -> braces' $ render e
    InstanceArg _ e -> dbraces $ render e
    Lam _ bs (AbsurdLam _ h) -> lambda <+> fsep (fmap render (toList bs)) <+> absurd h
    Lam _ bs e -> sep [lambda <+> fsep (fmap render (toList bs)) <+> arrow, render e]
    AbsurdLam _ h -> lambda <+> absurd h
    ExtendedLam range _ pes -> lambda <+> bracesAndSemicolons (fmap render (toList pes))
    Fun _ e1 e2 ->
      sep
        [ renderCohesion e1 (renderQuantity e1 (render e1)) <+> arrow,
          render e2
        ]
    Pi tel e ->
      sep
        [ render (Tel $ smashTel (toList tel)) <+> arrow,
          render e
        ]
    Let _ ds me ->
      sep
        [ "let" <+> vcat (fmap render (toList ds)),
          maybe mempty (\e -> "in" <+> render e) me
        ]
    Paren _ e -> parens $ render e
    IdiomBrackets _ exprs ->
      case exprs of
        [] -> emptyIdiomBrkt
        [e] -> leftIdiomBrkt <+> render e <+> rightIdiomBrkt
        e : es -> leftIdiomBrkt <+> render e <+> fsep (fmap (("|" <+>) . render) es) <+> rightIdiomBrkt
    DoBlock _ ss -> "do" <+> vcat (fmap render (toList ss))
    As _ x e -> render x <> "@" <> render e
    Dot _ e -> "." <> render e
    DoubleDot _ e -> ".." <> render e
    Absurd _ -> "()"
    Rec _ xs -> sep ["record", bracesAndSemicolons (fmap render xs)]
    RecUpdate _ e xs ->
      sep ["record" <+> render e, bracesAndSemicolons (fmap render xs)]
    ETel [] -> "()"
    ETel tel -> fsep $ fmap render tel
    Quote _ -> "quote"
    QuoteTerm _ -> "quoteTerm"
    Unquote _ -> "unquote"
    Tactic _ t -> "tactic" <+> render t
    -- Andreas, 2011-10-03 print irrelevant things as .(e)
    DontCare e -> "." <> parens (render e)
    Equal _ a b -> render a <+> "=" <+> render b
    Ellipsis _ -> "..."
    Generalized e -> render e
    where
      absurd NotHidden = "()"
      absurd Instance {} = "{{}}"
      absurd Hidden = "{}"

-- instance RenderTCM Expr where
--   renderTCM = render

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

instance (Render a, Render b) => Render (Either a b) where
  render = either render render

instance Render a => Render (FieldAssignment' a) where
  render (FieldAssignment x e) = sep [render x <+> "=", render e]

instance Render ModuleAssignment where
  render (ModuleAssignment m es i) = fsep (render m : fmap render es) <+> render i

instance Render LamClause where
  render (LamClause lhs rhs _) =
    sep
      [ render lhs,
        render' rhs
      ]
    where
      render' (RHS e) = arrow <+> render e
      render' AbsurdRHS = mempty

instance Render BoundName where
  render BName {boundName = x} = render x

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

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

-- | NamedBinding
instance Render NamedBinding where
  render (NamedBinding withH x) =
    prH $
      if
          | Just l <- isLabeled x -> text l <> " = " <> render xb
          | otherwise -> render xb
    where
      xb = namedArg x
      bn = binderName xb
      prH
        | withH =
          renderRelevance x
            . renderHiding x mparens'
            . renderCohesion x
            . renderQuantity x
            . renderTactic bn
        | otherwise = id
      -- Parentheses are needed when an attribute @... is present
      mparens'
        | noUserQuantity x, Nothing <- bnameTactic bn = id
        | otherwise = parens

renderTactic :: BoundName -> Inlines -> Inlines
renderTactic = renderTactic' . bnameTactic

renderTactic' :: TacticAttribute -> Inlines -> Inlines
renderTactic' Nothing d = d
renderTactic' (Just t) d = "@" <> (parens ("tactic " <> render t) <+> d)

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

-- | LamBinding
instance Render LamBinding where
  render (DomainFree x) = render (NamedBinding True x)
  render (DomainFull b) = render b

-- | TypedBinding
instance Render TypedBinding where
  render (TLet _ ds) = parens $ "let" <+> vcat (fmap render (toList ds))
  render (TBind _ xs (Underscore _ Nothing)) =
    fsep (fmap (render . NamedBinding True) (toList xs))
  render (TBind _ binders e) =
    fsep
      [ renderRelevance y $
          renderHiding y parens $
            renderCohesion y $
              renderQuantity y $
                renderTactic (binderName $ namedArg y) $
                  sep
                    [ fsep (fmap (render . NamedBinding False) ys),
                      ":" <+> render e
                    ]
        | ys@(y : _) <- groupBinds (toList binders)
      ]
    where
      groupBinds [] = []
      groupBinds (x : xs)
        | Just {} <- isLabeled x = [x] : groupBinds xs
        | otherwise = (x : ys) : groupBinds zs
        where
          (ys, zs) = span (same x) xs
          same a b = getArgInfo a == getArgInfo b && isNothing (isLabeled b)

instance Render Tel where
  render (Tel tel)
    | any isMeta tel = forallQ <+> fsep (fmap render tel)
    | otherwise = fsep (fmap render tel)
    where
      isMeta (TBind _ _ (Underscore _ Nothing)) = True
      isMeta _ = False

smashTel :: Telescope -> Telescope
smashTel
  ( TBind r xs e
      : TBind _ ys e'
      : tel
    )
    | show e == show e' = smashTel (TBind r (fromList (toList xs ++ toList ys)) e : tel)
smashTel (b : tel) = b : smashTel tel
smashTel [] = []

instance Render RHS where
  render (RHS e) = "=" <+> render e
  render AbsurdRHS = mempty

instance Render WhereClause where
  render NoWhere = mempty
  render (AnyWhere _range [Module _ x [] ds])
    | isNoName (unqualify x) =
      vcat ["where", vcat $ fmap render ds]
  render (AnyWhere _range ds) = vcat ["where", vcat $ fmap render ds]
  render (SomeWhere _range m a ds) =
    vcat
      [ hsep $
          applyWhen
            (a == PrivateAccess UserWritten)
            ("private" :)
            ["module", render m, "where"],
        vcat $ fmap render ds
      ]

instance Render LHS where
  render (LHS p eqs es) =
    sep
      [ render p,
        if null eqs then mempty else fsep $ fmap render eqs,
        prefixedThings "with" (fmap renderWithd es)
      ]
    where
      renderWithd :: WithExpr -> Inlines
      renderWithd (Named nm wh) =
        let e = render wh in
        case nm of
          Nothing -> e
          Just n  -> render n <+> ":" <+> e

instance Render LHSCore where
  render (LHSHead f ps) = sep $ render f : fmap (parens . render) ps
  render (LHSProj d ps lhscore ps') =
    sep $
      render d :
      fmap (parens . render) ps
        ++ parens (render lhscore) :
      fmap (parens . render) ps'
  render (LHSWith h wps ps) =
    if null ps
      then doc
      else sep $ parens doc : fmap (parens . render) ps
    where
      doc = sep $ render h : fmap (("|" <+>) . render) wps
  render (LHSEllipsis r p) = "..."

instance Render ModuleApplication where
  render (SectionApp _ bs e) = fsep (fmap render bs) <+> "=" <+> render e
  render (RecordModuleInstance _ rec) = "=" <+> render rec <+> "{{...}}"

instance Render DoStmt where
  render (DoBind _ p e cs) =
    fsep [render p <+> "←", render e, prCs cs]
    where
      prCs [] = mempty
      prCs cs' = fsep ["where", vcat (fmap render cs')]
  render (DoThen e) = render e
  render (DoLet _ ds) = "let" <+> vcat (fmap render $ toList ds)

instance Render Declaration where
  render d =
    case d of
      TypeSig i tac x e ->
        sep
          [ renderTactic' tac $ renderRelevance i $ renderCohesion i $ renderQuantity i $ render x <+> ":",
            render e
          ]
      FieldSig inst tac x (Arg i e) ->
        mkInst inst $
          mkOverlap i $
            renderRelevance i $
              renderHiding i id $
                renderCohesion i $
                  renderQuantity i $
                    render $ TypeSig (setRelevance Relevant i) tac x e
        where
          mkInst (InstanceDef _) f = sep ["instance", f]
          mkInst NotInstanceDef f = f

          mkOverlap j f
            | isOverlappable j = "overlap" <+> f
            | otherwise = f
      Field _ fs ->
        sep
          [ "field",
            vcat (fmap render fs)
          ]
      FunClause lhs rhs wh _ ->
        sep
          [ render lhs,
            render rhs,
            render wh
          ]
      DataSig _ x tel e ->
        fsep
          [ hsep
              [ "data",
                render x,
                fcat (fmap render tel)
              ],
            hsep
              [ ":",
                render e
              ]
          ]
      Data _ x tel e cs ->
        fsep
          [ hsep
              [ "data",
                render x,
                fcat (fmap render tel)
              ],
            hsep
              [ ":",
                render e,
                "where"
              ],
            vcat $ fmap render cs
          ]
      DataDef _ x tel cs ->
        sep
          [ hsep
              [ "data",
                render x,
                fcat (fmap render tel)
              ],
            "where",
            vcat $ fmap render cs
          ]
      RecordSig _ x tel e ->
        sep
          [ hsep
              [ "record",
                render x,
                fcat (fmap render tel)
              ],
            hsep
              [ ":",
                render e
              ]
          ]
      Record _ x dir tel e cs ->
        pRecord x dir tel (Just e) cs
      RecordDef _ x dir tel cs ->
        pRecord x dir tel Nothing cs
      RecordDirective r -> pRecordDirective r
      Infix f xs -> render f <+> fsep (punctuate "," $ fmap render (toList xs))
      Syntax n _ -> "syntax" <+> render n <+> "..."
      PatternSyn _ n as p ->
        "pattern" <+> render n <+> fsep (fmap render as)
          <+> "="
          <+> render p
      Mutual _ ds -> namedBlock "mutual" ds
      InterleavedMutual _ ds  -> namedBlock "interleaved mutual" ds
      LoneConstructor _ ds -> namedBlock "constructor" ds
      Abstract _ ds -> namedBlock "abstract" ds
      Private _ _ ds -> namedBlock "private" ds
      InstanceB _ ds -> namedBlock "instance" ds
      Macro _ ds -> namedBlock "macro" ds
      Postulate _ ds -> namedBlock "postulate" ds
      Primitive _ ds -> namedBlock "primitive" ds
      Generalize _ ds -> namedBlock "variable" ds
      Module _ x tel ds ->
        fsep
          [ hsep
              [ "module",
                render x,
                fcat (fmap render tel),
                "where"
              ],
            vcat $ fmap render ds
          ]
      ModuleMacro _ x (SectionApp _ [] e) DoOpen i
        | isNoName x ->
          fsep
            [ render DoOpen,
              render e,
              render i
            ]
      ModuleMacro _ x (SectionApp _ tel e) open i ->
        fsep
          [ render open <+> "module" <+> render x <+> fcat (fmap render tel),
            "=" <+> render e <+> render i
          ]
      ModuleMacro _ x (RecordModuleInstance _ rec) open _ ->
        fsep
          [ render open <+> "module" <+> render x,
            "=" <+> render rec <+> "{{...}}"
          ]
      Open _ x i -> hsep ["open", render x, render i]
      Import _ x rn open i ->
        hsep [render open, "import", render x, as rn, render i]
        where
          as Nothing = mempty
          as (Just y) = "as" <+> render (asName y)
      UnquoteDecl _ xs t ->
        fsep ["unquoteDecl" <+> fsep (fmap render xs) <+> "=", render t]
      UnquoteDef _ xs t ->
        fsep ["unquoteDef" <+> fsep (fmap render xs) <+> "=", render t]
      Pragma pr -> sep ["{-#" <+> render pr, "#-}"]
    where
      namedBlock s ds =
        fsep
          [ text s,
            vcat $ fmap render ds
          ]

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

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


pRecord ::
  Name ->
  RecordDirectives ->
  [LamBinding] ->
  Maybe Expr ->
  [Declaration] ->
  Inlines
pRecord x (RecordDirectives ind eta pat con) tel me cs =
  sep
    [ hsep
        [ "record",
          render x,
          fcat (fmap render tel)
        ],
      pType me,
      vcat $
        pInd
          ++ pEta
          ++ pCon
          ++ fmap render cs
    ]
  where
    pType (Just e) =
      hsep
        [ ":",
          render e,
          "where"
        ]
    pType Nothing =
      "where"
    pInd = maybeToList $ text . show . rangedThing <$> ind
    pEta =
      maybeToList $
        eta <&> \case
          YesEta -> "eta-equality"
          NoEta _ -> "no-eta-equality"
    pCon = maybeToList $ (("constructor" <+>) . render) . fst <$> con

instance Render OpenShortHand where
  render DoOpen = "open"
  render DontOpen = mempty

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

instance Render Fixity where
  render (Fixity _ Unrelated _) = __IMPOSSIBLE__
  render (Fixity _ (Related d) ass) = s <+> text (toStringWithoutDotZero d)
    where
      s = case ass of
        LeftAssoc -> "infixl"
        RightAssoc -> "infixr"
        NonAssoc -> "infix"

instance Render GenPart where
  render (IdPart x) = text $ rangedThing x
  render BindHole {} = "_"
  render NormalHole {} = "_"
  render WildHole {} = "_"

instance Render Fixity' where
  render (Fixity' fix nota _)
    | nota == noNotation = render fix
    | otherwise = "syntax" <+> render nota

-- | Arg
instance Render a => Render (Arg a) where
  renderPrec p (Arg ai e) = renderHiding ai localParens $ renderPrec p' e
    where
      p'
        | visible ai = p
        | otherwise = 0
      localParens
        | getOrigin ai == Substitution = parens
        | otherwise = id

-- | Named NamedName (Named_)
instance Render e => Render (Named NamedName e) where
  renderPrec p (Named nm e)
    | Just s <- bareNameOf nm = mparens (p > 0) $ sep [text s <> " =", render e]
    | otherwise = renderPrec p e

instance Render Pattern where
  render = \case
    IdentP x -> render x
    AppP p1 p2 -> fsep [render p1, render p2]
    RawAppP _ ps -> fsep $ fmap render (List2.toList ps)
    OpAppP _ q _ ps -> fsep $ renderOpApp q (fmap (fmap (fmap (NoPlaceholder Strict.Nothing))) ps)
    HiddenP _ p -> braces' $ render p
    InstanceP _ p -> dbraces $ render p
    ParenP _ p -> parens $ render p
    WildP _ -> "_"
    AsP _ x p -> render x <> "@" <> render p
    DotP _ p -> "." <> render p
    AbsurdP _ -> "()"
    LitP _ l -> render l
    QuoteP _ -> "quote"
    RecP _ fs -> sep ["record", bracesAndSemicolons (fmap render fs)]
    EqualP _ es -> sep $ [parens (sep [render e1, "=", render e2]) | (e1, e2) <- es]
    EllipsisP _ mp -> "..."
    WithP _ p -> "|" <+> render p

bracesAndSemicolons :: [Inlines] -> Inlines
bracesAndSemicolons [] = "{}"
bracesAndSemicolons (d : ds) = sep (["{" <+> d] ++ fmap (";" <+>) ds ++ ["}"])

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

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

    prOp _ [] es = fmap (\e -> (render e, Nothing)) es

    qual ms' doc = hcat $ punctuate "." $ fmap render ms' ++ [doc]

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

    mergeRight before d after =
      reverse before
        ++ case merge [] after of
          [] -> [d]
          a : as -> (d <> a) : as

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

instance (Render a, Render b) => Render (ImportDirective' a b) where
  render i =
    sep
      [ public (publicOpen i),
        render $ using i,
        renderHiding' $ hiding i,
        rename $ impRenaming i
      ]
    where
      public Just {} = "public"
      public Nothing = mempty

      renderHiding' [] = mempty
      renderHiding' xs = "hiding" <+> parens (fsep $ punctuate ";" $ fmap render xs)

      rename [] = mempty
      rename xs =
        hsep
          [ "renaming",
            parens $ fsep $ punctuate ";" $ fmap render xs
          ]

instance (Render a, Render b) => Render (Using' a b) where
  render UseEverything = mempty
  render (Using xs) =
    "using" <+> parens (fsep $ punctuate ";" $ fmap render xs)

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

instance (Render a, Render b) => Render (ImportedName' a b) where
  render (ImportedName a) = render a
  render (ImportedModule b) = "module" <+> render b