From 1d7796d6d39eb9d7ff79ac3d1fee1e107ce204f4 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 11 Apr 2019 14:38:20 +0200 Subject: more robust pattern-matching in *op_eq --- mppa_k1c/Asmblockdeps.v | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'mppa_k1c/Asmblockdeps.v') 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: -- cgit