module StructurallyRecursiveDescentParsing.DepthFirst where
open import Data.Bool as Bool
open import Data.Product as Prod
import Data.List as L; open L using (List)
import Data.List.Effectful
open import Data.Nat
open import Data.Nat.Properties
open import Data.Vec using ([]; _∷_)
open import Data.Vec.Bounded hiding ([]; _∷_)
open import Effect.Applicative.Indexed
open import Effect.Monad.Indexed
open import Effect.Monad.State.Indexed
open import Function
open import Codata.Musical.Notation
import Level
open import StructurallyRecursiveDescentParsing.Simplified
private
P : Set → IFun ℕ Level.zero
P Tok = IStateT (Vec≤ Tok) List
open module M₁ {Tok : Set} =
RawIMonadPlus (StateTIMonadPlus (Vec≤ Tok)
Data.List.Effectful.monadPlus)
using ()
renaming ( return to return′
; _>>=_ to _>>=′_
; _>>_ to _>>′_
; ∅ to fail′
; _∣_ to _∣′_
)
open module M₂ {Tok : Set} =
RawIMonadState (StateTIMonadState (Vec≤ Tok)
Data.List.Effectful.monad)
using ()
renaming ( get to get′
; put to put′
; modify to modify′
)
mutual
parse↓ : ∀ {Tok e R} n → Parser Tok e R →
P Tok n (if e then n else n ∸ 1) R
parse↓ n (return x) = return′ x
parse↓ n fail = fail′
parse↓ n (_∣_ {true} p₁ p₂) = parse↓ n p₁ ∣′ parse↑ n p₂
parse↓ n (_∣_ {false} {true} p₁ p₂) = parse↑ n p₁ ∣′ parse↓ n p₂
parse↓ n (_∣_ {false} {false} p₁ p₂) = parse↓ n p₁ ∣′ parse↓ n p₂
parse↓ n (p₁ ?>>= p₂) = parse↓ n p₁ >>=′ λ x → parse↓ n (p₂ x)
parse↓ zero (p₁ !>>= p₂) = fail′
parse↓ (suc n) (p₁ !>>= p₂) = parse↓ (suc n) p₁ >>=′ λ x → parse↑ n (♭ (p₂ x))
parse↓ n token = get′ >>=′ eat
where
eat : ∀ {Tok n} → Vec≤ Tok n → P Tok n (n ∸ 1) Tok
eat ([] , _) = fail′
eat s@(c ∷ _ , _) = put′ (drop 1 s) >>′ return′ c
parse↑ : ∀ {e Tok R} n → Parser Tok e R → P Tok n n R
parse↑ {true} n p = parse↓ n p
parse↑ {false} zero p = fail′
parse↑ {false} (suc n) p = parse↓ (suc n) p >>=′ λ r →
modify′ (≤-cast (n≤1+n _)) >>′
return′ r
parse : ∀ {Tok i R} → Parser Tok i R → List Tok → List (R × List Tok)
parse p s = L.map (Prod.map id toList) (parse↓ _ p (fromList s))
parseComplete : ∀ {Tok i R} → Parser Tok i R → List Tok → List R
parseComplete p s =
L.map proj₁ (L.filter ((Bool._≟ true) ∘ L.null ∘ proj₂) (parse p s))