Remove infer_input_format option

src/bin/common/parse_command.ml

@@ -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;

src/bin/common/solving_loop.ml

@@ -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
@@ -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 (

src/bin/js/options_interface.ml

@@ -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;

src/lib/util/options.ml

@@ -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
@@ -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
 
@@ -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

src/lib/util/options.mli

@@ -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}
 
@@ -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
 
@@ -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

src/parsers/parsers.ml

@@ -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