module TotalParserCombinators.Examples.PBM where
open import Data.Bool
open import Data.Char as Char using (Char; _==_)
open import Data.List as List using (List)
open import Data.Maybe hiding (_>>=_)
open import Data.Nat hiding (_^_)
import Data.Nat.Show as ℕ
open import Data.String as String
using (String) renaming (_++_ to _<+>_)
open import Data.Unit
open import Data.Vec as Vec using (Vec; _++_; [_])
open import Function
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import TotalParserCombinators.BreadthFirst
open import TotalParserCombinators.Lib
open import TotalParserCombinators.Parser
open Token Char Char._≟_
module PBM where
data Colour : Set where
white : Colour
black : Colour
Matrix : Set → ℕ → ℕ → Set
Matrix A rows cols = Vec (Vec A cols) rows
record PBM : Set where
constructor toPBM
field
{rows cols} : ℕ
matrix : Matrix Colour rows cols
open PBM public
showColour : Colour → Char
showColour white = '0'
showColour black = '1'
show : PBM → String
show i = "P1\n" <+>
ℕ.show (cols i) <+> " " <+> ℕ.show (rows i) <+> "\n" <+>
showMatrix (matrix i)
where
showMatrix = String.fromList ∘
Vec.toList ∘
Vec.concat ∘
Vec.map ((λ xs → xs ++ [ '\n' ]) ∘ Vec.map showColour)
open PBM
comment : Parser Char ⊤ _
comment =
tok '#' >>= λ _ →
sat′ (not ∘ _==_ '\n') ⋆ >>= λ _ →
tok '\n' >>= λ _ →
return tt
colour : Parser Char Colour _
colour = const white <$> tok '0'
∣ const black <$> tok '1'
pbm : Parser Char PBM _
pbm =
w∣c ⋆ >>= λ _ →
tok 'P' >>= λ _ → tok '1' >>= λ _ →
w∣c ⋆ >>= λ _ →
number >>= λ cols →
w∣c + >>= λ _ →
number >>= λ rows →
w∣c >>= λ _ →
(w∣c ⋆ >>= λ _ → colour) ^ cols ^ rows >>= λ m →
token ⋆ >>= λ _ →
return (toPBM m)
where
w∣c = whitespace ∣ comment