diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-11 14:38:20 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2019-04-11 14:38:20 +0200 |
commit | 1d7796d6d39eb9d7ff79ac3d1fee1e107ce204f4 (patch) | |
tree | 8957acffeaf27757831ca57f14f60e347f50ebd6 /mppa_k1c | |
parent | c21b97b0e18691205afe056e76b4c18da9d909d1 (diff) | |
download | compcert-kvx-1d7796d6d39eb9d7ff79ac3d1fee1e107ce204f4.tar.gz compcert-kvx-1d7796d6d39eb9d7ff79ac3d1fee1e107ce204f4.zip |
more robust pattern-matching in *op_eq
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asmblockdeps.v | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v index a676d7b2..4559dd62 100644 --- a/mppa_k1c/Asmblockdeps.v +++ b/mppa_k1c/Asmblockdeps.v @@ -346,10 +346,11 @@ Hint Resolve arith_op_eq_correct: wlp. Opaque arith_op_eq_correct. Definition load_op_eq (o1 o2: load_op): ?? bool := - match o1, o2 with - | OLoadRRO n1 ofs1, OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) - | OLoadRRR n1, OLoadRRR n2 => phys_eq n1 n2 - | _, _ => RET false + match o1 with + | OLoadRRO n1 ofs1 => + match o2 with OLoadRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + | OLoadRRR n1 => + match o2 with OLoadRRR n2 => phys_eq n1 n2 | _ => RET false end end. Lemma load_op_eq_correct o1 o2: @@ -364,10 +365,11 @@ Opaque load_op_eq_correct. Definition store_op_eq (o1 o2: store_op): ?? bool := - match o1, o2 with - | OStoreRRO n1 ofs1, OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) - | OStoreRRR n1, OStoreRRR n2 => phys_eq n1 n2 - | _, _ => RET false + match o1 with + | OStoreRRO n1 ofs1 => + match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end + | OStoreRRR n1 => + match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end end. Lemma store_op_eq_correct o1 o2: |