Skip to content

Commit 600b674

Browse files
stschaefstschaef
authored
Properties of grammars, make things opaque (#15)
* Rename top, epsilon, and bottom * negation def, move top->string into top.agda * Move kleenstar imports * Grammar.Properties for unambig, total parseability, decidability * initial/terminal defs. work towards umambig bot * strict initiality for bottom * initiality, monomorphism, parseability * parseablity to unambiguous, dec eq for strings, external unambiguity * progress toward unambiguous string and dfas * unambiguity' * string rename; remove search, decpropgrammar, parser; fix DFA examples * opaque for good goals. need distributive coproduct proofs * opaque fixes, distributive coproducts * need to make binop work with opaque. sync with main
1 parent 23be922 commit 600b674

33 files changed

+1671
-1285
lines changed

‎code/cubical/DFA/Base.agda

Lines changed: 25 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ open import Cubical.Foundations.Structure
88
open import Cubical.Relation.Nullary.DecidablePropositions
99

1010
open import Cubical.Data.FinSet
11+
open import Cubical.Data.Empty as Empty
1112

1213
open import Grammar Alphabet
1314
open import Grammar.Equivalence Alphabet
@@ -30,25 +31,19 @@ record DFA : Type (ℓ-suc ℓD) where
3031
isAcc negate q = negateDecProp (isAcc q)
3132
δ negate = δ
3233

33-
acc? : ⟨ Q ⟩ → Grammar ℓD
34-
acc? q = DecProp-grammar' {ℓG = ℓD} (isAcc q)
35-
36-
rej? : ⟨ Q ⟩ → Grammar ℓD
37-
rej? q = DecProp-grammar' {ℓG = ℓD} (negateDecProp (isAcc q))
38-
3934
module _ (q-end : ⟨ Q ⟩) where
4035
-- The grammar "Trace q" denotes the type of traces in the DFA
4136
-- from state q to q-end
4237
data Trace : (q : ⟨ Q ⟩) → Grammar ℓD where
43-
nil : ε-grammar ⊢ Trace q-end
38+
nil : ε ⊢ Trace q-end
4439
cons : ∀ q c →
4540
literal c ⊗ Trace (δ q c) ⊢ Trace q
4641

4742
record Algebra : Typeω where
4843
field
4944
the-ℓs : ⟨ Q ⟩ → Level
5045
G : (q : ⟨ Q ⟩) → Grammar (the-ℓs q)
51-
nil-case : ε-grammar ⊢ G q-end
46+
nil-case : ε ⊢ G q-end
5247
cons-case : ∀ q c →
5348
literal c ⊗ G (δ q c) ⊢ G q
5449

@@ -149,13 +144,31 @@ record DFA : Type (ℓ-suc ℓD) where
149144
algebra-η e = initial→initial≡id e _
150145

151146
module _ (q-start : ⟨ Q ⟩) where
147+
module _ (q-end : ⟨ Q ⟩) where
148+
AcceptingTrace : Grammar ℓD
149+
AcceptingTrace =
150+
LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
151+
152+
Parse = AcceptingTrace
153+
154+
RejectingTrace : Grammar ℓD
155+
RejectingTrace =
156+
LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
157+
152158
TraceFrom : Grammar ℓD
153159
TraceFrom = LinΣ[ q-end ∈ ⟨ Q ⟩ ] Trace q-end q-start
154160

155-
ParseFrom : Grammar ℓD
156-
ParseFrom =
157-
LinΣ[ q-end ∈ (Σ[ q ∈ ⟨ Q ⟩ ] isAcc q .fst .fst) ]
158-
Trace (q-end .fst) q-start
161+
AcceptingTraceFrom : Grammar ℓD
162+
AcceptingTraceFrom =
163+
LinΣ[ q-end ∈ ⟨ Q ⟩ ]
164+
LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
165+
166+
ParseFrom = AcceptingTraceFrom
167+
168+
RejectingTraceFrom : Grammar ℓD
169+
RejectingTraceFrom =
170+
LinΣ[ q-end ∈ ⟨ Q ⟩ ]
171+
LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
159172

160173
InitTrace : Grammar ℓD
161174
InitTrace = TraceFrom init

‎code/cubical/DFA/Decider.agda

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -5,21 +5,20 @@ module DFA.Decider (Alphabet : hSet ℓ-zero) where
55

66
open import Cubical.Foundations.Structure
77

8-
open import Cubical.Relation.Nullary.Base
8+
open import Cubical.Relation.Nullary.Base hiding (¬_)
99
open import Cubical.Relation.Nullary.Properties
1010
open import Cubical.Relation.Nullary.DecidablePropositions
1111

1212
open import Cubical.Data.FinSet
13-
open import Cubical.Data.Bool
13+
open import Cubical.Data.Bool hiding (_⊕_)
1414
open import Cubical.Data.Sum
1515
open import Cubical.Data.SumFin
1616
open import Cubical.Data.Unit
17-
open import Cubical.Data.Empty as ⊥
17+
open import Cubical.Data.Empty as Empty
1818
open import Cubical.Data.List hiding (init)
1919

2020
open import Grammar Alphabet
2121
open import Grammar.Equivalence Alphabet
22-
open import Grammar.KleeneStar Alphabet
2322
open import Term Alphabet
2423
open import DFA.Base Alphabet
2524
open import Helper
@@ -34,7 +33,7 @@ module _ (D : DFA {ℓD}) where
3433
open Algebra
3534
open AlgebraHom
3635

37-
run-from-state : string-grammar ⊢ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
36+
run-from-state : string ⊢ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
3837
run-from-state = foldKL*r char the-alg
3938
where
4039
the-alg : *r-Algebra char
@@ -51,18 +50,33 @@ module _ (D : DFA {ℓD}) where
5150
Trace.cons q c))
5251
∘g LinΠ-app (δ q c))))))
5352

54-
check-accept : {q-start : ⟨ Q ⟩} (q : ⟨ Q ⟩) →
55-
Trace q q-start ⊢ LinΣ[ b ∈ Bool ] TraceFrom q-start
53+
check-accept : {q-start : ⟨ Q ⟩} (q-end : ⟨ Q ⟩) →
54+
Trace q-end q-start ⊢
55+
AcceptingTrace q-start q-end ⊕ RejectingTrace q-start q-end
5656
check-accept q =
57-
LinΣ-intro
58-
(decRec (λ _ → true) (λ _ → false) (isAcc q .snd)) ∘g
59-
LinΣ-intro q
57+
decRec
58+
(λ acc → ⊕-inl ∘g LinΣ-intro acc)
59+
(λ rej → ⊕-inr ∘g LinΣ-intro rej)
60+
(isAcc q .snd)
6061

61-
run : string-grammar ⊢ InitTrace
62-
run = LinΠ-app init ∘g run-from-state
62+
check-accept-from : (q-start : ⟨ Q ⟩) →
63+
TraceFrom q-start ⊢
64+
AcceptingTraceFrom q-start ⊕ RejectingTraceFrom q-start
65+
check-accept-from q-start =
66+
LinΣ-elim (λ q-end →
67+
⊕-elim (⊕-inl ∘g LinΣ-intro q-end) (⊕-inr ∘g LinΣ-intro q-end) ∘g
68+
check-accept q-end)
6369

6470
decide :
65-
string-grammar ⊢ LinΣ[ b ∈ Bool ] InitTrace
71+
string ⊢
72+
LinΠ[ q ∈ ⟨ Q ⟩ ] (AcceptingTraceFrom q ⊕ RejectingTraceFrom q)
6673
decide =
67-
LinΣ-elim (λ q → check-accept q) ∘g
68-
run
74+
LinΠ-intro (λ q →
75+
check-accept-from q ∘g
76+
LinΠ-app q) ∘g
77+
run-from-state
78+
79+
decideInit :
80+
string ⊢
81+
(AcceptingTraceFrom init ⊕ RejectingTraceFrom init)
82+
decideInit = LinΠ-app init ∘g decide

‎code/cubical/DFA/Examples.agda

Lines changed: 74 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -10,84 +10,97 @@ open import Cubical.Relation.Nullary.Properties
1010
open import Cubical.Relation.Nullary.DecidablePropositions
1111

1212
open import Cubical.Data.FinSet
13-
open import Cubical.Data.Bool
14-
open import Cubical.Data.Sum
13+
open import Cubical.Data.Bool hiding (_⊕_)
14+
open import Cubical.Data.Sum as Sum
1515
open import Cubical.Data.SumFin
1616
open import Cubical.Data.Unit
17-
open import Cubical.Data.Empty as ⊥
17+
open import Cubical.Data.Empty as Empty hiding (⊥ ; ⊥*)
1818
open import Cubical.Data.List hiding (init)
1919

2020
Alphabet : hSet ℓ-zero
2121
Alphabet = (Fin 2) , (isFinSet→isSet isFinSetFin)
2222

2323
open import Grammar Alphabet
2424
open import Grammar.Equivalence Alphabet
25-
open import Grammar.KleeneStar Alphabet
2625
open import Term Alphabet
2726
open import DFA.Base Alphabet
2827
open import DFA.Decider Alphabet
2928
open import Helper
3029

30+
private
31+
variable
32+
ℓg ℓh : Level
33+
g : Grammar ℓg
34+
h : Grammar ℓh
35+
3136
module examples where
3237
-- examples are over alphabet drawn from Fin 2
3338
-- characters are fzero and (fsuc fzero)
3439

3540
open DFA
3641

37-
D : DFA
38-
D .Q = Fin 3 , isFinSetFin
39-
D .init = fzero
40-
D .isAcc fzero = (Unit , isPropUnit ) , yes _
41-
D .isAcc (fsuc x) = (⊥* , isProp⊥*) , no lower
42-
δ D fzero fzero = fromℕ 0
43-
δ D fzero (fsuc fzero) = fromℕ 1
44-
δ D (fsuc fzero) fzero = fromℕ 2
45-
δ D (fsuc fzero) (fsuc fzero) = fromℕ 0
46-
δ D (fsuc (fsuc fzero)) fzero = fromℕ 1
47-
δ D (fsuc (fsuc fzero)) (fsuc fzero) = fromℕ 2
48-
49-
w : String
50-
w = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fzero ∷ []
51-
52-
w' : String
53-
w' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
54-
55-
w'' : String
56-
w'' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
57-
58-
_ : decide D _ (⌈ w ⌉) .fst ≡ true
59-
_ = refl
60-
61-
_ : decide D _ (⌈ w' ⌉) .fst ≡ true
62-
_ = refl
63-
64-
_ : decide D _ ⌈ w'' ⌉ .fst ≡ false
65-
_ = refl
66-
67-
_ : decide D _ ⌈ [] ⌉ .fst ≡ true
68-
_ = refl
69-
70-
71-
{-- 0
72-
-- 0 --------> 1
73-
-- <--------
74-
-- 0
75-
-- and self loops for 1. state 1 is acc
76-
--
77-
--}
78-
D' : DFA
79-
Q D' = (Fin 2) , isFinSetFin
80-
init D' = inl _
81-
isAcc D' x =
82-
((x ≡ fsuc fzero) , isSetFin x (fsuc fzero)) ,
83-
discreteFin x (fsuc fzero)
84-
δ D' fzero fzero = fromℕ 1
85-
δ D' fzero (fsuc fzero) = fromℕ 0
86-
δ D' (fsuc fzero) fzero = fromℕ 0
87-
δ D' (fsuc fzero) (fsuc fzero) = fromℕ 1
88-
89-
s : String
90-
s = fsuc fzero ∷ fzero ∷ []
91-
92-
_ : decide D' _ ⌈ s ⌉ .fst ≡ true
93-
_ = refl
42+
opaque
43+
unfolding _⊕_ ⊕-elim ⊕-inl ⊕-inr ⟜-intro ⊸-intro
44+
is-inl : ∀ w → (g : Grammar ℓg) (h : Grammar ℓh) → (g ⊕ h) w → Bool
45+
is-inl w g h p = Sum.rec (λ _ → true) (λ _ → false) p
46+
47+
mktest : ∀ {ℓd} → String → DFA {ℓd} → Bool
48+
mktest w dfa =
49+
is-inl w
50+
(AcceptingTraceFrom dfa (dfa .init)) (RejectingTraceFrom dfa (dfa .init))
51+
((decideInit dfa ∘g (⌈w⌉→string {w = w})) w (internalize w))
52+
53+
D : DFA {ℓ-zero}
54+
D .Q = Fin 3 , isFinSetFin
55+
D .init = fzero
56+
D .isAcc fzero = (Unit , isPropUnit ) , yes _
57+
D .isAcc (fsuc x) = (Empty.⊥* , isProp⊥*) , no lower
58+
δ D fzero fzero = fromℕ 0
59+
δ D fzero (fsuc fzero) = fromℕ 1
60+
δ D (fsuc fzero) fzero = fromℕ 2
61+
δ D (fsuc fzero) (fsuc fzero) = fromℕ 0
62+
δ D (fsuc (fsuc fzero)) fzero = fromℕ 1
63+
δ D (fsuc (fsuc fzero)) (fsuc fzero) = fromℕ 2
64+
65+
w : String
66+
w = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fzero ∷ []
67+
68+
w' : String
69+
w' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
70+
71+
w'' : String
72+
w'' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
73+
74+
_ : mktest w' D ≡ true
75+
_ = refl
76+
77+
_ : mktest w'' D ≡ false
78+
_ = refl
79+
80+
_ : mktest [] D ≡ true
81+
_ = refl
82+
83+
84+
{-- 0
85+
-- 0 --------> 1
86+
-- <--------
87+
-- 0
88+
-- and self loops for 1. state 1 is acc
89+
--
90+
--}
91+
D' : DFA {ℓ-zero}
92+
Q D' = (Fin 2) , isFinSetFin
93+
init D' = inl _
94+
isAcc D' x =
95+
((x ≡ fsuc fzero) , isSetFin x (fsuc fzero)) ,
96+
discreteFin x (fsuc fzero)
97+
δ D' fzero fzero = fromℕ 1
98+
δ D' fzero (fsuc fzero) = fromℕ 0
99+
δ D' (fsuc fzero) fzero = fromℕ 0
100+
δ D' (fsuc fzero) (fsuc fzero) = fromℕ 1
101+
102+
s : String
103+
s = fsuc fzero ∷ fzero ∷ []
104+
105+
_ : mktest s D' ≡ true
106+
_ = refl

0 commit comments

Comments
 (0)