module nfa-list where open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Data.List open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) data States1 : Set where sr : States1 ss : States1 st : States1 data In2 : Set where i0 : In2 i1 : In2 transition1 : States1 → In2 → States1 transition1 sr i0 = sr transition1 sr i1 = ss transition1 ss i0 = sr transition1 ss i1 = st transition1 st i0 = sr transition1 st i1 = st fin1 : States1 → Bool fin1 st = true fin1 _ = false s1id : States1 → ℕ s1id sr = 0 s1id ss = 1 s1id st = 2 record NAutomaton ( Q : Set ) ( Σ : Set ) : Set where field nδ : Q → Σ → List Q sid : Q → ℕ nstart : Q nend : Q → Bool open NAutomaton insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q insert M [] q = q ∷ [] insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') ... | yes _ = insert M T q' ... | no _ = q ∷ (insert M T q' ) merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q merge M L1 [] = L1 merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H Nmoves : { Q : Set } { Σ : Set } → NAutomaton Q Σ → List Q → List Σ → List Q Nmoves {Q} { Σ} M q L = Nmoves1 q L [] where Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q Nmoves1 q [] _ = q Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) Naccept : { Q : Set } { Σ : Set } → NAutomaton Q Σ → List Σ → Bool Naccept {Q} { Σ} M L = checkAccept ( Nmoves M ((nstart M) ∷ [] ) L ) where checkAccept : (q : List Q ) → Bool checkAccept [] = false checkAccept ( H ∷ L ) with (nend M) H ... | true = true ... | false = checkAccept L transition2 : States1 → In2 → List States1 transition2 sr i0 = (sr ∷ []) transition2 sr i1 = (ss ∷ sr ∷ [] ) transition2 ss i0 = (sr ∷ []) transition2 ss i1 = (st ∷ []) transition2 st i0 = (sr ∷ []) transition2 st i1 = (st ∷ []) am2 : NAutomaton States1 In2 am2 = record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1} example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] ) example2-2 = Naccept am2 ( i1 ∷ i1 ∷ i1 ∷ [] )