Created
September 15, 2022 03:32
-
-
Save sjolsen/49581dc26519a08f5af6c67b428cbb5c to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| module Grammar where | |
| open import Category.Applicative | |
| open import Data.Char using (Char) | |
| open import Data.List using (List) | |
| open import Data.List.NonEmpty using (List⁺; map; foldl₁; fromList) | |
| open import Data.Maybe using (from-just) | |
| open import Data.Nat using (ℕ; _+_; _*_) | |
| open import Data.String using (String; toList) | |
| open import Data.Unit | |
| open import Function | |
| open import Level | |
| private | |
| variable | |
| ℓ : Level | |
| P : Set ℓ → Set ℓ | |
| i : Level | |
| I : Set i | |
| record ProductionRule (P : Set ℓ → Set ℓ) : Set (suc ℓ) where | |
| field | |
| alternative : RawAlternative P | |
| end : P (Lift _ ⊤) | |
| open RawAlternative alternative public | |
| open ProductionRule {{...}} public | |
| record RecProductionRule (P : Set ℓ → Set ℓ) {i} {I : Set i} (R : I → Set ℓ) : Set (suc ℓ ⊔ i) where | |
| field | |
| {{productionRule}} : ProductionRule P | |
| ⟨_⟩ : (ix : I) → P (R ix) | |
| open RecProductionRule {{...}} public | |
| record LoopProductionRule (P : Set ℓ → Set ℓ) {i} {I : Set i} (R : I → Set ℓ) : Set (suc ℓ ⊔ i) where | |
| field | |
| {{recProductionRule}} : RecProductionRule P R | |
| ⟨_⟩* : (ix : I) → P (List (R ix)) | |
| ⟨_⟩+ : (ix : I) → P (List⁺ (R ix)) | |
| open LoopProductionRule {{...}} public | |
| record TokenProductionRule (P : Set ℓ → Set ℓ) (T : Set ℓ) : Set (suc ℓ) where | |
| field | |
| token : T → P T | |
| open TokenProductionRule {{...}} public | |
| tokenRange : ∀ {T} → {{_ : ProductionRule P}} → {{_ : TokenProductionRule P T}} → List⁺ T → P T | |
| tokenRange = foldl₁ _∣_ ∘ map token | |
| PatternFunctor : ∀ ℓ → Set i → Set (suc ℓ ⊔ i) | |
| PatternFunctor ℓ I = (I → Set ℓ) → I → Set ℓ | |
| ExtendedContextFreeGrammar : ∀ {i} {I : Set i} → PatternFunctor ℓ I → Set ℓ → Set (suc ℓ ⊔ i) | |
| ExtendedContextFreeGrammar {I = I} pf T = ∀ {P R} | |
| → {{_ : LoopProductionRule P R}} | |
| → {{_ : TokenProductionRule P T}} | |
| → (ix : I) → P (pf R ix) | |
| Processor : ∀ {i} {I : Set i} → PatternFunctor ℓ I → (I → Set ℓ) → Set (ℓ ⊔ i) | |
| Processor {I = I} pf R = {ix : I} → pf R ix → R ix | |
| module Example where | |
| data ϕ : Set where | |
| Line Expr Term Factor Digit : ϕ | |
| data Calc (R : ϕ → Set ℓ) : ϕ → Set ℓ where | |
| line : R Expr → Calc R Line | |
| term : R Term → Calc R Expr | |
| sum : R Expr → R Term → Calc R Expr | |
| factor : R Factor → Calc R Term | |
| product : R Term → R Factor → Calc R Term | |
| paren : R Expr → Calc R Factor | |
| number : List⁺ (R Digit) → Calc R Factor | |
| digit : Char → Calc R Digit | |
| allDigits : List⁺ Char | |
| allDigits = from-just (fromList (toList "0123456789")) | |
| grammar : ExtendedContextFreeGrammar Calc Char | |
| grammar Line = line <$> ⟨ Expr ⟩ <⊛ end | |
| grammar Expr = term <$> ⟨ Term ⟩ | |
| ∣ sum <$> ⟨ Expr ⟩ <⊛ token '+' ⊛ ⟨ Term ⟩ | |
| grammar Term = factor <$> ⟨ Factor ⟩ | |
| ∣ product <$> ⟨ Term ⟩ <⊛ token '*' ⊛ ⟨ Factor ⟩ | |
| grammar Factor = paren <$ token '(' ⊛ ⟨ Expr ⟩ <⊛ token ')' | |
| ∣ number <$> ⟨ Digit ⟩+ | |
| grammar Digit = digit <$> tokenRange allDigits | |
| Eval : ϕ → Set | |
| Eval Line = ℕ | |
| Eval Expr = ℕ | |
| Eval Term = ℕ | |
| Eval Factor = ℕ | |
| Eval Digit = Char | |
| data ⟦⟧ : ϕ → Set where | |
| ⟦_⟧ : {ix : ϕ} → Eval ix → ⟦⟧ ix | |
| calc : Processor Calc ⟦⟧ | |
| calc (line ⟦ x ⟧) = ⟦ x ⟧ | |
| calc (term ⟦ x ⟧) = ⟦ x ⟧ | |
| calc (sum ⟦ a ⟧ ⟦ b ⟧) = ⟦ a + b ⟧ | |
| calc (factor ⟦ x ⟧) = ⟦ x ⟧ | |
| calc (product ⟦ a ⟧ ⟦ b ⟧) = ⟦ a * b ⟧ | |
| calc (paren ⟦ x ⟧) = ⟦ x ⟧ | |
| calc (number x) = {!!} | |
| calc (digit x) = {!!} |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment