Commit 210a23a8 authored by Heiko Becker's avatar Heiko Becker

Finish implementation of parser

parent 1636dcb5
......@@ -102,13 +102,13 @@ case fuel of
| _ => NIL)
| _ => NIL`;
(* Prefix form parser for expressions *)
(** Prefix form parser for expressions **)
val parseExp_def = Define `
parseExp (tokList:Token list) fuel :(real exp # Token list) option =
case fuel of
| SUC fuel' =>
(case tokList of
| DCONST n :: DFRAC :: DCONST m :: tokRest => SOME (Const ((&n):real / &m), tokRest)
| DFRAC :: DCONST n :: DCONST m :: tokRest => SOME (Const ((&n):real / &m), tokRest)
| DCONST n :: tokRest => SOME (Const &n, tokRest)
| DVAR :: DCONST n :: tokRest => SOME (Var n, tokRest)
| DNEG :: tokRest =>
......@@ -181,18 +181,106 @@ val parseLet_def = Define `
| _ => NONE) (* fail if we cannot find a variable *)
| _ => NONE`; (* fail if there is no fuel left *)
val parseIV_def = Define `
parseIV (input:Token list) :(interval # Token list) option =
case input of
| DFRAC :: DCONST nlo :: DCONST mlo :: DFRAC :: DCONST nhi :: DCONST mhi :: tokRest =>
SOME (((&nlo):real / &mlo, (&nhi):real / &mhi),tokRest)
| _ => NONE`;
val defaultPre_def = Define
`defaultPre:precond = \x. (0,0)`;
val updPre_def = Define
`updPre (n:num) (iv:interval) (P:precond) =
\m. if (n = m) then iv else P m`;
(** Precondition parser:
The precondition should be encoded in the following format:
PRECOND ::= DCOND DCONST FRACTION FRACTION PRECOND | EPSILON
The beginning of the precondition is marked by the DPRE token
**)
val parsePrecondRec_def = Define `
parsePrecondRec (input:Token list) (fuel:num) :(precond # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
| DCOND :: DCONST n :: fracRest =>
(case parseIV fracRest of
| SOME (iv, precondRest) =>
(case parsePrecondRec precondRest (fuel - 1) of
| SOME (P, tokRest) => SOME (updPre n iv P, tokRest)
| NONE => SOME (updPre n iv defaultPre, precondRest))
| _ => NONE)
| _ => NONE)
| _ => NONE `;
val parseFrac_def = Define
`parseFrac (input: Token list) =
case input of
| DFRAC :: DCONST n :: DCONST m :: tokRest => SOME ((&n):real / &m, tokRest)
| _ => NONE`;
val defaultAbsenv_def = Define
`defaultAbsenv:analysisResult = \e. ((0,0),0)`;
val updAbsenv_def = Define
`updAbsenv (e:real exp) (iv:interval) (err:real) (A:analysisResult) =
\e'. if (e = e') then (iv,err) else A e'`;
(** Abstract environment parser:
The abstract environment should be encoded in the following format:
ABSENV ::= ? EXPRESSION FRACTION FRACTION FRACTION ABSENV | EPSILON
The beginning of the abstract environment is marked by the DABS token
**)
val parseAbsEnvRec_def = Define `
parseAbsenvRec (input:Token list) (fuel:num) :(analysisResult # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
| DCOND :: expRest =>
(case parseExp expRest (fuel - 1) of
| SOME (e,fracRest) =>
(case parseIV fracRest of
| SOME (iv, errRest) =>
(case parseFrac errRest of
| SOME (err, absenvRest) =>
(case parseAbsenvRec absenvRest (fuel - 1) of
| SOME (A, tokRest) => SOME (updAbsenv e iv err A, tokRest)
| NONE => SOME (updAbsenv e iv err defaultAbsenv, absenvRest))
| NONE => NONE)
| _ => NONE)
| NONE => NONE)
| _ => NONE)
| _ => NONE `;
(* Global parsing function FIXME: should parse all three definitions (cmd, absenv and precond) or fail otherwise*)
val parse_def = Define `
parse input fuel =
case fuel of
| SUC fuel' =>
(case input of
| DLET :: tokRest => SOME (parseLet tokRest fuel)
| DRET :: tokRest => SOME (parseRet tokRest fuel)
| DPRE :: tokRest => NONE (*SOME (parsePrecond input fuel) *)
| DABS :: tokRest => NONE (*SOME (parseAbsEnv input fuel) *)
| _ => NONE )
| _ => NONE`;
parse (input:Token list) =
let cmdParse = (case input of
| DLET :: tokRest => parseLet tokRest (LENGTH input)
| DRET :: tokRest => parseRet tokRest (LENGTH input)
| _ => NONE) in
case cmdParse of
| SOME (dCmd, tokRest) =>
(case tokRest of
| DPRE :: tokRest =>
(case parsePrecondRec tokRest (LENGTH tokRest) of
| SOME (P, absenvRest) =>
(case parseAbsenvRec absenvRest (LENGTH absenvRest) of
| SOME (A, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| DABS :: tokRest =>
(case parseAbsenvRec tokRest (LENGTH tokRest) of
| SOME (A, precondRest) =>
(case parsePrecondRec precondRest (LENGTH precondRest) of
| SOME (P, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| _ => NONE)
| _ => NONE`;
(* TESTING STATEMENTS
EVAL ``case (EXPLODE "abc") of
......
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