From f8a140b4070faa6cf06ec4fcc1af4c928e271c85 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Basile=20Cl=C3=A9ment?=
 <129742207+bclement-ocp@users.noreply.github.com>
Date: Tue, 17 Sep 2024 14:21:46 +0200
Subject: [PATCH] fix: Do not load preludes twice (#1235)

The `--enable-theories` option should be a no-op w.r.t. the theories
that are already enabled, but it currently causes the theory preludes to
be enabled twice due to an oversight in the option parsing code.

Switch the option parsing code to use a set instead of a list to
represent the enabled theories, ensuring uniqueness.
---
 src/bin/common/parse_command.ml | 15 ++++++++-------
 src/lib/util/theories.ml        | 28 +++++++++++++++++++++++++++-
 2 files changed, 35 insertions(+), 8 deletions(-)

diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
index 5d83f65b1..d5fa49d20 100644
--- a/src/bin/common/parse_command.ml
+++ b/src/bin/common/parse_command.ml
@@ -1509,21 +1509,22 @@ let parse_theory_opt =
       Term.(const mk_disable_theories $ disable_theories $ disable_adts $ no_ac)
     in
     let preludes enable_theories disable_theories =
-      let theories = Theories.default in
+      let theories = Theories.Set.of_list Theories.default in
       let rec aux th en dis =
         match en, dis with
-        | _ :: _, [] -> aux (List.rev_append en th) [] []
+        | _ :: _, [] ->
+          aux (List.fold_left (fun th en -> Theories.Set.add en th) th en) [] []
         | e :: _, d :: _ when e = d ->
           Fmt.error_msg "theory prelude '%a' cannot be both enabled and
           disabled" Theories.pp e
-        | e :: en, d :: _ when e < d -> aux (e :: th) en dis
-        | _ , d :: dis -> aux (List.filter ((<>) d) th) en dis
-        | [], [] -> Ok th
+        | e :: en, d :: _ when e < d -> aux (Theories.Set.add e th) en dis
+        | _ , d :: dis -> aux (Theories.Set.filter ((<>) d) th) en dis
+        | [], [] -> Ok (Theories.Set.elements th)
       in
       aux
         theories
-        (List.fast_sort compare enable_theories)
-        (List.fast_sort compare disable_theories)
+        (List.fast_sort Theories.compare enable_theories)
+        (List.fast_sort Theories.compare disable_theories)
     in
     Term.(
       cli_parse_result (
diff --git a/src/lib/util/theories.ml b/src/lib/util/theories.ml
index 8e2aaf32f..2c39ca2c6 100644
--- a/src/lib/util/theories.ml
+++ b/src/lib/util/theories.ml
@@ -16,19 +16,43 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type prelude = Fpa | Ria | Nra [@@deriving eq]
+type prelude = Nra | Ria | Fpa [@@deriving eq]
 
 let pp_prelude ppf = function
   | Fpa -> Format.fprintf ppf "fpa"
   | Ria -> Format.fprintf ppf "ria"
   | Nra -> Format.fprintf ppf "nra"
 
+let compare_prelude p1 p2 =
+  match p1, p2 with
+  | Nra, Nra -> 0
+  | Nra, _ -> -1
+  | _, Nra -> 1
+
+  | Ria, Ria -> 0
+  | Ria, _ -> -1
+  | _, Ria -> 1
+
+  | Fpa, Fpa -> 0
+
 type t =
   | Prelude of prelude
   | ADT
   | AC
 [@@deriving eq]
 
+let compare t1 t2 =
+  match t1, t2 with
+  | Prelude p1, Prelude p2 -> compare_prelude p1 p2
+  | Prelude _, _ -> -1
+  | _, Prelude _ -> 1
+
+  | ADT, ADT -> 0
+  | ADT, _ -> -1
+  | _, ADT -> 1
+
+  | AC, AC -> 0
+
 let pp ppf = function
   | Prelude p -> pp_prelude ppf p
   | ADT -> Format.fprintf ppf "adt"
@@ -52,3 +76,5 @@ let default = all
 
 let preludes =
   List.filter_map (function | Prelude p -> Some p | _ -> None)
+
+module Set = Set.Make(struct type nonrec t = t let compare = compare end)