fix: check accumlated clauses in the Db only

Author: gares

src/coq_elpi_vernacular.ml

@@ -192,12 +192,14 @@ let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_
         | Summary.Stage.Synterp -> Coq_elpi_builtins_synterp.clauses_for_later_synterp
         | Summary.Stage.Interp  -> Coq_elpi_builtins.clauses_for_later_interp)
         state in
+
+    (* TODO: this code is duplicate, see set_accumulate_to_db_* *)
     let elpi = P.ensure_initialized () in
     let clauses_to_add = clauses_to_add |> group_clauses |>
       List.map (fun (dbname,asts,vs,scope) ->
+        let base = P.get_and_compile_existing_db ~loc dbname in
         (* maybe this should be a fold otherwise all clauses have to be independent (the second cannot mention the first one) *)
-        let units = asts |> List.map (fun ast -> P.unit_from_ast ~elpi None ~base:program_ast ~loc ast) in
-      (* let units = units |> List.map (fun unit -> P.intern_unit (None,unit,flags)) in *)
+        let units = asts |> List.map (fun ast -> P.unit_from_ast ~elpi None ~base ~loc ast) in
       dbname,units,vs,scope) in
     clauses_to_add |> List.iter (fun (dbname,units,vs,scope) ->
       P.accumulate_to_db dbname units vs ~scope);

tests/test_API2.v

@@ -404,3 +404,15 @@ main _ :-
 Elpi Accumulate Db foo.db.
 
 Elpi query_foo.
+
+
+Elpi Command acc_foo.
+Elpi Accumulate Db Header foo.db.
+Elpi Accumulate lp:{{
+pred r i:list int.
+main _ :-
+  coq.elpi.accumulate _ "foo.db" (clause _ _ (r [])).
+}}.
+Elpi Accumulate Db foo.db.
+
+Fail Elpi acc_foo. (* since r has no type in foo.db *)