{-# OPTIONS --termination-depth=2 #-}
module TotalParserCombinators.Force where
open import Codata.Musical.Notation
import Data.List.Effectful as ListMonad
open import Data.Maybe hiding (_>>=_)
open import Data.Nat
open import Function.Base
import Relation.Binary.PropositionalEquality as P
open import TotalParserCombinators.Congruence
open import TotalParserCombinators.Laws
open import TotalParserCombinators.Parser
force : ∀ {Tok R xs} → ℕ → Parser Tok R xs → Parser Tok R xs
force zero p = p
force n (return x) = return x
force n fail = fail
force n token = token
force n (p₁ ∣ p₂) = force n p₁ ∣ force n p₂
force n (f <$> p) = f <$> force n p
force n (nonempty p) = nonempty (force n p)
force n (cast xs₁≈xs₂ p) = cast xs₁≈xs₂ (force n p)
force (suc n) (p₁ ⊛ p₂) with forced? p₁ | forced? p₂
... | just xs | nothing = force (suc n) p₁ ⊛ force n (♭ p₂)
... | just xs | just fs = force (suc n) p₁ ⊛ force (suc n) p₂
... | nothing | nothing = force n (♭ p₁) ⊛ force n (♭ p₂)
... | nothing | just fs =
P.subst (Parser _ _) (ListMonad.Applicative.right-zero fs) $
force n (♭ p₁) ⊛ force (suc n) p₂
force (suc n) (p₁ >>= p₂) with forced? p₁ | forced?′ p₂
... | just f | nothing = force (suc n) p₁ >>= λ x → force n (♭ (p₂ x))
... | just f | just xs = force (suc n) p₁ >>= λ x → force (suc n) (p₂ x)
... | nothing | nothing = force n (♭ p₁) >>= λ x → force n (♭ (p₂ x))
... | nothing | just xs =
P.subst (Parser _ _) (ListMonad.MonadProperties.right-zero xs) $
force n (♭ p₁) >>= λ x → force (suc n) (p₂ x)
correct : ∀ {Tok R xs} (n : ℕ) (p : Parser Tok R xs) → force n p ≅P p
correct zero p = p ∎
correct (suc n) (return x) = return x ∎
correct (suc n) fail = fail ∎
correct (suc n) token = token ∎
correct (suc n) (p₁ ∣ p₂) = correct (suc n) p₁ ∣ correct (suc n) p₂
correct (suc n) (f <$> p) = (λ _ → P.refl) <$> correct (suc n) p
correct (suc n) (nonempty p) = nonempty (correct (suc n) p)
correct (suc n) (cast xs₁≈xs₂ p) = cast (correct (suc n) p)
correct (suc n) (p₁ ⊛ p₂) with forced? p₁ | forced? p₂
... | just xs | nothing = [ ○ - ○ - ○ - ◌ ] correct (suc n) p₁ ⊛ correct n (♭ p₂)
... | just xs | just fs = [ ○ - ○ - ○ - ○ ] correct (suc n) p₁ ⊛ correct (suc n) p₂
... | nothing | nothing = [ ○ - ◌ - ○ - ◌ ] correct n (♭ p₁) ⊛ correct n (♭ p₂)
... | nothing | just fs =
P.subst (Parser _ _) lemma forced ≅⟨ Subst.correct lemma ⟩
forced ≅⟨ [ ○ - ◌ - ○ - ○ ] correct n (♭ p₁) ⊛ correct (suc n) p₂ ⟩
p₁ ⊛ p₂ ∎
where
lemma = ListMonad.Applicative.right-zero fs
forced = force n (♭ p₁) ⊛ force (suc n) p₂
correct (suc n) (p₁ >>= p₂) with forced? p₁ | forced?′ p₂
... | just f | nothing = [ ○ - ○ - ○ - ◌ ] correct (suc n) p₁ >>= λ x → correct n (♭ (p₂ x))
... | just f | just xs = [ ○ - ○ - ○ - ○ ] correct (suc n) p₁ >>= λ x → correct (suc n) (p₂ x)
... | nothing | nothing = [ ○ - ◌ - ○ - ◌ ] correct n (♭ p₁) >>= λ x → correct n (♭ (p₂ x))
... | nothing | just xs =
P.subst (Parser _ _) lemma forced ≅⟨ Subst.correct lemma ⟩
forced ≅⟨ [ ○ - ◌ - ○ - ○ ] correct n (♭ p₁) >>= (λ x → correct (suc n) (p₂ x)) ⟩
p₁ >>= p₂ ∎
where
forced = force n (♭ p₁) >>= λ x → force (suc n) (p₂ x)
lemma = ListMonad.MonadProperties.right-zero xs