Commit 12fad0df authored by Sylvain Boulmé's avatar Sylvain Boulmé
Browse files

remove some useless "OK tt"

parent b8e73be7
Pipeline #56274 passed with stages
in 518 minutes and 36 seconds
......@@ -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 *)
......
......@@ -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 *)
......
Supports Markdown
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