Commit 9af160f8 authored by Heiko Becker's avatar Heiko Becker

Fix merge conflict since Magnus and I added the same feature at the same time

parents 0b8b3d00 96c50dae
......@@ -60,121 +60,167 @@ val strSize_def = Define `
| 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`;
val lexName_imp = prove(
``!s s1 s2. lexName s = (s1,s2) ==> (s = s1 ++ s2)``,
Induct \\ simp [Once lexName_def]
\\ rw [] \\ pairarg_tac \\ fs []);
val lexConst_imp = prove(
``!s n s1 s2. lexConst s n = (s1,s2) ==> LENGTH s2 <= LENGTH s``,
Induct \\ simp [Once lexConst_def]
\\ rw [] \\ res_tac \\ fs []);
val lex_def = tDefine "lex" `
lex input =
case input of
| STRING char input' =>
if isDigit char
then
let (num, input'') = lexConst input 0 in
DCONST num :: lex input''
else
if isAlpha char
then
let (name, input'') = lexName input in
case name of
| "Ret" => DRET :: lex input''
| "Let" => DLET :: lex input''
| "PRE" => DPRE :: lex input''
| "ABS" => DABS :: lex input''
| "Var" => DVAR :: lex input''
| _ => NIL
else
(case char of
| #"+" => DPLUS :: lex input'
| #"-" => DSUB :: lex input'
| #"*" => DMUL :: lex input'
| #"/" => DDIV :: lex input'
| #"#" => DFRAC :: lex input'
| #"?" => DCOND :: lex input'
| #"~" => DNEG :: lex input'
| #" " => lex input'
| _ => NIL)
| _ => NIL`
(WF_REL_TAC `measure LENGTH` \\ rw [] \\ fs []
\\ imp_res_tac (GSYM lexName_imp) \\ fs [] \\ rveq \\ fs []
\\ fs [Once lexConst_def] \\ rfs []
\\ imp_res_tac (GSYM lexConst_imp) \\ fs [] \\ rveq \\ fs []);
val fix_res_def = Define `
fix_res xs NONE = NONE /\
fix_res xs (SOME (x,y)) =
if LENGTH xs < LENGTH y then SOME (x,xs) else SOME (x,y)`
val fix_res_imp = prove(
``fix_res xs a = SOME (x,y) ==> LENGTH y <= LENGTH xs``,
Cases_on `a` \\ rw [fix_res_def]
\\ Cases_on `x'` \\ fs [fix_res_def]
\\ every_case_tac \\ fs [] \\ rveq \\ fs []);
(** 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 parseExp_def = tDefine "parseExp" `
parseExp (tokList:Token list) :(real exp # Token list) option =
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) of
| SOME (e1,tokRest') => SOME (Unop Neg e1, tokRest')
| NONE => NONE)
| DPLUS :: tokRest =>
(case fix_res tokRest (parseExp tokRest) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest') of
| SOME (e2, tokRest'') => SOME (Binop Plus e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DSUB :: tokRest =>
(case fix_res tokRest (parseExp tokRest) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest') of
| SOME (e2, tokRest'') => SOME (Binop Sub e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DMUL :: tokRest =>
(case fix_res tokRest (parseExp tokRest) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest') of
| SOME (e2, tokRest'') => SOME (Binop Mult e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| DDIV :: tokRest =>
(case fix_res tokRest (parseExp tokRest) of
| SOME (e1,tokRest') =>
(case (parseExp tokRest') of
| SOME (e2, tokRest'') => SOME (Binop Div e1 e2, tokRest'')
| NONE => NONE)
| NONE => NONE)
| _ => NONE`
(WF_REL_TAC `measure LENGTH`
\\ rw [] \\ fs []
\\ imp_res_tac fix_res_imp \\ fs []);
val parseExp_ind = fetch "-" "parseExp_ind";
val parseExp_LESS_EQ = prove(
``!xs x y. parseExp xs = SOME (x,y) ==> LENGTH y <= LENGTH xs``,
recInduct parseExp_ind
\\ rw [] \\ fs [] \\ pop_assum mp_tac
\\ once_rewrite_tac [parseExp_def]
\\ ntac 8 (TRY (TOP_CASE_TAC \\ fs [])) \\ rw []
\\ fs [] \\ imp_res_tac fix_res_imp \\ fs [])
val fix_res_parseExp = prove(
``fix_res xs (parseExp xs) = parseExp xs``,
Cases_on `parseExp xs` \\ fs [fix_res_def]
\\ Cases_on `x` \\ fs [fix_res_def]
\\ imp_res_tac parseExp_LESS_EQ \\ fs []);
val parseExp_def = save_thm("parseExp_def",
parseExp_def |> REWRITE_RULE [fix_res_parseExp]);
val parseExp_ind = save_thm("parseExp_ind",
parseExp_ind |> REWRITE_RULE [fix_res_parseExp]);
val parseRet_def = Define `
parseRet input fuel :(real cmd # Token list) option =
case parseExp input fuel of
parseRet input :(real cmd # Token list) option =
case parseExp input 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 parseLet_def = tDefine "parseLet" `
parseLet input :(real cmd # Token list) option =
case input of
(* We have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
(* so we parse an expression *)
(case parseExp expLetRest of
| SOME (e, letRest) =>
(case letRest of
(* If we continue with a let *)
| DLET :: letBodyRest =>
(* Parse it *)
(case (parseLet letRest) 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) 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 *)
(WF_REL_TAC `measure LENGTH`
\\ rw [] \\ imp_res_tac fix_res_imp \\ fs []
\\ imp_res_tac parseExp_LESS_EQ \\ fs [])
val parseLet_ind = fetch "-" "parseLet_ind";
val parseFrac_def = Define `
parseFrac (input:Token list) :(real # Token list) option =
......@@ -201,31 +247,39 @@ val updPre_def = Define
`updPre (n:num) (iv:interval) (P:precond) =
\m. if (n = m) then iv else P m`;
val parseFrac_LESS_EQ = prove(
``parseFrac xs = SOME (x,y) ==> LENGTH y <= LENGTH xs``,
fs [parseFrac_def] \\ every_case_tac \\ fs []);
val parseIV_LESS_EQ = prove(
``parseIV xs = SOME (x,y) ==> LENGTH y <= LENGTH xs``,
fs [parseIV_def] \\ every_case_tac \\ fs []
\\ imp_res_tac parseFrac_LESS_EQ \\ fs [] \\ rw [] \\ fs []);
(** 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' =>
val parsePrecondRec_def = tDefine "parsePrecondRec" `
parsePrecondRec (input:Token list) :(precond # Token list) option =
(case input of
| DCOND :: DVAR :: DCONST n :: fracRest =>
(case parseIV fracRest of
| SOME (iv, precondRest) =>
(case parsePrecondRec precondRest (fuel - 1) of
(case parsePrecondRec precondRest of
| SOME (P, tokRest) => SOME (updPre n iv P, tokRest)
| NONE => SOME (updPre n iv defaultPre, precondRest))
| _ => NONE)
| _ => NONE)
| _ => NONE `;
| _ => NONE) `
(WF_REL_TAC `measure LENGTH` \\ rw []
\\ imp_res_tac parseIV_LESS_EQ \\ fs []);
val parsePrecond_def = Define `
parsePrecond (input :Token list) (fuel:num) =
case input of
| DPRE :: tokRest => parsePrecondRec tokRest fuel
| _ => NONE`;
parsePrecond (input :Token list) =
case input of
| DPRE :: tokRest => parsePrecondRec tokRest
| _ => NONE`;
val defaultAbsenv_def = Define
`defaultAbsenv:analysisResult = \e. ((0,0),0)`;
......@@ -239,59 +293,60 @@ val updAbsenv_def = Define
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' =>
val parseAbsEnvRec_def = tDefine "parseAbsEnvRec" `
parseAbsEnvRec (input:Token list) :(analysisResult # Token list) option =
(case input of
| DCOND :: expRest =>
(case parseExp expRest (fuel - 1) of
(case parseExp expRest of
| SOME (e,fracRest) =>
(case parseIV fracRest of
| SOME (iv, errRest) =>
(case parseFrac errRest of
| SOME (err, absenvRest) =>
(case parseAbsEnvRec absenvRest (fuel - 1) of
(case parseAbsEnvRec absenvRest 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 `;
| _ => SOME (defaultAbsenv, input))`
(WF_REL_TAC `measure LENGTH` \\ rw []
\\ imp_res_tac parseFrac_LESS_EQ
\\ imp_res_tac parseIV_LESS_EQ
\\ imp_res_tac parseExp_LESS_EQ
\\ fs []);
val parseAbsEnv_def = Define `
parseAbsEnv (input:Token list) (fuel:num) =
case input of
| DABS :: tokRest => parseAbsEnvRec tokRest fuel
| _ => NONE`;
parseAbsEnv (input:Token list) =
case input of
| DABS :: tokRest => parseAbsEnvRec tokRest
| _ => 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)
| DLET :: tokRest => parseLet tokRest
| DRET :: tokRest => parseRet tokRest
| _ => NONE) in
case cmdParse of
| SOME (dCmd, tokRest) =>
(case tokRest of
| DPRE :: preRest =>
(case parsePrecond tokRest (LENGTH preRest) of
(case parsePrecond tokRest of
| SOME (P, absenvRest) =>
(case parseAbsEnv absenvRest (LENGTH absenvRest) of
(case parseAbsEnv absenvRest of
| SOME (A, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| DABS :: absRest =>
(case parseAbsEnv tokRest (LENGTH absRest) of
(case parseAbsEnv tokRest of
| SOME (A, precondRest) =>
(case parsePrecond precondRest (LENGTH precondRest) of
(case parsePrecond precondRest of
| SOME (P, NIL) => SOME (dCmd, P, A)
| _ => NONE)
| NONE => NONE)
| _ => NONE)
| _ => NONE`;
val _ = export_theory();
......@@ -16,13 +16,13 @@ val _ = translate lookup_def;
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"`;
let tokList = lex input in
case parse tokList of
| SOME (dCmd, P, A) =>
if CertificateCheckerCmd dCmd A P
then "True"
else "False"
| NONE => "parse failure"`;
(* TESTING STATEMENTS
EVAL ``case (EXPLODE "abc") of
......@@ -61,19 +61,13 @@ val validIvbounds_v_thm = translate validIntervalbounds_def;
*)
val translated_parseExp_def = translate parseExp_def;
val res = translate parseExp_def;
val parseexp_side_def = fetch "-" "parseexp_side_def";
val parseexp_v_thm = fetch "-" "parseexp_v_thm";
val parseexp_side_true = prove (
``!(tokList: Token list) (fuel:num).
parseexp_side tokList fuel``,
recInduct parseExp_ind
\\ rpt strip_tac
\\ once_rewrite_tac [parseexp_side_def]
\\ rpt strip_tac \\ fs[]) |> update_precondition;
val parseexp_side_true = prove(
``!x. parseexp_side x = T``,
recInduct parseExp_ind \\ rw []
\\ once_rewrite_tac [fetch "-" "parseexp_side_def"] \\ rw [])
|> update_precondition;
val res = translate CertificateCheckerCmd_def;
......@@ -93,7 +87,7 @@ val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";
val precond_validIntervalbounds_true = prove (
``!f absenv P (dVars:num_set).
(v. v (domain dVars) valid (FST (absenv (Var v)))) ==>
(!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
validintervalbounds_side f absenv P dVars``,
recInduct validIntervalbounds_ind
\\ rw[]
......@@ -133,7 +127,7 @@ val precond_validIntervalbounds_true = prove (
val precond_validIntervalboundsCmd_true = prove (
``!f absenv P (dVars:num_set).
(v. v (domain dVars) valid (FST (absenv (Var v)))) ==>
(!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
validintervalboundscmd_side f absenv P dVars``,
recInduct validIntervalboundsCmd_ind
\\ rpt strip_tac
......@@ -150,7 +144,7 @@ val precond_validIntervalboundsCmd_true = prove (
val precond_validErrorbound_true = prove (``
!P f absenv (dVars:num_set).
(v. v (domain dVars) valid (FST (absenv (Var v)))) /\
(!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) /\
validIntervalbounds f absenv P dVars ==>
validerrorbound_side f absenv dVars``,
gen_tac
......@@ -199,15 +193,15 @@ val precond_validErrorbound_true = prove (``
by (drule err_always_positive
\\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
\\ fs [])
\\ `e2lo - err2 0 /\ e2hi + err2 0`
\\ `e2lo - err2 <> 0 /\ e2hi + err2 <> 0`
by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
\\ conj_tac \\ REAL_ASM_ARITH_TAC)
\\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
by (drule validIntervalbounds_noDivzero_real
\\ fs [])
\\ `abs (e2lo - err2) 0 /\ abs (e2hi + err2) 0`
\\ `abs (e2lo - err2) <> 0 /\ abs (e2hi + err2) <> 0`
by (REAL_ASM_ARITH_TAC)
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) 0`
\\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) <> 0`
by (fs [min_def]
\\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
\\ fs [] \\ REAL_ASM_ARITH_TAC)
......@@ -217,7 +211,7 @@ val precond_validErrorbound_true = prove (``
val precond_errorbounds_true = prove (``
!P f absenv dVars.
(v. v domain dVars valid (FST (absenv (Var v)))) /\
(!v. v IN domain dVars ==> valid (FST (absenv (Var v)))) /\
validIntervalboundsCmd f absenv P dVars ==>
validerrorboundcmd_side f absenv dVars``,
gen_tac
......@@ -251,8 +245,8 @@ val precond_is_true = prove (
>- (match_mp_tac precond_validIntervalboundsCmd_true
\\ fs [])
>- (strip_tac \\ match_mp_tac precond_errorbounds_true
\\ qexists_tac `P` \\ fs [])) |> update_precondition;
\\ qexists_tac `P` \\ fs []))
|> update_precondition;
val res' = translate runChecker_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