Merge pull request #604 from rlepigre/janno/structured-synterp

Structured synterp actions

Author: gares

Changelog.md

@@ -6,6 +6,10 @@
 - 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)
+- New `coq.replay-next-synterp-actions` to replay all synterp actions until the next beginning/end of a synterp group
 
 ## [2.0.2] - 01/02/2024
 

README.md

@@ -290,11 +290,23 @@ 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.
+
+One can use `coq.replay-next-synterp-actions` to replay all synterp actions
+until the next beginning/end of a synterp group. However, this is discouraged
+in favour of using groups explicitly, as this is more modular. Code that used
+to rely on the now-removed `coq.replay-all-missing-synterp-actions` predicate
+can rely on `coq.replay-next-synterp-actions` instead, but this is discouraged
+in favour of using groups explicitly)
 
 ##### 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

@@ -89,8 +89,12 @@ pred ns->string i:list string, o:string.
 ns->string NS S :- std.string.concat "." NS S.
 
 pred begin-path i:list string, o:list prop.
-begin-path [] [].
+begin-path [] [] :- std.do! [
+  coq.begin-synterp-group "nes.begin-path" Group,
+  coq.end-synterp-group Group,
+].
 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 +111,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.
@@ -118,18 +122,25 @@ std.time-do! [P|PS] :-
   std.time-do! PS.
 
 pred end-path i:list string, o:list prop.
-end-path [] [].
+end-path [] [] :- std.do! [
+  coq.begin-synterp-group "nes.end-path" Group,
+  coq.end-synterp-group Group,
+].
 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 ------------------------------------------------------------