From 0515cf4f807c4d09a5eee1aafd82b5814d8f3c2b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Gwena=C3=ABl=20Delaval?= <gwenael.delaval@inria.fr>
Date: Mon, 13 Mar 2017 18:01:05 +0100
Subject: [PATCH] Handling of implication operator in Ctrln back-end

---
 compiler/global/initial.ml               | 1 +
 compiler/heptagon/ctrln/ctrlNbacAsEpt.ml | 4 ++++
 2 files changed, 5 insertions(+)

diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml
index 55ae51b..5080974 100644
--- a/compiler/global/initial.ml
+++ b/compiler/global/initial.ml
@@ -41,6 +41,7 @@ let pfalse = { qual = Pervasives; name = "false" }
 let por = { qual = Pervasives; name = "or" }
 let pand = { qual = Pervasives; name = "&" }
 let pnot = { qual = Pervasives; name = "not" }
+let pimp = { qual = Pervasives; name = "=>" }
 let pint = { qual = Pervasives; name = "int" }
 let tint = Types.Tid pint
 let pfloat = { qual = Pervasives; name = "float" }
diff --git a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
index 48f79e5..9092ebb 100644
--- a/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
+++ b/compiler/heptagon/ctrln/ctrlNbacAsEpt.ml
@@ -163,6 +163,9 @@ let nnop t : nnop -> fun_name =
 let buop: buop -> fun_name = function
   | `Neg -> Initial.pnot
 
+let bbop: bbop -> fun_name = function
+  | `Imp -> Initial.pimp
+
 let bnop: bnop -> fun_name = function
   | `Conj -> Initial.pand
   | `Disj -> Initial.por
@@ -212,6 +215,7 @@ let translate_expr gd e =
     | `Ref v -> mkb (Evar (ts gd v))
     | `Bool b -> mkb (Econst (Initial.mk_static_bool b))
     | `Buop (op, e) -> mkb (mk_uapp (Efun (buop op)) (tb e))
+    | `Bbop (op, e, f) -> mkb (mk_bapp (Efun (bbop op)) (tb e) (tb f))
     | `Bnop (op, e, f, l) -> mkb_bapp ?flag (Efun (bnop op)) tb e f l
     | `Bcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tb e) (tb f))
     | `Ecmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (te e) (te f))