Minor fixes to interpreter and binary

bin/main.ml

@@ -19,46 +19,40 @@
 open Smtml
 open Solver_dispatcher
 
-let run debug solver prover_mode _print_statistics file =
+let get_solver debug solver prover_mode =
   let module Mappings =
     (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
   in
   Mappings.set_debug debug;
-  let module Solver =
-    ( val match prover_mode with
-          | Options.Batch -> (module Solver.Batch (Mappings))
-          | Cached -> (module Solver.Cached (Mappings))
-          | Incremental -> (module Solver.Incremental (Mappings))
-        : Solver_intf.S )
-  in
+  match prover_mode with
+  | Options.Batch -> (module Solver.Batch (Mappings) : Solver_intf.S)
+  | Cached -> (module Solver.Cached (Mappings))
+  | Incremental -> (module Solver.Incremental (Mappings))
+
+let run debug solver prover_mode _print_statistics file =
+  let module Solver = (val get_solver debug solver prover_mode) in
   let module Interpret = Interpret.Make (Solver) in
   let ast = Compile.until_rewrite file in
-  let _ = Interpret.start ast in
+  let _ : Interpret.exec_state = Interpret.start ast in
   ()
 
 let test debug solver prover_mode print_statistics files =
-  let module Mappings =
-    (val mappings_of_solver solver : Mappings_intf.S_with_fresh)
-  in
-  Mappings.set_debug debug;
-  let module Solver =
-    ( val match prover_mode with
-          | Options.Batch -> (module Solver.Batch (Mappings))
-          | Cached -> (module Solver.Cached (Mappings))
-          | Incremental -> (module Solver.Incremental (Mappings))
-        : Solver_intf.S )
-  in
+  let module Solver = (val get_solver debug solver prover_mode) in
   let module Interpret = Interpret.Make (Solver) in
+  (* TODO: Add proper logs *)
+  let debug fmt k = if debug then k (Fmt.epr fmt) in
   let rec test_path state path =
     if Sys.is_directory (Fpath.to_string path) then test_dir state path
-    else
+    else begin
+      debug "File %a...@." (fun k -> k Fpath.pp path);
       let ast = Compile.until_rewrite path in
       Some (Interpret.start ?state ast)
+    end
   and test_dir state d =
     let result =
       Bos.OS.Dir.fold_contents
         (fun path state ->
-          if Fpath.has_ext ".smtml" path then test_path state path else state )
+          if Fpath.has_ext ".smt2" path then test_path state path else state )
         state d
     in
     match result with Error (`Msg e) -> failwith e | Ok state -> state

src/ast/symbol.ml

@@ -98,7 +98,7 @@ let pp_namespace fmt = function
 let pp_name fmt = function
   | Simple name -> Fmt.string fmt name
   | Indexed { basename; indices } ->
-    Fmt.pf fmt "(%s@ %a)" basename (Fmt.list ~sep:Fmt.sp Fmt.string) indices
+    Fmt.pf fmt "(%s %a)" basename (Fmt.list ~sep:Fmt.sp Fmt.string) indices
 
 let pp fmt { name; _ } = pp_name fmt name
 

src/interpret/interpret.ml

@@ -18,6 +18,11 @@
 
 include Interpret_intf
 
+(* TODO: Add proper logs *)
+let debug_interpreter = false
+
+let debug fmt k = if debug_interpreter then k (Fmt.epr fmt)
+
 module Make (Solver : Solver_intf.S) = struct
   open Ast
 
@@ -65,8 +70,11 @@ module Make (Solver : Solver_intf.S) = struct
       let solver = Solver.create ~logic () in
       Solver.push solver;
       { state with solver }
+    | Set_info attr ->
+      debug "Ignoring (set-info %a)@." (fun k -> k Expr.pp attr);
+      state
     | Get_assertions | Get_assignment | Reset | Reset_assertions | Get_info _
-    | Get_option _ | Get_value _ | Set_info _ | Set_option _ ->
+    | Get_option _ | Get_value _ | Set_option _ ->
       Fmt.failwith "eval: TODO evaluation of command"
 
   let rec loop (state : exec_state) : exec_state =