From 95bb1a72adcccac59d3329b821a119c57b24ba06 Mon Sep 17 00:00:00 2001 From: Nicolas Berthier Date: Fri, 2 Mar 2018 14:26:10 +0000 Subject: [PATCH] Handle implication operator in Sigali backend --- compiler/minils/sigali/sigalimain.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/compiler/minils/sigali/sigalimain.ml b/compiler/minils/sigali/sigalimain.ml index fd2da98..de2c8ae 100644 --- a/compiler/minils/sigali/sigalimain.ml +++ b/compiler/minils/sigali/sigalimain.ml @@ -135,6 +135,8 @@ let rec translate prefix ({ Minils.e_desc = desc } as e) = | "not", [e] -> Snot(translate_ext prefix e) | "or", [e1;e2] -> Sor((translate_ext prefix e1), (translate_ext prefix e2)) + | "=>", [e1;e2] -> Sor(Snot (translate_ext prefix e1), + (translate_ext prefix e2)) | "&", [e1;e2] -> Sand((translate_ext prefix e1), (translate_ext prefix e2)) | "=", [e1;e2] when (actual_ty e1.Minils.w_ty) = Tbool ->