{-# 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ᴿ
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 ]
lastWidth : ℕ
last : [ s ∈ String ∣ length s ≡ lastWidth ]
maxWidth : [ n ∈ ℕ ∣ lastWidth ≤ n × All≤ n (block .value) ]
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 : Block
empty = text ""
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)
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 }
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 }
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