module StructurallyRecursiveDescentParsing.PBM where
import Data.Vec as Vec
import Data.List as List
open import Codata.Musical.Notation
open import Data.Bool
open import Data.Char using (_==_)
import Data.Char.Properties as Char
import Data.String as String
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality
open import StructurallyRecursiveDescentParsing.Grammar
open import StructurallyRecursiveDescentParsing.Lib
open import StructurallyRecursiveDescentParsing.DepthFirst
open Token Char.decSetoid
open import TotalParserCombinators.Examples.PBM using (module PBM)
open PBM
mutual
comment : Parser EmptyNT _ _ _
comment = tt <$ tok '#'
<⊛ sat' (not ∘ _==_ '\n') ⋆
<⊛ tok '\n'
colour = white <$ tok '0'
∣ black <$ tok '1'
pbm =
w∣c ⋆ ⊛>
theString (String.toVec "P1") ⊛>
w∣c ⋆ ⊛>
number !>>= λ cols → ♯
(w∣c + ⊛>
number >>= λ rows →
w∣c ⊛>
(toPBM <$> exactly rows (exactly cols (w∣c ⋆ ⊛> colour))) <⊛
any ⋆)
where w∣c = whitespace ∣ comment
module Example where
open Vec
image = toPBM ((white ∷ black ∷ white ∷ []) ∷
(black ∷ white ∷ black ∷ []) ∷
(white ∷ black ∷ white ∷ []) ∷ [])
ex : parseComplete (⟦ pbm ⟧ emptyGrammar)
(String.toList (show image)) ≡
List.[_] image
ex = refl