Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix: Do not load preludes twice #1235

Merged
merged 1 commit into from
Sep 17, 2024
Merged

fix: Do not load preludes twice #1235

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 8 additions & 7 deletions src/bin/common/parse_command.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand Down
28 changes: 27 additions & 1 deletion src/lib/util/theories.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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)
Loading