diff options
author | 2010-09-02 12:42:19 +0000 | |
---|---|---|
committer | 2010-09-02 12:42:19 +0000 | |
commit | 265fa07b34a813ba9d8249ddad82d71e6002c10d (patch) | |
tree | 45831b1793c7920b10969fc7cf6316c202d78e91 /common/Errors.v | |
parent | 94470fb6a652cb993982269fcb7a0e8319b54488 (diff) |
Merge of the reuse-temps branch:
- Reload temporaries are marked as destroyed (set to Vundef) across
operations in the semantics of LTL, LTLin, Linear and Mach,
allowing Asmgen to reuse them.
- Added IA32 port.
- Cleaned up float conversions and axiomatization of floats.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1499 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Errors.v')
-rw-r--r-- | common/Errors.v | 40 |
1 files changed, 38 insertions, 2 deletions
diff --git a/common/Errors.v b/common/Errors.v index 2165db3..36e70c5 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -93,10 +93,37 @@ Proof. intros; discriminate. Qed. -Open Local Scope error_monad_scope. +(** Assertions *) + +Definition assertion (b: bool) : res unit := + if b then OK tt else Error(msg "Assertion failed"). + +Remark assertion_inversion: + forall b x, assertion b = OK x -> b = true. +Proof. + unfold assertion; intros. destruct b; inv H; auto. +Qed. + +Remark assertion_inversion_1: + forall (P Q: Prop) (a: {P}+{Q}) x, + assertion (proj_sumbool a) = OK x -> P. +Proof. + intros. exploit assertion_inversion; eauto. + unfold proj_sumbool. destruct a. auto. congruence. +Qed. + +Remark assertion_inversion_2: + forall (P Q: Prop) (a: {P}+{Q}) x, + assertion (negb(proj_sumbool a)) = OK x -> Q. +Proof. + intros. exploit assertion_inversion; eauto. + unfold proj_sumbool. destruct a; simpl. congruence. auto. +Qed. (** This is the familiar monadic map iterator. *) +Open Local Scope error_monad_scope. + Fixpoint mmap (A B: Type) (f: A -> res B) (l: list A) {struct l} : res (list B) := match l with | nil => OK nil @@ -152,6 +179,15 @@ Ltac monadInv1 H := destruct (bind2_inversion F G H) as [x1 [x2 [EQ1 EQ2]]]; clear H; try (monadInv1 EQ2))))) + | (assertion (negb (proj_sumbool ?a)) = OK ?X) => + let A := fresh "A" in (generalize (assertion_inversion_2 _ H); intro A); + clear H + | (assertion (proj_sumbool ?a) = OK ?X) => + let A := fresh "A" in (generalize (assertion_inversion_1 _ H); intro A); + clear H + | (assertion ?b = OK ?X) => + let A := fresh "A" in (generalize (assertion_inversion _ H); intro A); + clear H | (mmap ?F ?L = OK ?M) => generalize (mmap_inversion F L H); intro end. @@ -162,6 +198,7 @@ Ltac monadInv H := | (Error _ = OK _) => monadInv1 H | (bind ?F ?G = OK ?X) => monadInv1 H | (bind2 ?F ?G = OK ?X) => monadInv1 H + | (assertion _ = OK _) => monadInv1 H | (?F _ _ _ _ _ _ _ _ = OK _) => ((progress simpl in H) || unfold F in H); monadInv1 H | (?F _ _ _ _ _ _ _ = OK _) => @@ -179,4 +216,3 @@ Ltac monadInv H := | (?F _ = OK _) => ((progress simpl in H) || unfold F in H); monadInv1 H end. - |