Commit 70e00619 authored by Heiko Becker's avatar Heiko Becker

Fix parser in HOL4

parent 088816d1
...@@ -19,7 +19,8 @@ val _ = Datatype ` ...@@ -19,7 +19,8 @@ val _ = Datatype `
| DSUB | DSUB
| DMUL | DMUL
| DDIV | DDIV
| DFRAC`; | DFRAC
| DCAST `;
val getConst_def = Define ` val getConst_def = Define `
getConst (c:char) = ORD c - 48`; getConst (c:char) = ORD c - 48`;
...@@ -77,7 +78,9 @@ val lex_def = tDefine "lex" ` ...@@ -77,7 +78,9 @@ val lex_def = tDefine "lex" `
| "Let" => DLET :: lex input'' | "Let" => DLET :: lex input''
| "PRE" => DPRE :: lex input'' | "PRE" => DPRE :: lex input''
| "ABS" => DABS :: lex input'' | "ABS" => DABS :: lex input''
| "GAMMA" => DGAMMA :: lex input''
| "Var" => DVAR :: lex input'' | "Var" => DVAR :: lex input''
| "Cast" => DCAST :: lex input''
| "MTYPE" => let ts = lex input'' in | "MTYPE" => let ts = lex input'' in
(case ts of (case ts of
| DCONST 32 :: ts' => DTYPE M32 :: ts' | DCONST 32 :: ts' => DTYPE M32 :: ts'
...@@ -85,7 +88,6 @@ val lex_def = tDefine "lex" ` ...@@ -85,7 +88,6 @@ val lex_def = tDefine "lex" `
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *) (* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *) (* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => NIL) | _ => NIL)
| "Gamma" => DGAMMA :: lex input''
| _ => NIL | _ => NIL
else else
(case char of (case char of
...@@ -105,10 +107,14 @@ val lex_def = tDefine "lex" ` ...@@ -105,10 +107,14 @@ val lex_def = tDefine "lex" `
\\ fs [Once lexConst_def] \\ rfs [] \\ fs [Once lexConst_def] \\ rfs []
\\ imp_res_tac (GSYM lexConst_imp) \\ fs [] \\ rveq \\ fs []); \\ imp_res_tac (GSYM lexConst_imp) \\ fs [] \\ rveq \\ fs []);
val str_join_def = Define `
(str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\
(str_join "" s2 = s2)`;
val str_of_num_def = Define ` val str_of_num_def = Define `
str_of_num (n:num) = str_of_num (n:num) =
if n < 10 then STRING (CHR (n + 48)) "" if n < 10 then STRING (CHR (n + 48)) ""
else STRING (CHR ( (n MOD 10) + 48)) (str_of_num (n DIV 10))` else str_join (str_of_num (n DIV 10)) (STRING (CHR ( (n MOD 10) + 48)) "")`
val type_to_string = Define ` val type_to_string = Define `
(type_to_string (M16) = "MTYPE 16") /\ (type_to_string (M16) = "MTYPE 16") /\
...@@ -125,26 +131,23 @@ val pp_token_def = Define ` ...@@ -125,26 +131,23 @@ val pp_token_def = Define `
| DPRE => "PRE" | DPRE => "PRE"
| DABS => "ABS" | DABS => "ABS"
| DCOND => "?" | DCOND => "?"
| DGAMMA => "Gamma"
| DTYPE m => type_to_string m
| DVAR => "Var" | DVAR => "Var"
| DCONST num => str_of_num num | DCONST num => str_of_num num
| DGAMMA => "Gamma"
| DTYPE m => type_to_string m
| DNEG => "~" | DNEG => "~"
| DPLUS => "+" | DPLUS => "+"
| DSUB => "-" | DSUB => "-"
| DMUL => "*" | DMUL => "*"
| DDIV => "/" | DDIV => "/"
| DFRAC => "#"`; | DFRAC => "#"
| DCAST => "Cast"`;
(* val pp_token_correct = store_thm ("pp_token_correct", *) (* val pp_token_correct = store_thm ("pp_token_correct", *)
(* ``!t. lex (pp_token t) = [t]``, *) (* ``!t. lex (pp_token t) = [t]``, *)
(* Induct_on `t` \\ EVAL_TAC fs[pp_token_def, lex_def] *) (* Induct_on `t` \\ EVAL_TAC fs[pp_token_def, lex_def] *)
(* ); *) (* ); *)
val str_join_def = Define `
(str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\
(str_join "" s2 = s2)`;
(* val str_join_empty = store_thm ("str_join_empty", *) (* val str_join_empty = store_thm ("str_join_empty", *)
(* ``!s. str_join s "" = s``, *) (* ``!s. str_join s "" = s``, *)
(* Induct \\ fs[str_join_def]); *) (* Induct \\ fs[str_join_def]); *)
...@@ -209,7 +212,7 @@ val fix_res_imp = prove( ...@@ -209,7 +212,7 @@ val fix_res_imp = prove(
val parseExp_def = tDefine "parseExp" ` val parseExp_def = tDefine "parseExp" `
parseExp (tokList:Token list) :(real exp # Token list) option = parseExp (tokList:Token list) :(real exp # Token list) option =
case tokList of case tokList of
| DTYPE t :: DCONST n :: DFRAC :: DCONST m :: tokRest => | DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
if (m = 0) then NONE else SOME (Const t ((&n):real / &m), tokRest) if (m = 0) then NONE else SOME (Const t ((&n):real / &m), tokRest)
| DVAR :: DCONST n :: tokRest => SOME (Var n, tokRest) | DVAR :: DCONST n :: tokRest => SOME (Var n, tokRest)
| DNEG :: tokRest => | DNEG :: tokRest =>
...@@ -245,6 +248,10 @@ val parseExp_def = tDefine "parseExp" ` ...@@ -245,6 +248,10 @@ val parseExp_def = tDefine "parseExp" `
| SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'') | SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'')
| NONE => NONE) | NONE => NONE)
| NONE => NONE) | NONE => NONE)
| DCAST :: DTYPE m :: tokRest =>
(case fix_res tokRest (parseExp tokRest) of
| SOME (e1, tokRest') => SOME (Downcast m e1,tokRest')
| _ => NONE)
| _ => NONE` | _ => NONE`
(WF_REL_TAC `measure LENGTH` (WF_REL_TAC `measure LENGTH`
\\ rw [] \\ fs [] \\ rw [] \\ fs []
...@@ -282,7 +289,7 @@ val parseLet_def = tDefine "parseLet" ` ...@@ -282,7 +289,7 @@ val parseLet_def = tDefine "parseLet" `
parseLet input :(real cmd # Token list) option = parseLet input :(real cmd # Token list) option =
case input of case input of
(* We have a valid let binding *) (* We have a valid let binding *)
| DVAR :: DTYPE m :: DCONST n :: expLetRest => | DVAR :: DCONST n :: DTYPE m :: expLetRest =>
(* so we parse an expression *) (* so we parse an expression *)
(case parseExp expLetRest of (case parseExp expLetRest of
| SOME (e, letRest) => | SOME (e, letRest) =>
......
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