From 5f096e8a03cb8ab0b40ee85ad6587e7ca28fc064 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Wed, 16 Oct 2013 15:44:12 +0200
Subject: [PATCH] Alt-Ergo: Discard arithmetic triggers, as they cause syntax
 errors. (Fix for bug #16454)

---
 drivers/alt_ergo_bare.drv | 15 +++++++++++++++
 src/printer/alt_ergo.ml   | 13 ++++++++++---
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/drivers/alt_ergo_bare.drv b/drivers/alt_ergo_bare.drv
index 135a0258a..2a5f43dde 100644
--- a/drivers/alt_ergo_bare.drv
+++ b/drivers/alt_ergo_bare.drv
@@ -48,6 +48,11 @@ theory int.Int
   syntax function (*)  "(%1 * %2)"
   syntax function (-_) "(-%1)"
 
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
   syntax predicate (<=) "(%1 <= %2)"
   syntax predicate (<)  "(%1 <  %2)"
   syntax predicate (>=) "(%1 >= %2)"
@@ -89,6 +94,11 @@ theory real.Real
   syntax function (-_) "(-%1)"
   syntax function inv  "(1.0 / %1)"
 
+  meta "invalid trigger" predicate (<=)
+  meta "invalid trigger" predicate (<)
+  meta "invalid trigger" predicate (>=)
+  meta "invalid trigger" predicate (>)
+
   syntax predicate (<=) "(%1 <= %2)"
   syntax predicate (<)  "(%1 <  %2)"
   syntax predicate (>=) "(%1 >= %2)"
@@ -124,6 +134,11 @@ theory real.RealInfix
   syntax function (/.)  "(%1 / %2)"
   syntax function (-._) "(-%1)"
 
+  meta "invalid trigger" predicate (<=.)
+  meta "invalid trigger" predicate (<.)
+  meta "invalid trigger" predicate (>=.)
+  meta "invalid trigger" predicate (>.)
+
   syntax predicate (<=.) "(%1 <= %2)"
   syntax predicate (<.)  "(%1 <  %2)"
   syntax predicate (>=.) "(%1 >= %2)"
diff --git a/src/printer/alt_ergo.ml b/src/printer/alt_ergo.ml
index e7adeb94b..d6f21c11d 100644
--- a/src/printer/alt_ergo.ml
+++ b/src/printer/alt_ergo.ml
@@ -26,6 +26,10 @@ let meta_printer_option =
   Theory.register_meta "printer_option" [Theory.MTstring]
     ~desc:"Pass@ additional@ parameters@ to@ the@ pretty-printer."
 
+let meta_invalid_trigger =
+  Theory.register_meta "invalid trigger" [Theory.MTlsymbol]
+  ~desc:"Specify@ that@ a@ symbol@ is@ not@ allowed@ in@ a@ trigger."
+
 type info = {
   info_syn : syntax_map;
   info_ac  : Sls.t;
@@ -34,6 +38,7 @@ type info = {
   info_csm : lsymbol list Mls.t;
   info_pjs : Sls.t;
   info_axs : Spr.t;
+  info_inv_trig : Sls.t;
 }
 
 let ident_printer =
@@ -222,7 +227,7 @@ and print_expr info fmt =
 and print_triggers info fmt tl =
   let filter = function
     | { t_ty = Some _ } -> true
-    | { t_node = Tapp (ps,_) } -> not (ls_equal ps ps_equ)
+    | { t_node = Tapp (ps,_) } -> not (Sls.mem ps info.info_inv_trig)
     | _ -> false in
   let tl = List.map (List.filter filter) tl in
   let tl = List.filter (function [] -> false | _::_ -> true) tl in
@@ -373,7 +378,7 @@ let () = register_printer "alt-ergo-old"
 *)
 
 let print_decls =
-  let print ac sl tc csm pjs axs sm fmt d =
+  let print inv_trig ac sl tc csm pjs axs sm fmt d =
     let info = {
       info_syn = sm;
       info_ac  = ac;
@@ -382,8 +387,10 @@ let print_decls =
       info_csm = Mls.map Array.to_list csm;
       info_pjs = pjs;
       info_axs = axs;
+      info_inv_trig = Sls.add ps_equ inv_trig;
     } in
     print_decl info fmt d in
+  Trans.on_tagged_ls meta_invalid_trigger (fun inv_trig ->
   Trans.on_tagged_ls meta_ac (fun ac ->
   Trans.on_meta meta_printer_option (fun args ->
     let sl = List.fold_left check_showlabels false args in
@@ -391,7 +398,7 @@ let print_decls =
   Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
     let csm,pjs,axs = List.fold_left
       add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
-    Printer.sprint_decls (print ac sl tc csm pjs axs))))
+    Printer.sprint_decls (print inv_trig ac sl tc csm pjs axs)))))
 
 let print_task _env pr thpr _blacklist ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is a no-no *)
-- 
2.24.1