Update Dolmen state creation

colibri2/solver/input.ml

@@ -152,6 +152,9 @@ module Typer = struct
 
   include
     Dolmen_loop.Typer.Make (Dolmen.Std.Expr) (Dolmen.Std.Expr.Print) (State) (T)
+
+  let init_pipe = init
+  let init = T.init
 end
 
 type tag_colibri2 = Goal
@@ -571,8 +574,8 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
   let () = if bt then Printexc.record_backtrace true in
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout) in
   (* State creation *)
+  let dir, source = split_input input in
   let logic_file : _ State.file =
-    let dir, source = split_input input in
     {
       lang = input_lang;
       mode = input_mode;
@@ -581,26 +584,30 @@ let mk_state ?(gc = false) ?(gc_opt = Gc.get ()) ?(bt = true) ?(colors = true)
       loc = Dolmen.Std.Loc.mk_file "";
     }
   in
+  let response_file : _ State.file =
+    {
+      lang = None;
+      mode = None;
+      dir;
+      source = `Raw ("", "");
+      loc = Dolmen.Std.Loc.mk_file "";
+    }
+  in
   let ctx =
     create_ctx ?step_limit ?last_effort_limit ?options ?print_success
       ?negate_goal learning theories
   in
   (* State creation *)
   let set = State.set in
-  State.empty |> set solver_state ctx |> set State.debug debug
-  |> set State.report_style Contextual
-  |> set State.reports
-       (Dolmen_loop.Report.Conf.mk
-          ~default:Dolmen_loop.Report.Warning.Status.Disabled)
-  |> set State.max_warn max_warn
-  |> set State.cur_warn 0
-  |> set State.time_limit time_limit
-  |> set State.size_limit size_limit
-  |> set State.logic_file logic_file
-  |> set Header.header_check header_check
-  |> set Header.header_state Dolmen_loop.Headers.empty
-  |> set Header.header_licenses header_licenses
-  |> set Header.header_lang_version header_lang_version
-  |> set Typer.type_check type_check
-  |> set Typer.ty_state (Dolmen_loop.Typer.new_state ())
-  |> set Typer.smtlib2_forced_logic None
+  State.empty |> set solver_state ctx
+  |> State.init ~debug ~report_style:Contextual
+       ~reports:
+         (Dolmen_loop.Report.Conf.mk
+            ~default:Dolmen_loop.Report.Warning.Status.Disabled)
+       ~max_warn ~time_limit ~size_limit ~logic_file ~response_file
+  |> Parser.init
+  |> Typer.init
+       ~ty_state:(Dolmen_loop.Typer.new_state ())
+       ~smtlib2_forced_logic:None
+  |> Typer.init_pipe ~type_check
+  |> Header.init ~header_check ~header_licenses ~header_lang_version

colibrics/bin/loop.ml

@@ -13,6 +13,9 @@ module Typer = struct
   module T = Dolmen_loop.Typer.Typer(State)
   include T
   include Dolmen_loop.Typer.Make(Dolmen.Std.Expr)(Dolmen.Std.Expr.Print)(State)(T)
+
+  let init_pipe = init
+  let init = T.init
 end
 
 let solver_state : Dolmen_to_colibrics.t State.key = State.create_key ~pipe:"" "solver_state"

colibrics/bin/options.ml

@@ -46,8 +46,8 @@ let mk_state
   let () = if bt then Printexc.record_backtrace true in
   let () = if gc then at_exit (fun () -> Gc.print_stat stdout) in
   (* State creation *)
-  let logic_file : _ State.file =
     let dir, source = split_input input in
+  let logic_file : _ State.file =
     {
       lang = input_lang;
       mode = input_mode;
@@ -56,27 +56,28 @@ let mk_state
       loc = Dolmen.Std.Loc.mk_file "";
     }
   in
+  let response_file : _ State.file = {
+    lang = None; mode = None; dir;
+    loc = Dolmen.Std.Loc.mk_file "";
+    source = `Raw ("", "");
+  } in
   let ctx = Dolmen_to_colibrics.create ()
   in
   (* State creation *)
   let set = State.set in
-  State.empty |> set solver_state ctx |> set State.debug debug
-  |> set State.report_style Minimal
-  |> set State.reports
-       (Dolmen_loop.Report.Conf.mk
-          ~default:Dolmen_loop.Report.Warning.Status.Disabled)
-  |> set State.max_warn max_warn
-  |> set State.cur_warn 0
-  |> set State.time_limit time_limit
-  |> set State.size_limit size_limit
-  |> set State.logic_file logic_file
-  |> set Header.header_check header_check
+  State.empty |> set solver_state ctx
   |> set Header.header_state Dolmen_loop.Headers.empty
-  |> set Header.header_licenses header_licenses
-  |> set Header.header_lang_version header_lang_version
-  |> set Typer.type_check type_check
-  |> set Typer.ty_state (Dolmen_loop.Typer.new_state ())
-  |> set Typer.smtlib2_forced_logic None
+  |> State.init ~debug ~report_style:Minimal
+       ~reports:
+         (Dolmen_loop.Report.Conf.mk
+            ~default:Dolmen_loop.Report.Warning.Status.Disabled)
+       ~max_warn ~time_limit ~size_limit ~logic_file ~response_file
+  |> Parser.init
+  |> Typer.init
+       ~ty_state:(Dolmen_loop.Typer.new_state ())
+       ~smtlib2_forced_logic:None
+  |> Typer.init_pipe ~type_check
+  |> Header.init ~header_check ~header_licenses ~header_lang_version
 
 (* Input source converter *)
 (* ************************************************************************* *)