{-# 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"
    }