From eda2872c976c039467f7b0f81e37b9cbbdd571ba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Basile=20Cl=C3=A9ment?= Date: Tue, 27 Feb 2024 18:39:31 +0100 Subject: [PATCH] fix(dolmen): Preserve trigger order In spite of what the comment says, the Dolmen frontend currently reverses the order in which triggers are considered. This patch ensures that the trigger order is preserved by using `List.map` instead of `List.rev_map` (there is usually only very few triggers and the `mk_expr` itself is not tail-recursive). --- src/lib/frontend/d_cnf.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 571c3928b..a86741957 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1578,12 +1578,11 @@ let rec mk_expr (* All the triggers that are encoutered at this level are assumed to be user-defined. *) let triggers = - List.rev_map ( + List.map ( fun t -> make_trigger ~loc ~name_base ~decl_kind ~in_theory name hyp (t, true) ) trgs - (* double reverse to produce expressions with the right tags. *) in let mk = begin match e with