Commit 97b9a584 authored by Heiko Becker's avatar Heiko Becker

Port validator function to finite maps

parent bb5d9056
......@@ -10,7 +10,7 @@ open preamble
open simpLib realTheory realLib RealArith pred_setTheory
open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics MachineTypeTheory
open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory TypingTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory DaisyMapTheory
val _ = new_theory "ErrorValidation";
......@@ -18,59 +18,66 @@ val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val validErrorbound_def = Define `
validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)=
let (intv, err) = absenv e in
let mopt = typeMap e in
case mopt of
| NONE => F
| SOME m =>
if (0 <= err) then
validErrorbound e (typeMap: (real exp # mType) binTree) (A:analysisResult) (dVars:num_set)=
case DaisyMapTree_find e A, DaisyMapTree_find e typeMap of
| SOME (intv, err), SOME m =>
(if (0 <= err) then
case e of
| Var v => if (lookup v dVars = SOME ()) then T else (maxAbs intv * (mTypeToQ m) <= err)
| Const _ n => (maxAbs intv * (mTypeToQ m) <= err)
| Unop Neg f =>
if (validErrorbound f typeMap absenv dVars) then
err = (SND (absenv f))
else
F
| Unop Inv f => F
| Binop op f1 f2 =>
(if (validErrorbound f1 typeMap absenv dVars /\ validErrorbound f2 typeMap absenv dVars) then
let (ive1, err1) = absenv f1 in
let (ive2, err2) = absenv f2 in
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Div =>
(if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
then
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err)
else F)
| Unop Neg e1 =>
if (validErrorbound e1 typeMap A dVars)
then
case (DaisyMapTree_find e1 A) of
| SOME (_, err1) => err = err1
| _ => F
else F
| Unop Inv e1 => F
| Binop op e1 e2 =>
(if (validErrorbound e1 typeMap A dVars /\ validErrorbound e2 typeMap A dVars)
then
case DaisyMapTree_find e1 A, DaisyMapTree_find e2 A of
| SOME (ive1, err1), SOME (ive2, err2) =>
let errIve1 = widenInterval ive1 err1 in
let errIve2 = widenInterval ive2 err2 in
let upperBoundE1 = maxAbs ive1 in
let upperBoundE2 = maxAbs ive2 in
(case op of
| Plus => err1 + err2 + (maxAbs (addInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Sub => err1 + err2 + (maxAbs (subtractInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Mult => (upperBoundE1 * err2 + upperBoundE2 * err1 + err1 * err2) + (maxAbs (multInterval errIve1 errIve2) * (mTypeToQ m)) <= err
| Div =>
(if (IVhi errIve2 < 0 \/ 0 < IVlo errIve2)
then
let upperBoundInvE2 = maxAbs (invertInterval ive2) in
let minAbsIve2 = minAbsFun (errIve2) in
let errInv = (1 / (minAbsIve2 * minAbsIve2)) * err2 in
((upperBoundE1 * errInv + upperBoundInvE2 * err1 + err1 * errInv) + (maxAbs (divideInterval errIve1 errIve2) * (mTypeToQ m)) <= err)
else F))
| _, _ => F
else F)
| Downcast m1 e1 =>
let (ive1, err1) = absenv e1 in
let rec_res = validErrorbound e1 typeMap absenv dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err)
else F`;
case DaisyMapTree_find e1 A of
| SOME (ive1, err1) =>
let rec_res = validErrorbound e1 typeMap A dVars in
let errIve1 = widenInterval ive1 err1 in
rec_res /\ ( (err1 + maxAbs errIve1 * (mTypeToQ m1)) <= err)
else F)
| _, _ => F`;
val validErrorboundCmd_def = Define `
validErrorboundCmd (f:real cmd) (typeMap: real exp -> mType option) (env:analysisResult) (dVars:num_set)=
validErrorboundCmd (f:real cmd) (typeMap: (real exp # mType) binTree)
(A:analysisResult) (dVars:num_set) =
case f of
| Let m x e g =>
if (validErrorbound e typeMap env dVars /\ (env e = env (Var x))) then
validErrorboundCmd g typeMap env (insert x () dVars)
else F
(case DaisyMapTree_find e A, DaisyMapTree_find (Var x) A of
| SOME (iv_e, err_e), SOME (iv_x, err_x) =>
if (validErrorbound e typeMap A dVars /\ err_e = err_x)
then validErrorboundCmd g typeMap A (insert x () dVars)
else F
| _ , _ => F)
| Ret e =>
validErrorbound e typeMap env dVars`;
validErrorbound e typeMap A dVars`;
val err_always_positive = store_thm (
"err_always_positive",
......
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