fix: avoid accumulating Db's header twice

Author: gares

src/coq_elpi_programs.ml

@@ -16,16 +16,18 @@ module SLSet = Set.Make(struct type t = qualified_name let compare = compare_qua
 type src =
   | File of src_file
   | EmbeddedString of src_string
-  | Database of qualified_name
+  | DatabaseBody of qualified_name
+  | DatabaseHeader of src_db_header
 and src_file = {
   fname : string;
   fast : cunit;
 }
 and src_string = {
-  (* sloc : API.Ast.Loc.t;
-  sdata : string; *)
   sast : cunit;
 }
+and src_db_header = {
+  dast : cunit;
+}
 
 let alpha = 65599
 let combine_hash h1 h2 = h1 * alpha + h2
@@ -398,11 +400,13 @@ let get ?(fail_if_not_exists=false) p =
       (* undup *)
       | File { fast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
       | EmbeddedString { sast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
-      | Database n  when SLSet.mem n dbs -> units, dbs, prog
+      | DatabaseHeader { dast = (kn,_) } when Names.KNset.mem kn units -> units, dbs, prog
+      | DatabaseBody n  when SLSet.mem n dbs -> units, dbs, prog
       (* add *)
       | File { fast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
       | EmbeddedString { sast = (kn,_ as u) } -> (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
-      | Database n ->  units, SLSet.add n dbs, Some (Code.snoc_db_opt Hashtbl.hash n prog)
+      | DatabaseHeader { dast = (kn,_ as u) } ->  (Names.KNset.add kn units), dbs, Some (Code.snoc_opt u prog)
+      | DatabaseBody n ->  units, SLSet.add n dbs, Some (Code.snoc_db_opt Hashtbl.hash n prog)
       in
     let prog = Option.get prog in
     { units; dbs; sources_rev = prog; empty = empty && from = Initialization }
@@ -663,9 +667,8 @@ let compile ~loc src =
       lookup_chunk bh h src
     with Not_found ->
       match src with
-      | Chunk.Base { base = (k,u) } ->
-          let prog = extend_w_units ~base ~loc [u] in
-          cache_chunk bh h prog src
+      | Chunk.Base _ ->
+          base (* the base of dbs is accumulated with a Snoc so to avoid accumulating it twice when "Accumulate Db Header" is followed by "Accumulate Db" *)
       | Chunk.Snoc { prev; source_rev } ->
           let base = compile_chunk bh base prev in
           let prog = extend_w_units ~base ~loc (List.rev_map snd source_rev) in

src/coq_elpi_programs.mli

@@ -11,16 +11,19 @@ type program_name = Loc.t * qualified_name
 type src =
   | File of src_file
   | EmbeddedString of src_string
-  | Database of qualified_name
+  | DatabaseBody of qualified_name
+  | DatabaseHeader of src_db_header
 and src_file = {
   fname : string;
   fast : cunit;
 }
 and src_string = {
-  (* sloc : Ast.Loc.t;
-  sdata : string; *)
   sast : cunit;
 }
+and src_db_header = {
+  dast : cunit;
+}
+
 type nature = Command of { raw_args : bool } | Tactic | Program of { raw_args : bool } 
 
 

src/coq_elpi_vernacular.ml

@@ -277,19 +277,19 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
       P.accumulate_to_db program [new_ast] [] ~scope:Coq_elpi_utils.Regular
     | `Program base ->
       let new_ast = P.unit_from_string ~elpi ~base ~loc sloc s in
-      P.accumulate program [EmbeddedString { (*sloc = loc; sdata = s;*) sast = new_ast}]
+      P.accumulate program [EmbeddedString { sast = new_ast}]
   let accumulate_string ~atts:(only,ph) ~loc ?program sloc = skip ~only ~ph (accumulate_string ~loc ?program) sloc
 
 
   let accumulate_db ~loc ?(program=current_program()) name =
     let _ = P.ensure_initialized () in
-    if P.db_exists name then P.accumulate program [Database name]
+    if P.db_exists name then P.accumulate program [DatabaseHeader { dast = P.(header_of_db name) };DatabaseBody name]
     else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name name ++ str" not found")
   let accumulate_db ~atts:(only,ph) ~loc ?program name = skip ~only ~ph (accumulate_db ~loc ?program) name
 
   let accumulate_db_header ~loc ?(program=current_program()) name =
     let _ = P.ensure_initialized () in
-    if P.db_exists name then P.accumulate program [EmbeddedString { sast = P.header_of_db name } ]
+    if P.db_exists name then P.accumulate program [DatabaseHeader { dast = P.(header_of_db name) }]
     else CErrors.user_err Pp.(str "Db " ++ pr_qualified_name name ++ str" not found")
   let accumulate_db_header ~atts:(only,ph) ~loc ?program name = skip ~only ~ph (accumulate_db_header ~loc ?program) name
 

tests/test_API2.v

@@ -386,3 +386,21 @@ Elpi Query lp:{{
      test {{ fun z => S (fun x y => z z x y) }} {{ fun z => S (z z) }},
    ].
 }}.
+
+
+Elpi Db foo.db lp:{{ 
+  pred p o:int.
+  p 1.
+}}.
+Elpi Accumulate foo.db lp:{{
+  p 2.
+}}.
+Elpi Command query_foo.
+Elpi Accumulate Db Header foo.db.
+Elpi Accumulate lp:{{
+main _ :-
+  std.findall (p _) [p 1, p 2].
+}}.
+Elpi Accumulate Db foo.db.
+
+Elpi query_foo.