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''))" |