synterp

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,7 @@ 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-parsing-phase.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/coq-lib.elpi "$(COQLIBINSTALL)/$$df";\
 	install -m 0644 elpi/elpi_elaborator.elpi "$(COQLIBINSTALL)/$$df"
 

_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,
+  ].
+}
+
+
+}

apps/NES/elpi/nes.elpi → apps/NES/elpi/nes_synterp.elpi

@@ -6,6 +6,9 @@ ns->modpath (ns _ M) M.
 pred open-ns->string i:prop, o:string.
 open-ns->string (open-ns S _) S.
 
+pred mk-fresh i:string, o:string.
+mk-fresh NS Fresh :- Fresh is NS ^ "_aux_" ^ {std.any->string {new_int} }.
+
 pred begin-ns i:string, i:list string, i:list prop, o:list prop.
 begin-ns NS Path In Out :-
   if (Path = [])
@@ -86,13 +89,7 @@ string->ns "" [] :- !.
 string->ns S L :- string->non-empty-ns S L.
 
 pred ns->string i:list string, o:string.
-ns->string NS S :- nes.join "." NS S.
-
-:index (_ 1)
-pred join i:string, i:list string,  o:string.
-join _ [] "".
-join _ [X] X :- !.
-join Sep [X|XS] S :- join Sep XS S0, S is X ^ Sep ^ S0.
+ns->string NS S :- std.string.concat "." NS S.
 
 pred begin-path i:list string, o:list prop.
 begin-path [] [].
@@ -101,7 +98,7 @@ begin-path ([_|_] as Path) Out :- std.do! [
   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,
   if (Stack = []) true (std.do! [
-    coq.locate-all {join "." Path} L,
+    coq.locate-all {std.string.concat "." Path} L,
     if (std.do! [
        std.mem L (loc-modpath M),
        coq.modpath->path M MP,
@@ -173,93 +170,13 @@ resolve.walk S Ctx SP Path :- std.do! [
 pred resolve.err i:string.
 resolve.err S :- coq.error "NES: Namespace not found:" S.
 
-% The (closed) namespace [NS] containing global [GR], or [].
-pred gref->path i:gref, o:list string.
-gref->path GR NS :- std.do! [
-  coq.gref->path GR MP,
-  if (gref->path.aux MP NS) true (NS = []),
-].
-pred gref->path.aux i:list string, o:list string.
-gref->path.aux MP NS :- ns NS M, coq.modpath->path M MP, !.
-
-% 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 {nes.join "." 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,
-  ].
-}
+% % The (closed) namespace [NS] containing global [GR], or [].
+% pred gref->path i:gref, o:list string.
+% gref->path GR NS :- std.do! [
+%   coq.gref->path GR MP,
+%   if (gref->path.aux MP NS) true (NS = []),
+% ].
+% pred gref->path.aux i:list string, o:list string.
+% gref->path.aux MP NS :- ns NS M, coq.modpath->path M MP, !.
 
 }

apps/NES/tests/test_NES.v

@@ -11,6 +11,7 @@ Fail NES.Begin "A._.B".
 
 (* name space creation *)
 NES.Begin Foo.
+#[synterp] Elpi Print NES.End.
 Definition x := 3.
 NES.End Foo.
 Print Foo.x.

apps/NES/tests/test_NES_lib.v

@@ -1,23 +1,29 @@
-From elpi.apps.NES Extra Dependency "nes.elpi" as nes.
+From elpi.apps.NES Extra Dependency "nes_synterp.elpi" as nes_synterp.
 From elpi.apps Require Import NES.
 
 Elpi Command Make.
-Elpi Accumulate Db NES.db.
-Elpi Accumulate File nes.
-Elpi Accumulate lp:{{
+#[synterp] Elpi Accumulate Db NES.db.
+#[synterp] Elpi Accumulate File nes_synterp.
+#[synterp] Elpi Accumulate lp:{{
 
-  main [str Path] :- std.do! [
+  main-synterp [str Path] ActionsToOpen :- std.do! [
     nes.string->ns Path NS,
     nes.begin-path NS OpenNS,
-    OpenNS => std.do! [
-      coq.env.add-const "x" {{ 42 }} _ @transparent! _C,
-      nes.end-path NS _NewNS,
-    ],
+    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,
+    coq.env.add-const "x" {{ 42 }} _ @transparent! _C,
+    coq.replay-all-missin-synterp-actions,
+  ].
+}}.
 Elpi Typecheck.
 Elpi Export Make.
 
 Make Cats.And.Dogs.
+Print Cats.And.Dogs.x.