Commit 5f096e8a authored by Guillaume Melquiond's avatar Guillaume Melquiond

Alt-Ergo: Discard arithmetic triggers, as they cause syntax errors. (Fix for bug #16454)

parent d00dd702
......@@ -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)"
......
......@@ -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 *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment