{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}

module Render.Internal where

import Agda.Syntax.Common (Hiding (..), LensHiding (getHiding), Named (namedThing))
import Agda.Syntax.Internal hiding (telToList)
import qualified Data.List as List
import Render.Class
import Render.Common (renderHiding)
import Render.Concrete ()
import Render.RichText

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

instance Render a => Render (Substitution' a) where
  renderPrec = pr
    where
      pr p input = case input of
        IdS -> "idS"
        EmptyS _ -> "emptyS"
        t :# rho -> mparens (p > 2) $ sep [pr 2 rho <> ",", renderPrec 3 t]
        Strengthen _ rho -> mparens (p > 9) $ "strS" <+> pr 10 rho
        Wk n rho -> mparens (p > 9) $ text ("wkS " ++ show n) <+> pr 10 rho
        Lift n rho -> mparens (p > 9) $ text ("liftS " ++ show n) <+> pr 10 rho

-- | Term
instance Render Term where
  renderPrec p val =
    case val of
      Var x els -> text ("@" ++ show x) `pApp` els
      Lam ai b ->
        mparens (p > 0) $
          fsep
            [ "λ" <+> renderHiding ai id (text . absName $ b) <+> "->",
              render (unAbs b)
            ]
      Lit l -> render l
      Def q els -> render q `pApp` els
      Con c _ vs -> render (conName c) `pApp` vs
      Pi a (NoAbs _ b) ->
        mparens (p > 0) $
          fsep
            [ renderPrec 1 (unDom a) <+> "->",
              render b
            ]
      Pi a b ->
        mparens (p > 0) $
          fsep
            [ renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a)) <+> "->",
              render (unAbs b)
            ]
      Sort s -> renderPrec p s
      Level l -> renderPrec p l
      MetaV x els -> render x `pApp` els
      DontCare v -> renderPrec p v
      Dummy s es -> parens (text s) `pApp` es
    where
      pApp d els =
        mparens (not (null els) && p > 9) $
          fsep [d, fsep (map (renderPrec 10) els)]

instance (Render t, Render e) => Render (Dom' t e) where
  render dom = pTac <+> renderDom dom (render $ unDom dom)
    where
      pTac
        | Just t <- domTactic dom = "@" <> parens ("tactic" <+> render t)
        | otherwise = mempty

renderDom :: LensHiding a => a -> Inlines -> Inlines
renderDom i =
  case getHiding i of
    NotHidden -> parens
    Hidden -> braces
    Instance {} -> braces . braces

instance Render Clause where
  render Clause {clauseTel = tel, namedClausePats = ps, clauseBody = body, clauseType = ty} =
    sep
      [ render tel <+> "|-",
        fsep
          [ fsep (map (renderPrec 10) ps) <+> "=",
            pBody body ty
          ]
      ]
    where
      pBody Nothing _ = "(absurd)"
      pBody (Just b) Nothing = render b
      pBody (Just b) (Just t) = fsep [render b <+> ":", render t]

instance Render a => Render (Tele (Dom a)) where
  render tel = fsep [renderDom a (text x <+> ":" <+> render (unDom a)) | (x, a) <- telToList tel]
    where
      telToList EmptyTel = []
      telToList (ExtendTel a tel') = (absName tel', a) : telToList (unAbs tel')

renderPrecLevelSucs :: Int -> Integer -> (Int -> Inlines) -> Inlines
renderPrecLevelSucs p 0 d = d p
renderPrecLevelSucs p n d = mparens (p > 9) $ "lsuc" <+> renderPrecLevelSucs 10 (n - 1) d

instance Render Level where
  renderPrec p (Max n as) =
    case as of
      [] -> renderN
      [a] | n == 0 -> renderPrec p a
      _ ->
        mparens (p > 9) $
          List.foldr1 (\a b -> "lub" <+> a <+> b) $
            [renderN | n > 0] ++ map (renderPrec 10) as
    where
      renderN = renderPrecLevelSucs p n (const "lzero")

instance Render PlusLevel where
  renderPrec p (Plus n a) = renderPrecLevelSucs p n $ \p' -> renderPrec p' a

instance Render LevelAtom where
  renderPrec p a =
    case a of
      MetaLevel x els -> renderPrec p (MetaV x els)
      BlockedLevel _ v -> renderPrec p v
      NeutralLevel _ v -> renderPrec p v
      UnreducedLevel v -> renderPrec p v

instance Render Sort where
  renderPrec p srt =
    case srt of
      Type (ClosedLevel 0) -> "Set"
      Type (ClosedLevel n) -> text $ "Set" ++ show n
      Type l -> mparens (p > 9) $ "Set" <+> renderPrec 10 l
      Prop (ClosedLevel 0) -> "Prop"
      Prop (ClosedLevel n) -> text $ "Prop" ++ show n
      Prop l -> mparens (p > 9) $ "Prop" <+> renderPrec 10 l
      Inf -> "Setω"
      SizeUniv -> "SizeUniv"
      PiSort a b ->
        mparens (p > 9) $
          "piSort" <+> renderDom (domInfo a) (text (absName b) <+> ":" <+> render (unDom a))
            <+> parens
              ( fsep
                  [ text ("λ " ++ absName b ++ " ->"),
                    render (unAbs b)
                  ]
              )
      FunSort a b ->
        mparens (p > 9) $
          "funSort" <+> renderPrec 10 a <+> renderPrec 10 b
      UnivSort s -> mparens (p > 9) $ "univSort" <+> renderPrec 10 s
      MetaS x es -> renderPrec p $ MetaV x es
      DefS d es -> renderPrec p $ Def d es
      DummyS s -> parens $ text s

instance Render Type where
  renderPrec p (El _ a) = renderPrec p a

instance Render tm => Render (Elim' tm) where
  renderPrec p (Apply v) = renderPrec p v
  renderPrec _ (Proj _o x) = "." <> render x
  renderPrec p (IApply _ _ r) = renderPrec p r

instance Render DBPatVar where
  renderPrec _ x = text $ patVarNameToString (dbPatVarName x) ++ "@" ++ show (dbPatVarIndex x)

instance Render a => Render (Pattern' a) where
  renderPrec n (VarP _o x) = renderPrec n x
  renderPrec _ (DotP _o t) = "." <> renderPrec 10 t
  renderPrec n (ConP c i nps) =
    mparens (n > 0 && not (null nps)) $
      (lazy <> render (conName c)) <+> fsep (map (renderPrec 10) ps)
    where
      ps = map (fmap namedThing) nps
      lazy
        | conPLazy i = "~"
        | otherwise = mempty
  renderPrec n (DefP _ q nps) =
    mparens (n > 0 && not (null nps)) $
      render q <+> fsep (map (renderPrec 10) ps)
    where
      ps = map (fmap namedThing) nps
  -- -- Version with printing record type:
  -- renderPrec _ (ConP c i ps) = (if b then braces else parens) $ prTy $
  --   text (show $ conName c) <+> fsep (map (render . namedArg) ps)
  --   where
  --     b = maybe False (== ConOSystem) $ conPRecord i
  --     prTy d = caseMaybe (conPType i) d $ \ t -> d  <+> ":" <+> render t
  renderPrec _ (LitP _ l) = render l
  renderPrec _ (ProjP _o q) = "." <> render q
  renderPrec n (IApplyP _o _ _ x) = renderPrec n x