Commit e257e52b authored by Heiko Becker's avatar Heiko Becker

Some more type annotations and remove unused lemma

parent 53aba077
......@@ -21,7 +21,7 @@ Fixpoint freeVars (V:Type) (f:exp V) : list nat:=
|Binop o f1 f2 => (freeVars V f1) ++ (freeVars V f2)
end.
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) validVars :=
Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :=
let (intv, _) := absenv e in
match e with
| Var _ v => NatSet.mem v validVars
......@@ -70,7 +70,7 @@ Fixpoint validIntervalbounds (e:exp Q) (absenv:analysisResult) (P:precond) valid
andb rec opres
end.
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) validVars {struct f} :bool:=
Fixpoint validIntervalboundsCmd (f:cmd Q) (absenv:analysisResult) (P:precond) (validVars:NatSet.t) :bool:=
match f with
| Let _ x e g =>
validIntervalbounds e absenv P validVars &&
......@@ -156,7 +156,6 @@ Qed.
Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) V VarEnv ParamEnv:
forall vR,
(* precondValidForExec P cenv ->*)
validIntervalbounds f absenv P V = true ->
(forall v, NatSet.mem v V = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
......@@ -458,72 +457,6 @@ Proof.
rewrite <- Q2R_max4 in valid_div_hi; auto. }
Qed.
Theorem ssaVars_are_sound (f:cmd Q) freeVars outVars (absenv:analysisResult)
(v_lo v_hi err:R) VarEnv ParamEnv P TEnv:
ssaPrg Q f (freeVars) (outVars) ->
bstep (toRCmd f) VarEnv ParamEnv P 0%R (Nop R) TEnv ->
(forall v, NatSet.mem v freeVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= VarEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R) ->
validIntervalboundsCmd f absenv P (freeVars) = true ->
forall v:nat, NatSet.mem v outVars = true ->
(Q2R (fst (fst (absenv (Var Q v)))) <= TEnv v <= Q2R (snd (fst (absenv (Var Q v)))))%R.
Proof.
intros ssa_f.
revert VarEnv.
induction ssa_f; intros VarEnv bstep_f freeVars_sound validBounds v in_outVars;
unfold validIntervalbounds in validBounds;
andb_to_prop validBounds.
- (* First rename auto-generated hyp names*)
rename L into eq_lo;
rename R1 into eq_hi;
rename L0 into validBounds_e.
inversion bstep_f; subst.
eapply IHssa_f; eauto.
+ intros v1 mem_Vx.
rewrite NatSet.mem_spec, NatSet.add_spec in mem_Vx.
unfold updEnv.
case_eq (v1 =? x); intros v1_eq_dec.
* assert (Q2R (fst (fst (absenv e))) <= v0 <= Q2R (snd (fst (absenv e))))%R
as validIV_e by (eapply validIntervalbounds_sound; eauto).
rewrite Nat.eqb_eq in v1_eq_dec.
rewrite v1_eq_dec.
apply Qeq_bool_iff in eq_lo.
apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi.
apply Qeq_eqR in eq_hi.
rewrite <- eq_lo, <- eq_hi.
auto.
* destruct mem_Vx.
{ subst.
rewrite Nat.eqb_neq in v1_eq_dec.
hnf in v1_eq_dec.
exfalso. apply v1_eq_dec. reflexivity. }
{ apply freeVars_sound.
rewrite NatSet.mem_spec; auto. }
- rename H into eq_V_Vterm.
rewrite NatSet.equal_spec in eq_V_Vterm.
rewrite NatSet.mem_spec in in_outVars.
hnf in eq_V_Vterm.
rewrite <- eq_V_Vterm in in_outVars.
rewrite <- NatSet.mem_spec in in_outVars.
inversion bstep_f; subst.
unfold updEnv.
case_eq (v =? 0); intros v_eq.
+ assert (Q2R (fst (fst (absenv e))) <= v0 <= Q2R (snd (fst (absenv e))))%R
by (eapply validIntervalbounds_sound; eauto).
rename L0 into eq_lo;
rename R0 into eq_hi.
apply Qeq_bool_iff in eq_lo;
apply Qeq_eqR in eq_lo.
apply Qeq_bool_iff in eq_hi;
apply Qeq_eqR in eq_hi.
rewrite Nat.eqb_eq in v_eq.
subst.
rewrite <- eq_lo, <- eq_hi.
assumption.
+ apply freeVars_sound; auto.
Qed.
Theorem validIntervalboundsCmd_sound (f:cmd Q) (absenv:analysisResult):
forall VarEnv ParamEnv envR inVars outVars elo ehi err P,
ssaPrg Q f inVars outVars ->
......
......@@ -2,7 +2,7 @@ Require Import Coq.MSets.MSets Coq.Arith.PeanoNat.
Require Export Daisy.Commands.
(**
Module for an ordered type with leibniz, based on code from coq-club code
Module for an ordered type with leibniz, based on code from coq-club mailing list
http://coq-club.inria.narkive.com/zptqoou2/how-to-use-msets
**)
Module OWL.
......@@ -40,6 +40,7 @@ Fixpoint validVars (V:Type) (f:exp V) Vs :bool :=
| Binop o f1 f2 => validVars V f1 Vs && validVars V f2 Vs
end.
(* TODO: This still allows overwriting of return value *)
Inductive ssaPrg (V:Type): (cmd V) -> (NatSet.t) -> (NatSet.t) -> Prop :=
ssaLet x e s inVars Vterm:
validVars V e inVars = true->
......
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