diff options
author | 2013-04-20 07:54:52 +0000 | |
---|---|---|
committer | 2013-04-20 07:54:52 +0000 | |
commit | 255cee09b71255051c2b40eae0c88bffce1f6f32 (patch) | |
tree | 7951b1b13e8fd5e525b9223e8be0580e83550f55 /common/Errors.v | |
parent | 6e5041958df01c56762e90770abd704b95a36e5d (diff) |
Big merge of the newregalloc-int64 branch. Lots of changes in two directions:
1- new register allocator (+ live range splitting, spilling&reloading, etc)
based on a posteriori validation using the Rideau-Leroy algorithm
2- support for 64-bit integer arithmetic (type "long long").
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'common/Errors.v')
-rw-r--r-- | common/Errors.v | 48 |
1 files changed, 11 insertions, 37 deletions
diff --git a/common/Errors.v b/common/Errors.v index 6b863a0..78e1199 100644 --- a/common/Errors.v +++ b/common/Errors.v @@ -96,30 +96,11 @@ Qed. (** Assertions *) -Definition assertion (b: bool) : res unit := - if b then OK tt else Error(msg "Assertion failed"). +Definition assertion_failed {A: Type} : res A := 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. +Notation "'assertion' A ; B" := (if A then B else assertion_failed) + (at level 200, A at level 100, B at level 200) + : error_monad_scope. (** This is the familiar monadic map iterator. *) @@ -180,26 +161,19 @@ 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 + | (match ?X with left _ => _ | right _ => assertion_failed end = OK _) => + destruct X; [try (monadInv1 H) | discriminate] + | (match (negb ?X) with true => _ | false => assertion_failed end = OK _) => + destruct X as [] eqn:?; [discriminate | try (monadInv1 H)] + | (match ?X with true => _ | false => assertion_failed end = OK _) => + destruct X as [] eqn:?; [try (monadInv1 H) | discriminate] | (mmap ?F ?L = OK ?M) => generalize (mmap_inversion F L H); intro end. Ltac monadInv H := + monadInv1 H || match type of H with - | (OK _ = OK _) => monadInv1 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 _) => |