Commit ba63dafc authored by Heiko Becker's avatar Heiko Becker

Fix some parsing bugs in transScript

parent a3d410ab
......@@ -111,7 +111,8 @@ val parseExp_def = Define `
case fuel of
| SUC fuel' =>
(case tokList of
| DCONST n :: DFRAC :: DCONST m :: tokRest => SOME (Const ((&n):real / &m), tokRest)
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m = 0) then NONE else SOME (Const ((&n):real / &m), tokRest)
| DCONST n :: tokRest => SOME (Const &n, tokRest)
| DVAR :: DCONST n :: tokRest => SOME (Var n, tokRest)
| DNEG :: tokRest =>
......@@ -187,8 +188,10 @@ val parseLet_def = Define `
val parseFrac_def = Define `
parseFrac (input:Token list) :(real # Token list) option =
case input of
| DSUB :: DCONST n :: DFRAC :: DCONST m :: tokRest => SOME ((- &n):real / (&m),tokRest)
| DCONST n :: DFRAC :: DCONST m :: tokRest => SOME ((&n):real / (&m),tokRest)
| DSUB :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m = 0) then NONE else SOME ((- &n):real / (&m),tokRest)
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
if (m = 0) then NONE else SOME ((&n):real / (&m),tokRest)
| _ => NONE `;
val parseIV_def = Define `
......@@ -364,6 +367,8 @@ val validerrorboundcmd_side_def = fetch "-" "validerrorboundcmd_side_def";
val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";
val parsefrac_side_def = fetch "-" "parsefrac_side_def";
val parseiv_side_def = fetch "-" "parseiv_side_def";
val parseprecond_side_def = fetch "-" "parseprecondrec_side_def";
......
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