module SSG.Djot.Block

import SSG.Parser.Core
import SSG.Parser.Util

import SSG.Djot.Common
import SSG.Djot.Inline

import Data.List1
import Data.Vect
import Data.Nat
import Data.String

import Control.Eff
import Derive.Prelude

-- For iutils unit tests
import System

%language ElabReflection

--**************
--* Data Types *
--**************

public export
data HeaderLevel : Type where
  H1 : HeaderLevel
  H2 : HeaderLevel
  H3 : HeaderLevel
  H4 : HeaderLevel
  H5 : HeaderLevel
  H6 : HeaderLevel

%runElab derive "HeaderLevel" [Eq]

export
Show HeaderLevel where
  show H1 = "1"
  show H2 = "2"
  show H3 = "3"
  show H4 = "4"
  show H5 = "5"
  show H6 = "6"

namespace HeaderLevel
  public export
  integerToHeader : Integer -> Maybe HeaderLevel
  integerToHeader 1 = Just H1
  integerToHeader 2 = Just H2
  integerToHeader 3 = Just H3
  integerToHeader 4 = Just H4
  integerToHeader 5 = Just H5
  integerToHeader 6 = Just H6
  integerToHeader i = Nothing

  export
  fromInteger : (x : Integer) -> {auto prf : IsJust (integerToHeader x)} -> HeaderLevel
  fromInteger x = fromJust $ integerToHeader x

public export
data Block : Type where
  Paragraph : (contents : List1 Inline) -> Block
  Heading : (level : HeaderLevel) -> (contents : List1 Inline) -> Block

%runElab derive "Block" [Show, Eq]

--**************
--*   Syntax   *
--**************

---------------
-- Paragraph --
---------------

paragraph : PS Block
paragraph = do
  inlines <- inline
  blankLineOrEnd
  pure $ Paragraph inlines

-------------
-- Heading --
-------------

heading : PS Block
heading = do
  levelMarker <- atLeastOne "Expected Header Marker" $ thisString "#"
  ws <- atLeastOne "Expected Whitespace after header marker" $ space
  case integerToHeader (natToInteger $ length levelMarker) of
    Nothing => throw "Invalid header length: \{show $ length levelMarker}"
    Just level => do
      inlines <- inline
      pure $ Heading level inlines

--------------------------
-- Overall Block Parser --
--------------------------

export
block : PS Block
block = do
  -- eat up any blank lines
  _ <- many blankLine
  oneOfE "" [
    heading
  , paragraph
  ]

export
blocks : PS (List Block)
blocks = many block

--**************
--* Unit Tests *
--**************

------------------------
-- Block Syntax Tests --
------------------------

-- @@test Paragraph
blockParagraphSmoke : IO Bool
blockParagraphSmoke =
  let input = "Hello World"
      ref = [Paragraph (inlineFromString' "Hello World")]
  in golden input ref blocks

-- @@test Two Paragraph
blockTwoParagraphSmoke : IO Bool
blockTwoParagraphSmoke =
  let input = "Hello World\n\nHello Again"
      ref = [
        Paragraph (inlineFromString' "Hello World")
      , Paragraph (inlineFromString' "Hello Again")
      ]
  in golden input ref blocks

-- @@test Level 1 heading
blockLevelOneHeadingSmoke : IO Bool
blockLevelOneHeadingSmoke =
  let input = "# Level 1"
      ref = [
        Heading 1 (inlineFromString' "Level 1")
      ]
  in golden input ref blocks

-- @@test Level 2 heading
blockLevelTwoHeadingSmoke : IO Bool
blockLevelTwoHeadingSmoke =
  let input = "## Level 2"
      ref = [
        Heading 2 (inlineFromString' "Level 2")
      ]
  in golden input ref blocks