module Mixfix.Cyclic.Lib where
open import Algebra
open import Codata.Musical.Notation
open import Function using (const)
open import Data.Bool using (Bool; true; false)
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Data.List using (List; []; _∷_; _++_)
import Data.List.Properties
private module LM {A : Set} = Monoid (Data.List.Properties.++-monoid A)
open import Data.List.NonEmpty using (List⁺; _∷_; [_]; _∷⁺_)
open import Data.Maybe using (Maybe; just; nothing; maybe)
open import Data.Vec using (Vec; []; _∷_)
open import Data.Product
import Data.String.Properties as String
open import Relation.Binary
open DecSetoid String.≡-decSetoid using (_≟_)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality as P using (_≡_; refl)
open import TotalParserCombinators.Parser
renaming (_⊛_ to _⊛′_; _<$>_ to _<$>′_)
import TotalParserCombinators.Lib as Lib
open import Mixfix.Operator using (NamePart)
private
open module Tok = Lib.Token NamePart _≟_ using (tok)
infix 55 _+
infixl 50 _⊛_ _⊛∞_ _<$>_
infixl 5 _∣_
infixr 5 _∥_
data ParserProg : Set → Set₁ where
fail : ∀ {R} → ParserProg R
_∣_ : ∀ {R}
(p₁ : ParserProg R)
(p₂ : ParserProg R) →
ParserProg R
_⊛_ : ∀ {R₁ R₂}
(p₁ : ParserProg (R₁ → R₂))
(p₂ : ParserProg R₁) →
ParserProg R₂
_⊛∞_ : ∀ {R₁ R₂}
(p₁ : ∞ (ParserProg (R₁ → R₂)))
(p₂ : ∞ (ParserProg R₁)) →
ParserProg R₂
_<$>_ : ∀ {R₁ R₂} (f : R₁ → R₂)
(p : ParserProg R₁) →
ParserProg R₂
_+ : ∀ {R} (p : ParserProg R) →
ParserProg (List⁺ R)
_between_ : ∀ {R n}
(p : ∞ (ParserProg R)) (toks : Vec NamePart (1 + n)) →
ParserProg (Vec R n)
_∥_ : ∀ {I i} {R : I → Set}
(p₁ : ParserProg (R i))
(p₂ : ParserProg (∃ R)) →
ParserProg (∃ R)
⟦_⟧ : ∀ {R} → ParserProg R → Parser NamePart R []
⟦ fail ⟧ = fail
⟦ p₁ ∣ p₂ ⟧ = ⟦ p₁ ⟧ ∣ ⟦ p₂ ⟧
⟦ p₁ ⊛ p₂ ⟧ = ⟦ p₁ ⟧ ⊛′ ⟦ p₂ ⟧
⟦ p₁ ⊛∞ p₂ ⟧ = ♯ ⟦ ♭ p₁ ⟧ ⊛′ ♯ ⟦ ♭ p₂ ⟧
⟦ f <$> p ⟧ = f <$>′ ⟦ p ⟧
⟦ p + ⟧ = one <$>′ ⟦ p ⟧
⊛′ ♯ (⟦ just <$> p + ⟧ ∣ return nothing)
where one = λ x → maybe (_∷⁺_ x) [ x ]
⟦ p between (t ∷ []) ⟧ = const [] <$>′ tok t
⟦ p between
(t ∷ t′ ∷ ts) ⟧ = const _∷_ <$>′ tok t
⊛′ ♯ ⟦ ♭ p ⟧
⊛′ ♯ ⟦ p between (t′ ∷ ts) ⟧
⟦ p₁ ∥ p₂ ⟧ = -,_ <$>′ ⟦ p₁ ⟧
∣ ⟦ p₂ ⟧
module Semantics where
open import TotalParserCombinators.Semantics as Sem
renaming ([_-_]_⊛_ to [_-_]_⊛′_)
infix 60 <$>_
infixl 50 _⊛_ _⊛∞_
infix 4 _∈⟦_⟧·_
data _∈⟦_⟧·_ : ∀ {R} → R → ParserProg R → List NamePart → Set₁ where
∣ˡ : ∀ {R x s}
{p₁ : ParserProg R} {p₂ : ParserProg R}
(x∈p₁ : x ∈⟦ p₁ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
∣ʳ : ∀ {R x s}
{p₁ : ParserProg R} {p₂ : ParserProg R}
(x∈p₂ : x ∈⟦ p₂ ⟧· s) → x ∈⟦ p₁ ∣ p₂ ⟧· s
_⊛_ : ∀ {s₁ s₂ R₁ R₂ f x}
{p₁ : ParserProg (R₁ → R₂)}
{p₂ : ParserProg R₁}
(f∈p₁ : f ∈⟦ p₁ ⟧· s₁)
(x∈p₂ : x ∈⟦ p₂ ⟧· s₂) →
f x ∈⟦ p₁ ⊛ p₂ ⟧· s₁ ++ s₂
_⊛∞_ : ∀ {s₁ s₂ R₁ R₂ f x}
{p₁ : ∞ (ParserProg (R₁ → R₂))}
{p₂ : ∞ (ParserProg R₁)}
(f∈p₁ : f ∈⟦ ♭ p₁ ⟧· s₁)
(x∈p₂ : x ∈⟦ ♭ p₂ ⟧· s₂) →
f x ∈⟦ p₁ ⊛∞ p₂ ⟧· s₁ ++ s₂
<$>_ : ∀ {s R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
(x∈p : x ∈⟦ p ⟧· s) → f x ∈⟦ f <$> p ⟧· s
+-[] : ∀ {R x s} {p : ParserProg R}
(x∈p : x ∈⟦ p ⟧· s) → [ x ] ∈⟦ p + ⟧· s
+-∷ : ∀ {R x s₁ s₂ xs} {p : ParserProg R}
(x∈p : x ∈⟦ p ⟧· s₁) (xs∈p : xs ∈⟦ p + ⟧· s₂) →
x ∷⁺ xs ∈⟦ p + ⟧· s₁ ++ s₂
between-[] : ∀ {R t} {p : ∞ (ParserProg R)} →
[] ∈⟦ p between (t ∷ []) ⟧· t ∷ []
between-∷ : ∀ {R n t x xs s₁ s₂}
{p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
(x∈p : x ∈⟦ ♭ p ⟧· s₁)
(xs∈⋯ : xs ∈⟦ p between ts ⟧· s₂) →
x ∷ xs ∈⟦ p between (t ∷ ts) ⟧· t ∷ s₁ ++ s₂
∥ˡ : ∀ {I i} {R : I → Set} {x s}
{p₁ : ParserProg (R i)}
{p₂ : ParserProg (∃ R)}
(x∈p₁ : x ∈⟦ p₁ ⟧· s) → (-, x) ∈⟦ p₁ ∥ p₂ ⟧· s
∥ʳ : ∀ {I i} {R : I → Set} {s i′} {x : R i′}
{p₁ : ParserProg (R i)}
{p₂ : ParserProg (∃ R)}
(x∈p₂ : (-, x) ∈⟦ p₂ ⟧· s) → (-, x) ∈⟦ p₁ ∥ p₂ ⟧· s
sound : ∀ {R x s} {p : ParserProg R} →
x ∈⟦ p ⟧· s → x ∈ ⟦ p ⟧ · s
sound (∣ˡ x∈p₁) = ∣-left (sound x∈p₁)
sound (∣ʳ x∈p₂) = ∣-right [] (sound x∈p₂)
sound (f∈p₁ ⊛ x∈p₂) = [ ○ - ○ ] sound f∈p₁ ⊛′ sound x∈p₂
sound (f∈p₁ ⊛∞ x∈p₂) = [ ◌ - ◌ ] sound f∈p₁ ⊛′ sound x∈p₂
sound (<$> x∈p) = <$> sound x∈p
sound (+-[] x∈p) = cast∈ refl refl (proj₂ LM.identity _)
([ ○ - ◌ ] <$> sound x∈p ⊛′ ∣-right [] return)
sound (+-∷ x∈p xs∈p) = [ ○ - ◌ ] <$> sound x∈p ⊛′ ∣-left (<$> sound xs∈p)
sound (∥ˡ x∈p₁) = ∣-left {x = (-, _)} (<$> sound x∈p₁)
sound (∥ʳ x∈p₂) = ∣-right [] (sound x∈p₂)
sound between-[] = <$> Tok.complete
sound (between-∷ {ts = _ ∷ _} x∈p xs∈⋯) =
[ ○ - ◌ ] [ ○ - ◌ ] <$> Tok.complete ⊛′ sound x∈p ⊛′ sound xs∈⋯
complete : ∀ {R x s} (p : ParserProg R) →
x ∈ ⟦ p ⟧ · s → x ∈⟦ p ⟧· s
complete fail ()
complete (p₁ ∣ p₂) (∣-left x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
complete (p₁ ∣ p₂) (∣-right .[] x∈p₂) = ∣ʳ (complete p₂ x∈p₂)
complete (p₁ ⊛ p₂) (f∈p₁ ⊛ y∈p₂) = complete p₁ f∈p₁ ⊛ complete p₂ y∈p₂
complete (p₁ ⊛∞ p₂) (f∈p₁ ⊛ y∈p₂) = complete (♭ p₁) f∈p₁ ⊛∞ complete (♭ p₂) y∈p₂
complete (f <$> p) (<$> x∈p) = <$> complete p x∈p
complete (p +) (<$> x∈p ⊛ ∣-left (<$> xs∈p+)) =
+-∷ (complete p x∈p) (complete (p +) xs∈p+)
complete (p +) (_⊛_ {s₁ = s} (<$> x∈p) (∣-right .[] return)) =
P.subst (λ s → _ ∈⟦ p + ⟧· s)
(P.sym (proj₂ LM.identity s))
(+-[] (complete p x∈p))
complete (p between (t ∷ [])) (<$> t∈) with Tok.sound t t∈
... | (refl , refl) = between-[]
complete (p between (t ∷ t′ ∷ ts)) (<$> t∈ ⊛ x∈p ⊛ xs∈)
with Tok.sound t t∈
... | (refl , refl) =
between-∷ (complete (♭ p) x∈p) (complete (p between (t′ ∷ ts)) xs∈)
complete (p₁ ∥ p₂) (∣-left (<$> x∈p₁)) = ∥ˡ (complete p₁ x∈p₁)
complete (p₁ ∥ p₂) (∣-right .[] x∈p₂) = ∥ʳ (complete p₂ x∈p₂)
module Semantics-⊕ where
open import TotalParserCombinators.Semantics.Continuation as ContSem
hiding (sound; complete)
infix 60 <$>_
infixl 50 _⊛_ _⊛∞_
infix 4 _⊕_∈⟦_⟧·_
data _⊕_∈⟦_⟧·_ : ∀ {R} →
R → List NamePart →
ParserProg R → List NamePart → Set₁ where
∣ˡ : ∀ {R x s s₁}
{p₁ : ParserProg R} {p₂ : ParserProg R}
(x∈p₁ : x ⊕ s₁ ∈⟦ p₁ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
∣ʳ : ∀ {R x s s₁}
{p₁ : ParserProg R} {p₂ : ParserProg R}
(x∈p₂ : x ⊕ s₁ ∈⟦ p₂ ⟧· s) → x ⊕ s₁ ∈⟦ p₁ ∣ p₂ ⟧· s
_⊛_ : ∀ {s s₁ s₂ R₁ R₂ f x}
{p₁ : ParserProg (R₁ → R₂)}
{p₂ : ParserProg R₁}
(f∈p₁ : f ⊕ s₁ ∈⟦ p₁ ⟧· s)
(x∈p₂ : x ⊕ s₂ ∈⟦ p₂ ⟧· s₁) →
f x ⊕ s₂ ∈⟦ p₁ ⊛ p₂ ⟧· s
_⊛∞_ : ∀ {s s₁ s₂ R₁ R₂ f x}
{p₁ : ∞ (ParserProg (R₁ → R₂))}
{p₂ : ∞ (ParserProg R₁)}
(f∈p₁ : f ⊕ s₁ ∈⟦ ♭ p₁ ⟧· s)
(x∈p₂ : x ⊕ s₂ ∈⟦ ♭ p₂ ⟧· s₁) →
f x ⊕ s₂ ∈⟦ p₁ ⊛∞ p₂ ⟧· s
<$>_ : ∀ {s s′ R₁ R₂ x} {f : R₁ → R₂} {p : ParserProg R₁}
(x∈p : x ⊕ s′ ∈⟦ p ⟧· s) → f x ⊕ s′ ∈⟦ f <$> p ⟧· s
+-[] : ∀ {R x s s₁} {p : ParserProg R}
(x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) → [ x ] ⊕ s₁ ∈⟦ p + ⟧· s
+-∷ : ∀ {R x s s₁ s₂ xs} {p : ParserProg R}
(x∈p : x ⊕ s₁ ∈⟦ p ⟧· s) (xs∈p : xs ⊕ s₂ ∈⟦ p + ⟧· s₁) →
x ∷⁺ xs ⊕ s₂ ∈⟦ p + ⟧· s
between-[] : ∀ {R t s} {p : ∞ (ParserProg R)} →
[] ⊕ s ∈⟦ p between (t ∷ []) ⟧· t ∷ s
between-∷ : ∀ {R n t x xs s s₁ s₂}
{p : ∞ (ParserProg R)} {ts : Vec NamePart (suc n)}
(x∈p : x ⊕ s₁ ∈⟦ ♭ p ⟧· s)
(xs∈⋯ : xs ⊕ s₂ ∈⟦ p between ts ⟧· s₁) →
x ∷ xs ⊕ s₂ ∈⟦ p between (t ∷ ts) ⟧· t ∷ s
∥ˡ : ∀ {I i} {R : I → Set} {x s s′}
{p₁ : ParserProg (R i)}
{p₂ : ParserProg (∃ R)}
(x∈p₁ : x ⊕ s′ ∈⟦ p₁ ⟧· s) →
(-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s
∥ʳ : ∀ {I i} {R : I → Set} {s s′ i′} {x : R i′}
{p₁ : ParserProg (R i)}
{p₂ : ParserProg (∃ R)}
(x∈p₂ : (-, x) ⊕ s′ ∈⟦ p₂ ⟧· s) →
(-, x) ⊕ s′ ∈⟦ p₁ ∥ p₂ ⟧· s
tok-sound : ∀ t {t′ s₁ s} →
t′ ⊕ s₁ ∈ tok t · s →
t ≡ t′ × s ≡ t′ ∷ s₁
tok-sound t ∈ with ContSem.sound′ ∈
tok-sound t ∈ | (s , refl , ∈′) with Tok.sound t ∈′
tok-sound t ∈ | (.(t ∷ []) , refl , ∈′) | (refl , refl) = (refl , refl)
tok-complete : ∀ {t s} → t ⊕ s ∈ tok t · t ∷ s
tok-complete = ContSem.complete′ (_ , refl , Tok.complete)
sound : ∀ {R x s s′} {p : ParserProg R} →
x ⊕ s′ ∈⟦ p ⟧· s → x ⊕ s′ ∈ ⟦ p ⟧ · s
sound (∣ˡ x∈p₁) = ∣-left (sound x∈p₁)
sound (∣ʳ x∈p₂) = ∣-right [] (sound x∈p₂)
sound (f∈p₁ ⊛ x∈p₂) = [ ○ - ○ ] sound f∈p₁ ⊛ sound x∈p₂
sound (f∈p₁ ⊛∞ x∈p₂) = [ ◌ - ◌ ] sound f∈p₁ ⊛ sound x∈p₂
sound (<$> x∈p) = <$> sound x∈p
sound (+-[] x∈p) = [ ○ - ◌ ] <$> sound x∈p ⊛ ∣-right [] return
sound (+-∷ x∈p xs∈p) = [ ○ - ◌ ] <$> sound x∈p ⊛ ∣-left (<$> sound xs∈p)
sound (∥ˡ x∈p₁) = ∣-left {x = (-, _)} (<$> sound x∈p₁)
sound (∥ʳ x∈p₂) = ∣-right [] (sound x∈p₂)
sound between-[] = <$> tok-complete
sound (between-∷ {ts = _ ∷ _} x∈p xs∈⋯) =
[ ○ - ◌ ] [ ○ - ◌ ] <$> tok-complete ⊛ sound x∈p ⊛ sound xs∈⋯
complete : ∀ {R x s s′} (p : ParserProg R) →
x ⊕ s′ ∈ ⟦ p ⟧ · s → x ⊕ s′ ∈⟦ p ⟧· s
complete fail ()
complete (p₁ ∣ p₂) (∣-left x∈p₁) = ∣ˡ (complete p₁ x∈p₁)
complete (p₁ ∣ p₂) (∣-right .[] x∈p₂) = ∣ʳ (complete p₂ x∈p₂)
complete (p₁ ⊛ p₂) ([ .○ - .○ ] f∈p₁ ⊛ y∈p₂) = complete p₁ f∈p₁ ⊛ complete p₂ y∈p₂
complete (p₁ ⊛∞ p₂) ([ .◌ - .◌ ] f∈p₁ ⊛ y∈p₂) = complete (♭ p₁) f∈p₁ ⊛∞ complete (♭ p₂) y∈p₂
complete (f <$> p) (<$> x∈p) = <$> complete p x∈p
complete (p +) ([ .○ - .◌ ] <$> x∈p ⊛ ∣-left (<$> xs∈p+)) = +-∷ (complete p x∈p) (complete (p +) xs∈p+)
complete (p +) ([ .○ - .◌ ] <$> x∈p ⊛ ∣-right .[] return) = +-[] (complete p x∈p)
complete (p between (t ∷ [])) (<$> t∈) with tok-sound t t∈
... | (refl , refl) = between-[]
complete (p between (t ∷ t′ ∷ ts)) ([ .○ - .◌ ] [ .○ - .◌ ] <$> t∈ ⊛ x∈p ⊛ xs∈)
with tok-sound t t∈
... | (refl , refl) =
between-∷ (complete (♭ p) x∈p) (complete (p between (t′ ∷ ts)) xs∈)
complete (p₁ ∥ p₂) (∣-left (<$> x∈p₁)) = ∥ˡ (complete p₁ x∈p₁)
complete (p₁ ∥ p₂) (∣-right .[] x∈p₂) = ∥ʳ (complete p₂ x∈p₂)