From 6f05c86e614797b76d92bc3dbbd4c0ece683168e Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Thu, 3 Oct 2019 16:31:03 +0200
Subject: Proof for Iop

---
 backend/Duplicate.v | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'backend/Duplicate.v')

diff --git a/backend/Duplicate.v b/backend/Duplicate.v
index ce6c436f..a96d0826 100644
--- a/backend/Duplicate.v
+++ b/backend/Duplicate.v
@@ -2,7 +2,7 @@
   structures *)
 
 Require Import AST RTL Maps Globalenvs.
-Require Import Coqlib Errors.
+Require Import Coqlib Errors Op.
 
 Local Open Scope error_monad_scope.
 Local Open Scope positive_scope.
@@ -45,9 +45,21 @@ Definition verify_is_copy revmap n n' :=
   | Some revn => match (Pos.compare n revn) with Eq => OK tt | _ => Error(msg "verify_is_copy invalid map") end
   end.
 
+
 Definition verify_match_inst revmap inst tinst :=
   match inst with
   | Inop n => match tinst with Inop n' => do u <- verify_is_copy revmap n n'; OK tt | _ => Error(msg "verify_match_inst Inop") end
+  | Iop op lr r n => match tinst with
+      Iop op' lr' r' n' =>
+          do u <- verify_is_copy revmap n n';
+          if (eq_operation op op') then
+            if (list_eq_dec Pos.eq_dec lr lr') then
+              if (Pos.eq_dec r r') then
+                OK tt
+              else Error (msg "Different r in Iop")
+            else Error (msg "Different lr in Iop")
+          else Error(msg "Different operations in Iop")
+      | _ => Error(msg "verify_match_inst Inop") end
   | _ => Error(msg "not implemented")
   end.
 
-- 
cgit