27 function |
27 function |
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
28 decode' :: "bit list \<Rightarrow> rexp \<Rightarrow> (val * bit list)" |
29 where |
29 where |
30 "decode' ds ZERO = (Void, [])" |
30 "decode' ds ZERO = (Void, [])" |
31 | "decode' ds ONE = (Void, ds)" |
31 | "decode' ds ONE = (Void, ds)" |
32 | "decode' ds (CHAR d) = (Char d, ds)" |
32 | "decode' ds (CH d) = (Char d, ds)" |
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
33 | "decode' [] (ALT r1 r2) = (Void, [])" |
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
34 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))" |
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
35 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))" |
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
36 | "decode' ds (SEQ r1 r2) = (let (v1, ds') = decode' ds r1 in |
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
37 let (v2, ds'') = decode' ds' r2 in (Seq v1 v2, ds''))" |
86 |
86 |
87 |
87 |
88 datatype arexp = |
88 datatype arexp = |
89 AZERO |
89 AZERO |
90 | AONE "bit list" |
90 | AONE "bit list" |
91 | ACHAR "bit list" char |
91 | ACH "bit list" char |
92 | ASEQ "bit list" arexp arexp |
92 | ASEQ "bit list" arexp arexp |
93 | AALT "bit list" arexp arexp |
93 | AALT "bit list" arexp arexp |
94 | ASTAR "bit list" arexp |
94 | ASTAR "bit list" arexp |
95 |
95 |
96 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
96 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where |
97 "fuse bs AZERO = AZERO" |
97 "fuse bs AZERO = AZERO" |
98 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
98 | "fuse bs (AONE cs) = AONE (bs @ cs)" |
99 | "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c" |
99 | "fuse bs (ACH cs c) = ACH (bs @ cs) c" |
100 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2" |
100 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2" |
101 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
101 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2" |
102 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
102 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r" |
103 |
103 |
104 fun intern :: "rexp \<Rightarrow> arexp" where |
104 fun intern :: "rexp \<Rightarrow> arexp" where |
105 "intern ZERO = AZERO" |
105 "intern ZERO = AZERO" |
106 | "intern ONE = AONE []" |
106 | "intern ONE = AONE []" |
107 | "intern (CHAR c) = ACHAR [] c" |
107 | "intern (CH c) = ACH [] c" |
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
108 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
109 (fuse [S] (intern r2))" |
109 (fuse [S] (intern r2))" |
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
110 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
111 | "intern (STAR r) = ASTAR [] (intern r)" |
111 | "intern (STAR r) = ASTAR [] (intern r)" |
112 |
112 |
113 |
113 |
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
114 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where |
115 "retrieve (AONE bs) Void = bs" |
115 "retrieve (AONE bs) Void = bs" |
116 | "retrieve (ACHAR bs c) (Char d) = bs" |
116 | "retrieve (ACH bs c) (Char d) = bs" |
117 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" |
117 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v" |
118 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" |
118 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v" |
119 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
119 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2" |
120 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
120 | "retrieve (ASTAR bs r) (Stars []) = bs @ [S]" |
121 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
121 | "retrieve (ASTAR bs r) (Stars (v#vs)) = |
124 fun |
124 fun |
125 erase :: "arexp \<Rightarrow> rexp" |
125 erase :: "arexp \<Rightarrow> rexp" |
126 where |
126 where |
127 "erase AZERO = ZERO" |
127 "erase AZERO = ZERO" |
128 | "erase (AONE _) = ONE" |
128 | "erase (AONE _) = ONE" |
129 | "erase (ACHAR _ c) = CHAR c" |
129 | "erase (ACH _ c) = CH c" |
130 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)" |
130 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)" |
131 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
131 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
132 | "erase (ASTAR _ r) = STAR (erase r)" |
132 | "erase (ASTAR _ r) = STAR (erase r)" |
133 |
133 |
134 fun |
134 fun |
135 bnullable :: "arexp \<Rightarrow> bool" |
135 bnullable :: "arexp \<Rightarrow> bool" |
136 where |
136 where |
137 "bnullable (AZERO) = False" |
137 "bnullable (AZERO) = False" |
138 | "bnullable (AONE bs) = True" |
138 | "bnullable (AONE bs) = True" |
139 | "bnullable (ACHAR bs c) = False" |
139 | "bnullable (ACH bs c) = False" |
140 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)" |
140 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)" |
141 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
141 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)" |
142 | "bnullable (ASTAR bs r) = True" |
142 | "bnullable (ASTAR bs r) = True" |
143 |
143 |
144 fun |
144 fun |
153 fun |
153 fun |
154 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
154 bder :: "char \<Rightarrow> arexp \<Rightarrow> arexp" |
155 where |
155 where |
156 "bder c (AZERO) = AZERO" |
156 "bder c (AZERO) = AZERO" |
157 | "bder c (AONE bs) = AZERO" |
157 | "bder c (AONE bs) = AZERO" |
158 | "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)" |
158 | "bder c (ACH bs d) = (if c = d then AONE bs else AZERO)" |
159 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)" |
159 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)" |
160 | "bder c (ASEQ bs r1 r2) = |
160 | "bder c (ASEQ bs r1 r2) = |
161 (if bnullable r1 |
161 (if bnullable r1 |
162 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
162 then AALT bs (ASEQ [] (bder c r1) r2) (fuse (bmkeps r1) (bder c r2)) |
163 else ASEQ bs (bder c r1) r2)" |
163 else ASEQ bs (bder c r1) r2)" |