fix: Do not load preludes twice (#1235) (#1237)

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.

Author: bclement-ocp

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 (

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)