Mercurial > hg > Members > kono > Proof > automaton

comparison agda/regex.agda @ 5:f3de819eb3d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 11:25:46 +0900
parents 843f155846fb
children 8e8bca295494
comparison
equal deleted inserted replaced
4:843f155846fb 5:f3de819eb3d0
38 field 38 field
39 Rstates : List ( RST Σ ) 39 Rstates : List ( RST Σ )
40 Rstart : RST Σ 40 Rstart : RST Σ
41 Rend : RST Σ 41 Rend : RST Σ
42 Rnum : ℕ 42 Rnum : ℕ
43 43
44 open RNFA 44 open RNFA
45 45
46 mergeℕ : List ℕ → List ℕ → List ℕ 46 mergeℕ : List ℕ → List ℕ → List ℕ
47 mergeℕ [] L = L 47 mergeℕ [] L = L
48 mergeℕ (h ∷ t ) L with member h L 48 mergeℕ (h ∷ t ) L with member h L
70 move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ] 70 move0 nothing = mergeℕ (move (Rstart R') nothing) [ state (Rend R') ]
71 move0 (just x) = move (Rstart R') (just x ) 71 move0 (just x) = move (Rstart R') (just x )
72 move1 : Maybe Σ → List ℕ 72 move1 : Maybe Σ → List ℕ
73 move1 nothing = mergeℕ (move (Rstart R') nothing) ( state (Rend R') ∷ state (Rend R') ∷ [] ) 73 move1 nothing = mergeℕ (move (Rstart R') nothing) ( state (Rend R') ∷ state (Rend R') ∷ [] )
74 move1 (just x) = move (Rstart R') (just x ) 74 move1 (just x) = move (Rstart R') (just x )
75 generate (x & y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ; 75 generate (x & y) R = record R1 { Rend = Rend R2 ;
76 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 } 76 Rstates = Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 }
77 where 77 where
78 R2 : RNFA Σ 78 R2 : RNFA Σ
79 R2 = generate y R 79 R2 = generate y R
80 R1 : RNFA Σ 80 R1 : RNFA Σ
81 R1 = generate x ( record R2 { Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2 ; RSTend = false ; move = {!!} } } ) 81 R1 = generate x ( record R2 { Rstart = record (Rstart R1) { move = move0 } ; Rend = record (Rend R1) { move = move1 } } )
82 move0 : Maybe Σ → List ℕ 82 move0 : Maybe Σ → List ℕ
83 move0 nothing = mergeℕ (move (Rstart R2) nothing) [ state (Rend R2) ] 83 move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
84 move0 (just x) = {!!} 84 move0 (just x) = move (Rstart R1) (just x )
85 move1 : Maybe Σ → List ℕ
86 move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
87 move1 (just x) = move (Rend R1) (just x )
85 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ; 88 generate (x || y) R = record R1 { Rstart = Rstart R1 ; Rend = Rend R2 ;
86 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] } 89 Rstates = [ Rstart R1 ] ++ Rstates R1 ++ [ Rend R1 ] ++ [ Rstart R2 ] ++ Rstates R2 ++ [ Rend R2 ] }
87 where 90 where
88 R1 = generate x ( record R { Rnum = Rnum R + 1 ; Rend = Rstart R ; Rstart = record { state = Rnum R ; RSTend = false ; move = {!!} } } ) 91 S1 : RST Σ
89 R2 = generate y ( record R2 { Rnum = Rnum R2 + 1 ; Rend = Rstart R2 ; Rstart = record { state = Rnum R2 ; RSTend = false ; move = {!!} } } ) 92 S1 = record { state = Rnum R ; RSTend = RSTend R ; move = λ q → [] }
93 R1 = generate x ( record R { Rnum = Rnum R +1 } )
94 R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1 } )
95 move0 : Maybe Σ → List ℕ
96 move0 nothing = mergeℕ (move (Rstart R1) nothing) [ state (Rstart R2) ]
97 move0 (just x) = move (Rstart R1) (just x )
98 move1 : Maybe Σ → List ℕ
99 move1 nothing = mergeℕ (move (Rend R1) nothing) [ state (Rend R2) ]
100 move1 (just x) = move (Rend R1) (just x )
90 generate < x > R = record R { 101 generate < x > R = record R {
91 Rnum = Rnum R + 1 ; 102 Rnum = Rnum R + 1 ;
92 Rstates = Rstates R ++ ( 103 Rstart = record {
93 record {
94 state = Rnum R 104 state = Rnum R
95 ; move = λ q → listcase q x ( state (Rstart R) ) 105 ; move = λ q → listcase q x ( state (Rstart R) )
96 ; RSTend = false 106 ; RSTend = false
97 } ∷ [] ) } 107 }
98 108 Rstates = Rstart R ∷ Rstate R }
99 109
100 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2 110 regex2nfa : (regex : Regex In2 ) → εAutomaton (RST In2) In2
101 regex2nfa regex = record { 111 regex2nfa regex = record {
102 εδ = λ s i → {!!} -- move s i 112 εδ = λ s i → {!!} -- move s i
103 ; εid = λ s → state s 113 ; εid = λ s → state s