diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:42:08 +0100 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 21:42:08 +0100 |
| commit | 12fad0dfecb626ceafcbb6e75c6adfd5e108b420 (patch) | |
| tree | 3d14ce842874c8de15d9cddc73b22b27410cd996 | |
| parent | b8e73be77abdef268594e747bdc6fc1ba503dc1f (diff) | |
| download | compcert-kvx-12fad0dfecb626ceafcbb6e75c6adfd5e108b420.tar.gz compcert-kvx-12fad0dfecb626ceafcbb6e75c6adfd5e108b420.zip | |
remove some useless "OK tt"
| -rw-r--r-- | backend/Duplicate.v | 8 | ||||
| -rw-r--r-- | backend/Duplicateproof.v | 14 |
2 files changed, 11 insertions, 11 deletions
diff --git a/backend/Duplicate.v b/backend/Duplicate.v index 40db4e45..3fd86728 100644 --- a/backend/Duplicate.v +++ b/backend/Duplicate.v @@ -86,7 +86,7 @@ Global Opaque builtin_res_eq_pos. Definition verify_match_inst dupmap inst tinst := match inst with - | Inop n => match tinst with Inop n' => do u <- verify_is_copy dupmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end + | Inop n => match tinst with Inop n' => verify_is_copy dupmap n n' | _ => Error(msg "verify_match_inst Inop") end | Iop op lr r n => match tinst with Iop op' lr' r' n' => @@ -167,10 +167,10 @@ Definition verify_match_inst dupmap inst tinst := if (list_eq_dec Pos.eq_dec lr lr') then if (eq_condition cond cond') then do u1 <- verify_is_copy dupmap n1 n1'; - do u2 <- verify_is_copy dupmap n2 n2'; OK tt + verify_is_copy dupmap n2 n2' else if (eq_condition (negate_condition cond) cond') then do u1 <- verify_is_copy dupmap n1 n2'; - do u2 <- verify_is_copy dupmap n2 n1'; OK tt + verify_is_copy dupmap n2 n1' else Error (msg "Incompatible conditions in Icond") else Error (msg "Different lr in Icond") | _ => Error (msg "verify_match_inst Icond") end @@ -212,7 +212,7 @@ Definition verify_mapping_match_nodes dupmap (f f': function): res unit := (** Verifies that the [dupmap] of the translated function [f'] is giving correct information in regards to [f] *) Definition verify_mapping dupmap (f f': function) : res unit := do u <- verify_mapping_entrypoint dupmap f f'; - do v <- verify_mapping_match_nodes dupmap f f'; OK tt. + verify_mapping_match_nodes dupmap f f'. (** * Entry points *) diff --git a/backend/Duplicateproof.v b/backend/Duplicateproof.v index cc24104f..2f3bad2f 100644 --- a/backend/Duplicateproof.v +++ b/backend/Duplicateproof.v @@ -144,8 +144,8 @@ Proof. intros. unfold verify_match_inst in H. destruct i; try (inversion H; fail). (* Inop *) - - destruct i'; try (inversion H; fail). monadInv H. - destruct x. eapply verify_is_copy_correct in EQ. + - destruct i'; try (inversion H; fail). + eapply verify_is_copy_correct in H. constructor; eauto. (* Iop *) - destruct i'; try (inversion H; fail). monadInv H. @@ -197,12 +197,12 @@ Proof. destruct (list_eq_dec _ _ _); try discriminate. subst. destruct (eq_condition _ _); try discriminate. + monadInv H. destruct x. eapply verify_is_copy_correct in EQ. - destruct x0. eapply verify_is_copy_correct in EQ1. - constructor; assumption. + eapply verify_is_copy_correct in EQ0. + subst; constructor; assumption. + destruct (eq_condition _ _); try discriminate. monadInv H. destruct x. eapply verify_is_copy_correct in EQ. - destruct x0. eapply verify_is_copy_correct in EQ1. - constructor; assumption. + eapply verify_is_copy_correct in EQ0. + subst; constructor; assumption. (* Ijumptable *) - destruct i'; try (inversion H; fail). monadInv H. destruct x. eapply verify_is_copy_list_correct in EQ. @@ -257,7 +257,7 @@ Proof. exists mp; constructor 1; simpl; auto. + (* correct *) intros until n'. intros REVM i FNC. - unfold verify_mapping_match_nodes in EQ. simpl in EQ. destruct x1. + unfold verify_mapping_match_nodes in EQ1. simpl in EQ1. destruct x. eapply verify_mapping_mn_rec_correct; eauto. simpl; eauto. + (* entrypoint *) |