Mercurial > hg > Members > kono > Proof > automaton

changeset 7:f1fbe6603066

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
εAutomaton using Tree
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 14:37:11 +0900
parents 8e8bca295494
children cdf75ae6f0c1
files agda/automaton.agda agda/regex.agda
diffstat 2 files changed, 88 insertions(+), 66 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Aug 15 11:59:36 2018 +0900
+++ b/agda/automaton.agda	Wed Aug 15 14:37:11 2018 +0900
@@ -153,21 +153,43 @@
 ... | yes _ = true
 ... | no _ =  member n t
 
+
+data Tree (E : Set ) : Set where
+   empty :  Tree E
+   leaf :  ℕ → E → Tree E
+   node :  ℕ → E → Tree E  → Tree E → Tree E
+
+insertT :  {E : Set} → ℕ → E → Tree E → Tree E
+insertT {E} n e empty = leaf n e
+insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1 
+... | yes _ |  _ = leaf n e
+... | no _ | yes _  = node n e ( leaf n1 e1 ) empty
+... | no _ | no _  = node n e empty (  leaf n1 e1 )
+insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1
+... | yes _ |  _ = node n e left right
+... | no _ | yes _  = node n1 e1 ( insertT n e left ) right
+... | no _ | no _   = node n1 e1 left ( insertT n e right ) 
+
+memberT :  {E : Set } → ℕ → Tree E → Maybe E
+memberT _ empty = nothing
+memberT n (leaf n1 e) with n ≟ n1
+... | yes _ = just e
+... | no _ = nothing
+memberT n (node n1 e1 left right) with n ≟ n1 | n ≤? n1
+... | yes _ | _ = just e1
+memberT n (node n1 e1 left right) | no ¬p | (yes p) = memberT n left
+memberT n (node n1 e1 left right) | no ¬p | (no ¬p₁) = memberT n right
+
+
 record εAutomaton ( Q : Set ) ( Σ : Set  ) 
        : Set  where
     field
-          εδ : Q → Maybe Σ → List Q
+          εδ : Q → Maybe Σ → Tree Q
           εid : Q  →  ℕ
-          allState : List Q
+          allState : Tree Q
           εstart : Q
           εend  : Q → Bool 
 
-findSbyNum : {Q : Set } → ℕ → List Q → ( Q  →  ℕ )  → Maybe Q
-findSbyNum _ [] _ = nothing
-findSbyNum n ( s  ∷ t ) sid with sid s  ≟ n
-... | yes _ = just s
-... | no _ = findSbyNum n t sid
-
 open εAutomaton
 
 --
@@ -176,24 +198,26 @@
 --    if already tracked, skip it
 εclosure : { Q : Set } { Σ : Set  }
     → εAutomaton Q  Σ
-    → List ( List  ℕ )
-εclosure {Q} { Σ} M  = closure (  ℕList ( allState  M) )
+    → Tree ( Tree  Q )
+εclosure {Q} { Σ} M  = closure (  allState  M )
     where
-         ℕList : List Q  → List  ℕ
-         ℕList  [] = []
-         ℕList ( q  ∷ t  ) =  (εid M q ) ∷ ℕList t
-         closure2 :  List Q →  List ℕ →  List  ℕ 
-         closure2 [] C = C
-         closure2 ( n1  ∷ t  ) C with member (εid M n1) C
-         ... | false =  closure2 t ( (εid M n1)  ∷ C )
-         ... | true  =  closure2 t C
-         closure1 : ℕ →  List  ℕ 
-         closure1 n with findSbyNum n (allState  M) (εid M)
-         ... | nothing = []
-         ... | just q = closure2 (εδ M q nothing) [ n ]
-         closure :  List  ℕ → List ( List  ℕ )
-         closure [] = []
-         closure (n  ∷ t ) = ( closure1 n ∷ closure t )
+         closure2 :  Tree Q →  Tree Q →  Tree Q 
+         closure2 empty C = C
+         closure2 ( leaf n1 q ) C with memberT n1 C
+         ... | just _  =  C
+         ... | nothing =  insertT n1 q C 
+         closure2 ( node n1 q left right ) C with memberT n1 C
+         ... | just _  =  closure2 left ( closure2 right C )
+         ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
+         closure1 : ℕ →  Tree  Q 
+         closure1 n with memberT n (allState  M) 
+         ... | nothing = empty
+         ... | just q = closure2 (εδ M q nothing) ( leaf n q )
+         closure :  Tree Q  → Tree ( Tree  Q )
+         closure empty = empty
+         closure (leaf n e) = (leaf n (closure1 n)  )
+         closure (node n e left right) =
+              node n (closure1 n) ( closure left ) ( closure right ) 
 
 εAutomaton2U : { Q : Set } { Σ : Set  }
     → εAutomaton Q  Σ → NAutomaton Q  Σ
@@ -203,17 +227,14 @@
      nstart = εstart M  ;
      nend =  εend M
   } where
-     MList :  List ( List  ℕ )
-     MList = εclosure M
-     DummyUA : NAutomaton Q  Σ
-     DummyUA = record { nδ = λ n i → [] ;  sid = εid M ; nstart = εstart M  ; nend =  εend M  }
-     nδ1 : List  ℕ → Σ → List Q
-     nδ1 [] _ = []
-     nδ1 (h  ∷ t ) i with findSbyNum h ( allState  M) (εid M)
-     ... | nothing =  nδ1 t i
-     ... | just q = merge DummyUA ( εδ M q ( just i )) ( nδ1 t i )
+     MTree :  Tree ( Tree  Q )
+     MTree = εclosure M
+     nδ1 : Tree Q → Σ → List Q
+     nδ1 empty i = []
+     nδ1 (leaf n q) i = [ q ]
+     nδ1 (node n q left right) i = nδ1 left i ++ [ q ] ++ nδ1 right i
      nδ' : Q → Σ → List Q
-     nδ' q i with nth ( εid M q ) MList 
+     nδ' q i with memberT ( εid M q ) MTree
      ... | nothing = []
      ... | just x = nδ1 x i
 
--- a/agda/regex.agda	Wed Aug 15 11:59:36 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 14:37:11 2018 +0900
@@ -3,7 +3,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Fin
 open import Data.Nat
-open import Data.List 
+-- open import Data.List 
 open import Data.Maybe 
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
@@ -26,9 +26,10 @@
 
 record RST ( Σ : Set )
      : Set where
+   inductive
    field
       state :  ℕ
-      move  :  Maybe Σ → List ℕ
+      move  :  Maybe Σ → Tree (RST Σ)
       RSTend : Bool
 
 open RST
@@ -36,28 +37,37 @@
 record RNFA ( Σ : Set )
      : Set where
    field
-      Rstates : List ( RST Σ )
+      Rstates : Tree ( RST Σ )
       Rstart :   RST Σ
       Rend :   RST Σ
       Rnum :  ℕ
    
 open RNFA
 
-mergeℕ :  List ℕ → List ℕ → List ℕ
-mergeℕ [] L = L
-mergeℕ (h ∷ t ) L with member h L
-... | true = mergeℕ t L
-... | false =  h  ∷  mergeℕ t L
+[_] : { Σ : Set} → RST Σ  → Tree (RST Σ )
+[ x ] = leaf ( state x ) x
+
+[] : { Σ : Set} → Tree (RST Σ )
+[] = empty
+
+
+infixr 5 _++_ 
+
+_++_ : { Σ : Set} → Tree (RST Σ ) → Tree (RST Σ ) → Tree (RST Σ )
+empty ++ t = t
+leaf n e ++ t = insertT n e t
+node n e left right ++ t =
+        left ++ ( insertT n e  (right ++ t ) )
 
 generateRNFA :  { Σ : Set  } → ( Regex  Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) →  RNFA  Σ
 generateRNFA  {Σ} regex _≟_ = generate regex (
       record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
                                 Rend = record { state = 0 ; move = λ q → [] ; RSTend = true }  ; Rnum = 1 } )
  where
-  literal :  Maybe Σ →  Σ → ℕ → List ℕ
-  literal nothing _ _ = []
+  literal :  Maybe Σ →  Σ → ℕ → Tree (RST  Σ)
+  literal nothing  q' n = []
   literal (just q)  q' n with q ≟  q'
-  ... | yes _ = [ n ]
+  ... | yes _ = [ record { state = n ; move = λ i → empty ; RSTend = true  } ]
   ... | no _ = []
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
@@ -65,12 +75,12 @@
     where
        R' : RNFA Σ 
        R' = generate x R
-       move0 : Maybe Σ → List ℕ
-       move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
+       move0 : Maybe Σ → Tree (RST  Σ)
        move0 (just x) =  move (Rstart R') (just x )
-       move1 : Maybe Σ → List ℕ
-       move1 nothing = mergeℕ (move (Rstart R') nothing) (  state (Rend R')  ∷ state (Rend R')  ∷ [] ) 
+       move0 nothing = move (Rstart R') nothing ++ [ Rend R' ]
+       move1 : Maybe Σ → Tree (RST  Σ)
        move1 (just x) =  move (Rstart R') (just x )
+       move1 nothing = move (Rstart R') nothing ++  [ Rstart R' ]  ++ [ Rend R'  ]
   generate (x & y) R = record R1 { Rend = Rend R2 ;
                                    Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
     where
@@ -87,12 +97,12 @@
        S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] }
        R2 :  RNFA  Σ
        R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
-       move0 : Maybe Σ → List ℕ
-       move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
+       move0 : Maybe Σ → Tree (RST  Σ)
        move0 (just x) =  move (Rstart R1) (just x )
-       move1 : Maybe Σ → List ℕ
-       move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
+       move0 nothing = move (Rstart R1) nothing ++ [ Rstart R2 ]
+       move1 : Maybe Σ → Tree (RST  Σ)
        move1 (just x) =  move (Rend R1) (just x )
+       move1 nothing = move (Rend R1) nothing ++ [ Rend R2 ]
   generate < x > R = record R {
        Rnum = Rnum R + 1 ;
        Rstart = record {
@@ -100,21 +110,12 @@
              ; move = λ q → literal q x ( state (Rstart R) )
              ; RSTend = false
             } ;
-       Rstates =  Rstart R  ∷  Rstates R }
-
-moveRegex : { Σ : Set } → List (RST Σ)  → ( RST Σ → ℕ )  → RST  Σ  → Maybe Σ →   List (RST  Σ)
-moveRegex { Σ} L sid s i = toRST ( move s i )
-   where
-       toRST : List ℕ → List ( RST  Σ )
-       toRST [] = []
-       toRST (h  ∷ t ) with findSbyNum h L sid
-       ... | nothing = toRST t 
-       ... | just s = s ∷ toRST t 
-
+       Rstates =  [ Rstart R ] ++ Rstates R 
+     }
 
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
-      εδ = moveRegex ( Rstates G ) state
+      εδ =  move 
     ; εid = λ s → state s
     ; allState = Rstates G
     ; εstart =   Rstart G