module Examples.Identifier where
open import Coinduction
open import Data.Bool
open import Data.Char
open import Data.List.NonEmpty
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary
open import Grammar.Infinite as Grammar using (Grammar)
open import Pretty using (Doc; Pretty-printer)
open import Renderer
open import Utilities
is-lower : Char → Bool
is-lower t = ('a' ≤?C t) ∧ (t ≤?C 'z')
module Problematic where
identifier : Grammar (List⁺ Char)
identifier = (proj₁ <$> sat is-lower) +
where open Grammar
no-printer : ¬ Pretty-printer identifier
no-printer identifier-printer = no-doc (identifier-printer [ 'A' ])
where
open Grammar
lemma : ∀ {p : Char → Bool} {t s s′} →
t ∷ s ∈ (proj₁ <$> sat p) + · s′ → T (p t)
lemma (⊛-sem (<$>-sem (<$>-sem {x = _ , ok} _)) _) = ok
no-doc : ¬ Doc identifier [ 'A' ]
no-doc d = lemma (proj₂ (Renderer.string-exists d))
Identifier : Set
Identifier = List⁺ (∃ λ t → T (is-lower t))
identifier : Grammar Identifier
identifier = sat is-lower +
where open Grammar
identifier-printer : Pretty-printer identifier
identifier-printer = map+ (sat is-lower)
where open Pretty
identifier-w : Grammar Identifier
identifier-w = identifier <⊛ whitespace ⋆
where open Grammar
identifier-w-printer : Pretty-printer identifier-w
identifier-w-printer n = identifier-printer n <⊛ nil-⋆
where open Pretty
test : render 80 (identifier-w-printer (str⁺ "aaa")) ≡ "aaa"
test = refl