Unambig

code/cubical/DFA/Base.agda

@@ -8,6 +8,7 @@ open import Cubical.Foundations.Structure
 open import Cubical.Relation.Nullary.DecidablePropositions
 
 open import Cubical.Data.FinSet
+open import Cubical.Data.Empty as Empty
 
 open import Grammar Alphabet
 open import Grammar.Equivalence Alphabet
@@ -30,25 +31,19 @@ record DFA : Type (ℓ-suc ℓD) where
   isAcc negate q = negateDecProp (isAcc q)
   δ negate = δ
 
-  acc? : ⟨ Q ⟩ → Grammar ℓD
-  acc? q = DecProp-grammar' {ℓG = ℓD} (isAcc q)
-
-  rej? : ⟨ Q ⟩ → Grammar ℓD
-  rej? q = DecProp-grammar' {ℓG = ℓD} (negateDecProp (isAcc q))
-
   module _ (q-end : ⟨ Q ⟩) where
     -- The grammar "Trace q" denotes the type of traces in the DFA
     -- from state q to q-end
     data Trace : (q : ⟨ Q ⟩) → Grammar ℓD where
-      nil : ε-grammar ⊢ Trace q-end
+      nil : ε ⊢ Trace q-end
       cons : ∀ q c →
         literal c ⊗ Trace (δ q c) ⊢ Trace q
 
     record Algebra : Typeω where
       field
         the-ℓs : ⟨ Q ⟩ → Level
         G : (q : ⟨ Q ⟩) → Grammar (the-ℓs q)
-        nil-case : ε-grammar ⊢ G q-end
+        nil-case : ε ⊢ G q-end
         cons-case : ∀ q c →
           literal c ⊗ G (δ q c) ⊢ G q
 
@@ -149,13 +144,31 @@ record DFA : Type (ℓ-suc ℓD) where
     algebra-η e = initial→initial≡id e _
 
   module _ (q-start : ⟨ Q ⟩) where
+    module _ (q-end : ⟨ Q ⟩) where
+      AcceptingTrace : Grammar ℓD
+      AcceptingTrace =
+        LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
+
+      Parse = AcceptingTrace
+
+      RejectingTrace : Grammar ℓD
+      RejectingTrace =
+        LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
+
     TraceFrom : Grammar ℓD
     TraceFrom = LinΣ[ q-end ∈ ⟨ Q ⟩ ] Trace q-end q-start
 
-    ParseFrom : Grammar ℓD
-    ParseFrom =
-      LinΣ[ q-end ∈ (Σ[ q ∈ ⟨ Q ⟩ ] isAcc q .fst .fst) ]
-        Trace (q-end .fst) q-start
+    AcceptingTraceFrom : Grammar ℓD
+    AcceptingTraceFrom =
+      LinΣ[ q-end ∈ ⟨ Q ⟩ ]
+        LinΣ[ acc ∈ ⟨ isAcc q-end .fst ⟩ ] Trace q-end q-start
+
+    ParseFrom = AcceptingTraceFrom
+
+    RejectingTraceFrom : Grammar ℓD
+    RejectingTraceFrom =
+      LinΣ[ q-end ∈ ⟨ Q ⟩ ]
+        LinΣ[ acc ∈ (⟨ isAcc q-end .fst ⟩ → Empty.⊥) ] Trace q-end q-start
 
   InitTrace : Grammar ℓD
   InitTrace = TraceFrom init

code/cubical/DFA/Decider.agda

@@ -5,21 +5,20 @@ module DFA.Decider (Alphabet : hSet ℓ-zero) where
 
 open import Cubical.Foundations.Structure
 
-open import Cubical.Relation.Nullary.Base
+open import Cubical.Relation.Nullary.Base hiding (¬_)
 open import Cubical.Relation.Nullary.Properties
 open import Cubical.Relation.Nullary.DecidablePropositions
 
 open import Cubical.Data.FinSet
-open import Cubical.Data.Bool
+open import Cubical.Data.Bool hiding (_⊕_)
 open import Cubical.Data.Sum
 open import Cubical.Data.SumFin
 open import Cubical.Data.Unit
-open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Empty as Empty
 open import Cubical.Data.List hiding (init)
 
 open import Grammar Alphabet
 open import Grammar.Equivalence Alphabet
-open import Grammar.KleeneStar Alphabet
 open import Term Alphabet
 open import DFA.Base Alphabet
 open import Helper
@@ -34,7 +33,7 @@ module _ (D : DFA {ℓD}) where
   open Algebra
   open AlgebraHom
 
-  run-from-state : string-grammar ⊢ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
+  run-from-state : string ⊢ LinΠ[ q ∈ ⟨ Q ⟩ ] TraceFrom q
   run-from-state = foldKL*r char the-alg
     where
     the-alg : *r-Algebra char
@@ -51,18 +50,33 @@ module _ (D : DFA {ℓD}) where
                   Trace.cons q c))
             ∘g LinΠ-app (δ q c))))))
 
-  check-accept : {q-start : ⟨ Q ⟩} (q : ⟨ Q ⟩) →
-    Trace q q-start ⊢ LinΣ[ b ∈ Bool ] TraceFrom q-start
+  check-accept : {q-start : ⟨ Q ⟩} (q-end : ⟨ Q ⟩) →
+    Trace q-end q-start ⊢
+      AcceptingTrace q-start q-end ⊕ RejectingTrace q-start q-end
   check-accept q =
-    LinΣ-intro
-      (decRec (λ _ → true) (λ _ → false) (isAcc q .snd)) ∘g
-    LinΣ-intro q
+    decRec
+      (λ acc → ⊕-inl ∘g LinΣ-intro acc)
+      (λ rej → ⊕-inr ∘g LinΣ-intro rej)
+      (isAcc q .snd)
 
-  run : string-grammar ⊢ InitTrace
-  run = LinΠ-app init ∘g run-from-state
+  check-accept-from : (q-start : ⟨ Q ⟩) →
+    TraceFrom q-start ⊢
+      AcceptingTraceFrom q-start ⊕ RejectingTraceFrom q-start
+  check-accept-from q-start =
+    LinΣ-elim (λ q-end →
+      ⊕-elim (⊕-inl ∘g LinΣ-intro q-end) (⊕-inr ∘g LinΣ-intro q-end) ∘g
+      check-accept q-end)
 
   decide :
-    string-grammar ⊢ LinΣ[ b ∈ Bool ] InitTrace
+    string ⊢
+      LinΠ[ q ∈ ⟨ Q ⟩ ] (AcceptingTraceFrom q ⊕ RejectingTraceFrom q)
   decide =
-    LinΣ-elim (λ q → check-accept q) ∘g
-    run
+    LinΠ-intro (λ q →
+      check-accept-from q ∘g
+      LinΠ-app q) ∘g
+    run-from-state
+
+  decideInit :
+    string ⊢
+      (AcceptingTraceFrom init ⊕ RejectingTraceFrom init)
+  decideInit = LinΠ-app init ∘g decide

code/cubical/DFA/Examples.agda

@@ -10,84 +10,97 @@ open import Cubical.Relation.Nullary.Properties
 open import Cubical.Relation.Nullary.DecidablePropositions
 
 open import Cubical.Data.FinSet
-open import Cubical.Data.Bool
-open import Cubical.Data.Sum
+open import Cubical.Data.Bool hiding (_⊕_)
+open import Cubical.Data.Sum as Sum
 open import Cubical.Data.SumFin
 open import Cubical.Data.Unit
-open import Cubical.Data.Empty as ⊥
+open import Cubical.Data.Empty as Empty hiding (⊥ ; ⊥*)
 open import Cubical.Data.List hiding (init)
 
 Alphabet : hSet ℓ-zero
 Alphabet = (Fin 2) , (isFinSet→isSet isFinSetFin)
 
 open import Grammar Alphabet
 open import Grammar.Equivalence Alphabet
-open import Grammar.KleeneStar Alphabet
 open import Term Alphabet
 open import DFA.Base Alphabet
 open import DFA.Decider Alphabet
 open import Helper
 
+private
+  variable
+    ℓg ℓh : Level
+    g : Grammar ℓg
+    h : Grammar ℓh
+
 module examples where
   -- examples are over alphabet drawn from Fin 2
   -- characters are fzero and (fsuc fzero)
 
   open DFA
 
-  D : DFA
-  D .Q = Fin 3 , isFinSetFin
-  D .init = fzero
-  D .isAcc fzero = (Unit , isPropUnit ) , yes _
-  D .isAcc (fsuc x) = (⊥* , isProp⊥*) , no lower
-  δ D fzero fzero = fromℕ 0
-  δ D fzero (fsuc fzero) = fromℕ 1
-  δ D (fsuc fzero) fzero = fromℕ 2
-  δ D (fsuc fzero) (fsuc fzero) = fromℕ 0
-  δ D (fsuc (fsuc fzero)) fzero = fromℕ 1
-  δ D (fsuc (fsuc fzero)) (fsuc fzero) = fromℕ 2
-
-  w : String
-  w = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fzero ∷ []
-
-  w' : String
-  w' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
-
-  w'' : String
-  w'' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
-
-  _ : decide D _ (⌈ w ⌉) .fst ≡ true
-  _ = refl
-
-  _ : decide D _ (⌈ w' ⌉) .fst ≡ true
-  _ = refl
-
-  _ : decide D _ ⌈ w'' ⌉ .fst ≡ false
-  _ = refl
-
-  _ : decide D _ ⌈ [] ⌉ .fst ≡ true
-  _ = refl
-
-
- {--       0
- -- 0  --------> 1
- --    <--------
- --        0
- -- and self loops for 1. state 1 is acc
- --
- --}
-  D' : DFA
-  Q D' = (Fin 2) , isFinSetFin
-  init D' = inl _
-  isAcc D' x =
-    ((x ≡ fsuc fzero) , isSetFin x (fsuc fzero)) ,
-    discreteFin x (fsuc fzero)
-  δ D' fzero fzero = fromℕ 1
-  δ D' fzero (fsuc fzero) = fromℕ 0
-  δ D' (fsuc fzero) fzero = fromℕ 0
-  δ D' (fsuc fzero) (fsuc fzero) = fromℕ 1
-
-  s : String
-  s = fsuc fzero ∷ fzero ∷ []
-
-  _ : decide D' _ ⌈ s ⌉ .fst ≡ true
-  _ = refl
+  opaque
+    unfolding _⊕_ ⊕-elim ⊕-inl ⊕-inr ⟜-intro ⊸-intro
+    is-inl : ∀ w → (g : Grammar ℓg) (h : Grammar ℓh) → (g ⊕ h) w → Bool
+    is-inl w g h p = Sum.rec (λ _ → true) (λ _ → false) p
+
+    mktest : ∀ {ℓd} → String → DFA {ℓd} → Bool
+    mktest w dfa =
+      is-inl w
+        (AcceptingTraceFrom dfa (dfa .init)) (RejectingTraceFrom dfa (dfa .init))
+        ((decideInit dfa ∘g (⌈w⌉→string {w = w})) w (internalize w))
+
+    D : DFA {ℓ-zero}
+    D .Q = Fin 3 , isFinSetFin
+    D .init = fzero
+    D .isAcc fzero = (Unit , isPropUnit ) , yes _
+    D .isAcc (fsuc x) = (Empty.⊥* , isProp⊥*) , no lower
+    δ D fzero fzero = fromℕ 0
+    δ D fzero (fsuc fzero) = fromℕ 1
+    δ D (fsuc fzero) fzero = fromℕ 2
+    δ D (fsuc fzero) (fsuc fzero) = fromℕ 0
+    δ D (fsuc (fsuc fzero)) fzero = fromℕ 1
+    δ D (fsuc (fsuc fzero)) (fsuc fzero) = fromℕ 2
+
+    w : String
+    w = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fzero ∷ []
+
+    w' : String
+    w' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
+
+    w'' : String
+    w'' = fzero ∷ fsuc fzero ∷ fsuc fzero ∷ fsuc fzero ∷ []
+
+    _ : mktest w' D ≡ true
+    _ = refl
+
+    _ : mktest w'' D ≡ false
+    _ = refl
+
+    _ : mktest [] D ≡ true
+    _ = refl
+
+
+   {--       0
+   -- 0  --------> 1
+   --    <--------
+   --        0
+   -- and self loops for 1. state 1 is acc
+   --
+   --}
+    D' : DFA {ℓ-zero}
+    Q D' = (Fin 2) , isFinSetFin
+    init D' = inl _
+    isAcc D' x =
+      ((x ≡ fsuc fzero) , isSetFin x (fsuc fzero)) ,
+      discreteFin x (fsuc fzero)
+    δ D' fzero fzero = fromℕ 1
+    δ D' fzero (fsuc fzero) = fromℕ 0
+    δ D' (fsuc fzero) fzero = fromℕ 0
+    δ D' (fsuc fzero) (fsuc fzero) = fromℕ 1
+
+    s : String
+    s = fsuc fzero ∷ fzero ∷ []
+
+    _ : mktest s D' ≡ true
+    _ = refl