Skip to content

Commit

Permalink
fix(dolmen): Preserve trigger order (#1046)
Browse files Browse the repository at this point in the history
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).
  • Loading branch information
bclement-ocp authored Feb 28, 2024
1 parent 8c188f1 commit 472710d
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions src/lib/frontend/d_cnf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 472710d

Please sign in to comment.