Merge pull request #600 from proux01/accumulate_db_from_file

Enable loading db from files

Author: gares

README.md

@@ -181,13 +181,13 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
 - `Elpi Program <qname> <code>` lower level primitive letting one crate a
   command/tactic with a custom preamble `<code>`.
-- `From some.load.path Extra Dependency "filename" as <fname>`.
-- `Elpi Accumulate [<qname>] [<code>|File <fname>|Db <dbname>]`
-  adds code to the current program (or `<qname>` if specified).
+- `From some.load.path Extra Dependency <filename> as <fname>`.
+- `Elpi Accumulate [<dbname>|<qname>] [<code>|File <fname>|Db <dbname>]`
+  adds code to the current program (or `<dbname>` or `<qname>` if specified).
   The code can be verbatim, from a file or a Db.
+  File names `<fname>` must have been previously declared with the above command.
   It understands the `#[skip="rex"]` and `#[only="rex"]` which make the command
   a no op if the Coq version is matched (or not) by the given regular expression.
-  File names `<fname>` must have been previously declared with the above command.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).

src/coq_elpi_vernacular.ml

@@ -318,23 +318,31 @@ let run_in_program ?(program = current_program ()) ?(st_setup=fun x -> x) (loc,
           str" is unknown; please add a directive like 'From .. Extra Dependency .. as " ++
           Names.Id.print id ++ str"'.")) in
     try
-      let new_src_ast = List.map (fun fname ->
-        File {
-          fname;
-          fast = P.unit_from_file ~elpi fname;
-        }) s in
+      let new_src_ast = List.map (fun fname -> P.unit_from_file ~elpi fname) s in
+      if P.db_exists program then
+        P.accumulate_to_db program new_src_ast [] ~scope:Coq_elpi_utils.Regular
+      else
+        let new_src_ast = List.map2 (fun fname funit ->
+          File {
+            fname;
+            fast = funit;
+          }) s new_src_ast in
         P.accumulate program new_src_ast
     with Failure s ->  CErrors.user_err Pp.(str s)
   let accumulate_extra_deps ~atts:(only,ph) ?program ids = skip ~only ~ph (accumulate_extra_deps ?program) ids
 
   let accumulate_files ?(program=current_program()) s =
     let elpi = P.ensure_initialized () in
     try
-      let new_src_ast = List.map (fun fname ->
-        File {
-          fname;
-          fast = P.unit_from_file ~elpi fname;
-        }) s in
+      let new_src_ast = List.map (fun fname -> P.unit_from_file ~elpi fname) s in
+      if P.db_exists program then
+        P.accumulate_to_db program new_src_ast [] ~scope:Coq_elpi_utils.Regular
+      else
+        let new_src_ast = List.map2 (fun fname funit ->
+          File {
+            fname;
+            fast = funit;
+          }) s new_src_ast in
         P.accumulate program new_src_ast
     with Failure s ->  CErrors.user_err Pp.(str s)
   let accumulate_files ~atts:(only,ph) ?program s = skip ~only ~ph (accumulate_files ?program) s