Commit d2581f0d authored by Heiko Becker's avatar Heiko Becker

Test parser and lexer and build a top level string manipulating function

parent 0231234f
......@@ -50,7 +50,7 @@ val lexConst_def = Define`
| STRING char input' =>
if (isDigit char)
then lexConst input' (akk * 10 + (getConst char))
else (akk, input')
else (akk, input)
|"" => (akk, input)`;
val lexName_def = Define `
......@@ -62,12 +62,13 @@ val lexName_def = Define `
let (name, input') = lexName input' in
(STRING char name, input')
else ("", input)
| "" => ("","")`;
| "" => ("",input)`;
val strSize_def = Define `strSize str =
case str of
| STRING _ str' => 1 + strSize str'
| "" => 0`;
val strSize_def = Define `
strSize str :num=
case str of
| STRING _ str' => 1 + strSize str'
| "" => 0`;
val lex_def = Define `
lex input fuel =
......@@ -86,9 +87,9 @@ case fuel of
case name of
| "Ret" => DRET :: lex input'' fuel'
| "Let" => DLET :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| _ => NIL
else
(case char of
......@@ -110,7 +111,7 @@ val parseExp_def = Define `
case fuel of
| SUC fuel' =>
(case tokList of
| DFRAC :: DCONST n :: DCONST m :: tokRest => SOME (Const ((&n):real / &m), tokRest)
| DCONST n :: DFRAC :: 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 =>
......@@ -174,7 +175,7 @@ val parseLet_def = Define `
(* But if we have a return *)
| DRET :: retBodyRest =>
(* parse only this *)
(case (parseRet letRest (fuel - 1)) of
(case (parseRet retBodyRest (fuel - 1)) of
(* and construct the result *)
| SOME (retCmd, arbRest) => SOME (Let n e retCmd, arbRest)
| _ => NONE)
......@@ -183,13 +184,21 @@ val parseLet_def = Define `
| _ => NONE) (* fail if we cannot find a variable *)
| _ => NONE`; (* fail if there is no fuel left *)
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)
| _ => NONE `;
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`;
case (parseFrac input) of
| SOME (iv_lo, tokRest) =>
(case (parseFrac tokRest) of
| SOME (iv_hi, tokList) => SOME ((iv_lo, iv_hi), tokList)
| _ => NONE )
| _ => NONE`;
val defaultPre_def = Define
`defaultPre:precond = \x. (0,0)`;
......@@ -200,7 +209,7 @@ val updPre_def = Define
(** Precondition parser:
The precondition should be encoded in the following format:
PRECOND ::= DCOND DCONST FRACTION FRACTION PRECOND | EPSILON
PRECOND ::= DCOND DVAR DCONST FRACTION FRACTION PRECOND | EPSILON
The beginning of the precondition is marked by the DPRE token
**)
val parsePrecondRec_def = Define `
......@@ -208,7 +217,7 @@ val parsePrecondRec_def = Define `
case fuel of
| SUC fuel' =>
(case input of
| DCOND :: DCONST n :: fracRest =>
| DCOND :: DVAR :: DCONST n :: fracRest =>
(case parseIV fracRest of
| SOME (iv, precondRest) =>
(case parsePrecondRec precondRest (fuel - 1) of
......@@ -218,11 +227,11 @@ case fuel of
| _ => 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 parsePrecond_def = Define `
parsePrecond (input :Token list) (fuel:num) =
case input of
| DPRE :: tokRest => parsePrecondRec tokRest fuel
| _ => NONE`;
val defaultAbsenv_def = Define
`defaultAbsenv:analysisResult = \e. ((0,0),0)`;
......@@ -237,7 +246,7 @@ val updAbsenv_def = Define
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 =
parseAbsEnvRec (input:Token list) (fuel:num) :(analysisResult # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
......@@ -248,15 +257,21 @@ case fuel of
| SOME (iv, errRest) =>
(case parseFrac errRest of
| SOME (err, absenvRest) =>
(case parseAbsenvRec absenvRest (fuel - 1) of
(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)
| _ => SOME (defaultAbsenv, input))
| _ => NONE `;
val parseAbsEnv_def = Define `
parseAbsEnv (input:Token list) (fuel:num) =
case input of
| DABS :: tokRest => parseAbsEnvRec tokRest fuel
| _ => NONE`;
(* Global parsing function FIXME: should parse all three definitions (cmd, absenv and precond) or fail otherwise*)
val parse_def = Define `
parse (input:Token list) =
......@@ -267,23 +282,33 @@ val parse_def = Define `
case cmdParse of
| SOME (dCmd, tokRest) =>
(case tokRest of
| DPRE :: tokRest =>
(case parsePrecondRec tokRest (LENGTH tokRest) of
| DPRE :: preRest =>
(case parsePrecond tokRest (LENGTH preRest) of
| SOME (P, absenvRest) =>
(case parseAbsenvRec absenvRest (LENGTH absenvRest) of
(case parseAbsEnv absenvRest (LENGTH absenvRest) of
| SOME (A, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| DABS :: tokRest =>
(case parseAbsenvRec tokRest (LENGTH tokRest) of
| DABS :: absRest =>
(case parseAbsEnv tokRest (LENGTH absRest) of
| SOME (A, precondRest) =>
(case parsePrecondRec precondRest (LENGTH precondRest) of
(case parsePrecond precondRest (LENGTH precondRest) of
| SOME (P, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| _ => NONE)
| _ => NONE`;
val runChecker_def = Define `
runChecker (input:tvarN) =
let tokList = (lex input (strSize input)) in
case parse tokList of
| SOME (dCmd, P, A) =>
if CertificateCheckerCmd dCmd A P
then "True"
else "False"
| NONE => "False"`;
(* TESTING STATEMENTS
EVAL ``case (EXPLODE "abc") of
| STRING c s => SOME c
......
......@@ -204,7 +204,7 @@ object CertificatePhase extends DaisyPhase {
}else if (prv == "hol4"){
hol4Variable (id, varId, reporter)
}else {
(varId.toString(), varId.toString())
(s"Var $varId", s"Var $varId")
}
expressionNames += (e -> name)
(definition,name)
......@@ -396,7 +396,7 @@ object CertificatePhase extends DaisyPhase {
var theFunction = " PRE "
for ((id,intv) <- ranges) {
val ivBin = binaryInterval(intv)
theFunction += s" ${identifierNums(id)} $ivBin "
theFunction += s"? Var ${identifierNums(id)} $ivBin "
}
(theFunction, "")
}
......
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