Total parser combinators in guarded cubical agda.

1-Parser.agda

{-# OPTIONS --guarded --rewriting --cubical -WnoUnsupportedIndexedMatch #-}

module 1-Parser where

open import 2-Guarded

open import Data.Product hiding (_<*>_)
open import Data.Char hiding (_≤_)
open import Data.Bool hiding (_≤_)
open import Function
open import Data.Nat
open import Data.List using (List ; _∷_ ; [] ; length ; null ; _++_)
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Properties
import Data.String

data ParseType : Set where
  ● : ParseType
  ○ : ParseType

variable ◐ ◐′ ◐₁ ◐₂ : ParseType

String : Set
String = List Char

str : Data.String.String → String
str = Data.String.toList

variable n n₁ n₂ m m₁ m₂ k k₁ k₂ : ℕ
         A B : Set
         P Q R : ℕ → Set
         s : String
         c : Char

data Result (A : Set) : ParseType → String → ℕ → Set where
    done : A → (s : String) → Result A ○ s n
    step : Result A ◐ s n → Result A ◐′ (c ∷ s) m
    skip : ▹ Result A ◐ s n → Result A ◐ s (1 + n)
    fail : Result A ◐ s n

wk1 : Result A ◐ s n → Result A ◐ s (1 + n)
wk1 (done x _) = done x _
wk1 (step r) = step r
wk1 (skip x) = skip (λ t → wk1 (x t))
wk1 fail = fail

diff : n ≤ m → ∃ λ k → k + n ≡ m
diff {m = m} z≤n = m , +-identityʳ m
diff (s≤s {m = m} x) with diff x
… | k , refl = k , +-suc k m

wkk : (k : ℕ) → Result A ◐ s n → Result A ◐ s (k + n)
wkk 0 = id
wkk (suc k) r = wk1 (wkk k r)

wk≤ : (n ≤ m) → Result A ◐ s n → Result A ◐ s m
wk≤ n≤m r with diff n≤m
… | k , refl = wkk k r

wkˡ : Result A ◐ s n → Result A ◐ s (n ⊔ m)
wkˡ = wk≤ (m≤m⊔n _ _)

wkʳ : Result A ◐ s m → Result A ◐ s (n ⊔ m)
wkʳ = wk≤ (m≤n⊔m _ _)

mapR : (A → B) → Result A ◐ s n → Result B ◐ s n
mapR f (done x s) = done (f x) s
mapR f (step x) = step (mapR f x)
mapR f (skip x) = skip (λ t → mapR f (x t))
mapR _ fail = fail

_⊓◐_ : ParseType → ParseType → ParseType
○ ⊓◐ ○ = ○
● ⊓◐ ○ = ○
○ ⊓◐ ● = ○
● ⊓◐ ● = ●

_⊔◐_ : ParseType → ParseType → ParseType
○ ⊔◐ ○ = ○
● ⊔◐ ○ = ●
○ ⊔◐ ● = ●
● ⊔◐ ● = ●

wk◐ˡ : Result A ◐ s n → Result A (◐ ⊓◐ ◐′) s n
wk◐ˡ {◐′ = ●} (done x _) = done x _
wk◐ˡ {◐′ = ○} (done x _) = done x _
wk◐ˡ {◐′ = ●} (step r) = step r
wk◐ˡ {◐′ = ○} (step r) = step r
wk◐ˡ {◐ = ●} {◐′ = ●} (skip r) = skip r
wk◐ˡ {◐ = ○} {◐′ = ●} (skip r) = skip r
wk◐ˡ {◐ = ●} {◐′ = ○} (skip r) = skip (λ t → wk◐ˡ {◐′ = ○} (r t))
wk◐ˡ {◐ = ○} {◐′ = ○} (skip r) = skip r
wk◐ˡ {◐′ = ●} fail = fail
wk◐ˡ {◐′ = ○} fail = fail

wk◐ʳ : Result A ◐′ s n → Result A (◐ ⊓◐ ◐′) s n
wk◐ʳ {◐′ = .○} {◐ = ●} (done x _) = done x _
wk◐ʳ {◐′ = .○} {◐ = ○} (done x _) = done x _
wk◐ʳ {◐′ = ◐′} {◐ = ●} (step r) = step r
wk◐ʳ {◐′ = ◐′} {◐ = ○} (step r) = step r
wk◐ʳ {◐′ = ●} {◐ = ●} (skip r) = skip r
wk◐ʳ {◐′ = ○} {◐ = ●} (skip r) = skip r
wk◐ʳ {◐′ = ●} {◐ = ○} (skip r) = skip λ t → wk◐ʳ {◐ = ○} (r t)
wk◐ʳ {◐′ = ○} {◐ = ○} (skip r) = skip r
wk◐ʳ {◐′ = ◐′} {◐ = ●} fail = fail
wk◐ʳ {◐′ = ◐′} {◐ = ○} fail = fail

orR : ∀{n} → Result A ◐ s n → Result A ◐′ s n → Result A (◐ ⊓◐ ◐′) s n
orR (done x s) q = wk◐ˡ (done x s)
orR {s = _ ∷ s} (step p) (done x (_ ∷ s)) = step (orR {s = s} p (done x s))                   -- s <
orR {s = _ ∷ s} {n = n} (step p) (step q) = step (orR (wkˡ p) (wkʳ q))                        -- s <
orR {◐ = ◐} {s = s} {n = suc n} (step p) (skip x)   = skip λ t → orR {◐ = ◐} {s = s} {n = n} (step p) (x t)   -- s =, n <
orR {s = s} {n = suc n} (skip p) (done x s) = skip λ t → orR {s = s} {n = n} (p t) (done x s) -- s =, n <
orR {s = s} {◐′ = ◐′} {n = suc n} (skip p) (step q)   = skip λ t → orR {s = s} {◐′ = ◐′} {n = n} (p t) (step q)   -- s =, n <
orR {s = s} {n = suc n} (skip p) (skip q)   = skip λ t → orR {s = s} {n = n} (p t) (q t)      -- s =, n <
orR (step p) fail = step p
orR (skip p) fail = wk◐ˡ (skip p)
orR fail q = wk◐ʳ q

if○_then_else_ : ParseType → ℕ → ℕ → ℕ
if○_then_else_ ○ _ n′ = n′
if○_then_else_ ● n _ = n

_>>=R_ : ∀{n n′} → Result A ◐ s n → (A → (s′ : String) → Result B ◐′ s′ n′) → Result B (◐ ⊔◐ ◐′) s (if○ ◐ then n else (n + n′))
_>>=R_ {◐′ = ●} {n = n} (done x s) k = wkk n (k x s)
_>>=R_ {◐′ = ○} {n = n} (done x s) k = wkk n (k x s)
_>>=R_ {◐′ = ●} (step p) k = step (p >>=R k)
_>>=R_ {◐′ = ○} (step p) k = step (p >>=R k)
_>>=R_ {◐ = ●} {◐′ = ●} (skip p) k = skip λ t → p t >>=R k
_>>=R_ {◐ = ●} {◐′ = ○} (skip p) k = skip λ t → p t >>=R k
_>>=R_ {◐ = ○} {◐′ = ●} (skip p) k = skip λ t → p t >>=R k
_>>=R_ {◐ = ○} {◐′ = ○} (skip p) k = skip λ t → p t >>=R k
_>>=R_ {◐′ = ●} fail _ = fail
_>>=R_ {◐′ = ○} fail _ = fail

record Parser (◐ : ParseType) (n : ℕ) (A : Set) : Set where
    field
        parse : (i : String) → Result A ◐ i n
open Parser

_<$>_ : (A → B) → Parser ◐ n A → Parser ◐ n B
(f <$> p) .parse s = mapR f (parse p s)

_<|>_ : Parser ◐ n A → Parser ◐′ n A → Parser (◐ ⊓◐ ◐′) n A
(p <|> q) .parse s = orR (parse p s) (parse q s) 

sat : (Char → Bool) → Parser ● 0 Char
sat f .parse [] = fail
sat f .parse (x ∷ s) = step {n = 0} (if f x then done x _ else fail)

_>>=_ : ∀{n n′} → Parser ◐ n A → (A → Parser ◐′ n′ B) → Parser (◐ ⊔◐ ◐′) (if○ ◐ then n else (n + n′)) B
(p >>= k) .parse s = parse p s >>=R λ x s′ → parse (k x) s′

digit : Parser ● 0 ℕ
digit = (λ c → ∣ toℕ c - toℕ '0' ∣) <$> sat isDigit

pure : A → Parser ○ n A
pure x .parse s = done x s

roll : ▹ Parser ◐ n A → Parser ◐ (1 + n) A
roll p .parse s = skip (λ t → parse (p t) s)

fixp : (Parser ◐ (suc n) A → Parser ◐ n A) → Parser ◐ n A
fixp f = fix (λ p → f (roll p))

dnat : Parser ● 0 (ℕ → ℕ)
dnat = fixp λ p → digit >>= (λ d → ((λ f n → f (n ∥ d)) <$> p) <|> pure (_∥ d))
  where
    _∥_ : ℕ → ℕ → ℕ
    n ∥ d = n * 10 + d

nat : Parser ● 0 ℕ
nat = (λ f → f 0) <$> dnat

ex : Result ℕ ● (str "123") 0
ex = parse nat _

expf : ex ≡ step (skip λ _ → step (skip λ _ → step (skip λ _ → done 123 [])))
expf = refl

2-Guarded.agda

-- copied from https://github.com/agda/agda/blob/172366db528b28fb2eda03c5fc9804f2cdb1be18/test/Succeed/LaterPrims.agda

{-# OPTIONS --cubical --guarded --rewriting #-}
module 2-Guarded where

open import Agda.Primitive
open import Agda.Primitive.Cubical renaming (itIsOne to 1=1)
open import Agda.Builtin.Cubical.Path
open import Agda.Builtin.Cubical.Sub renaming (Sub to _[_↦_]; primSubOut to outS)

import Agda.Builtin.Equality as Eq
open import Agda.Builtin.Equality.Rewrite

module Prims where
  primitive
    primLockUniv : Set₁

open Prims renaming (primLockUniv to LockU) public

private
  variable
    l : Level
    A B : Set l

-- We postulate Tick as it is supposed to be an abstract sort.
postulate
  Tick : LockU

▹_ : ∀ {l} → Set l → Set l
▹_ A = (@tick x : Tick) -> A

▸_ : ∀ {l} → ▹ Set l → Set l
▸ A = (@tick x : Tick) → A x

next : A → ▹ A
next x _ = x

_⊛_ : ▹ (A → B) → ▹ A → ▹ B
_⊛_ f x a = f a (x a)

map▹ : (f : A → B) → ▹ A → ▹ B
map▹ f x α = f (x α)

transpLater : ∀ (A : I → ▹ Set) → ▸ (A i0) → ▸ (A i1)
transpLater A u0 a = primTransp (\ i → A i a) i0 (u0 a)

transpLater-prim : (A : I → ▹ Set) → (x : ▸ (A i0)) → ▸ (A i1)
transpLater-prim A x = primTransp (\ i → ▸ (A i)) i0 x

transpLater-test : ∀ (A : I → ▹ Set) → (x : ▸ (A i0)) → transpLater-prim A x ≡ transpLater A x
transpLater-test A x = \ _ → transpLater-prim A x


hcompLater-prim : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → ▸ A
hcompLater-prim A φ u u0 a = primHComp (\ { i (φ = i1) → u i 1=1 a }) (outS u0 a)


hcompLater : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → ▸ A
hcompLater A φ u u0 = primHComp (\ { i (φ = i1) → u i 1=1 }) (outS u0)

hcompLater-test : ∀ (A : ▹ Set) φ (u : I → Partial φ (▸ A)) → (u0 : (▸ A) [ φ ↦ u i0 ]) → hcompLater A φ u u0 ≡ hcompLater-prim A φ u u0
hcompLater-test A φ u x = \ _ → hcompLater-prim A φ u x

ap : ∀ {A B : Set} (f : A → B) → ∀ {x y} → x ≡ y → f x ≡ f y
ap f eq = \ i → f (eq i)

_$>_ : ∀ {A B : Set} {f g : A → B} → f ≡ g → ∀ x → f x ≡ g x
eq $> x = \ i → eq i x
later-ext : ∀ {A : Set} → {f g : ▹ A} → (▸ \ α → f α ≡ g α) → f ≡ g
later-ext eq = \ i α → eq α i

postulate
  dfix : ∀ {l} {A : Set l} → (▹ A → A) → ▹ A
  pfix : ∀ {l} {A : Set l} (f : ▹ A → A) → dfix f ≡ (\ _ → f (dfix f))

pfix' : ∀ {l} {A : Set l} (f : ▹ A → A) → ▸ \ α → dfix f α ≡ f (dfix f)
pfix' f α i = pfix f i α

fix : ∀ {l} {A : Set l} → (▹ A → A) → A
fix f = f (dfix f)

postulate +dfix : ∀{f : ▹ A → A} → dfix f Eq.≡ next (f (dfix f))
{-# REWRITE +dfix #-}