Add imperative mode

OCamlPro · Feb 6, 2025 · ed04f7c · ed04f7c
1 parent 6125ee1
commit ed04f7c
Show file tree

Hide file tree

Showing 11 changed files with 812 additions and 55 deletions.
diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml
@@ -358,7 +358,7 @@ let mk_context_opt replay replay_all_used_context replay_used_context
 let mk_execution_opt input_format parse_only ()
     preludes no_locs_in_answers colors_in_output no_headers_in_output
     no_formatting_in_output no_forced_flush_in_output pretty_output
-    type_only type_smt2
+    type_only type_smt2 imperative_mode
   =
   let answers_with_loc = not no_locs_in_answers in
   let output_with_colors = colors_in_output || pretty_output in
@@ -376,6 +376,7 @@ let mk_execution_opt input_format parse_only ()
   set_type_only type_only;
   set_type_smt2 type_smt2;
   set_preludes preludes;
+  set_imperative_mode imperative_mode;
   `Ok()
 
 let mk_internal_opt
@@ -789,12 +790,16 @@ let parse_execution_opt =
     let doc = "Stop after SMT2 typing." in
     Arg.(value & flag & info ["type-smt2"] ~docs ~doc) in
 
+  let imperative_mode =
+    let doc = "Starts Alt-Ergo in incremental mode" in
+    Arg.(value & flag & info ["incremental-mode"] ~docs ~doc)
+  in
 
   Term.(ret (const mk_execution_opt $
              input_format $ parse_only $ parsers $ preludes $
              no_locs_in_answers $ colors_in_output $ no_headers_in_output $
              no_formatting_in_output $ no_forced_flush_in_output $
-             pretty_output $ type_only $ type_smt2
+             pretty_output $ type_only $ type_smt2 $ imperative_mode
             ))
 
 let parse_halt_opt =