------------------------------------------------------------------------
-- The Agda standard library
--
-- Pretty Printing
-- This module is based on Jean-Philippe Bernardy's functional pearl
-- "A Pretty But Not Greedy Printer"
------------------------------------------------------------------------

{-# OPTIONS --with-K #-}

module Text.Pretty.Core where

import Level

open import Data.Bool.Base using (Bool)
open import Data.Irrelevant as Irrelevant using (Irrelevant) hiding (module Irrelevant)
open import Data.List.Base as List   using (List; []; _∷_)
open import Data.Nat.Base            using (ℕ; zero; suc; _+_; _⊔_; _≤_; z≤n)
open import Data.Nat.Properties      using (≤-refl; ≤-trans; +-identityʳ;
  module ≤-Reasoning; m≤n⊔m; +-monoʳ-≤; m≤m⊔n; +-comm; _≤?_)
open import Data.Product.Base as Prod using (_×_; _,_; uncurry; proj₁; proj₂)
import Data.Product.Relation.Unary.All as Allᴾ

open import Data.Tree.Binary as Tree using (Tree; leaf; node; #nodes; mapₙ)
open import Data.Tree.Binary.Relation.Unary.All as Allᵀ using (leaf; node)
open import Data.Unit.Base using (⊤; tt)
import Data.Tree.Binary.Relation.Unary.All.Properties as Allᵀ
import Data.Tree.Binary.Properties as Tree

open import Data.Maybe.Base as Maybe using (Maybe; nothing; just; maybe′)
open import Data.Maybe.Relation.Unary.All as Allᴹ using (nothing; just)

open import Data.String.Base as String
  using (String; length; replicate; _++_; unlines)
import Data.String.Unsafe as String
open import Function.Base using (_∘_; flip; _on_; id; _∘′_; _$_)
open import Relation.Nullary.Decidable.Core using (Dec)
open import Relation.Unary using (IUniversal; _⇒_; U)
open import Relation.Binary.PropositionalEquality.Core
  using (_≡_; refl; sym; cong; cong₂; subst)
open import Relation.Binary.PropositionalEquality.Properties
  using (module ≡-Reasoning)

open import Data.Refinement using (Refinement-syntax; _,_; value; proof)
import Data.Refinement.Relation.Unary.All as Allᴿ

------------------------------------------------------------------------
-- Block of text

-- Content is a representation of the first line and the middle of the
-- block. We use a tree rather than a list for the middle of the block
-- so that we can extend it with lines on the left and on the line for
-- free. We will ultimately render the block by traversing the tree left
-- to right in a depth-first manner.

Content : Set
Content = Maybe (String × Tree String ⊤)

size : Content → ℕ
size = maybe′ (suc ∘ #nodes ∘ proj₂) 0

All : ∀ {p} (P : String → Set p) → (Content → Set p)
All P = Allᴹ.All (Allᴾ.All P (Allᵀ.All P U))

All≤ : ℕ → Content → Set
All≤ n = All (λ s → length s ≤ n)

record Block : Set where
  field
    height    : ℕ
    block     : [ xs ∈ Content ∣ size xs ≡ height ]
  -- last line
    lastWidth : ℕ
    last      : [ s ∈ String ∣ length s ≡ lastWidth ]
  -- max of all the widths
    maxWidth  : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n (block .value) ]

------------------------------------------------------------------------
-- Raw string

text : String → Block
text s = record
  { height    = 0
  ; block     = nothing , ⦇ refl ⦈
  ; lastWidth = width
  ; last      = s , ⦇ refl ⦈
  ; maxWidth  = width , ⦇ (≤-refl , nothing) ⦈
  } where width = length s; open Irrelevant

------------------------------------------------------------------------
-- Empty

empty : Block
empty = text ""

------------------------------------------------------------------------
-- Helper functions

node? : Content → String → Tree String ⊤ → Content
node? (just (x , xs)) y ys = just (x , node xs y ys)
node? nothing         y ys = just (y , ys)

∣node?∣ : ∀ b y ys → size (node? b y ys)
                   ≡ size b + suc (#nodes ys)
∣node?∣ (just (x , xs)) y ys = refl
∣node?∣ nothing         y ys = refl

≤-Content : ∀ {m n} {b : Content} → m ≤ n → All≤ m b → All≤ n b
≤-Content {m} {n} m≤n = Allᴹ.map (Prod.map step (Allᵀ.mapₙ step))

  where

  step : ∀ {p} → p ≤ m → p ≤ n
  step = flip ≤-trans m≤n

All≤-node? : ∀ {l m r n} →
             All≤ n l → length m ≤ n → Allᵀ.All (λ s → length s ≤ n) U r →
             All≤ n (node? l m r)
All≤-node? nothing           py pys = just (py , pys)
All≤-node? (just (px , pxs)) py pys = just (px , node pxs py pys)

------------------------------------------------------------------------
-- Appending two documents

private
  module append (x y : Block) where

    module x = Block x
    module y = Block y

    blockx = x.block .value
    blocky = y.block .value

    widthx = x.maxWidth .value
    widthy = y.maxWidth .value

    lastx = x.last .value
    lasty = y.last .value

    height : ℕ
    height = (_+_ on Block.height) x y

    lastWidth : ℕ
    lastWidth = (_+_ on Block.lastWidth) x y

    pad : Maybe String
    pad with x.lastWidth
    ... | 0         = nothing
    ... | l@(suc _) = just (replicate l ' ')

    size-pad : maybe′ length 0 pad ≡ x.lastWidth
    size-pad with x.lastWidth
    ... | 0         = refl
    ... | l@(suc _) = String.length-replicate l

    indent : Maybe String → String → String
    indent = maybe′ _++_ id

    size-indent : ∀ ma str → length (indent ma str)
                ≡ maybe′ length 0 ma + length str
    size-indent nothing    str = refl
    size-indent (just pad) str = String.length-++ pad str

    indents : Maybe String → Tree String ⊤ → Tree String ⊤
    indents = maybe′ (mapₙ ∘ _++_) id

    size-indents : ∀ ma t → #nodes (indents ma t) ≡ #nodes t
    size-indents nothing    t = refl
    size-indents (just pad) t = Tree.#nodes-mapₙ (pad ++_) t

    unfold-indents : ∀ ma t → indents ma t ≡ mapₙ (indent ma) t
    unfold-indents nothing    t = sym (Tree.map-id t)
    unfold-indents (just pad) t = refl

    vContent : Content × String
    vContent with blocky
    ... | nothing        = blockx
                         , lastx ++ lasty
    ... | just (hd , tl) = node?
      {-,--------------,-}
      {-|-} blockx   {-|-}
      {-|-}          {-'---,-}    {-,------------------,-}
      {-|-} (lastx       {-|-} ++ {-|-}  hd)         {-|-}
      {-'------------------'-}    {-|-}              {-|-}
      (indents pad                {-|-}  tl)    {-,----'-}
      , indent pad                {-|-} lasty   {-|-}
                                  {-'-------------'-}

    vBlock = proj₁ vContent
    vLast  = proj₂ vContent

    isBlock : size blockx ≡ x.height → size blocky ≡ y.height →
              size vBlock ≡ height
    isBlock ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      size blockx         ≡⟨ ∣x∣ ⟩
      x.height            ≡⟨ +-identityʳ x.height ⟨
      x.height + 0        ≡⟨ cong (_ +_) ∣y∣ ⟩
      x.height + y.height ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      ∣node∣                            ≡⟨ ∣node?∣ blockx middle rest ⟩
      ∣blockx∣ + suc (#nodes rest) ≡⟨ cong ((size blockx +_) ∘′ suc) ∣rest∣ ⟩
      ∣blockx∣ + suc (#nodes tl)   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.height + y.height               ∎ where

      open ≡-Reasoning
      ∣blockx∣ = size blockx
      middle   = lastx ++ hd
      rest     = indents pad tl
      ∣rest∣   = size-indents pad tl
      ∣node∣   = size (node? blockx middle rest)

    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vBlock
    block .proof = ⦇ isBlock (Block.block x .proof) (Block.block y .proof) ⦈
      where open Irrelevant

    isLastLine : length lastx ≡ x.lastWidth →
                 length lasty ≡ y.lastWidth →
                 length vLast ≡ lastWidth
    isLastLine ∣x∣ ∣y∣ with blocky
    ... | nothing        = begin
      length (lastx ++ lasty)       ≡⟨ String.length-++ lastx lasty ⟩
      length lastx + length lasty   ≡⟨ cong₂ _+_ ∣x∣ ∣y∣ ⟩
      x.lastWidth + y.lastWidth     ∎ where open ≡-Reasoning
    ... | just (hd , tl) = begin
      length (indent pad lasty)          ≡⟨ size-indent pad lasty ⟩
      maybe′ length 0 pad + length lasty ≡⟨ cong₂ _+_ size-pad ∣y∣ ⟩
      x.lastWidth + y.lastWidth          ∎ where open ≡-Reasoning

    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last .value = vLast
    last .proof = ⦇ isLastLine (Block.last x .proof) (Block.last y .proof) ⦈
      where open Irrelevant

    vMaxWidth : ℕ
    vMaxWidth = widthx ⊔ (x.lastWidth + widthy)

    isMaxWidth₁ : y.lastWidth ≤ widthy → lastWidth ≤ vMaxWidth
    isMaxWidth₁ p = begin
      lastWidth            ≤⟨ +-monoʳ-≤ x.lastWidth p ⟩
      x.lastWidth + widthy ≤⟨ m≤n⊔m _ _ ⟩
      vMaxWidth            ∎ where open ≤-Reasoning

    isMaxWidth₂ : length lastx ≡ x.lastWidth →
                  x.lastWidth ≤ widthx →
                  All≤ widthx blockx →
                  All≤ widthy blocky →
                  All≤ vMaxWidth vBlock
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ ∣ys∣ with blocky
    ... | nothing        = ≤-Content (m≤m⊔n _ _) ∣xs∣
    isMaxWidth₂ ∣x∣≡ ∣x∣≤ ∣xs∣ (just (∣hd∣ , ∣tl∣))
        | just (hd , tl) =
      All≤-node? (≤-Content (m≤m⊔n _ _) ∣xs∣)
                 middle
                 (subst (Allᵀ.All _ U) (sym $ unfold-indents pad tl)
                 $ Allᵀ.mapₙ⁺ (indent pad) (Allᵀ.mapₙ (indented _) ∣tl∣))
      where

      middle : length (lastx ++ hd) ≤ vMaxWidth
      middle = begin
        length (lastx ++ hd)     ≡⟨ String.length-++ lastx hd ⟩
        length lastx + length hd ≡⟨ cong (_+ _) ∣x∣≡ ⟩
        x.lastWidth + length hd  ≤⟨ +-monoʳ-≤ x.lastWidth ∣hd∣ ⟩
        x.lastWidth + widthy     ≤⟨ m≤n⊔m _ _ ⟩
        vMaxWidth                ∎ where open ≤-Reasoning

      indented : ∀ s → length s ≤ widthy →
                 length (indent pad s) ≤ vMaxWidth
      indented s ∣s∣ = begin
        length (indent pad s)          ≡⟨ size-indent pad s ⟩
        maybe′ length 0 pad + length s ≡⟨ cong (_+ _) size-pad ⟩
        x.lastWidth + length s         ≤⟨ +-monoʳ-≤ x.lastWidth ∣s∣ ⟩
        x.lastWidth + widthy           ≤⟨ m≤n⊔m (widthx) _ ⟩
        vMaxWidth                      ∎ where open ≤-Reasoning

    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vBlock ]
    maxWidth .value = vMaxWidth
    maxWidth .proof =
      ⦇ _,_ ⦇ isMaxWidth₁ (map proj₁ (Block.maxWidth y .proof)) ⦈
            ⦇ isMaxWidth₂ (Block.last x .proof)
                          (map proj₁ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth x .proof))
                          (map proj₂ (Block.maxWidth y .proof))
            ⦈
      ⦈ where open Irrelevant

infixl 4 _<>_
_<>_ : Block → Block → Block
x <> y = record { append x y }

------------------------------------------------------------------------
-- Flush (introduces a new line)

private
  module flush (x : Block) where

    module x = Block x
    blockx  = x.block .value
    lastx   = x.last .value
    widthx  = x.maxWidth .value
    heightx = x.height

    height    = suc heightx
    lastWidth = 0
    vMaxWidth = widthx

    last : [ s ∈ String ∣ length s ≡ lastWidth ]
    last = "" , ⦇ refl ⦈ where open Irrelevant

    vContent = node? blockx lastx (leaf tt)

    isBlock : size blockx ≡ heightx → size vContent ≡ height
    isBlock ∣x∣ = begin
      size vContent   ≡⟨ ∣node?∣ blockx lastx (leaf tt) ⟩
      size blockx + 1 ≡⟨ cong (_+ 1) ∣x∣ ⟩
      heightx + 1     ≡⟨ +-comm heightx 1 ⟩
      height          ∎ where open ≡-Reasoning

    block : [ xs ∈ Content ∣ size xs ≡ height ]
    block .value = vContent
    block .proof = Irrelevant.map isBlock $ Block.block x .proof

    maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n vContent ]
    maxWidth .value = widthx
    maxWidth .proof = map (z≤n ,_)
      ⦇ All≤-node? ⦇ proj₂ (Block.maxWidth x .proof) ⦈
                   ⦇ middle (Block.last x .proof) ⦇ proj₁ (Block.maxWidth x .proof) ⦈ ⦈
                   (pure (leaf tt))
      ⦈ where

      open Irrelevant

      middle : length lastx ≡ x.lastWidth → x.lastWidth ≤ vMaxWidth →
               length lastx ≤ vMaxWidth
      middle p q = begin
        length lastx ≡⟨ p ⟩
        x.lastWidth  ≤⟨ q ⟩
        vMaxWidth    ∎ where open ≤-Reasoning

flush : Block → Block
flush x = record { flush x }

------------------------------------------------------------------------
-- Other functions

render : Block → String
render x = unlines
  $ maybe′ (uncurry (λ hd tl → hd ∷ Tree.Infix.toList tl)) []
  $ node? (Block.block x .value) (Block.last x .value) (leaf tt)

valid : (width : ℕ) (b : Block) → Dec (Block.maxWidth b .value ≤ width)
valid width b = Block.maxWidth b .value ≤? width