Merge pull request #719 from LPCIC/elpi-2.0

port to Elpi 2.0

.nix/config.nix

@@ -32,7 +32,7 @@ let master = [
         coq.override.version = "8.20";
       };
       ocamlPackages = {
-        elpi.override.version = "1.20.0";
+        elpi.override.version = "v2.0.3";
       };
     };
 
@@ -42,7 +42,7 @@ let master = [
         coqeal.job = false;  # broken in master, c.f. https://github.com/coq/coq/pull/19228
       };
       ocamlPackages = {
-        elpi.override.version = "1.20.0";
+        elpi.override.version = "v2.0.3";
       };
     };
 
@@ -54,7 +54,7 @@ let master = [
       ocamlPackages = {
         # when updating this, don't forget to update dune-project
         # then use it to regenerate coq-elpi.opam
-        elpi.override.version = "1.18.2";
+        elpi.override.version = "v2.0.3";
       };
     };
 

Changelog.md

@@ -1,5 +1,11 @@
 # Development version
 
+### Vernacular
+- `Elpi Accumulate Db Header <db>` to accumulate just the `Db` declaration
+  but no code added after that
+- `Elpi Typecheck` is deprecated and is a no-op since `Elpi Accumulate`
+  performs type checking incrementally
+
 ### Build system
 - Support dune workspace build with `elpi`
 

Makefile

@@ -2,10 +2,12 @@ dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
 all:
 	$(call dune,build)
+	$(call dune,build) builtin-doc
 .PHONY: all
 
 build-core:
 	$(call dune,build) theories
+	$(call dune,build) builtin-doc
 .PHONY: build-core
 
 build-apps:
@@ -14,6 +16,7 @@ build-apps:
 
 build:
 	$(call dune,build) -p coq-elpi @install
+	$(call dune,build) builtin-doc
 .PHONY: build
 
 test-core:
@@ -46,7 +49,7 @@ doc: build
 			-R $(shell pwd)/_build/install/default/lib/coq/user-contrib/elpi_elpi elpi_elpi \
 			-R $(shell pwd)/_build/install/default/lib/coq/user-contrib/elpi elpi \
 			$(tut) &&) true
-	@cp _build/default/examples/stlc.html doc/
+	@cp ./_build/default/examples/stlc.txt doc/
 	@cp etc/tracer.png doc/
 
 clean:

README.md

@@ -182,14 +182,39 @@ 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 [<dbname>|<qname>] [<code>|File <fname>|Db <dbname>]`
+- `From some.load.path Extra Dependency <filename> as <fname>` declares `<fname>`
+   as a piece of code that can be accumulated via `Elpi Accumulate File`.
+   The content is given in the external file `<filename>` to be found in
+   the Coq load path `some.load.path`.
+- `Elpi File <fname> <code>.` declares `<fname>`
+   as a piece of code that can be accumulated via `Elpi Accumulate File`.
+   This time the code is given in the .v file.
+   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
+- `Elpi Accumulate [<dbname>|<qname>] [<code>|File [Signature] <fname>|Db [Header] <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.
+  File names `<fname>` must have been previously declared with
+  `Extra Dependency` or `Elpi File`.
+  Accumulating `File Signature <fname>` only adds the signautre declarations
+  (kinds, types, modes, type abbreviations) from `<fname>` skipping the code
+  (clauses/rules).
+  Accumulating `Db Header <dbname>`, instead of `Db <dbname>`, accumulates
+  only the first chunk of code associated with Db, typically the type
+  declaration of the predicates that live in the Db. When defining a command
+  or tactic it can be useful to first accumulate the Db header, then some
+  code (possibly calling the predicate living in the Db), and finally
+  accumulating the (full) Db.
+  Note that when a command is executed it may need to be (partially)
+  recompiled, e.g. if the Db was updated. In this case all the code accumulated
+  after the Db (but not after its header) may need to be recompiled. Hence
+  we recommend to accumulate Dbs last.
   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.
-  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
+  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands).
+  It understands the `#[local]`, `#[global]`, and `#[superglobal]` scope attributes,
+  although only when accumulating to a `<dbname>` (all accumulations to a program
+  are `#[superglobal]`). Default accumulation to db is the equivalent of `#[export]`.
+  See the Coq reference manual for the meaning of these scopes.
 - `Elpi Typecheck [<qname>]` typechecks the current program (or `<qname>` if
   specified).
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
@@ -204,10 +229,9 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   tracing for Elpi's [trace browser]().
 - `Elpi Bound Steps <number>` limits the number of steps an Elpi program can
   make.
-- `Elpi Print <qname> [<string> <filter>*]` prints the program `<qname>` to an
-  HTML file named `<qname>.html` and a text file called `<qname>.txt`
-  (or `<string>` if provided) filtering out clauses whose file or clause-name
-  matches `<filter>`.
+- `Elpi Print <qname> [<string> <filter>*]` prints the program `<qname>` to 
+  a text file called `<qname>.txt` (or `<string>` if provided) filtering out
+  clauses whose file or clause-name matches `<filter>`.
   It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 
 where:
@@ -220,6 +244,8 @@ where:
   `lp:{{ coq.say "hello!" }}` becomes `" coq.say ""hello!"" "`).
 - `<filename>` is a string containing the path of an external file, e.g.
   `"this_file.elpi"`.
+- `<fname>` is a qualified Coq name, eg `foo.elpi` (note that `Extra Dependency`
+  only allows simple identifiers).
 - `<start>` and `<stop>` are numbers, e.g. `17 24`.
 - `<predicate-filter>` is a regexp against which the predicate name is matched,
   e.g. `"derive.*"`.

_CoqProject

@@ -57,72 +57,11 @@
 -Q _build/default/apps/tc/elpi elpi.apps.tc.elpi
 -Q apps/tc/examples elpi.apps.tc.examples
 -Q _build/default/apps/tc/examples elpi.apps.tc.examples
--Q apps/tc/tests elpi.apps.tc.tests
 -Q _build/default/apps/tc/tests elpi.apps.tc.tests
 -Q apps/tc/theories elpi.apps.tc
 -Q _build/default/apps/tc/theories elpi.apps.tc
 
 # Cram tests.
 
--Q tests/link_order5.t elpi.test
--Q tests/checker.t elpi.test
--Q tests/query_extra_dep.t elpi.test
--Q tests/libobject_C.t elpi.test
--Q tests/link_order3.t elpi.test
--Q tests/ltac3.t elpi.test
--Q tests/synterp.t elpi.test
--Q tests/link_order6.t elpi.test
--Q tests/API2.t elpi.test
--Q tests/glob.t elpi.test
--Q tests/require_bad_order.t elpi.test
--Q tests/API_arguments.t elpi.test
--Q tests/link_order9.t elpi.test
--Q tests/API_typecheck.t elpi.test
--Q tests/link_order7.t elpi.test
--Q tests/libobject_A.t elpi.test
--Q tests/libobject_B.t elpi.test
--Q tests/vernacular1.t elpi.test
--Q tests/API_section.t elpi.test
--Q tests/tactic.t elpi.test
--Q tests/link_perf.t elpi.test
--Q tests/API_elaborate.t elpi.test
--Q tests/link_order_import3.t elpi.test
--Q tests/COQ_ELPI_ATTRIBUTES.t elpi.test
--Q tests/elaborator.t elpi.test
--Q tests/HOAS.t elpi.test
--Q tests/API_notations.t elpi.test
--Q tests/arg_HOAS.t elpi.test
--Q tests/link_order_import2.t elpi.test
--Q tests/link_order2.t elpi.test
--Q tests/link_order8.t elpi.test
--Q tests/cache_async.t elpi.test
--Q tests/API_new_pred.t elpi.test
--Q tests/quotation.t elpi.test
--Q tests/ltac2.t elpi.test
--Q tests/perf_calls.t elpi.test
--Q tests/link_order1.t elpi.test
--Q tests/link_order_import0.t elpi.test
--Q tests/ltac.t elpi.test
--Q tests/link_order4.t elpi.test
--Q tests/API_env.t elpi.test
--Q tests/toposort.t elpi.test
--Q tests/link_order_import1.t elpi.test
--Q tests/API_module.t elpi.test
--Q tests/vernacular2.t elpi.test
--Q tests/API.t elpi.test
--Q tests/ctx_cache.t elpi.test
--Q tests/API_TC_CS.t elpi.test
--Q tests/example_abs_evars.t elpi.test
--Q tests/example_curry_howard_tactics.t elpi.test
--Q tests/example_data_base.t elpi.test
--Q tests/example_fuzzer.t elpi.test
--Q tests/example_generalize.t elpi.test
--Q tests/example_import_projections.t elpi.test
--Q tests/example_record_expansion.t elpi.test
--Q tests/example_record_to_sigma.t elpi.test
--Q tests/example_reduction_surgery.t elpi.test
--Q tests/example_reflexive_tactic.t elpi.test
--Q tests/tutorial_coq_elpi_command.t elpi.test
--Q tests/tutorial_coq_elpi_HOAS.t elpi.test
--Q tests/tutorial_coq_elpi_tactic.t elpi.test
--Q tests/tutorial_elpi_lang.t elpi.test
+-Q tests elpi.tests
+-Q _build/default/tests elpi.tests

apps/NES/tests/test_NES_lib.v

@@ -23,7 +23,7 @@ Elpi Command Make.
     nes.end-path,
   ].
 }}.
-Elpi Typecheck.
+
 Elpi Export Make.
 
 Make Cats.And.Dogs.

apps/NES/theories/NES.v

@@ -31,7 +31,7 @@ main _ :-
   coq.say "NES: registered namespaces" NS.
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.Status.
 
 Elpi Command NES.Begin.
@@ -45,7 +45,7 @@ Elpi Command NES.Begin.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.begin-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.Begin.
 
 Elpi Command NES.End.
@@ -59,7 +59,7 @@ Elpi Command NES.End.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.end-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.End.
 
 
@@ -74,7 +74,7 @@ Elpi Command NES.Open.
 
 }}.
 #[interp] Elpi Accumulate lp:{{ main _ :- nes.open-path. }}.
-Elpi Typecheck.
+
 Elpi Export NES.Open.
 
 (* List the contents a namespace *)
@@ -93,7 +93,7 @@ Elpi Command NES.List.
   main _ :- coq.error "usage: NES.List <DotSeparatedPath>".
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.List.
 
 (* NES.List with types *)
@@ -118,5 +118,5 @@ Elpi Accumulate lp:{{
   main _ :- coq.error "usage: NES.Print <DotSeparatedPath>".
 
 }}.
-Elpi Typecheck.
+
 Elpi Export NES.Print.

apps/coercion/README.md

@@ -36,7 +36,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
 coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck coercion. (* checks the elpi program is OK *)
 
 Check True && False.
 ```

apps/coercion/src/coq_elpi_coercion_hook.mlg

@@ -24,23 +24,25 @@ let build_expected_type env sigma expected =
 let return s g t = Some (s,g,t)
 
 let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected =
-  let loc = API.Ast.Loc.initial "(unknown)" in
   let atts = [] in
   let sigma, expected, retype = build_expected_type env sigma expected in
   let sigma, goal = Evarutil.new_evar env sigma expected in
   let goal_evar, _ = EConstr.destEvar sigma goal in
-  let query ~depth state =
-    let state, (loc, q), gls =
-      Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [v; inferred])
-        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth state in
+  let query state =
+    let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in
+    let depth = 0 in
+    let state, q, gls =
+      Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[v; inferred]
+        ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth ~base:() state in
     let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in
     let state = API.State.set Coq_elpi_builtins.tactic_mode state true in
-    state, (loc, qatts), gls
+    state, qatts, gls
   in
-  match Interp.get_and_compile program with
+  let loc = Loc.initial Loc.ToplevelInput in
+  match Interp.get_and_compile ~loc program with
   | None -> None
   | Some (cprogram, _) ->
-    match Interp.run ~static_check:false cprogram (`Fun query) with
+    match Interp.run ~loc cprogram (Fun (query)) with
     | API.Execute.Success solution ->
       let gls = Evar.Set.singleton goal_evar in
       let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in

apps/coercion/tests/coercion.t/test.v

@@ -8,7 +8,6 @@ coercion _ {{ True }} {{ Prop }} {{ bool }} {{ true }}.
 coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
-Elpi Typecheck coercion.
 
 Check True && False.
 
@@ -22,7 +21,6 @@ coercion _ N {{ nat }} {{ ringType_sort lp:R }} {{ natmul lp:R lp:N }} :-
   coq.typecheck R {{ ringType }} ok.
 
 }}.
-Elpi Typecheck coercion.
 
 Section TestNatMul.
 

apps/coercion/tests/coercion_open.t/test.v

@@ -4,7 +4,7 @@ From Coq Require Import Arith ssreflect.
 
 Ltac my_solver := trivial with arith.
 
-Elpi Accumulate coercion.db lp:{{
+Elpi Accumulate coercion lp:{{
 
 coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
   % we unfold letins since the solve is dumb
@@ -17,7 +17,6 @@ coercion _ X Ty {{ @sig lp:Ty lp:P }} Solution :- std.do! [
 ].
 
 }}.
-Elpi Typecheck coercion.
 
 Goal {x : nat | x > 0}.
 apply: 3.

apps/coercion/theories/coercion.v

@@ -15,11 +15,12 @@ pred coercion i:goal-ctx, i:term, i:term, i:term, o:term.
 }}.
 
 Elpi Tactic coercion.
+Elpi Accumulate Db Header coercion.db.
 Elpi Accumulate lp:{{
 
 solve (goal Ctx _ Ty Sol [trm V, trm VTy]) _ :- coercion Ctx V VTy Ty Sol.
 
 }}.
 Elpi Accumulate Db coercion.db.
-Elpi Typecheck.
+
 Elpi CoercionFallbackTactic coercion.

apps/cs/README.md

@@ -38,7 +38,6 @@ cs _ {{ sort lp:Sol }} {{ nat }} :-
   Sol = {{ Build_S nat }}.
 
 }}.
-Elpi Typecheck canonical_solution.
 
 Check eq_refl _ : (sort _) = nat.
 ```