diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index 36d9ddf2d..8ad8e05dd 100644 --- a/src/coq_elpi_vernacular.ml +++ b/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); diff --git a/tests/test_API2.v b/tests/test_API2.v index 389b6ff12..bc665e26a 100644 --- a/tests/test_API2.v +++ b/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 *)