nor implemente

1 files changed, 10 insertions, 0 deletions

diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 4d3d5ad0..028c2eb1 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -726,6 +726,8 @@ Nondetfunction notint (e: expr) :=
   match e with
   | Eop Oand (e1:::e2:::Enil) => Eop Onand (e1:::e2:::Enil)
   | Eop (Oandimm n) (e1:::Enil) => Eop (Onandimm n) (e1:::Enil)
+  | Eop Oor (e1:::e2:::Enil) => Eop Onor (e1:::e2:::Enil)
+  | Eop (Oorimm n) (e1:::Enil) => Eop (Onorimm n) (e1:::Enil)
   | _ => xorimm Int.mone e
   end.
 >>
@@ -734,12 +736,16 @@ Nondetfunction notint (e: expr) :=
 Inductive notint_cases: forall (e: expr), Type :=
   | notint_case1: forall e1 e2, notint_cases (Eop Oand (e1:::e2:::Enil))
   | notint_case2: forall n e1, notint_cases (Eop (Oandimm n) (e1:::Enil))
+  | notint_case3: forall e1 e2, notint_cases (Eop Oor (e1:::e2:::Enil))
+  | notint_case4: forall n e1, notint_cases (Eop (Oorimm n) (e1:::Enil))
   | notint_default: forall (e: expr), notint_cases e.
 
 Definition notint_match (e: expr) :=
   match e as zz1 return notint_cases zz1 with
   | Eop Oand (e1:::e2:::Enil) => notint_case1 e1 e2
   | Eop (Oandimm n) (e1:::Enil) => notint_case2 n e1
+  | Eop Oor (e1:::e2:::Enil) => notint_case3 e1 e2
+  | Eop (Oorimm n) (e1:::Enil) => notint_case4 n e1
   | e => notint_default e
   end.
 
@@ -749,6 +755,10 @@ Definition notint (e: expr) :=
       Eop Onand (e1:::e2:::Enil)
   | notint_case2 n e1 => (* Eop (Oandimm n) (e1:::Enil) *) 
       Eop (Onandimm n) (e1:::Enil)
+  | notint_case3 e1 e2 => (* Eop Oor (e1:::e2:::Enil) *) 
+      Eop Onor (e1:::e2:::Enil)
+  | notint_case4 n e1 => (* Eop (Oorimm n) (e1:::Enil) *) 
+      Eop (Onorimm n) (e1:::Enil)
   | notint_default e =>
       xorimm Int.mone e
   end.