{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}

module Render.RichText
  ( Block(..),
    Inlines (..),
    -- LinkTarget (..),
    space,
    text,
    text',
    parens,
    -- link,
    linkRange,
    linkHole,
    icon,
    -- combinators
    (<+>),
    punctuate,
    braces,
    braces',
    dbraces,
    mparens,
    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 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           Data.String (IsString (..))
import qualified Data.Strict.Maybe as Strict

import           GHC.Generics (Generic)

--------------------------------------------------------------------------------
-- | 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 (forall x. Rep Block x -> Block
forall x. Block -> Rep Block x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Block x -> Block
$cfrom :: forall x. Block -> Rep Block x
Generic)

instance ToJSON Block

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

newtype Inlines = Inlines {Inlines -> Seq Inline
unInlines :: Seq Inline}

-- Represent Inlines with String literals
instance IsString Inlines where
  fromString :: String -> Inlines
fromString String
s = Seq Inline -> Inlines
Inlines (forall a. a -> Seq a
Seq.singleton (String -> ClassNames -> Inline
Text String
s forall a. Monoid a => a
mempty))

instance Semigroup Inlines where
  Inlines Seq Inline
as <> :: Inlines -> Inlines -> Inlines
<> Inlines Seq Inline
bs = Seq Inline -> Inlines
Inlines (Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
as Seq Inline
bs)
    where
      merge :: Seq Inline -> Seq Inline -> Seq Inline
      merge :: Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
Empty      Seq Inline
ys = Seq Inline
ys
      merge (Seq Inline
xs :|> Inline
x) Seq Inline
ys = Seq Inline -> Seq Inline -> Seq Inline
merge Seq Inline
xs (Inline -> Seq Inline -> Seq Inline
cons Inline
x Seq Inline
ys)

      cons :: Inline -> Seq Inline -> Seq Inline
      cons :: Inline -> Seq Inline -> Seq Inline
cons (Text String
s ClassNames
c) (Text String
t ClassNames
d :<| Seq Inline
xs)
        -- merge 2 adjacent Text if they have the same classnames
        | ClassNames
c forall a. Eq a => a -> a -> Bool
== ClassNames
d    = String -> ClassNames -> Inline
Text (String
s forall a. Semigroup a => a -> a -> a
<> String
t) ClassNames
c forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs 
        | Bool
otherwise = String -> ClassNames -> Inline
Text String
s ClassNames
c forall a. a -> Seq a -> Seq a
:<| String -> ClassNames -> Inline
Text String
t ClassNames
d forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs
      cons (Text String
s ClassNames
c) (Horz [] :<| Seq Inline
xs) = Inline -> Seq Inline -> Seq Inline
cons (String -> ClassNames -> Inline
Text String
s ClassNames
c) Seq Inline
xs
      cons (Text String
s ClassNames
c) (Horz (Inlines Seq Inline
t:[Inlines]
ts) :<| Seq Inline
xs)
        -- merge Text with Horz when possible
        = [Inlines] -> Inline
Horz (Seq Inline -> Inlines
Inlines (Inline -> Seq Inline -> Seq Inline
cons (String -> ClassNames -> Inline
Text String
s ClassNames
c) Seq Inline
t) forall a. a -> [a] -> [a]
:[Inlines]
ts) forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs
      cons Inline
x Seq Inline
xs = Inline
x forall a. a -> Seq a -> Seq a
:<| Seq Inline
xs


instance Monoid Inlines where
  mempty :: Inlines
mempty = Seq Inline -> Inlines
Inlines forall a. Monoid a => a
mempty

instance ToJSON Inlines where
  toJSON :: Inlines -> Value
toJSON (Inlines Seq Inline
xs) = forall a. ToJSON a => a -> Value
toJSON Seq Inline
xs

instance Show Inlines where
  show :: Inlines -> String
show (Inlines Seq Inline
xs) = ClassNames -> String
unwords forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Inline
xs

-- | see if the rendered text is "empty"
isEmpty :: Inlines -> Bool
isEmpty :: Inlines -> Bool
isEmpty (Inlines Seq Inline
elems) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inline -> Bool
elemIsEmpty (forall a. Seq a -> ViewL a
Seq.viewl Seq Inline
elems)
  where
    elemIsEmpty :: Inline -> Bool
    elemIsEmpty :: Inline -> Bool
elemIsEmpty (Icon String
_ ClassNames
_) = Bool
False
    elemIsEmpty (Text String
"" ClassNames
_) = Bool
True
    elemIsEmpty (Text String
_ ClassNames
_) = Bool
False
    elemIsEmpty (Link Range
_ Inlines
xs ClassNames
_) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inline -> Bool
elemIsEmpty forall a b. (a -> b) -> a -> b
$ Inlines -> Seq Inline
unInlines Inlines
xs
    elemIsEmpty (Hole Int
_) = Bool
False
    elemIsEmpty (Horz [Inlines]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inlines -> Bool
isEmpty [Inlines]
xs
    elemIsEmpty (Vert [Inlines]
xs) = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Inlines -> Bool
isEmpty [Inlines]
xs
    elemIsEmpty (Parn Inlines
_) = Bool
False
    elemIsEmpty (PrHz [Inlines]
_) = Bool
False

infixr 6 <+> 

(<+>) :: Inlines -> Inlines -> Inlines
Inlines
x <+> :: Inlines -> Inlines -> Inlines
<+> Inlines
y
  | Inlines -> Bool
isEmpty Inlines
x = Inlines
y
  | Inlines -> Bool
isEmpty Inlines
y = Inlines
x
  | Bool
otherwise = Inlines
x forall a. Semigroup a => a -> a -> a
<> Inlines
" " forall a. Semigroup a => a -> a -> a
<> Inlines
y

-- | Whitespace
space :: Inlines
space :: Inlines
space = Inlines
" "

text :: String -> Inlines
text :: String -> Inlines
text String
s = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Text String
s forall a. Monoid a => a
mempty

text' :: ClassNames -> String -> Inlines
text' :: ClassNames -> String -> Inlines
text' ClassNames
cs String
s = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Text String
s ClassNames
cs

-- When there's only 1 Horz inside a Parn, convert it to PrHz
parens :: Inlines -> Inlines
parens :: Inlines -> Inlines
parens (Inlines (Horz [Inlines]
xs :<| Seq Inline
Empty)) = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ [Inlines] -> Inline
PrHz [Inlines]
xs
parens Inlines
others = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ Inlines -> Inline
Parn Inlines
others

icon :: String -> Inlines
icon :: String -> Inlines
icon String
s = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ String -> ClassNames -> Inline
Icon String
s []

linkRange :: Agda.Range -> Inlines -> Inlines
linkRange :: Range -> Inlines -> Inlines
linkRange Range
range Inlines
xs = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ Range -> Inlines -> ClassNames -> Inline
Link Range
range Inlines
xs forall a. Monoid a => a
mempty

linkHole :: Int -> Inlines
linkHole :: Int -> Inlines
linkHole Int
i = Seq Inline -> Inlines
Inlines forall a b. (a -> b) -> a -> b
$ forall a. a -> Seq a
Seq.singleton forall a b. (a -> b) -> a -> b
$ Int -> Inline
Hole Int
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 (forall x. Rep Inline x -> Inline
forall x. Inline -> Rep Inline x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Inline x -> Inline
$cfrom :: forall x. Inline -> Rep Inline x
Generic)

instance ToJSON Inline

instance Show Inline where
  show :: Inline -> String
show (Icon String
s ClassNames
_) = String
s
  show (Text String
s ClassNames
_) = String
s
  show (Link Range
_ Inlines
xs ClassNames
_) = forall a. Monoid a => [a] -> a
mconcat (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Inlines -> Seq Inline
unInlines Inlines
xs)
  show (Hole Int
i) = String
"?" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
i
  show (Horz [Inlines]
xs) = ClassNames -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs)
  show (Vert [Inlines]
xs) = ClassNames -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs)
  show (Parn Inlines
x) = String
"(" forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show Inlines
x forall a. Semigroup a => a -> a -> a
<> String
")" 
  show (PrHz [Inlines]
xs) = String
"(" forall a. Semigroup a => a -> a -> a
<> ClassNames -> String
unwords (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList [Inlines]
xs) forall a. Semigroup a => a -> a -> a
<> String
")" 

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

-- | ToJSON instances for A.types
instance {-# OVERLAPS #-} ToJSON Agda.Range

instance ToJSON (Agda.Interval' ()) where
  toJSON :: Interval' () -> Value
toJSON (Agda.Interval Position' ()
start Position' ()
end) = forall a. ToJSON a => a -> Value
toJSON (Position' ()
start, Position' ()
end)

instance ToJSON (Agda.Position' ()) where
  toJSON :: Position' () -> Value
toJSON (Agda.Pn () Int32
pos Int32
line Int32
col) = forall a. ToJSON a => a -> Value
toJSON [Int32
line, Int32
col, Int32
pos]

instance {-# OVERLAPS #-} ToJSON Agda.SrcFile where
  toJSON :: SrcFile -> Value
toJSON SrcFile
Strict.Nothing = Value
Null
  toJSON (Strict.Just AbsolutePath
path) = forall a. ToJSON a => a -> Value
toJSON AbsolutePath
path

instance ToJSON Agda.AbsolutePath where
  toJSON :: AbsolutePath -> Value
toJSON (Agda.AbsolutePath Text
path) = forall a. ToJSON a => a -> Value
toJSON Text
path

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

-- | Utilities / Combinators

-- -- TODO: implement this
-- indent :: Inlines -> Inlines
-- indent x = "  " <> x

punctuate :: Inlines -> [Inlines] -> [Inlines]
punctuate :: Inlines -> [Inlines] -> [Inlines]
punctuate Inlines
_ [] = []
punctuate Inlines
delim [Inlines]
xs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a. Semigroup a => a -> a -> a
(<>) [Inlines]
xs (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Inlines]
xs forall a. Num a => a -> a -> a
- Int
1) Inlines
delim forall a. [a] -> [a] -> [a]
++ [forall a. Monoid a => a
mempty])

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

-- | Just pure concatenation, no grouping or whatsoever
hcat :: [Inlines] -> Inlines
hcat :: [Inlines] -> Inlines
hcat = forall a. Monoid a => [a] -> a
mconcat

hsep :: [Inlines] -> Inlines
hsep :: [Inlines] -> Inlines
hsep [] = forall a. Monoid a => a
mempty
hsep [Inlines
x] = Inlines
x
hsep (Inlines
x : [Inlines]
xs) = Inlines
x Inlines -> Inlines -> Inlines
<+> [Inlines] -> Inlines
hsep [Inlines]
xs

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

-- | Vertical listing
vcat :: [Inlines] -> Inlines
vcat :: [Inlines] -> Inlines
vcat = Seq Inline -> Inlines
Inlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Inlines] -> Inline
Vert

-- | Horizontal listing
sep :: [Inlines] -> Inlines
sep :: [Inlines] -> Inlines
sep = Seq Inline -> Inlines
Inlines forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Inlines] -> Inline
Horz

fsep :: [Inlines] -> Inlines
fsep :: [Inlines] -> Inlines
fsep = [Inlines] -> Inlines
sep

fcat :: [Inlines] -> Inlines
fcat :: [Inlines] -> Inlines
fcat = [Inlines] -> Inlines
sep

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

-- | Single braces
braces :: Inlines -> Inlines
braces :: Inlines -> Inlines
braces Inlines
x = Inlines
"{" forall a. Semigroup a => a -> a -> a
<> Inlines
x forall a. Semigroup a => a -> a -> a
<> Inlines
"}"

-- | Double braces
dbraces :: Inlines -> Inlines
dbraces :: Inlines -> Inlines
dbraces = SpecialCharacters -> Inlines -> Inlines
_dbraces SpecialCharacters
specialCharacters

arrow :: Inlines
arrow :: Inlines
arrow = SpecialCharacters -> Inlines
_arrow SpecialCharacters
specialCharacters

lambda :: Inlines
lambda :: Inlines
lambda = SpecialCharacters -> Inlines
_lambda SpecialCharacters
specialCharacters

forallQ :: Inlines
forallQ :: Inlines
forallQ = SpecialCharacters -> Inlines
_forallQ SpecialCharacters
specialCharacters

-- left, right, and empty idiom bracket
leftIdiomBrkt, rightIdiomBrkt, emptyIdiomBrkt :: Inlines
leftIdiomBrkt :: Inlines
leftIdiomBrkt = SpecialCharacters -> Inlines
_leftIdiomBrkt SpecialCharacters
specialCharacters
rightIdiomBrkt :: Inlines
rightIdiomBrkt = SpecialCharacters -> Inlines
_rightIdiomBrkt SpecialCharacters
specialCharacters
emptyIdiomBrkt :: Inlines
emptyIdiomBrkt = SpecialCharacters -> Inlines
_emptyIdiomBrkt SpecialCharacters
specialCharacters

-- | Apply 'parens' to 'Doc' if boolean is true.
mparens :: Bool -> Inlines -> Inlines
mparens :: Bool -> Inlines -> Inlines
mparens Bool
True = Inlines -> Inlines
parens
mparens Bool
False = forall a. a -> a
id

-- | From braces'
braces' :: Inlines -> Inlines
braces' :: Inlines -> Inlines
braces' Inlines
d =
  let s :: String
s = forall a. Show a => a -> String
show Inlines
d
   in if forall a. Null a => a -> Bool
Agda.null String
s
        then Inlines -> Inlines
braces Inlines
d
        else Inlines -> Inlines
braces (forall {a}. (IsString a, Monoid a) => Char -> a
spaceIfDash (forall a. [a] -> a
head String
s) forall a. Semigroup a => a -> a -> a
<> Inlines
d forall a. Semigroup a => a -> a -> a
<> forall {a}. (IsString a, Monoid a) => Char -> a
spaceIfDash (forall a. [a] -> a
last String
s))
  where
    -- Add space to avoid starting a comment (Ulf, 2010-09-13, #269)
    -- Andreas, 2018-07-21, #3161: Also avoid ending a comment
    spaceIfDash :: Char -> a
spaceIfDash Char
'-' = a
" "
    spaceIfDash Char
_ = forall a. Monoid a => a
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 :: forall i. (Show i, Integral i) => i -> String
showIndex = forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toSubscriptDigit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String
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
  { SpecialCharacters -> Inlines -> Inlines
_dbraces :: Inlines -> Inlines,
    SpecialCharacters -> Inlines
_lambda :: Inlines,
    SpecialCharacters -> Inlines
_arrow :: Inlines,
    SpecialCharacters -> Inlines
_forallQ :: Inlines,
    SpecialCharacters -> Inlines
_leftIdiomBrkt :: Inlines,
    SpecialCharacters -> Inlines
_rightIdiomBrkt :: Inlines,
    SpecialCharacters -> Inlines
_emptyIdiomBrkt :: Inlines
  }

{-# NOINLINE specialCharacters #-}
specialCharacters :: SpecialCharacters
specialCharacters :: SpecialCharacters
specialCharacters =
  SpecialCharacters
    { _dbraces :: Inlines -> Inlines
_dbraces = (Inlines
"\x2983 " forall a. Semigroup a => a -> a -> a
<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. Semigroup a => a -> a -> a
<> Inlines
" \x2984"),
      _lambda :: Inlines
_lambda = Inlines
"\x03bb",
      _arrow :: Inlines
_arrow = Inlines
"\x2192",
      _forallQ :: Inlines
_forallQ = Inlines
"\x2200",
      _leftIdiomBrkt :: Inlines
_leftIdiomBrkt = Inlines
"\x2987",
      _rightIdiomBrkt :: Inlines
_rightIdiomBrkt = Inlines
"\x2988",
      _emptyIdiomBrkt :: Inlines
_emptyIdiomBrkt = Inlines
"\x2987\x2988"
    }