Commit d8510caf authored by Heiko Becker's avatar Heiko Becker

Add simple pretty printer and start working on lexer lemma

parent bc345e35
......@@ -106,6 +106,77 @@ val lex_def = tDefine "lex" `
\\ fs [Once lexConst_def] \\ rfs []
\\ imp_res_tac (GSYM lexConst_imp) \\ fs [] \\ rveq \\ fs []);
val str_of_num_def = Define `
str_of_num (n:num) =
if n < 10 then STRING (CHR (n + 48)) ""
else STRING (CHR ( (n MOD 10) + 48)) (str_of_num (n DIV 10))`
val pp_token_def = Define `
pp_token (token:Token) =
case token of
| DLET => "Let"
| DRET => "Ret"
| DPRE => "PRE"
| DABS => "ABS"
| DCOND => "?"
| DVAR => "Var"
| DCONST num => str_of_num num
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
| DMUL => "*"
| DDIV => "/"
| DFRAC => "#"`;
val str_join_def = Define `
str_join s1 s2 =
case s1 of
| STRING c s1' => STRING c (str_join s1' s2)
| "" => s2`;
(* Pretty Printer for Tokens *)
val pp_def = Define `
pp (tokList:Token list) =
case tokList of
| token :: tokRest => str_join (pp_token token) (pp tokRest)
| NIL => ""`;
val lexConst_thm = prove (
``!s c akk s'. lexConst s akk = (c, s') ==> lexConst (str_join (str_of_num c) s') akk = (c, s')``,
cheat (*Induct
>- (once_rewrite_tac [lexConst_def]
\\ fs []
\\ once_rewrite_tac [str_of_num_def]
\\ rw [])
>- () *))
val lex_thm = prove (
``!s.
lex (pp (lex s)) = lex s``,
Induct
>- (EVAL_TAC)
>- (strip_tac
\\ qspec_then `STRING h s` (fn thm => rw [Once thm]) lex_def
>- (cheat)
>- (cheat)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"+" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"-" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"*" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"/" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"#" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"?" s` (fn thm => rw [Once thm]) lex_def)
>- (rw [Once pp_def, Once str_join_def, pp_token_def, Once str_join_def, Once lex_def]
\\ qspec_then `STRING #"~" s` (fn thm => rw [Once thm]) lex_def)
>- (qspec_then `STRING #" " s` (fn thm => rw [Once thm]) lex_def)
>- (qspec_then `STRING h s` (fn thm => rw [Once thm]) lex_def
\\ rw [Once pp_def, Once lex_def])));
val fix_res_def = Define `
fix_res xs NONE = NONE /\
fix_res xs (SOME (x,y)) =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment