------------------------------------------------------------------------
-- An alternative backend
------------------------------------------------------------------------

-- Acknowledgements:
--
-- • The use of parsing "processes" is based on implementation C from
--   Koen Claessen's paper Parallel parsing processes.
--
-- • The idea to use toProc is due to Jean-Philippe Bernardy.

-- It is not obvious how to adapt this backend so that it can handle
-- parsers which are simultaneously left and right recursive, like
-- TotalRecognisers.LeftRecursion.leftRight.

open import Relation.Binary
open import Relation.Binary.PropositionalEquality

module TotalRecognisers.Simple.AlternativeBackend
         (Tok : Set)
         (_≟_ : Decidable (_≡_ {A = Tok}))
         -- The tokens must come with decidable equality.
         where

open import Coinduction
open import Data.Bool hiding (_≟_)
open import Data.List
open import Relation.Nullary.Decidable

import TotalRecognisers.Simple as S
open S Tok _≟_ hiding (_∈?_)

------------------------------------------------------------------------
-- Parsing "processes"

data Proc : Set where
  tokenBind : (p : Tok   Proc)  Proc
  emptyOr   : (p : Proc)  Proc
  fail      : Proc

-- The semantics of Proc is given by run: run p s is true iff s is a
-- member of the language defined by p.

run : Proc  List Tok  Bool
run (tokenBind p) (c  s) = run ( (p c)) s
run (emptyOr p)   s       = null s  run p s
run _             _       = false

------------------------------------------------------------------------
-- Parsers can be turned into processes

-- Here I use my technique for "beating the productivity checker".

-- Process "programs".

infixl 5 _∣_

data ProcP : Set where
  -- Process primitives.
  tokenBind : (p : Tok   ProcP)  ProcP
  emptyOr   : (p : ProcP)  ProcP
  fail      : ProcP

  -- Symmetric choice.
  _∣_     : (p₁ p₂ : ProcP)  ProcP

  -- Embedding of parsers.
  toProc  :  {n} (p : P n) (κ : ProcP)  ProcP

-- WHNFs.

data ProcW : Set where
  tokenBind : (p : Tok   ProcP)  ProcW
  emptyOr   : (p : ProcW)  ProcW
  fail      : ProcW

-- WHNFs can be turned into programs.

program : ProcW  ProcP
program (tokenBind p) = tokenBind p
program (emptyOr p)   = emptyOr (program p)
program fail          = fail

-- Symmetric choice for WHNFs.

_∣W_ : ProcW  ProcW  ProcW
tokenBind p₁ ∣W tokenBind p₂ = tokenBind  c   ( (p₁ c)   (p₂ c)))
emptyOr p₁   ∣W emptyOr p₂   = emptyOr (p₁ ∣W p₂)
emptyOr p₁   ∣W p₂           = emptyOr (p₁ ∣W p₂)
p₁           ∣W emptyOr p₂   = emptyOr (p₁ ∣W p₂)
fail         ∣W p₂           = p₂
p₁           ∣W fail         = p₁

-- Interpretation of toProc.

mutual

  toProcW′ :  {n}  P n  if n then ProcW else ProcP  ProcW
  toProcW′ fail                                  κ = fail
  toProcW′ empty                                 κ = κ
  toProcW′ (tok t)                               κ = tokenBind  t′ 
                                                       if  t  t′  then  κ else  fail)
  toProcW′ (_∣_ {n₁ = true } {n₂ = true } p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_∣_ {n₁ = true } {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW  p₂ κ
  toProcW′ (_∣_ {n₁ = false} {n₂ = true } p₁ p₂) κ = toProcW  p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_∣_ {n₁ = false} {n₂ = false} p₁ p₂) κ = toProcW′ p₁ κ ∣W toProcW′ p₂ κ
  toProcW′ (_·_ {n₁ = true }              p₁ p₂) κ = toProcW′ p₁ (toProcW′  p₂  κ)
  toProcW′ (_·_ {n₁ = false}              p₁ p₂) κ = toProcW′ p₁ (toProc ( p₂) κ)

  toProcW :  {n}  P n  ProcW  ProcW
  toProcW {true } p κ = toProcW′ p          κ
  toProcW {false} p κ = toProcW′ p (program κ)

-- Programs can be turned into WHNFs.

whnf : ProcP  ProcW
whnf (tokenBind p) = tokenBind p
whnf (emptyOr p)   = emptyOr (whnf p)
whnf fail          = fail
whnf (p₁  p₂)     = whnf p₁ ∣W whnf p₂
whnf (toProc p κ)  = toProcW p (whnf κ)

-- Programs can be turned into processes.

mutual

  ⟦_⟧W : ProcW  Proc
   tokenBind p ⟧W = tokenBind  c     (p c) ⟧P)
   emptyOr p   ⟧W = emptyOr  p ⟧W
   fail        ⟧W = fail

  ⟦_⟧P : ProcP  Proc
   p ⟧P =  whnf p ⟧W

------------------------------------------------------------------------
-- Alternative backend

-- I have not proved that this implementation is correct.

infix 4 _∈?_

_∈?_ :  {n}  List Tok  P n  Bool
s ∈? p = run  toProc p (emptyOr fail) ⟧P s