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''))" |
109 fun |
109 fun |
110 erase :: "arexp \<Rightarrow> rexp" |
110 erase :: "arexp \<Rightarrow> rexp" |
111 where |
111 where |
112 "erase AZERO = ZERO" |
112 "erase AZERO = ZERO" |
113 | "erase (AONE _) = ONE" |
113 | "erase (AONE _) = ONE" |
114 | "erase (ACHAR _ c) = CHAR c" |
114 | "erase (ACHAR _ c) = CH c" |
115 | "erase (AALTs _ []) = ZERO" |
115 | "erase (AALTs _ []) = ZERO" |
116 | "erase (AALTs _ [r]) = (erase r)" |
116 | "erase (AALTs _ [r]) = (erase r)" |
117 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
117 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))" |
118 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
118 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)" |
119 | "erase (ASTAR _ r) = STAR (erase r)" |
119 | "erase (ASTAR _ r) = STAR (erase r)" |
163 |
163 |
164 |
164 |
165 fun intern :: "rexp \<Rightarrow> arexp" where |
165 fun intern :: "rexp \<Rightarrow> arexp" where |
166 "intern ZERO = AZERO" |
166 "intern ZERO = AZERO" |
167 | "intern ONE = AONE []" |
167 | "intern ONE = AONE []" |
168 | "intern (CHAR c) = ACHAR [] c" |
168 | "intern (CH c) = ACHAR [] c" |
169 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
169 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) |
170 (fuse [S] (intern r2))" |
170 (fuse [S] (intern r2))" |
171 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
171 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)" |
172 | "intern (STAR r) = ASTAR [] (intern r)" |
172 | "intern (STAR r) = ASTAR [] (intern r)" |
173 |
173 |