Add a notion of synterp action group.

Groups can be created around synterp actions, and the containing
actions replayed all at once at interp.

This allows for better composition of commands that don't have an
interesting interp phase (like NES).

Co-authored-by: Rodolphe Lepigre <[email protected]>

Changelog.md

@@ -6,6 +6,9 @@
 - New `coq.parse-attributes` support for the `attlabel` specification,
   see `coq-lib-common.elpi` for its documentation.
 - New `coq.goal->pp`
+- Replace `coq.replay-all-missing-synterp-actions` by (nestable) groups of actions
+- New `coq.begin-synterp-group` and `coq.end-synterp-group` primitives
+- New `coq.replay-synterp-action-group` primitive (replaces `coq.replay-all-missing-synterp-actions` in conjunction with a group)
 
 ## [2.0.2] - 01/02/2024
 

README.md

@@ -290,11 +290,16 @@ 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`.
+Such synterp actions can be recorded into (nested) groups whose structure is
+declared using well-bracketed calls to predicates `coq.begin-synterp-group`
+and `coq.end-synterp-group` in the synterp phase. In the interp phase, one can
+then use predicate `coq.replay-synterp-action-group` to replay all the synterp
+actions of the group with the given name at once.
+
+In the case where one wishes to interleave code between the actions of a given
+group, it is also possible to match the synterp group structure at interp, via
+`coq.begin-synterp-group` and `coq.end-synterp-group`. Individual actions that
+are contained in the group then need to be replayed individually.
 
 ##### Syntax of the `#[phase]` attribute
 

_CoqProject.test

@@ -56,3 +56,4 @@ tests/test_query_extra_dep.v
 tests/test_toposort.v
 tests/test_synterp.v
 tests/test_checker.v
+tests/test_replay.v

apps/NES/elpi/nes_interp.elpi

@@ -8,6 +8,15 @@ print-path Path PP :- std.do! [
   coq.say {coq.pp->string Out},
 ].
 
+pred begin-path.
+begin-path :- coq.replay-synterp-action-group "nes.begin-path".
+
+pred end-path.
+end-path :- coq.replay-synterp-action-group "nes.end-path".
+
+pred open-path.
+open-path :- coq.replay-synterp-action-group "nes.open-path".
+
 namespace print {
 
   pred pp-list i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
@@ -82,4 +91,4 @@ namespace print {
 }
 
 
-}
+}

apps/NES/elpi/nes_synterp.elpi

@@ -91,6 +91,7 @@ ns->string NS S :- std.string.concat "." NS S.
 pred begin-path i:list string, o:list prop.
 begin-path [] [].
 begin-path ([_|_] as Path) Out :- std.do! [
+  coq.begin-synterp-group "nes.begin-path" Group,
   coq.env.current-path CP,
   if (open-ns _ NSCP) (std.assert! (NSCP = CP) "NS: cannot begin a namespace inside a module that is inside a namespace") true,
   std.map {std.findall (open-ns Y_ P_)} open-ns->string Stack,
@@ -107,7 +108,7 @@ begin-path ([_|_] as Path) Out :- std.do! [
   iter<- Stack {std.rev Path} begin-ns [] Out,
 
   open-super-path Path [],
-
+  coq.end-synterp-group Group,
 ].
 
 pred std.time-do! i:list prop.
@@ -120,16 +121,20 @@ std.time-do! [P|PS] :-
 pred end-path i:list string, o:list prop.
 end-path [] [].
 end-path ([_|_] as Path) Out :- std.do! [
+  coq.begin-synterp-group "nes.end-path" Group,
   std.map {std.findall (open-ns X_ P_)} nes.open-ns->string Stack,
   std.assert! (std.appendR {std.rev Path} Bottom Stack) "NES: Ending a namespace that is not begun",
   nes.iter-> Bottom {std.rev Path} nes.end-ns [] Out,
+  coq.end-synterp-group Group,
 ].
 
 
 pred open-path i:list string.
 open-path Path :- std.do! [
+  coq.begin-synterp-group "nes.open-path" Group,
   std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
-  std.forall Mods coq.env.import-module
+  std.forall Mods coq.env.import-module,
+  coq.end-synterp-group Group,
 ].
 
 pred open-super-path i:list string, i:list string.

apps/NES/tests/test_NES.v

@@ -74,4 +74,4 @@ NES.Begin X.
 Module Y.
 Fail NES.Begin Z.
 End Y.
-NES.End X.
+NES.End X.

apps/NES/tests/test_NES_lib.v

@@ -1,25 +1,26 @@
 From elpi.apps.NES Extra Dependency "nes_synterp.elpi" as nes_synterp.
+From elpi.apps.NES Extra Dependency "nes_interp.elpi" as nes_interp.
 From elpi.apps Require Import NES.
 
 Elpi Command Make.
-#[synterp] Elpi Accumulate Db NES.db.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
+#[interp] Elpi Accumulate File nes_interp.
 #[synterp] Elpi Accumulate lp:{{
 
-  main-synterp [str Path] ActionsToOpen :- std.do! [
+  main [str Path] :- std.do! [
     nes.string->ns Path NS,
     nes.begin-path NS OpenNS,
-    coq.synterp-actions ActionsToOpen,
     OpenNS => nes.end-path NS _NewNS,
   ].
   main _ :- coq.error "usage: Make <DotSeparatedPath>".
 
 }}.
 #[interp] Elpi Accumulate lp:{{
-  main-interp [str _] ActionsBefore :- std.do! [
-    std.forall ActionsBefore coq.replay-synterp-action,
+  main _ :- std.do! [
+    nes.begin-path,
     coq.env.add-const "x" {{ 42 }} _ @transparent! _C,
-    coq.replay-all-missing-synterp-actions,
+    nes.end-path,
   ].
 }}.
 Elpi Typecheck.

apps/NES/theories/NES.v

@@ -9,11 +9,14 @@ pred open-ns o:string, o:list string.
 :name "open-ns:begin"
 open-ns _ _ :- fail.
 
+}}.
+
+#[phase="both"] Elpi Accumulate NES.db lp:{{
+
 typeabbrev path (list string).
 
 :index (2)
 pred ns o:path, o:modpath.
-
 }}.
 
 Elpi Command NES.Status.
@@ -32,56 +35,56 @@ Elpi Export NES.Status.
 
 Elpi Command NES.Begin.
 #[synterp] Elpi Accumulate File nes_synterp.
+#[interp] Elpi Accumulate File nes_interp.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate lp:{{
 
   main [str NS] :- !, nes.begin-path {nes.string->non-empty-ns NS} _.
   main _ :- coq.error "usage: NES.Begin <DotSeparatedPath>".
 
 }}.
-#[synterp] Elpi Accumulate Db NES.db.
-#[interp] Elpi Accumulate lp:{{ main _ :- coq.replay-all-missing-synterp-actions. }}.
+#[interp] Elpi Accumulate lp:{{ main _ :- nes.begin-path. }}.
 Elpi Typecheck.
 Elpi Export NES.Begin.
 
 Elpi Command NES.End.
 #[synterp] Elpi Accumulate File nes_synterp.
+#[interp] Elpi Accumulate File nes_interp.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate lp:{{
 
   main [str NS] :- nes.end-path {nes.string->non-empty-ns NS} _.
   main _ :- coq.error "usage: NES.End <DotSeparatedPath>".
 
 }}.
-#[synterp] Elpi Accumulate Db NES.db.
-#[interp] Elpi Accumulate lp:{{ main _ :- coq.replay-all-missing-synterp-actions. }}.
+#[interp] Elpi Accumulate lp:{{ main _ :- nes.end-path. }}.
 Elpi Typecheck.
 Elpi Export NES.End.
 
 
 Elpi Command NES.Open.
-#[synterp] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
+#[interp] Elpi Accumulate File nes_interp.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate lp:{{
 
   main [str NS] :- nes.open-path {nes.resolve NS}.
   main _ :- coq.error "usage: NES.Open <DotSeparatedPath>".
 
 }}.
-#[interp] Elpi Accumulate lp:{{ main _ :- coq.replay-all-missing-synterp-actions. }}.
+#[interp] Elpi Accumulate lp:{{ main _ :- nes.open-path. }}.
 Elpi Typecheck.
 Elpi Export NES.Open.
 
 (* List the contents a namespace *)
 Elpi Command NES.List.
-#[synterp] Elpi Accumulate Db NES.db.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
 #[interp] Elpi Accumulate File nes_interp.
 #[synterp] Elpi Accumulate lp:{{
   main-synterp [str NS] (pr DB Path) :- nes.resolve NS Path, std.findall (ns O_ P_) DB.
 }}.
 #[interp] Elpi Accumulate lp:{{
-  typeabbrev path (list string).
-  pred ns o:path, o:modpath.
-
   pred pp-gref i:gref, o:coq.pp.
   pp-gref GR PP :- coq.term->pp (global GR) PP.
 
@@ -94,16 +97,13 @@ Elpi Export NES.List.
 
 (* NES.List with types *)
 Elpi Command NES.Print.
-#[synterp] Elpi Accumulate Db NES.db.
+#[phase="both"] Elpi Accumulate Db NES.db.
 #[synterp] Elpi Accumulate File nes_synterp.
 #[interp] Elpi Accumulate File nes_interp.
 #[synterp] Elpi Accumulate lp:{{
   main-synterp [str NS] (pr DB Path) :- nes.resolve NS Path, std.findall (ns O_ P_) DB.
 }}.
 Elpi Accumulate lp:{{
-  typeabbrev path (list string).
-  pred ns o:path, o:modpath.
-
   pred pp-gref i:gref, o:coq.pp.
   pp-gref GR PP :- std.do! [
     coq.env.typeof GR Ty,

coq-builtin-synterp.elpi

@@ -363,6 +363,14 @@ type export-module modpath -> synterp-action.
 % parsing phase (aka synterp) up to now.
 external pred coq.synterp-actions o:list synterp-action.
 
+% [coq.begin-synterp-group ID Group] Create and open a new synterp action
+% group with the given name.
+external pred coq.begin-synterp-group i:id, o:group.
+
+% [coq.end-synterp-group Group] End the synterp action group Group. Group
+% must refer to the most recently openned group.
+external pred coq.end-synterp-group i:group.
+
 % Generic attribute value
 kind attribute-value type.
 type leaf-str string -> attribute-value.

coq-builtin.elpi

@@ -1797,14 +1797,29 @@ type include-module-type modtypath -> synterp-action.
 type import-module modpath -> synterp-action.
 type export-module modpath -> synterp-action.
 
+% Synterp action group
+typeabbrev group (ctype "group").
+
+
 % [coq.next-synterp-action A] Get the next action performed during parsing
 % (aka synterp), that is also the next action to be performed during
 % execution (aka interp). See also coq.replay-synterp-action
 external pred coq.next-synterp-action o:synterp-action.
 
-% [coq.replay-all-missing-synterp-actions] Execute all actions needed in
-% order to match the actions performed at parsing time (aka synterp)
-external pred coq.replay-all-missing-synterp-actions .
+% [coq.replay-synterp-action-group ID] Execute all actions of synterp action
+% group ID. ID must be the name of the next group, it must not be opened
+% already, and there must not be any actions before it.
+external pred coq.replay-synterp-action-group i:id.
+
+% [coq.begin-synterp-group ID Group] Match a begin-synterp-group synterp
+% operation. ID must be the name of the next synterp action group and there
+% must not be any actions before it.
+external pred coq.begin-synterp-group i:id, o:group.
+
+% [coq.end-synterp-group Group] Match a end-synterp-group synterp operation.
+% Group must be the currently opened synterp action group and the group must
+% not have any more synterp actions or groups left to replay.
+external pred coq.end-synterp-group i:group.
 
 % -- Utils ------------------------------------------------------------