content: {-# LANGUAGE CPP #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleInstances #-}
  
  module Render.RichText
    ( Block (..),
      Inlines (..),
      -- LinkTarget (..),
      space,
      text,
      text',
      parens,
      -- link,
      linkRange,
      linkHole,
      icon,
      -- combinators
      (<+>),
      (<?>),
      punctuate,
      braces,
      braces',
      dbraces,
      mparens,
      textNonEmpty,
      hcat,
      hsep,
      sep,
      fsep,
      vcat,
      fcat,
      -- symbols
      arrow,
      lambda,
      forallQ,
      showIndex,
      leftIdiomBrkt,
      rightIdiomBrkt,
      emptyIdiomBrkt,
    )
  where
  
  -- import qualified Agda.Interaction.Options   as Agda
  -- import qualified Agda.Syntax.Concrete.Glyph as Agda
  import qualified Agda.Syntax.Position as Agda
  import qualified Agda.Utils.FileName as Agda
  import Agda.Utils.List (caseList, last1)
  import Agda.Utils.Null
  import qualified Agda.Utils.Null as Agda
  import Agda.Utils.Suffix (toSubscriptDigit)
  import Data.Aeson (ToJSON (toJSON), Value (Null))
  import Data.Foldable (toList)
  import Data.Sequence (Seq (..))
  import qualified Data.Sequence as Seq
  import qualified Data.Strict.Maybe as Strict
  import Data.String (IsString (..))
  import GHC.Generics (Generic)
  import Prelude hiding (null)
  
  --------------------------------------------------------------------------------
  
  -- | Block elements
  data Block
    = -- for blocks like "Goal" & "Have"
      Labeled Inlines (Maybe String) (Maybe Agda.Range) String String
    | -- for ordinary goals & context
      Unlabeled Inlines (Maybe String) (Maybe Agda.Range)
    | -- headers
      Header String
    deriving (Generic)
  
  instance ToJSON Block
  
  --------------------------------------------------------------------------------
  
  newtype Inlines = Inlines {unInlines :: Seq Inline}
  
  -- Represent Inlines with String literals
  instance IsString Inlines where
    fromString s = Inlines (Seq.singleton (Text s mempty))
  
  instance Semigroup Inlines where
    Inlines as <> Inlines bs = Inlines (merge as bs)
      where
        merge :: Seq Inline -> Seq Inline -> Seq Inline
        merge Empty ys = ys
        merge (xs :|> x) ys = merge xs (cons x ys)
  
        cons :: Inline -> Seq Inline -> Seq Inline
        cons (Text s c) (Text t d :<| xs)
          -- merge 2 adjacent Text if they have the same classnames
          | c == d = Text (s <> t) c :<| xs
          | otherwise = Text s c :<| Text t d :<| xs
        cons (Text s c) (Horz [] :<| xs) = cons (Text s c) xs
        cons (Text s c) (Horz (Inlines t : ts) :<| xs) =
          -- merge Text with Horz when possible
          Horz (Inlines (cons (Text s c) t) : ts) :<| xs
        cons x xs = x :<| xs
  
  instance Monoid Inlines where
    mempty = Inlines mempty
  
  instance ToJSON Inlines where
    toJSON (Inlines xs) = toJSON xs
  
  instance Show Inlines where
    show (Inlines xs) = unwords $ map show $ toList xs
  
  instance Null Inlines where
    empty = mempty
    null (Inlines elems) = all elemIsNull (Seq.viewl elems)
      where
        elemIsNull :: Inline -> Bool
        elemIsNull (Icon _ _) = False
        elemIsNull (Text "" _) = True
        elemIsNull (Text _ _) = False
        elemIsNull (Link _ xs _) = all elemIsNull $ unInlines xs
        elemIsNull (Hole _) = False
        elemIsNull (Horz xs) = all null xs
        elemIsNull (Vert xs) = all null xs
        elemIsNull (Parn _) = False
        elemIsNull (PrHz _) = False
  
  -- -- | see if the rendered text is "empty"
  
  infixr 6 <+>
  
  (<+>) :: Inlines -> Inlines -> Inlines
  x <+> y
    | null x = y
    | null y = x
    | otherwise = x <> " " <> y
  
  infixl 6 <?>
  
  -- | A synonym for '<+>' at the moment
  (<?>) :: Inlines -> Inlines -> Inlines
  (<?>) = (<+>)
  
  -- | Whitespace
  space :: Inlines
  space = " "
  
  text :: String -> Inlines
  text s = Inlines $ Seq.singleton $ Text s mempty
  
  text' :: ClassNames -> String -> Inlines
  text' cs s = Inlines $ Seq.singleton $ Text s cs
  
  -- When there's only 1 Horz inside a Parn, convert it to PrHz
  parens :: Inlines -> Inlines
  parens (Inlines (Horz xs :<| Empty)) = Inlines $ Seq.singleton $ PrHz xs
  parens others = Inlines $ Seq.singleton $ Parn others
  
  icon :: String -> Inlines
  icon s = Inlines $ Seq.singleton $ Icon s []
  
  linkRange :: Agda.Range -> Inlines -> Inlines
  linkRange range xs = Inlines $ Seq.singleton $ Link range xs mempty
  
  linkHole :: Int -> Inlines
  linkHole i = Inlines $ Seq.singleton $ Hole i
  
  --------------------------------------------------------------------------------
  
  type ClassNames = [String]
  
  --------------------------------------------------------------------------------
  
  -- | Internal type, to be converted to JSON values
  data Inline
    = Icon String ClassNames
    | Text String ClassNames
    | Link Agda.Range Inlines ClassNames
    | Hole Int
    | -- | Horizontal grouping, wrap when there's no space
      Horz [Inlines]
    | -- | Vertical grouping, each children would end with a newline
      Vert [Inlines]
    | -- | Parenthese
      Parn Inlines
    | -- | Parenthese around a Horizontal, special case
      PrHz [Inlines]
    deriving (Generic)
  
  instance ToJSON Inline
  
  instance Show Inline where
    show (Icon s _) = s
    show (Text s _) = s
    show (Link _ xs _) = mconcat (map show $ toList $ unInlines xs)
    show (Hole i) = "?" ++ show i
    show (Horz xs) = unwords (map show $ toList xs)
    show (Vert xs) = unlines (map show $ toList xs)
    show (Parn x) = "(" <> show x <> ")"
    show (PrHz xs) = "(" <> unwords (map show $ toList xs) <> ")"
  
  --------------------------------------------------------------------------------
  
  -- | ToJSON instances for A.types
  instance {-# OVERLAPS #-} ToJSON Agda.Range
  
  instance ToJSON (Agda.Interval' ()) where
  #if MIN_VERSION_Agda(2,8,0)
    toJSON (Agda.Interval () start end) = toJSON (start, end)
  #else
    toJSON (Agda.Interval start end) = toJSON (start, end)
  #endif
  
  instance ToJSON (Agda.Position' ()) where
    toJSON (Agda.Pn () pos line col) = toJSON [line, col, pos]
  
  instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where
    toJSON Strict.Nothing = Null
    toJSON (Strict.Just path) = toJSON path
  
  instance ToJSON Agda.AbsolutePath where
    toJSON (Agda.AbsolutePath path) = toJSON path
  
  instance ToJSON Agda.RangeFile where
    toJSON (Agda.RangeFile path _maybeTopLevelModuleName) = toJSON path
  
  --------------------------------------------------------------------------------
  
  -- | Utilities / Combinators
  
  -- TODO: implement this
  -- Modeled after `nest` defined in ‘Text.PrettyPrint.Annotated.HughesPJ’ (pretty-1.1.3.6)
  --
  -- Indent a Inline by a given number of positions (which may also be negative). `indent` satisfies the laws:
  --
  -- `indent`  0 x = x
  -- `indent`  k ( `indent`  k' x) =  `indent`  (k+k') x
  -- `indent`  k (x  `<>`  y)      =  `indent`  k z  `<>`   `indent`  k y
  -- `indent`  k (x  `$$`  y)      =  `indent`  k x  `$$`   `indent`  k y
  -- `indent`  k  `empty`          =  `empty`
  -- `x <> indent k y = x <> y` , if x non-empty
  -- indent :: Int -> Inlines -> Inlines
  -- indent 0 x = x
  
  punctuate :: Inlines -> [Inlines] -> [Inlines]
  punctuate _ [] = []
  punctuate delim xs = zipWith (<>) xs (replicate (length xs - 1) delim ++ [mempty])
  
  --------------------------------------------------------------------------------
  
  -- | Just pure concatenation, no grouping or whatsoever
  hcat :: [Inlines] -> Inlines
  hcat = mconcat
  
  hsep :: [Inlines] -> Inlines
  hsep [] = mempty
  hsep [x] = x
  hsep (x : xs) = x <+> hsep xs
  
  --------------------------------------------------------------------------------
  
  -- | Vertical listing
  vcat :: [Inlines] -> Inlines
  vcat = Inlines . pure . Vert
  
  -- | Horizontal listing
  sep :: [Inlines] -> Inlines
  sep = Inlines . pure . Horz
  
  fsep :: [Inlines] -> Inlines
  fsep = sep
  
  fcat :: [Inlines] -> Inlines
  fcat = sep
  
  --------------------------------------------------------------------------------
  
  -- | Single braces
  braces :: Inlines -> Inlines
  braces x = "{" <> x <> "}"
  
  -- | Double braces
  dbraces :: Inlines -> Inlines
  dbraces = _dbraces specialCharacters
  
  arrow :: Inlines
  arrow = _arrow specialCharacters
  
  lambda :: Inlines
  lambda = _lambda specialCharacters
  
  forallQ :: Inlines
  forallQ = _forallQ specialCharacters
  
  -- left, right, and empty idiom bracket
  leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Inlines
  leftIdiomBrkt = _leftIdiomBrkt specialCharacters
  rightIdiomBrkt = _rightIdiomBrkt specialCharacters
  emptyIdiomBrkt = _emptyIdiomBrkt specialCharacters
  
  -- | Apply 'parens' to 'Inlines' if boolean is true.
  mparens :: Bool -> Inlines -> Inlines
  mparens True = parens
  mparens False = id
  
  -- | Return 'empty' for empty strings.
  textNonEmpty :: String -> Inlines
  textNonEmpty = \case
    "" -> empty
    s  -> text s
  
  -- | From braces'. v2.7.0.1
  braces' :: Inlines -> Inlines
  braces' d = caseList (show d) (braces d {-else-}) $ \c cs -> braces (spaceIfDash c <> d <> spaceIfDash (last1 c cs))
    where
      -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
      -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
      spaceIfDash '-' = " "
      spaceIfDash _ = mempty
  
  -- | Shows a non-negative integer using the characters ₀-₉ instead of
  -- 0-9 unless the user explicitly asked us to not use any unicode characters.
  showIndex :: (Show i, Integral i) => i -> String
  showIndex = map toSubscriptDigit . show
  
  --------------------------------------------------------------------------------
  --
  
  -- | Picking the appropriate set of special characters depending on
  -- whether we are allowed to use unicode or have to limit ourselves
  -- to ascii.
  data SpecialCharacters = SpecialCharacters
    { _dbraces :: Inlines -> Inlines,
      _lambda :: Inlines,
      _arrow :: Inlines,
      _forallQ :: Inlines,
      _leftIdiomBrkt :: Inlines,
      _rightIdiomBrkt :: Inlines,
      _emptyIdiomBrkt :: Inlines
    }
  
  {-# NOINLINE specialCharacters #-}
  specialCharacters :: SpecialCharacters
  specialCharacters =
    SpecialCharacters
      { _dbraces = ("\x2983 " <>) . (<> " \x2984"),
        _lambda = "\x03bb",
        _arrow = "\x2192",
        _forallQ = "\x2200",
        _leftIdiomBrkt = "\x2987",
        _rightIdiomBrkt = "\x2988",
        _emptyIdiomBrkt = "\x2987\x2988"
      }
  