Commit bb5d9056 authored by Heiko Becker's avatar Heiko Becker

Further improvements to Daisy_compute and fix proofs of Interval validator for finite maps

parent 31c7a755
open preamble
open simpLib realTheory realLib RealArith sptreeTheory
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyTactics
open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyTactics DaisyMapTheory
val _ = new_theory "Environments";
......@@ -15,9 +15,11 @@ val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(abs (v1 - v2) <= abs v1 * (mTypeToQ m)) /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A (insert x () fVars) dVars (updEnv x v2 E2)) /\
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult) (fVars:num_set) (dVars:num_set) v1 v2 x.
(!(E1:env) (E2:env) (defVars: num -> mType option) (A:analysisResult)
(fVars:num_set) (dVars:num_set) v1 v2 x iv err.
approxEnv E1 defVars A fVars dVars E2 /\
(abs (v1 - v2) <= SND (A (Var x))) /\
DaisyMapTree_find (Var x) A = SOME (iv, err) /\
abs (v1 - v2) <= err /\
(lookup x (union fVars dVars) = NONE) ==>
approxEnv (updEnv x v1 E1) (updDefVars x m defVars) A fVars (insert x () dVars) (updEnv x v2 E2))`;
......@@ -86,41 +88,41 @@ val approxEnv_fVar_bounded = store_thm (
\\ fs[]));
val approxEnv_dVar_bounded = store_thm ("approxEnv_dVar_bounded",
``!E1 Gamma absenv fVars dVars E2 x v v2 m e.
approxEnv E1 Gamma absenv fVars dVars E2 /\
``!E1 Gamma A fVars dVars E2 x v v2 m iv e.
approxEnv E1 Gamma A fVars dVars E2 /\
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
SND (absenv (Var x)) = e ==>
DaisyMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e``,
rpt strip_tac
\\ qspec_then
`\E1 Gamma absenv fVars dVars E2.
`\E1 Gamma A fVars dVars E2.
!x v v2 m.
E1 x = SOME v /\
E2 x = SOME v2 /\
x IN (domain dVars) /\
Gamma x = SOME m /\
SND (absenv (Var x)) = e ==>
DaisyMapTree_find (Var x) A = SOME (iv, e) ==>
abs (v - v2) <= e`
(fn thm => irule (SIMP_RULE std_ss [] thm))
(fn thm => destruct (SIMP_RULE std_ss [] thm))
approxEnv_ind
\\ rpt strip_tac
>- (fs [emptyEnv_def])
>- (fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
>- (first_x_assum irule \\ fs[updDefVars_def]
>- (rpt conj_tac
>- (fs [emptyEnv_def])
>- (rpt strip_tac \\ fs [updEnv_def]
\\ EVERY_CASE_TAC \\ rveq \\ fs[lookup_union, domain_lookup]
>- (EVERY_CASE_TAC \\ fs[])
\\ first_x_assum irule \\ fs[updDefVars_def]
\\ rename1 `defVars x2 = SOME m2` \\ qexistsl_tac [`m2`, `x2`]
\\ fs[])
>- (rpt strip_tac \\ fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC \\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexistsl_tac [`m1`,`x1`]
\\ fs[]))
>- (fs [updEnv_def, updDefVars_def] \\ rveq \\ fs[]
\\ EVERY_CASE_TAC
\\ rveq \\ fs[]
\\ first_x_assum irule \\ fs[]
\\ rename1 `defVars x1 = SOME m1` \\ qexistsl_tac [`m1`,`x1`]
\\ fs[])
>- (qexistsl_tac [`E1`, `Gamma`, `absenv`, `fVars`, `dVars`, `E2`, `m`, `x`]
\\ fs[]));
\\ first_x_assum drule
\\ rpt (disch_then drule)
\\ disch_then MATCH_ACCEPT_TAC);
val _ = export_theory ();;
......@@ -170,12 +170,13 @@ fun Daisy_compute t =
\\ fs[]
\\ TRY (
REPEAT (
qpat_assum `option_CASE _ _ _`
((qpat_assum `option_CASE _ _ _`
(fn thm =>
let
val (t,t2,_) = optionSyntax.dest_option_case (concl thm) in
Cases_on `^t2` \\ fs[] end)
\\ split_pair_case_tac \\ fs[])))
Cases_on `^t2` \\ fs[] end))
ORELSE
(split_pair_case_tac)) \\ fs[])))
end;
(* val Daisy_compute:tactic = *)
......
This diff is collapsed.
......@@ -5,7 +5,7 @@ open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
val _ = new_theory "Typing";
val typeExpression_def = FDefine ``typeExpression`` `
val typeExpression_def = Define `
typeExpression (Gamma: num -> mType option) (e: real exp) : mType option =
case e of
| Var v => Gamma v
......@@ -23,21 +23,9 @@ val typeExpression_def = FDefine ``typeExpression`` `
| SOME m1 => if (morePrecise m1 m) then SOME m else NONE
| NONE => NONE`;
(* val typeMap_def = Define ` *)
(* typeMap (Gamma: num -> mType option) (e: real exp) (e': real exp) : mType option = *)
(* case e of *)
(* | Var v => (if (e = e') then Gamma v else NONE) *)
(* | Const m n => if e = e' then SOME m else NONE *)
(* | Unop u e1 => if e = e' then typeExpression Gamma e else typeMap Gamma e1 e' *)
(* | Binop b e1 e2 => if e = e' then typeExpression Gamma e *)
(* else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e') of *)
(* | SOME m1, SOME m2 => (if (m1 = m2) then SOME m1 else NONE) *)
(* | SOME m1, NONE => SOME m1 *)
(* | NONE, SOME m2 => SOME m2 *)
(* | NONE, NONE => NONE) *)
(* | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'` *)
val typeMap_def = FDefine ``typeMap`` `
add_unevaluated_function ``typeExpression``;
val typeMap_def = Define `
typeMap (Gamma:num -> mType option) (e:real exp) (tMap:typeMap) =
if (DaisyMapTree_mem e tMap)
then tMap
......@@ -70,32 +58,19 @@ val typeMap_def = FDefine ``typeMap`` `
else DaisyMapTree_empty)
| _ => DaisyMapTree_empty)`;
val typeCmd_def = FDefine ``typeCmd`` `
add_unevaluated_function ``typeMap``;
val typeCmd_def = Define `
typeCmd (Gamma: num -> mType option) (f: real cmd) : mType option =
case f of
| Let m n e c => (case typeExpression Gamma e of
| SOME m' => if morePrecise m m' then typeCmd Gamma c else NONE
| NONE => NONE)
| Ret e => typeExpression Gamma e`
(* val typeMapCmd_def = Define ` *)
(* typeMapCmd (Gamma: num -> mType option) (f: real cmd) (f': real exp) : mType option = *)
(* case f of *)
(* | Let m n e c => if f' = (Var n) then (*FIXME: This may fail because n not in Gamma... *) *)
(* (case Gamma n of *)
(* | SOME m' => if morePrecise m m' then SOME m else NONE *)
(* | NONE => NONE) *)
(* else *)
(* let te = typeMap Gamma e in *)
(* let tc = typeMapCmd Gamma c in *)
(* (case (te f', tc f') of *)
(* | SOME m1, SOME m2 => if (m1 = m2) then SOME m1 else NONE *)
(* | SOME m1, NONE => SOME m1 *)
(* | NONE, SOME m2 => SOME m2 *)
(* | NONE, NONE => NONE) *)
(* | Ret e => typeMap Gamma e f'` *)
val typeMapCmd_def = FDefine ``typeMapCmd`` `
| Ret e => typeExpression Gamma e`;
add_unevaluated_function ``typeCmd``;
val typeMapCmd_def = Define `
typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) =
case f of
| Let m n e c =>
......@@ -110,7 +85,9 @@ val typeMapCmd_def = FDefine ``typeMapCmd`` `
| _ => DaisyMapTree_empty)
| Ret e => typeMap Gamma e tMap`;
val typeCheck_def = FDefine ``typeCheck`` `
add_unevaluated_function ``typeMapCmd``;
val typeCheck_def = Define `
typeCheck (e:real exp) (Gamma: num -> mType option) (tMap:typeMap) : bool =
case e of
| Var v => (case DaisyMapTree_find e tMap, Gamma v of
......@@ -132,9 +109,11 @@ val typeCheck_def = FDefine ``typeCheck`` `
| Downcast m_ e1 => (case DaisyMapTree_find e tMap, DaisyMapTree_find e1 tMap of
| SOME m', SOME m1 => (m' = m_) /\ morePrecise m1 m_
/\ typeCheck e1 Gamma tMap
| _, _ => F)`
| _, _ => F)`;
add_unevaluated_function ``typeCheck``;
val typeCheckCmd_def = FDefine ``typeCheckCmd`` `
val typeCheckCmd_def = Define `
typeCheckCmd (c: real cmd) (Gamma: num -> mType option) (tMap:typeMap) : bool =
case c of
| Let m x e g => if (typeCheck e Gamma tMap)
......@@ -144,7 +123,9 @@ val typeCheckCmd_def = FDefine ``typeCheckCmd`` `
mx = m /\ me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
| _ => F
else F
| Ret e => typeCheck e Gamma tMap`
| Ret e => typeCheck e Gamma tMap`;
add_unevaluated_function ``typeCheckCmd``;
val typingSoundnessExp = store_thm("typingSoundnessExp",
``!(v:real) (m:mType) (expTypes:typeMap) E e Gamma.
......
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