Commit 0b8b3d00 authored by Heiko Becker's avatar Heiko Becker

No preconditions left anymore

parent 31c62d10
open preamble
open ExpressionsTheory CommandsTheory
val _ = new_theory "daisyParser";
val _ = Datatype `
Token =
| DLET
| DRET
| DPRE
| DABS
| DCOND
| DVAR
| DCONST num
| DNEG
| DPLUS
| DSUB
| DMUL
| DDIV
| DFRAC`;
val getChar_def = Define `
getChar input =
case input of
| "" => CHR 0
| STRING c input' => c`;
val getConst_def = Define `
getConst (c:char) = ORD c - 48`;
val suffix_def = Define `
suffix s = case s of
| STRING c s' => s'
| "" => ""`;
val lexConst_def = Define`
lexConst (input:tvarN) (akk:num) =
case input of
| STRING char input' =>
if (isDigit char)
then lexConst input' (akk * 10 + (getConst char))
else (akk, input)
|"" => (akk, input)`;
val lexName_def = Define `
lexName (input:tvarN) =
case input of
| STRING char input' =>
if (isAlphaNum char)
then
let (name, input') = lexName input' in
(STRING char name, input')
else ("", input)
| "" => ("",input)`;
val strSize_def = Define `
strSize str :num=
case str of
| STRING _ str' => 1 + strSize str'
| "" => 0`;
val lex_def = Define `
lex input fuel =
case fuel of
| SUC fuel' =>
(case input of
| STRING char input' =>
if isDigit char
then
let (num, input'') = lexConst input 0 in
DCONST num :: lex input'' fuel'
else
if isAlpha char
then
let (name, input'') = lexName input in
case name of
| "Ret" => DRET :: lex input'' fuel'
| "Let" => DLET :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| _ => NIL
else
(case char of
| #"+" => DPLUS :: lex input' fuel'
| #"-" => DSUB :: lex input' fuel'
| #"*" => DMUL :: lex input' fuel'
| #"/" => DDIV :: lex input' fuel'
| #"#" => DFRAC :: lex input' fuel'
| #"?" => DCOND :: lex input' fuel'
| #"~" => DNEG :: lex input' fuel'
| #" " => lex input' fuel'
| _ => NIL)
| _ => NIL)
| _ => NIL`;
(** 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 =>
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 =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') => SOME (Unop Neg e1, tokRest')
| NONE => NONE)
| DPLUS :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Plus e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DSUB :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Sub e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DMUL :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Mult e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DDIV :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| _ => NONE )
| _ => NONE`;
val parseRet_def = Define `
parseRet input fuel :(real cmd # Token list) option =
case parseExp input fuel of
| SOME (e, tokRest) => SOME (Ret e, tokRest)
| NONE => NONE`;
val parseLet_def = Define `
parseLet input fuel:(real cmd # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
(* We have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
(* so we parse an expression *)
(case parseExp expLetRest (fuel-1) of
| SOME (e, letRest) =>
(case letRest of
(* If we continue with a let *)
| DLET :: letBodyRest =>
(* Parse it *)
(case (parseLet letRest (fuel - 1)) of
(* And construct a result from it *)
| SOME (letCmd, arbRest) => SOME (Let n e letCmd, arbRest)
| _ => NONE)
(* But if we have a return *)
| DRET :: retBodyRest =>
(* parse only this *)
(case (parseRet retBodyRest (fuel - 1)) of
(* and construct the result *)
| SOME (retCmd, arbRest) => SOME (Let n e retCmd, arbRest)
| _ => NONE)
| _ => NONE) (* fail if there is no continuation for the let *)
| NONE => NONE) (* fail if we do not have an expression to bind *)
| _ => 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 =>
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 `
parseIV (input:Token list) :(interval # Token list) option =
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)`;
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 DVAR 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 :: DVAR :: 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 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)`;
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)
| _ => 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) =
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 :: preRest =>
(case parsePrecond tokRest (LENGTH preRest) of
| SOME (P, absenvRest) =>
(case parseAbsEnv absenvRest (LENGTH absenvRest) of
| SOME (A, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| DABS :: absRest =>
(case parseAbsEnv tokRest (LENGTH absRest) of
| SOME (A, precondRest) =>
(case parsePrecond precondRest (LENGTH precondRest) of
| SOME (P, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| _ => NONE)
| _ => NONE`;
val _ = export_theory();
......@@ -6,7 +6,7 @@ open stringTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory DaisyTactics
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory ErrorValidationTheory CertificateCheckerTheory
open CertificateCheckerTheory
open CertificateCheckerTheory daisyParserTheory
val _ = new_theory "trans";
......@@ -14,294 +14,6 @@ val _ = translation_extends "realProg";
val _ = translate lookup_def;
val _ = Datatype `
Token =
| DLET
| DRET
| DPRE
| DABS
| DCOND
| DVAR
| DCONST num
| DNEG
| DPLUS
| DSUB
| DMUL
| DDIV
| DFRAC`;
val getChar_def = Define `
getChar input =
case input of
| "" => CHR 0
| STRING c input' => c`;
val getConst_def = Define `
getConst (c:char) = ORD c - 48`;
val suffix_def = Define `
suffix s = case s of
| STRING c s' => s'
| "" => ""`;
val lexConst_def = Define`
lexConst (input:tvarN) (akk:num) =
case input of
| STRING char input' =>
if (isDigit char)
then lexConst input' (akk * 10 + (getConst char))
else (akk, input)
|"" => (akk, input)`;
val lexName_def = Define `
lexName (input:tvarN) =
case input of
| STRING char input' =>
if (isAlphaNum char)
then
let (name, input') = lexName input' in
(STRING char name, input')
else ("", input)
| "" => ("",input)`;
val strSize_def = Define `
strSize str :num=
case str of
| STRING _ str' => 1 + strSize str'
| "" => 0`;
val lex_def = Define `
lex input fuel =
case fuel of
| SUC fuel' =>
(case input of
| STRING char input' =>
if isDigit char
then
let (num, input'') = lexConst input 0 in
DCONST num :: lex input'' fuel'
else
if isAlpha char
then
let (name, input'') = lexName input in
case name of
| "Ret" => DRET :: lex input'' fuel'
| "Let" => DLET :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| _ => NIL
else
(case char of
| #"+" => DPLUS :: lex input' fuel'
| #"-" => DSUB :: lex input' fuel'
| #"*" => DMUL :: lex input' fuel'
| #"/" => DDIV :: lex input' fuel'
| #"#" => DFRAC :: lex input' fuel'
| #"?" => DCOND :: lex input' fuel'
| #"~" => DNEG :: lex input' fuel'
| #" " => lex input' fuel'
| _ => NIL)
| _ => NIL)
| _ => NIL`;
(** 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 =>
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 =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') => SOME (Unop Neg e1, tokRest')
| NONE => NONE)
| DPLUS :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Plus e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DSUB :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Sub e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DMUL :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Mult e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DDIV :: tokRest =>
(case (parseExp tokRest (fuel - 1)) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest' (fuel - 2)) of
| SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE))
| _ => NONE`;
val parseRet_def = Define `
parseRet input fuel :(real cmd # Token list) option =
case parseExp input fuel of
| SOME (e, tokRest) => SOME (Ret e, tokRest)
| NONE => NONE`;
val parseLet_def = Define `
parseLet input fuel:(real cmd # Token list) option =
case fuel of
| SUC fuel' =>
(case input of
(* We have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
(* so we parse an expression *)
(case parseExp expLetRest (fuel-1) of
| SOME (e, letRest) =>
(case letRest of
(* If we continue with a let *)
| DLET :: letBodyRest =>
(* Parse it *)
(case (parseLet letRest (fuel - 1)) of
(* And construct a result from it *)
| SOME (letCmd, arbRest) => SOME (Let n e letCmd, arbRest)
| _ => NONE)
(* But if we have a return *)
| DRET :: retBodyRest =>
(* parse only this *)
(case (parseRet retBodyRest (fuel - 1)) of
(* and construct the result *)
| SOME (retCmd, arbRest) => SOME (Let n e retCmd, arbRest)
| _ => NONE)
| _ => NONE) (* fail if there is no continuation for the let *)
| NONE => NONE) (* fail if we do not have an expression to bind *)
| _ => 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 =>
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 `
parseIV (input:Token list) :(interval # Token list) option =
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)`;
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 DVAR 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 :: DVAR :: 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 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)`;
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)
| _ => 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) =
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 :: preRest =>
(case parsePrecond tokRest (LENGTH preRest) of
| SOME (P, absenvRest) =>
(case parseAbsEnv absenvRest (LENGTH absenvRest) of
| SOME (A, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| DABS :: absRest =>
(case parseAbsEnv tokRest (LENGTH absRest) of
| SOME (A, precondRest) =>
(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
......@@ -349,9 +61,21 @@ val validIvbounds_v_thm = translate validIntervalbounds_def;