Add proper support for :named smtlib annotations

doc/tuto.md

@@ -69,8 +69,8 @@ let test file =
   (* We can loop over the parsed statements to generated the typed statements *)
   let final_state, rev_typed_stmts =
     List.fold_left (fun (state, acc) parsed_stmt ->
-      let state, typed_stmt = Typer.check state parsed_stmt in
-      (state, typed_stmt :: acc)
+      let state, typed_stmts = Typer.check state parsed_stmt in
+      (state, List.rev_append typed_stmts acc)
     ) (state, []) parsed_statements
   in
   let typed_stmts = List.rev rev_typed_stmts in

doc/type.md

@@ -42,8 +42,8 @@ let state =
 let () =
   let final_state, rev_typed_stmts =
     List.fold_left (fun (state, acc) parsed_stmt ->
-      let state, typed_stmt = Typer.check state parsed_stmt in
-      (state, typed_stmt :: acc)
+      let state, typed_stmts = Typer.check state parsed_stmt in
+      (state, List.rev_append typed_stmts acc)
     ) (state, []) parsed
   in
   let typed_stmts = List.rev rev_typed_stmts in

src/bin/main.ml

@@ -12,12 +12,15 @@ let debug_parsed_pipe st c =
       Dolmen.Std.Statement.print c;
   st, c
 
-let debug_typed_pipe st stmt =
-  if Loop.State.get Loop.State.debug st then
-    Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n@."
-      Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc
-      Loop.Typer_Pipe.print stmt;
-  st, stmt
+let debug_typed_pipe st stmts =
+  if Loop.State.get Loop.State.debug st then begin
+    List.iter (fun stmt ->
+        Format.eprintf "[logic][typed][%a] @[<hov>%a@]@\n"
+          Dolmen.Std.Loc.print_compact stmt.Loop.Typer_Pipe.loc
+          Loop.Typer_Pipe.print stmt) stmts;
+    Format.eprintf "@.";
+  end;
+  st, stmts
 
 
 (* Run dolmen (regular use) *)