{-# OPTIONS --guardedness #-}
module Pretty where
open import Data.Bool
open import Data.Char
open import Data.List hiding ([_])
open import Data.List.NonEmpty using (List⁺; _∷_; _∷⁺_)
open import Data.List.Properties
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Tactic.MonoidSolver
open import Grammar.Infinite as G
hiding (_<$>_; _<$_; _⊛_; _<⊛_; _⊛>_; token; tok; if-true; sat;
tok-sat; symbol; list; list⁺)
mutual
infixr 20 _◇_
data Doc : ∀ {A} → Grammar A → A → Set₁ where
_◇_ : ∀ {c₁ c₂ A B x y}
{g₁ : ∞Grammar c₁ A} {g₂ : A → ∞Grammar c₂ B} →
Doc (♭? g₁) x → Doc (♭? (g₂ x)) y → Doc (g₁ >>= g₂) y
text : ∀ {s} → Doc (string s) s
line : Doc (tt G.<$ whitespace +) tt
group : ∀ {A x} {g : Grammar A} → Doc g x → Doc g x
nest : ∀ {A x} {g : Grammar A} → ℕ → Doc g x → Doc g x
emb : ∀ {A B x y} {g₁ : Grammar A} {g₂ : Grammar B} →
(∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) →
Doc g₁ x → Doc g₂ y
fill : ∀ {A xs} {g : Grammar A} →
Docs g xs → Doc (g sep-by whitespace +) xs
infixr 5 _∷_
data Docs {A} (g : Grammar A) : List⁺ A → Set₁ where
[_] : ∀ {x} → Doc g x → Docs g (x ∷ [])
_∷_ : ∀ {x xs} → Doc g x → Docs g xs → Docs g (x ∷⁺ xs)
Pretty-printer : {A : Set} → Grammar A → Set₁
Pretty-printer g = ∀ x → Doc g x
Pretty-printer-for : {A : Set} → Grammar-for A → Set₁
Pretty-printer-for g = ∀ x → Doc (g x) (x , refl)
embed : ∀ {A B} {g₁ : Grammar A} {g₂ : Grammar B} {x y} →
(∀ {s} → x ∈ g₁ · s → y ∈ g₂ · s) → Doc g₁ x → Doc g₂ y
embed f (emb g d) = emb (f ∘ g) d
embed f d = emb f d
nil : ∀ {A} {x : A} → Doc (return x) x
nil = embed lemma text
where
lemma : ∀ {x s} → [] ∈ string [] · s → x ∈ return x · s
lemma return-sem = return-sem
token : ∀ {t} → Doc G.token t
token {t} = embed lemma text
where
lemma′ : ∀ {x s} → x ∈ string (t ∷ []) · s → x ≡ t ∷ [] →
t ∈ G.token · s
lemma′ (⊛-sem (<$>-sem tok-sem) return-sem) refl = token-sem
lemma : ∀ {s} → t ∷ [] ∈ string (t ∷ []) · s → t ∈ G.token · s
lemma t∈ = lemma′ t∈ refl
tok : ∀ {t} → Doc (G.tok t) t
tok {t} = embed lemma token
where
lemma : ∀ {s} → t ∈ G.token · s → t ∈ G.tok t · s
lemma token-sem = tok-sem
infix 21 <$>_ <$_
<$>_ : ∀ {c A B} {f : A → B} {x} {g : ∞Grammar c A} →
Doc (♭? g) x → Doc (f G.<$> g) (f x)
<$> d = embed <$>-sem d
<$_ : ∀ {c A B} {x : A} {y} {g : ∞Grammar c B} →
Doc (♭? g) y → Doc (x G.<$ g) x
<$ d = embed <$-sem d
infixl 20 _⊛_ _<⊛_ _⊛>_ _<⊛-tt_ _tt-⊛>_
_⊛_ : ∀ {c₁ c₂ A B f x}
{g₁ : ∞Grammar c₁ (A → B)} {g₂ : ∞Grammar c₂ A} →
Doc (♭? g₁) f → Doc (♭? g₂) x → Doc (g₁ G.⊛ g₂) (f x)
_⊛_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ <$> d₂)
where
lemma : ∀ {x s} →
x ∈ (g₁ >>= λ f → f G.<$> g₂) · s → x ∈ g₁ G.⊛ g₂ · s
lemma (>>=-sem f∈ (<$>-sem x∈)) = ⊛-sem f∈ x∈
_<⊛_ : ∀ {c₁ c₂ A B x y} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
Doc (♭? g₁) x → Doc (♭? g₂) y → Doc (g₁ G.<⊛ g₂) x
_<⊛_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ <$ d₂)
where
lemma : ∀ {x s} →
x ∈ (g₁ >>= λ x → x G.<$ g₂) · s → x ∈ g₁ G.<⊛ g₂ · s
lemma (>>=-sem x∈ (<$-sem y∈)) = <⊛-sem x∈ y∈
_⊛>_ : ∀ {c₁ c₂ A B x y} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
Doc (♭? g₁) x → Doc (♭? g₂) y → Doc (g₁ G.⊛> g₂) y
_⊛>_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ◇ d₂)
where
lemma : ∀ {y s} →
y ∈ (g₁ >>= λ _ → g₂) · s → y ∈ g₁ G.⊛> g₂ · s
lemma (>>=-sem x∈ y∈) = ⊛>-sem x∈ y∈
_<⊛-tt_ : ∀ {c₁ c₂ A B x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
Doc (♭? g₁) x → Doc (tt G.<$ g₂) tt → Doc (g₁ G.<⊛ g₂) x
_<⊛-tt_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ <⊛ d₂)
where
lemma : ∀ {x s} → x ∈ g₁ G.<⊛ (tt G.<$ g₂) · s → x ∈ g₁ G.<⊛ g₂ · s
lemma (<⊛-sem x∈ (<$-sem y∈)) = <⊛-sem x∈ y∈
_tt-⊛>_ : ∀ {c₁ c₂ A B x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ B} →
Doc (tt G.<$ g₁) tt → Doc (♭? g₂) x → Doc (g₁ G.⊛> g₂) x
_tt-⊛>_ {g₁ = g₁} {g₂} d₁ d₂ = embed lemma (d₁ ⊛> d₂)
where
lemma : ∀ {x s} → x ∈ (tt G.<$ g₁) G.⊛> g₂ · s → x ∈ g₁ G.⊛> g₂ · s
lemma (⊛>-sem (<$-sem x∈) y∈) = ⊛>-sem x∈ y∈
left : ∀ {c₁ c₂ A x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
Doc (♭? g₁) x → Doc (g₁ ∣ g₂) x
left d = embed left-sem d
right : ∀ {c₁ c₂ A x} {g₁ : ∞Grammar c₁ A} {g₂ : ∞Grammar c₂ A} →
Doc (♭? g₂) x → Doc (g₁ ∣ g₂) x
right d = embed right-sem d
nil-⋆ : ∀ {c A} {g : ∞Grammar c A} → Doc (g ⋆) []
nil-⋆ {A = A} {g} = embed lemma nil
where
lemma : ∀ {s} → [] ∈ return {A = List A} [] · s → [] ∈ g ⋆ · s
lemma return-sem = ⋆-[]-sem
cons-⋆+ : ∀ {c A} {g : ∞Grammar c A} {x xs} →
Doc (♭? g) x → Doc (g ⋆) xs → Doc (g +) (x ∷ xs)
cons-⋆+ d₁ d₂ = <$> d₁ ⊛ d₂
cons-⋆ : ∀ {c A} {g : ∞Grammar c A} {x xs} →
Doc (♭? g) x → Doc (g ⋆) xs → Doc (g ⋆) (x ∷ xs)
cons-⋆ d₁ d₂ = embed ⋆-+-sem (cons-⋆+ d₁ d₂)
if-true : ∀ b → Pretty-printer (G.if-true b)
if-true true _ = nil
if-true false ()
sat : (p : Char → Bool) → Pretty-printer (G.sat p)
sat p (t , proof) = token ◇ <$> if-true (p t) proof
tok-sat : {p : Char → Bool} → Pretty-printer-for (G.tok-sat p)
tok-sat _ = <$ tok
space : Doc (whitespace ⋆) (' ' ∷ [])
space = embed lemma tok
where
lemma : ∀ {s} →
' ' ∈ G.tok ' ' · s →
(' ' ∷ []) ∈ whitespace ⋆ · s
lemma tok-sem = ⋆-+-sem single-space-sem
line⋆ : Doc (tt G.<$ whitespace ⋆) tt
line⋆ = embed lemma line
where
lemma : ∀ {s} →
tt ∈ tt G.<$ whitespace + · s →
tt ∈ tt G.<$ whitespace ⋆ · s
lemma (<$-sem w+) = <$-sem (⋆-+-sem w+)
final-line′ : ∀ {A} {g : Grammar A} {x} →
Trailing-whitespace g → Doc g x → (i : ℕ) → Doc g x
final-line′ trailing d i = embed trailing (d <⊛-tt nest i line⋆)
final-line : ∀ {A} {g : Grammar A} {x} (n : ℕ)
{trailing : T (is-just (trailing-whitespace n g))} →
Doc g x → (i : ℕ) → Doc g x
final-line n {trailing} =
final-line′ (to-witness-T (trailing-whitespace n _) trailing)
final-line-+⋆ : ∀ {c A} {g : ∞Grammar c A} {x xs} (n : ℕ)
{trailing : T (is-just (trailing-whitespace n (g +)))} →
Doc (g +) (x ∷ xs) → (i : ℕ) → Doc (g ⋆) (x ∷ xs)
final-line-+⋆ n {trailing} d i =
embed ⋆-+-sem (final-line n {trailing} d i)
symbol : ∀ {s} → Doc (G.symbol s) s
symbol = text <⊛ nil-⋆
symbol-line : ∀ {s} → Doc (G.symbol s) s
symbol-line = final-line 1 symbol 0
symbol-space : ∀ {s} → Doc (G.symbol s) s
symbol-space = text <⊛ space
bracket : ∀ {c A x s₁ s₂} {g : ∞Grammar c A} (n : ℕ) →
{trailing : T (is-just (trailing-whitespace n (♭? g)))} →
Doc (♭? g) x → Doc (G.symbol s₁ G.⊛> g G.<⊛ G.symbol s₂) x
bracket n {trailing} d =
group (nest 2 symbol-line
⊛>
final-line n {trailing = trailing} (nest 2 d) 0
<⊛
symbol)
mutual
map⋆ : ∀ {c A} {g : ∞Grammar c A} →
Pretty-printer (♭? g) → Pretty-printer (g ⋆)
map⋆ p [] = nil-⋆
map⋆ p (x ∷ xs) = embed ⋆-+-sem (map+ p (x ∷ xs))
map+ : ∀ {c A} {g : ∞Grammar c A} →
Pretty-printer (♭? g) → Pretty-printer (g +)
map+ p (x ∷ xs) = cons-⋆+ (p x) (map⋆ p xs)
mutual
list : ∀ {A} {elem : Grammar-for A} →
Pretty-printer-for elem →
Pretty-printer-for (G.list elem)
list e [] = nil
list e (x ∷ xs) = <$> (list⁺ e (x ∷ xs))
list⁺ : ∀ {A} {elem : Grammar-for A} →
Pretty-printer-for elem →
Pretty-printer-for (G.list⁺ elem)
list⁺ e (x ∷ xs) = <$> (e x) ⊛ list e xs
fill+ : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
{trailing : T (is-just (trailing-whitespace n (♭? g)))} →
∀ {xs} → Docs (♭? g) xs → Doc (g +) xs
fill+ {g = g} n {trailing} ds = embed lemma (fill ds)
where
trailing! = to-witness-T (trailing-whitespace n (♭? g)) trailing
lemma′ : ∀ {x xs s₁ s₂} →
x ∈ ♭? g · s₁ → xs ∈ ♭? g prec-by whitespace + · s₂ →
x ∷ xs ∈ g + · s₁ ++ s₂
lemma′ x∈ ⋆-[]-sem = +-sem x∈ ⋆-[]-sem
lemma′ {s₁ = s₁} x∈ (⋆-+-sem (⊛-sem (<$>-sem (⊛>-sem w+ x′∈)) xs∈)) =
cast lemma″
(+-∷-sem (trailing! (<⊛-sem x∈ (⋆-+-sem w+))) (lemma′ x′∈ xs∈))
where
lemma″ :
∀ {s₂ s₃ s₄} → (s₁ ++ s₂) ++ s₃ ++ s₄ ≡ s₁ ++ (s₂ ++ s₃) ++ s₄
lemma″ = solve (++-monoid Char)
lemma : ∀ {s xs} → xs ∈ ♭? g sep-by whitespace + · s → xs ∈ g + · s
lemma (⊛-sem (<$>-sem x∈) xs∈) = lemma′ x∈ xs∈
map+-fill : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
{trailing : T (is-just (trailing-whitespace n (♭? g)))} →
Pretty-printer (♭? g) →
Pretty-printer (g +)
map+-fill {g = g} n {trailing} p (x ∷ xs) =
fill+ n {trailing = trailing} (to-docs x xs)
where
to-docs : ∀ x xs → Docs (♭? g) (x ∷ xs)
to-docs x [] = [ p x ]
to-docs x (x′ ∷ xs) = p x ∷ to-docs x′ xs
map⋆-fill : ∀ {c A} {g : ∞Grammar c A} (n : ℕ)
{trailing : T (is-just (trailing-whitespace n (♭? g)))} →
Pretty-printer (♭? g) →
Pretty-printer (g ⋆)
map⋆-fill n p [] = nil-⋆
map⋆-fill n {trailing} p (x ∷ xs) =
embed ⋆-+-sem (map+-fill n {trailing = trailing} p (x ∷ xs))