synterp

Author: gares

.github/workflows/doc.yml

@@ -25,7 +25,7 @@ jobs:
     - name: setup ocaml
       uses: avsm/setup-ocaml@v1
       with:
-        ocaml-version: 4.09.1
+        ocaml-version: 4.10.1
 
     - name: install deps
       run: |

.github/workflows/main.yml

@@ -18,8 +18,7 @@ jobs:
         coq_version:
           - '8.18'
         ocaml_version:
-          - '4.09-flambda'
-          - '4.13-flambda'
+          - '4.14-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

Changelog.md

@@ -1,6 +1,21 @@
 # Changelog
 
-## Unreleased - 09/11/2023
+## [2.0.0] - Unreleased
+
+Requires Elpi 1.18.1 and Coq 8.18.
+
+This major release accommodates for the separation of parsing from execution
+of Coq 8.18 enabling Coq-Elpi programs to be run efficiently (and correctly)
+under VSCoq 2.0.
+
+### Documentation
+- New section about parsing/execution separation in the [Writing commands in Elpi](https://lpcic.github.io/coq-elpi/tutorial_coq_elpi_command.html) tutorial
+
+### Commands
+- New `Elpi *` commands understand the `#[phase]` attribute, see the doc in
+  the [README](README.md#vernacular-commands) file, and the section
+  about the [separation of parsing from execution](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
+- New `Elpi Export` understands an `As` clause to rename or alias a program when exported
 
 ### API
 - Change `coq.elpi.add-predicate` now locality can be changed
@@ -13,6 +28,11 @@
 - New `coq.ltac.fresh-id` to generate fresh names in the proof context
 - New `@no-tc!` attribute supported by `coq.ltac.call-ltac1`
 - New `coq.TC.get-inst-prio` returns the `tc-priority` of an instance
+- New `synterp-action` datatype
+- New `coq.replay-all-missing-synterp-actions`
+- New `coq.replay-synterp-action`
+- New `coq.next-synterp-action`
+- New `coq.synterp-actions` (parsing phase only)
 
 ### Apps 
 - New `tc` app providing an implementation of a type class solver written in elpi.

Makefile

@@ -91,13 +91,19 @@ doc: $(DOCDEP)
 
 .PHONY: force build all test doc
 
-Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_config.ml _CoqProject
+Makefile.coq Makefile.coq.conf: src/coq_elpi_builtins_HOAS.ml src/coq_elpi_builtins_arg_HOAS.ml src/coq_elpi_config.ml _CoqProject
 	@$(COQBIN)/coq_makefile -f _CoqProject -o Makefile.coq
 	@$(MAKE) --no-print-directory -f Makefile.coq .merlin
 Makefile.test.coq Makefile.test.coq.conf: _CoqProject.test
 	@$(COQBIN)/coq_makefile -f _CoqProject.test -o Makefile.test.coq
 Makefile.examples.coq Makefile.examples.coq.conf: _CoqProject.examples
 	@$(COQBIN)/coq_makefile -f _CoqProject.examples -o Makefile.examples.coq
+src/coq_elpi_builtins_arg_HOAS.ml: elpi/coq-arg-HOAS.elpi Makefile.coq.local
+	echo "(* Automatically generated from $<, don't edit *)" > $@
+	echo "(* Regenerate via 'make $@' *)" >> $@
+	echo "let code = {|" >> $@
+	cat $< >> $@
+	echo "|}" >> $@
 src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local
 	echo "(* Automatically generated from $<, don't edit *)" > $@
 	echo "(* Regenerate via 'make $@' *)" >> $@

Makefile.coq.local

@@ -17,6 +17,8 @@ install-extra::
 	df="`$(COQMKFILE) -destination-of theories/elpi.vo $(COQLIBS)`";\
 	install -m 0644 elpi-builtin.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 coq-builtin.elpi "$(COQLIBINSTALL)/$$df";\
+	install -m 0644 coq-builtin-synterp.elpi "$(COQLIBINSTALL)/$$df";\
+	install -m 0644 elpi/coq-lib-common.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/coq-lib.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/elpi_elaborator.elpi "$(COQLIBINSTALL)/$$df"
 

README.md

@@ -176,6 +176,7 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
 - `Elpi Db <dbname> <code>` creates a Db (a program that is accumulated into
   other programs). `<code>` is the initial contents of the Db, including the
   type declaration of its constituting predicates.
+  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>`.
 
@@ -186,19 +187,26 @@ In order to load Coq-Elpi use `From elpi Require Import elpi`.
   a no op if the Coq version is matched (or not) by the given regular expression.
   File names are relative to the directory mapped to `<loadpath>`; if more than
   one such directory exists, the `<filename>` must exists only once.
+  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).
+  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Debug <string>` sets the variable `<string>`, relevant for conditional
   clause compilation (the `:if VARIABLE` clause attribute).
+  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 - `Elpi Trace [[<start> <stop>] <predicate-filter>*|Off]` enable/disable
   tracing, eventually limiting it to a specific range of execution steps or
   predicate names.
+  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
+- `Elpi Trace Browser` enable/disable
+  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>`.
+  It understands the `#[phase]` attribute, see [synterp-vs-interp](README.md#separation-of-parsing-from-execution-of-vernacular-commands)
 
 where:
 
@@ -216,6 +224,86 @@ where:
 
 </p></details>
 
+#### Separation of parsing from execution of vernacular commands
+
+<details><summary>(click to expand)</summary>
+
+Since version 8.18 Coq has separate parsing and execution phases,
+respectively called synterp and interp.
+
+Since Coq has an extensible grammar the parsing phase is not entirely
+performed by the parser: after parsing one sentence Coq evaluates its
+synterp action. The synterp actions of a command like `Import A.` are
+the subset of its effect which affect parsing, like enabling a notation.
+Later, during the execution phase Coq evaluates the its
+interp action, which includes effects like putting lemma names in scope or
+enables type class instances etc.
+
+Being able to parse an entire document quickly,
+without actually executing any sentence, is important for developing reactive
+user interfaces, but requires some extra work when defining new commands,
+in particular to separate their synterp actions from their interp ones.
+Each command defined with Coq-Elpi is split into two programs,
+one running during the parsing phase and the other one during the execution
+phase.
+
+##### Declaration of synterp actions
+
+Each `Elpi Command` internally declares two programs with the same name.
+One to be run while the Coq document is parsed, the synterp-command,
+and the other one while it is executed, the interp command.
+`Elpi Accumulate`, by default, adds code to the interp-command.
+The `#[phase]` attribute can be used to accumulate code to the synterp-command
+or to both commands. `Elpi Typecheck` checks both commands.
+
+Each `Elpi Db` internally declares one db, by default for the interp phase.
+The `#[phase]` attribute can be used crate a database for the synterp phase,
+or for both phases. Note that databases for the two phases are distinct, no
+data is shared among them. In particular the `coq.elpi.accumulate*` API exists
+in both phases and only acts on data bases for the current phase.
+
+##### The alignment of phases
+
+All synterp actions, i.e. calls to APIs dealing with modules and sections
+like begin/end-module or import/export, have to happen at *both* synterp and
+interp time and *in the same order*.
+
+In order to do so, the synterp-command may need to communicate data to the
+corresponding interp-command. There are two ways for doing so.
+
+The first one is to use, as the main entry points, the following ones:
+```
+pred main-synterp i:list argument, o:any.
+pred main-interp i:list argument, i:any.
+```
+Unlike `main` the former outputs a datum while the latter receives it in input.
+During the synterp phase the API `coq.synterp-actions` lists the actions
+performed so far. An excerpt from the [coq-builtin-synterp](coq-builtin-synterp.elpi) file:
+```
+% Action executed during the parsing phase (aka synterp)
+kind synterp-action type.
+type begin-module id -> synterp-action.
+type end-module modpath -> synterp-action.
+```
+The synterp-command can output data of that type, but also any other data it
+wishes.
+
+The second way to communicate data is implicit, but limited to synterp actions.
+During the interp phase commands can use the `coq.next-synterp-action` API to
+peek into the list of actions yet to be performed.
+Once an action is performed, the API reveals the next one. See also the
+related utilities `coq.replay-synterp-action` and
+`coq.replay-all-missing-synterp-actions`.
+
+##### Syntax of the `#[phase]` attribute
+
+- `#[phase="ph"]` where `"ph"` can be `"parsing"`,
+  `"execution"` or `"both"`
+- `#[synterp]` is a shorthand for `#[phase="parsing"]`
+- `#[interp]` is a shorthand for `#[phase="execution]`
+
+</p></details>
+
 #### Invocation of Elpi code
 
 <details><summary>(click to expand)</summary>
@@ -227,7 +315,8 @@ where:
   program passing a possible empty list of arguments and the current goal. This
   is how you invoke a tactic.
 
-- `Elpi Export <qname>` makes it possible to invoke command `<qname>` without
+- `Elpi Export <qname> [As <other-qname>]` makes it possible to invoke
+  command `<qname>` (or `<other-qname>` if given) without
   the `Elpi` prefix or invoke tactic `<qname>` in the middle of a term just
   writing `<qname> args` instead of `ltac:(elpi <qname> args)`. Note that in
   the case of tactics, all arguments are considered to be terms.
@@ -327,6 +416,9 @@ Arguments of type `uconstr` are passed raw.
 
 - `Elpi Query [<qname>] <code>` runs `<code>` in the current program (or in
   `<qname>` if specified).
+- `Elpi Query [<qname>] <synterp-code> <interp-code>` runs
+  `<synterp-code>` in the current (synterp) program (or in
+`<qname>` if specified) and `<interp-code>` in the current program (or `<qname>`).
 - `elpi query [<qname>] <string> <argument>*` runs the `<string>` predicate
   (that must have the same signature of the default predicate `solve`).
 
@@ -393,12 +485,13 @@ see [coq-builtin](coq-builtin.elpi).
 
 - [coq-builtin](coq-builtin.elpi) documents the HOAS encoding of Coq terms
   and the API to access Coq
+- [coq-builtin-synterp](coq-builtin-synterp.elpi) documents APIs to interact with Coq at parsing time
 - [elpi-buitin](elpi-builtin.elpi) documents Elpi's standard library, you may
   look here for list processing code
 - [coq-lib](elpi/coq-lib.elpi) provides some utilities to manipulate Coq terms;
   it is an addendum to coq-builtin
-- [elpi-command-template](elpi/elpi-command-template.elpi) provides the pre-loaded code for
-  `Elpi Command`
+- [elpi-command-template](elpi/elpi-command-template.elpi) provides the pre-loaded code for `Elpi Command` (execution phase)
+- [elpi-command-template-synterp](elpi/elpi-command-template-synterp.elpi) provides the pre-loaded code for `Elpi Command` (parsing phase)
 - [elpi-tactic-template](elpi/elpi-tactic-template.elpi) provides the pre-loaded code for `Elpi Tactic`
 
 #### Organization of the repository

_CoqProject

@@ -15,6 +15,7 @@
 
 # NES
 -R apps/NES/theories elpi.apps
+-R apps/NES/elpi     elpi.apps.NES
 -R apps/NES/tests    elpi.apps.NES.tests
 -R apps/NES/examples elpi.apps.NES.examples
 
@@ -59,7 +60,10 @@ src/coq_elpi_glob_quotation.mli
 src/coq_elpi_arg_HOAS.ml
 src/coq_elpi_arg_HOAS.mli
 src/coq_elpi_arg_syntax.mlg
+src/coq_elpi_builtins_arg_HOAS.ml
 src/coq_elpi_builtins_HOAS.ml
+src/coq_elpi_builtins_synterp.ml
+src/coq_elpi_builtins_synterp.mli
 src/coq_elpi_builtins.ml
 src/coq_elpi_builtins.mli
 src/coq_elpi_config.ml

_CoqProject.test

@@ -54,3 +54,4 @@ tests/test_link_order_import2.v
 tests/test_link_order_import3.v
 tests/test_query_extra_dep.v
 tests/test_toposort.v
+tests/test_synterp.v

apps/NES/elpi/nes_interp.elpi

@@ -0,0 +1,85 @@
+namespace nes {
+
+% Print a namespace
+pred print-path i:list string, i:(gref -> coq.pp -> prop).
+print-path Path PP :- std.do! [
+  std.map {std.findall (ns Path _)} (p\ mp\ p = ns _ mp) MPs,
+  print.pp-list MPs (print.pp-module Path PP) Out,
+  coq.say {coq.pp->string Out},
+].
+
+namespace print {
+
+  pred pp-list i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
+  pp-list L F Out :- std.do! [
+    std.map-filter L F PPs,
+    Out = coq.pp.box (coq.pp.v 0) {std.intersperse (coq.pp.brk 0 0) PPs},
+  ].
+
+  kind context type.
+  type context
+    list string ->	% readable path
+    int ->	% length of full path
+    (gref -> coq.pp -> prop) ->
+    context.
+
+  % Hides `aux` modules
+  pred readable-path i:context, i:list string, o:list string.
+  readable-path (context Prefix N _) FullPath Path :- std.do! [
+    std.drop N FullPath RelPath,
+    std.append Prefix RelPath Path,
+  ].
+
+  pred module-context i:list string, i:modpath, i:(gref -> coq.pp -> prop), o:context.
+  module-context Prefix MP PP Ctx :- std.do! [
+    coq.modpath->path MP FullPath,
+    Ctx = context Prefix {std.length FullPath} PP,
+  ].
+
+  pred submodule-context i:context, i:modpath, o:context.
+  submodule-context (context _ _ PP as Ctx) MP Ctx' :- std.do! [
+    coq.modpath->path MP FullPath,
+    readable-path Ctx FullPath Path,
+    Ctx' = context Path {std.length FullPath} PP,
+  ].
+
+  pred pp-module i:list string, i:(gref -> coq.pp -> prop), i:modpath, o:coq.pp.
+  pp-module Prefix PP MP Out :- std.do! [
+    pp-module-items {module-context Prefix MP PP} {coq.env.module MP} Out,
+  ].
+
+  pred pp-module-items i:context i:list module-item, o:coq.pp.
+  pp-module-items Ctx Items Out :-
+    pp-list Items (pp-module-item Ctx) Out.
+
+  pred pp-module-item i:context, i:module-item, o:coq.pp.
+  pp-module-item (context _ _ PP) (gref GR) Out :- PP GR Out, !.
+  pp-module-item Ctx (submodule MP Items) Out :- std.do! [
+    pp-module-items {submodule-context Ctx MP} Items Out,
+  ].
+  pp-module-item Ctx (module-type MTP) Out :- pp-modtypath Ctx MTP Out.
+  pp-module-item Ctx (module-type-functor MTP _) Out :- pp-modtypath Ctx MTP Out.
+  pp-module-item Ctx (module-functor MP _) Out :- pp-modpath Ctx MP Out.
+
+  pred pp-path i:context, i:string, i:list string, o:coq.pp.
+  pp-path Ctx What FullPath Out :- std.do! [
+    readable-path Ctx FullPath Path,
+    Out = coq.pp.box coq.pp.h [
+      coq.pp.str What, coq.pp.spc,
+      coq.pp.str {std.string.concat "." Path},
+    ],
+  ].
+
+  pred pp-modtypath i:context, i:modtypath, o:coq.pp.
+  pp-modtypath Ctx MTP Out :- std.do! [
+    pp-path Ctx "Module Type" {coq.modtypath->path MTP} Out,
+  ].
+
+  pred pp-modpath i:context, i:modpath, o:coq.pp.
+  pp-modpath Ctx MP Out :- std.do! [
+    pp-path Ctx "Module" {coq.modpath->path MP} Out,
+  ].
+}
+
+
+}