Add proper support for :named smtlib annotations (#199)

* Add implicit decls/defs

* changes + some error handling

* fix typo

Co-authored-by: Basile Clément <[email protected]>

* review

* change some assert false into proper errors

---------

Co-authored-by: Basile Clément <[email protected]>

CHANGES.md

@@ -35,6 +35,10 @@ next
   non linearity and other arithmetic restrictions (PR#184)
 - More information for reserved Id, resulting in more precise
   errors when smt2 scripts use reserved ids (PR#193)
+- Expose implicit declarations/definitions that happen during
+  typechecking (PR#199)
+- Treat smtlib `:named` annotations as implicit definitions as
+  required by the spec (PR#199)
 
 ### Loop
 

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) *)

src/loop/parser.ml

@@ -110,7 +110,6 @@ module Make(State : State.S) = struct
   (* Helper functions *)
   (* ************************************************************************ *)
 
-
   let gen_of_llist l =
     let l = ref l in
     (fun () -> match Lazy.force !l with

src/loop/report.ml

@@ -170,7 +170,7 @@ module Error = struct
   let internal_error =
     mk ~code:Code.bug ~mnemonic:"internal-error"
       ~message:(fun fmt t ->
-          Format.fprintf fmt "%t" t)
+          Format.fprintf fmt "@[<v>%t@ Please report upstream, ^^@]" t)
       ~name:"Internal Error" ()
 
   let uncaught_exn =