equal
deleted
inserted
replaced
1 |
1 |
2 theory Lexer |
2 theory Lexer |
3 imports Spec |
3 imports Spec |
4 begin |
4 begin |
5 |
5 |
6 |
6 section {* The Lexer Functions by Sulzmann and Lu (without simplification) *} |
7 section {* The Lexer Functions by Sulzmann and Lu *} |
|
8 |
7 |
9 fun |
8 fun |
10 mkeps :: "rexp \<Rightarrow> val" |
9 mkeps :: "rexp \<Rightarrow> val" |
11 where |
10 where |
12 "mkeps(ONE) = Void" |
11 "mkeps(ONE) = Void" |
272 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
271 and "(lexer r s = None) \<longleftrightarrow> \<not>(\<exists>v. s \<in> r \<rightarrow> v)" |
273 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
272 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce |
274 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
273 using Posix1(1) lexer_correct_None lexer_correct_Some by blast |
275 |
274 |
276 |
275 |
277 |
276 subsection {* A slight reformulation of the lexer algorithm using stacked functions*} |
278 |
277 |
279 fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)" |
278 fun flex :: "rexp \<Rightarrow> (val \<Rightarrow> val) => string \<Rightarrow> (val \<Rightarrow> val)" |
280 where |
279 where |
281 "flex r f [] = f" |
280 "flex r f [] = f" |
282 | "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s" |
281 | "flex r f (c#s) = flex (der c r) (\<lambda>v. f (injval r c v)) s" |