-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Equalizers, Dyck Trace Strong equiv, inductive strings, generic deter…
…minsitic automata (#26) * add an equalizer grammar * Finish the Dyck =~ Trace proof up to monoidal category lemmas in LinearProduct.agda * deduplicate quiver code for reachability * detangle imports, epsilon*, literal* * port over string definition to indexed inductives * deterministic automata * delete simple inductives --------- Co-authored-by: Max New <[email protected]>
- Loading branch information
Showing
42 changed files
with
1,930 additions
and
2,032 deletions.
There are no files selected for viewing
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,106 @@ | ||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.HLevels | ||
|
|
||
| module Automaton.Deterministic (Alphabet : hSet ℓ-zero) where | ||
|
|
||
| open import Cubical.Foundations.Structure | ||
|
|
||
| open import Cubical.Relation.Nullary.DecidablePropositions | ||
|
|
||
| open import Cubical.Data.FinSet | ||
| open import Cubical.Data.Bool | ||
|
|
||
| open import Grammar Alphabet | ||
| open import Grammar.String.Properties Alphabet | ||
| open import Grammar.Inductive.Indexed Alphabet | ||
| open import Grammar.Equivalence.Base Alphabet | ||
| import Cubical.Data.Equality as Eq | ||
| open import Term Alphabet | ||
| open import Helper | ||
|
|
||
| private | ||
| variable | ||
| ℓ : Level | ||
|
|
||
| record DeterministicAutomaton (Q : Type ℓ) : Type (ℓ-suc ℓ) where | ||
| field | ||
| init : Q | ||
| isAcc : Q → Bool | ||
| δ : Q → ⟨ Alphabet ⟩ → Q | ||
|
|
||
| data Tag : Type ℓ where | ||
| stop step : Tag | ||
|
|
||
| TraceTy : Bool → (q : Q) → Functor Q | ||
| TraceTy b q = ⊕e Tag λ { | ||
| stop → ⊕e (Lift (b Eq.≡ isAcc q)) λ { (lift acc) → k ε* } | ||
| ; step → ⊕e (Lift ⟨ Alphabet ⟩) (λ { (lift c) → ⊗e (k (literal* c)) (Var (δ q c)) }) } | ||
|
|
||
| Trace : Bool → (q : Q) → Grammar ℓ | ||
| Trace b = μ (TraceTy b) | ||
|
|
||
| open StrongEquivalence | ||
| parseAlg : Algebra (*Ty char) λ _ → &[ q ∈ Q ] ⊕[ b ∈ Bool ] Trace b q | ||
| parseAlg _ = ⊕ᴰ-elim (λ { | ||
| nil → &ᴰ-in (λ q → | ||
| ⊕ᴰ-in (isAcc q) ∘g | ||
| roll ∘g ⊕ᴰ-in stop ∘g ⊕ᴰ-in (lift Eq.refl) ∘g | ||
| liftG ∘g liftG ∘g lowerG ∘g lowerG) | ||
| ; cons → &ᴰ-in (λ q → ( | ||
| ⊕ᴰ-elim (λ c → | ||
| ⊕ᴰ-elim (λ b → ⊕ᴰ-in b ∘g roll ∘g ⊕ᴰ-in step ∘g ⊕ᴰ-in (lift c) ∘g (liftG ∘g liftG) ,⊗ liftG) | ||
| ∘g ⊕ᴰ-distR .fun | ||
| ∘g id ,⊗ &ᴰ-π (δ q c)) | ||
| ∘g ⊕ᴰ-distL .fun) | ||
| ∘g lowerG ,⊗ lowerG) }) | ||
|
|
||
| parse : string ⊢ &[ q ∈ Q ] ⊕[ b ∈ Bool ] Trace b q | ||
| parse = rec (*Ty char) parseAlg _ | ||
|
|
||
| printAlg : ∀ b → Algebra (TraceTy b) (λ _ → string) | ||
| printAlg b q = ⊕ᴰ-elim λ { | ||
| stop → ⊕ᴰ-elim (λ { (lift Eq.refl) → NIL ∘g lowerG ∘g lowerG }) | ||
| ; step → CONS ∘g ⊕ᴰ-elim (λ { (lift c) → ⊕ᴰ-in c ,⊗ id ∘g (lowerG ∘g lowerG) ,⊗ lowerG }) } | ||
|
|
||
| print : ∀ b → (q : Q) → Trace b q ⊢ string | ||
| print b q = rec (TraceTy b) (printAlg b) q | ||
|
|
||
| ⊕ᴰAlg : ∀ b → Algebra (TraceTy b) (λ q → ⊕[ b ∈ Bool ] Trace b q) | ||
| ⊕ᴰAlg b q = ⊕ᴰ-elim (λ { | ||
| stop → ⊕ᴰ-elim (λ { (lift Eq.refl) → ⊕ᴰ-in b ∘g roll ∘g ⊕ᴰ-in stop ∘g ⊕ᴰ-in (lift Eq.refl) }) | ||
| ; step → ⊕ᴰ-elim (λ c → | ||
| ⊕ᴰ-elim (λ b → ⊕ᴰ-in b ∘g roll ∘g ⊕ᴰ-in step ∘g ⊕ᴰ-in c ∘g (liftG ∘g liftG) ,⊗ liftG) | ||
| ∘g ⊕ᴰ-distR .fun ∘g (lowerG ∘g lowerG) ,⊗ lowerG) }) | ||
|
|
||
| Trace≅string : (q : Q) → StrongEquivalence (⊕[ b ∈ Bool ] Trace b q) string | ||
| Trace≅string q .fun = ⊕ᴰ-elim (λ b → print b q) | ||
| Trace≅string q .inv = &ᴰ-π q ∘g parse | ||
| Trace≅string q .sec = unambiguous-string _ _ | ||
| Trace≅string q .ret = isRetract | ||
| where | ||
| opaque | ||
| unfolding ⊕ᴰ-distR ⊕ᴰ-distL ⊗-intro | ||
| isRetract : &ᴰ-π q ∘g parse ∘g ⊕ᴰ-elim (λ b → print b q) ≡ id | ||
| isRetract = ⊕ᴰ≡ _ _ λ b → | ||
| ind' | ||
| (TraceTy b) | ||
| (⊕ᴰAlg b) | ||
| ((λ q' → &ᴰ-π q' ∘g parse ∘g print b q') , | ||
| λ q' → ⊕ᴰ≡ _ _ (λ { | ||
| stop → funExt λ w → funExt λ { | ||
| ((lift Eq.refl) , p) → refl} | ||
| ; step → ⊕ᴰ≡ _ _ (λ { (lift c) → refl }) | ||
| })) | ||
| ((λ q' → ⊕ᴰ-in b) , | ||
| λ q' → ⊕ᴰ≡ _ _ λ { | ||
| stop → funExt (λ w → funExt λ { | ||
| ((lift Eq.refl) , p) → refl}) | ||
| ; step → refl }) | ||
| q | ||
|
|
||
| unambiguous-⊕Trace : ∀ q → unambiguous (⊕[ b ∈ Bool ] Trace b q) | ||
| unambiguous-⊕Trace q = | ||
| unambiguous≅ (sym-strong-equivalence (Trace≅string q)) unambiguous-string | ||
|
|
||
| unambiguous-Trace : ∀ b q → unambiguous (Trace b q) | ||
| unambiguous-Trace b q = unambiguous⊕ᴰ isSetBool (unambiguous-⊕Trace q) b |
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
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
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
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,42 +1,19 @@ | ||
| open import Cubical.Foundations.Prelude | ||
| open import Cubical.Foundations.HLevels | ||
|
|
||
| module DFA.Base (Alphabet : hSet ℓ-zero) where | ||
|
|
||
| open import Cubical.Foundations.Structure | ||
|
|
||
| open import Cubical.Relation.Nullary.DecidablePropositions | ||
| module DFA.Base (Alphabet : hSet ℓ-zero) where | ||
|
|
||
| open import Cubical.Data.FinSet | ||
| open import Cubical.Data.Bool | ||
|
|
||
| open import Grammar Alphabet | ||
| open import Grammar.Lift Alphabet | ||
| open import Grammar.Inductive.Indexed Alphabet | ||
| open import Grammar.Equivalence Alphabet | ||
| import Cubical.Data.Equality as Eq | ||
| open import Term Alphabet | ||
| open import Helper | ||
| open import Automaton.Deterministic Alphabet public | ||
|
|
||
| private | ||
| variable ℓD ℓP ℓ : Level | ||
|
|
||
| record DFA ℓD : Type (ℓ-suc ℓD) where | ||
| field | ||
| Q : FinSet ℓD | ||
| init : ⟨ Q ⟩ | ||
| isAcc : ⟨ Q ⟩ → Bool | ||
| δ : ⟨ Q ⟩ → ⟨ Alphabet ⟩ → ⟨ Q ⟩ | ||
|
|
||
| data TraceTag : Type ℓD where | ||
| stop step : TraceTag | ||
| variable | ||
| ℓD : Level | ||
|
|
||
| TraceTy : Bool → (q : ⟨ Q ⟩) → Functor ⟨ Q ⟩ | ||
| TraceTy b q = ⊕e TraceTag λ { | ||
| stop → ⊕e (Lift (b Eq.≡ isAcc q)) | ||
| (λ (lift acc) → k (LiftG ℓD ε) ) | ||
| ; step → ⊕e (Lift ⟨ Alphabet ⟩) | ||
| λ { (lift c) → ⊗e (k (LiftG ℓD (literal c))) (Var (δ q c)) }} | ||
| open DeterministicAutomaton | ||
|
|
||
| Trace : Bool → (q : ⟨ Q ⟩) → Grammar ℓD | ||
| Trace b = μ (TraceTy b) | ||
| DFA : FinSet ℓD → Type (ℓ-suc ℓD) | ||
| DFA Q = DeterministicAutomaton ⟨ Q ⟩ |
This file was deleted.
Oops, something went wrong.
Oops, something went wrong.