Skip to content

Commit

Permalink
Remove infer_input_format option (#858)
Browse files Browse the repository at this point in the history
The use of `infer_input_format` / `input_format` is confusing:

 - By default, `infer_input_format` is `true`
 - We only ever look at `input_format` if `infer_input_format` is
   `false`
 - We only set `infer_input_format` to `false` when we explicitly
   set `input_format` to a non-default value

Since we can never look at the default value of `input_format`, this
patch removes `infer_input_format` and makes `input_format` an `option`
to better align with the way it is used.
  • Loading branch information
bclement-ocp authored Oct 4, 2023
1 parent d4afce1 commit af032ee
Show file tree
Hide file tree
Showing 6 changed files with 18 additions and 35 deletions.
5 changes: 0 additions & 5 deletions src/bin/common/parse_command.ml
Original file line number Diff line number Diff line change
Expand Up @@ -307,11 +307,6 @@ let mk_execution_opt input_format parse_only ()
let output_with_formatting = (not no_formatting_in_output) || pretty_output in
let output_with_forced_flush =
(not no_forced_flush_in_output) && (not pretty_output) in
set_infer_input_format (Option.is_none input_format);
let input_format = match input_format with
| None -> Native
| Some fmt -> fmt
in
set_answers_with_loc answers_with_loc;
set_output_with_colors output_with_colors;
set_output_with_headers output_with_headers;
Expand Down
15 changes: 7 additions & 8 deletions src/bin/common/solving_loop.ml
Original file line number Diff line number Diff line change
Expand Up @@ -161,16 +161,16 @@ let main () =
let with_infer_output_format =
with_opt Options.(get_infer_output_format, set_infer_output_format)
in
let with_infer_input_format =
with_opt Options.(get_infer_input_format, set_infer_input_format)
let with_input_format =
with_opt Options.(get_input_format, set_input_format)
in
let theory_preludes =
Options.get_theory_preludes ()
|> List.to_seq
|> Seq.flat_map (fun theory ->
let filename = Theories.filename theory in
let content = Theories.content theory in
with_infer_input_format true @@ fun () ->
with_input_format None @@ fun () ->
with_infer_output_format false @@ fun () ->
I.parse_file
~content
Expand Down Expand Up @@ -309,11 +309,10 @@ let main () =
let dir = Filename.dirname path in
let filename = Filename.basename path in
let lang =
if Options.get_infer_input_format() then None else
match Options.get_input_format () with
| Options.Native -> Some Dl.Logic.Alt_ergo
| Options.Smtlib2 -> Some (Dl.Logic.Smtlib2 `Latest)
| Options.Why3 | Options.Unknown _ -> None
match Options.get_input_format () with
| Some Native -> Some Dl.Logic.Alt_ergo
| Some Smtlib2 -> Some (Dl.Logic.Smtlib2 `Latest)
| None | Some (Why3 | Unknown _) -> None
in
let source =
if Filename.check_suffix path ".zip" then (
Expand Down
5 changes: 1 addition & 4 deletions src/bin/js/options_interface.ml
Original file line number Diff line number Diff line change
Expand Up @@ -140,10 +140,7 @@ let set_options r =
set_options_opt Options.set_save_used_context r.save_used_context;

set_options_opt Options.set_answers_with_loc r.answers_with_loc;
set_options_opt Options.set_input_format
(get_input_format r.input_format);
Options.set_infer_input_format
(get_input_format r.input_format |> Option.is_none);
Options.set_input_format (get_input_format r.input_format);
set_options_opt Options.set_parse_only r.parse_only;
set_options_opt Options.set_preludes r.preludes;
set_options_opt Options.set_type_only r.type_only;
Expand Down
5 changes: 1 addition & 4 deletions src/lib/util/options.ml
Original file line number Diff line number Diff line change
Expand Up @@ -260,8 +260,7 @@ let output_with_headers = ref true
let output_with_formatting = ref true
let output_with_forced_flush = ref true
let frontend = ref "legacy"
let input_format = ref Native
let infer_input_format = ref true
let input_format = ref None
let parse_only = ref false
let preludes = ref []
let theory_preludes = ref Theories.default_preludes
Expand All @@ -275,7 +274,6 @@ let set_output_with_formatting b = output_with_formatting := b
let set_output_with_forced_flush b = output_with_forced_flush := b
let set_frontend f = frontend := f
let set_input_format f = input_format := f
let set_infer_input_format b = infer_input_format := b
let set_parse_only b = parse_only := b
let set_preludes p = preludes := p

Expand All @@ -290,7 +288,6 @@ let get_output_with_formatting () = !output_with_formatting
let get_output_with_forced_flush () = !output_with_forced_flush
let get_frontend () = !frontend
let get_input_format () = !input_format
let get_infer_input_format () = !infer_input_format
let get_parse_only () = !parse_only
let get_preludes () = !preludes
let get_theory_preludes () = !theory_preludes
Expand Down
17 changes: 6 additions & 11 deletions src/lib/util/options.mli
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ val set_instantiation_heuristic : instantiation_heuristic -> unit
val set_inline_lets : bool -> unit

(** Set [input_format] accessible with {!val:get_input_format} *)
val set_input_format : input_format -> unit
val set_input_format : input_format option -> unit

(** Set [interpretation] accessible with {!val:get_interpretation}
Expand Down Expand Up @@ -338,9 +338,6 @@ val set_output_with_formatting : bool -> unit
{!val:get_output_with_forced_flush} *)
val set_output_with_forced_flush : bool -> unit

(** Set [infer_input_format] accessible with {!val:get_infer_input_format} *)
val set_infer_input_format : bool -> unit

(** Set [infer_output_format] accessible with {!val:get_infer_output_format} *)
val set_infer_output_format : bool -> unit

Expand Down Expand Up @@ -615,14 +612,12 @@ val get_frontend : unit -> string
(** Value specifying the default input format. Useful when the extension
does not allow to automatically select a parser (eg. JS mode, GUI
mode, ...). possible values are
{ul {- native} {- smtlib2} {- why3}} *)
val get_input_format : unit -> input_format
(** Default to [Native] *)
{ul {- native} {- smtlib2} {- why3}}
(** [true] if Alt-Ergo infers automatically the input format according to the
file extension. [false] if an input format is set with -i option *)
val get_infer_input_format : unit -> bool
(** Default to [true] *)
If [None], Alt-Ergo will automatically infer the input format according to
the file extension. *)
val get_input_format : unit -> input_format option
(** Default to [None] *)

(** [true] if the program shall stop after parsing. *)
val get_parse_only : unit -> bool
Expand Down
6 changes: 3 additions & 3 deletions src/parsers/parsers.ml
Original file line number Diff line number Diff line change
Expand Up @@ -82,15 +82,15 @@ let get_input_parser fmt =
| Options.Unknown s -> find_parser s s

let get_parser ext_opt =
if Options.get_infer_input_format () then
match Options.get_input_format () with
| Some input_format -> get_input_parser input_format
| None ->
match ext_opt with
| Some ext ->
get_input_parser (Options.match_extension ext)
| None ->
error
(Parser_error "Error: no extension found, can't infer input format@.")
else
get_input_parser (Options.get_input_format ())

let parse_file ?lang lexbuf =
let module Parser = (val get_parser lang : PARSER_INTERFACE) in
Expand Down

0 comments on commit af032ee

Please sign in to comment.