w

LPCIC · Dec 1, 2023 · b3cf0ab · b3cf0ab
1 parent 3c3d188
commit b3cf0ab
Show file tree

Hide file tree

Showing 10 changed files with 54 additions and 103 deletions.
diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v
@@ -96,9 +96,9 @@ usage :-
   declare-module-for-ind (parameter _ _ _ F) :-
     pi p\ declare-module-for-ind (F p).
   declare-module-for-ind (inductive N _ _ _) :-
-    parsing-effect (module_ N none [] _\_).
+    coq.env.begin-module N none, coq.env.end-module _.
   declare-module-for-ind (record N _ _ _) :-
-    parsing-effect (module_ N none [] _\_).
+    coq.env.begin-module N none, coq.env.end-module _.
 
 }}.
 Elpi Typecheck.

diff --git a/elpi/elpi-command-template-parsing-phase.elpi b/elpi/elpi-command-template-parsing-phase.elpi
diff --git a/elpi/elpi-command-template-synterp.elpi b/elpi/elpi-command-template-synterp.elpi
@@ -0,0 +1,3 @@
+/* Loaded when Elpi Command has a code accumulated at #[synterp] time        */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
diff --git a/tests/test_API2.v b/tests/test_API2.v
@@ -171,7 +171,7 @@ Elpi Query lp:{{
 #[local] Hint Opaque x : core.
 
 Elpi Query lp:{{
-  parsing-effects [module_ "xx" none [] xx\[import-module xx]]
+  std.do! [coq.env.begin-module "xx" none, coq.env.end-module XX, coq.env.import-module XX ]
 }} lp:{{
   std.do! [
     {{ x }} = global (const C1),
@@ -187,7 +187,7 @@ Elpi Query lp:{{
 }}.
 
 Elpi Query lp:{{
-  parsing-effects [module_ "xx2" none [] xx\[import-module xx]]
+  std.do! [coq.env.begin-module "xx2" none, coq.env.end-module XX, coq.env.import-module XX]
 }} lp:{{
   std.do! [
     {{ x }} = global (const C1),
@@ -205,7 +205,7 @@ Elpi Query lp:{{
 #[local] Hint Opaque x : core.
 
 Elpi Query lp:{{
-    parsing-effects [module_ "xx3" none [] xx\[]]
+    std.do! [coq.env.begin-module "xx3" none, coq.env.end-module _]
 }} lp:{{
   std.do! [
     {{ x }} = global (const C1),
@@ -251,7 +251,7 @@ Goal 0 = 1. solve [debug eauto with xxx]. Abort.
 
 (*Module Type T. Axiom Inline(1) T : Type. End T.*)
 Elpi Query lp:{{
-  parsing-effects [module-type "T" [] _\_]  
+  std.do! [ coq.env.begin-module-type "T", coq.env.end-module-type _, ]
 }} lp:{{
   coq.env.begin-module-type "T",
   @inline-at! 1 => coq.env.add-axiom "T" {{ Type }} _,
@@ -261,7 +261,7 @@ Elpi Query lp:{{
 
 (*Module F(P : T). Definition id (a : P.T) := a. End F.*)
 Elpi Query lp:{{
-  parsing-effects [module-functor "F" none (mparam "P" {coq.locate-module-type "T"} _\_) _\_]  
+  std.do! [coq.env.begin-module-functor "F" none [pr "P" {coq.locate-module-type "T"}], coq.env.end-module _]
 }} lp:{{
   coq.env.begin-module-functor "F" _ _,
   coq.locate "P.T" GR,
@@ -272,7 +272,7 @@ Elpi Query lp:{{
 
 (*Module X. Definition T := nat. End X.*)
 Elpi Query lp:{{
-  parsing-effects [module_ "X" none [] _\_]
+  std.do! [coq.env.begin-module "X" none, coq.env.end-module _]
 }} lp:{{
 
   coq.env.begin-module "X" _,
@@ -283,7 +283,7 @@ Elpi Query lp:{{
 
 (*Module G := F X [no inline].*)
 Elpi Query lp:{{
-  parsing-effects [apply-functor "G" none {coq.locate-module "F"} [{coq.locate-module "X"}] coq.inline.no _\_]
+  std.do! [coq.env.apply-module-functor "G" none {coq.locate-module "F"} [{coq.locate-module "X"}] coq.inline.no _]
 }} lp:{{
   coq.env.apply-module-functor "G" _ _ _ _ G,
   coq.say G
@@ -292,7 +292,7 @@ Print Module G.
 
 (*Module H := F X [inline at leve 2].*)
 Elpi Query lp:{{
-  parsing-effects [apply-functor "H" none {coq.locate-module "F"} [{coq.locate-module "X"}] (coq.inline.at 2) _\_]
+  std.do! [coq.env.apply-module-functor "H" none {coq.locate-module "F"} [{coq.locate-module "X"}] (coq.inline.at 2) _]
 }} lp:{{
   coq.env.apply-module-functor "H" _ _ _ _ H,
   coq.say H
@@ -313,7 +313,7 @@ Abort.
 
 (*Module Type FT (P : T). Axiom idT : P.T -> P.T. End FT.*)
 Elpi Query lp:{{
-  parsing-effects [module-type-functor "FT" (mparam "P" {coq.locate-module-type "T"} _\_) _\_]
+  std.do! [coq.env.begin-module-type-functor "FT" [pr "P" {coq.locate-module-type "T"}], coq.env.end-module-type _]
 }} lp:{{
 
   coq.env.begin-module-type-functor "FT" _,
@@ -326,7 +326,7 @@ Print Module Type FT.
 
 (*Module Type GT := FT X [no inline].*)
 Elpi Query lp:{{
-  parsing-effects [apply-type-functor "GT" {coq.locate-module-type "FT"} [{coq.locate-module "X"}] coq.inline.no _\_]
+  std.do! [coq.env.apply-module-type-functor "GT" {coq.locate-module-type "FT"} [{coq.locate-module "X"}] coq.inline.no _]
 }} lp:{{
   coq.env.apply-module-type-functor "GT" _ _ _ G,
   coq.say G
@@ -335,7 +335,7 @@ Print Module Type GT.
 
 (*Module Type HT := FT X [inline at leve 2].*)
 Elpi Query lp:{{
-  parsing-effects [apply-type-functor "HT" {coq.locate-module-type "FT"} [{coq.locate-module "X"}] (coq.inline.at 2) _\_]
+  std.do! [coq.env.apply-module-type-functor "HT" {coq.locate-module-type "FT"} [{coq.locate-module "X"}] (coq.inline.at 2) _]
 }} lp:{{
   coq.env.apply-module-type-functor "HT" _ _ _ H,
   coq.say H

diff --git a/tests/test_API_module.v b/tests/test_API_module.v
@@ -51,11 +51,14 @@ Elpi Query lp:{{
 }}.
 
 Elpi Query lp:{{
-  parsing-effects [
-    module-type "TA" [] mp_ta\[
-    module_ "A" (some mp_ta) [
-      module_ "B" none [] _\[]
-    ] _\[] ]]
+  std.do! [
+    coq.env.begin-module-type "TA",
+    coq.env.end-module-type Mp_ta,
+    coq.env.begin-module "A" (some Mp_ta),
+      coq.env.begin-module "B" none,
+      coq.env.end-module _,
+    coq.env.end-module _,
+   ]
 }} lp:{{
  std.do! [
    coq.env.begin-module-type "TA",
@@ -83,11 +86,13 @@ Fail Check A.i1_ind.
 
 Elpi Query lp:{{
   coq.locate-module-type "TA" MP_TA,
-  parsing-effects [
-    module-type "TF" [] tf\[
-    module-functor "F" (some tf) (mparam "a" MP_TA a\ mparam "b" MP_TA b\
-      meffects [import-module a]) _\[]
-    ]
+  std.do! [
+    coq.env.begin-module-type "TF",
+    coq.env.end-module-type TF,
+    coq.env.begin-module-functor "F" (some TF) [pr "a" MP_TA, pr "b" MP_TA],
+      coq.locate-module "a" A,
+      coq.env.import-module A,
+    coq.env.end-module _,
   ]
 }} lp:{{
  std.do! [
@@ -108,8 +113,9 @@ Print B.w.
 
 Elpi Query lp:{{
   coq.locate-module-type "TA" MP_TA,
-  parsing-effects [
-    module-type-functor "TB" (mparam "A" MP_TA a\_) _\[]
+  std.do! [
+    coq.env.begin-module-type-functor "TB" [pr "A" MP_TA],
+    coq.env.end-module-type _,
   ]  
 }} lp:{{
  std.do! [
@@ -119,9 +125,12 @@ Elpi Query lp:{{
 }}.
 Print TB.
 
-Elpi Query lp:{{
+Elpi Query lp:{{ std.do! [
   coq.locate-module "A" A,
-  parsing-effects [ module_ "IA" none [include-module A _] _\[] ]
+  coq.env.begin-module "IA" none,
+  coq.env.include-module A _,
+  coq.env.end-module _,
+]
 }} lp:{{
   coq.env.begin-module "IA" _,
   coq.env.include-module {coq.locate-module "A"} _,
@@ -133,18 +142,19 @@ Print IA.
 Module Tmp.
 Elpi Query
 lp:{{
-  parsing-effects [import-module { coq.locate-module "IA" }]
+  std.do! [coq.env.import-module { coq.locate-module "IA" }]
 }} lp:{{
   coq.env.import-module { coq.locate-module "IA" }
 }}.
 Check i.
 End Tmp.
 
 Elpi Query lp:{{
-  parsing-effects [module-type "ITA" [
-    include-module-type {coq.locate-module-type "TA"} (coq.inline.at 2)
-  ] _\[
-  ]]
+  std.do! [
+    coq.env.begin-module-type "ITA",
+    coq.env.include-module-type {coq.locate-module-type "TA"} (coq.inline.at 2),
+    coq.env.end-module-type _,
+  ]
 }} lp:{{
   coq.env.begin-module-type "ITA",
   coq.env.include-module-type {coq.locate-module-type "TA"} _,

diff --git a/tests/test_API_section.v b/tests/test_API_section.v
@@ -30,7 +30,7 @@ Check eq_refl : e2 = 3.
 End SA.
 
 Elpi Query lp:{{
-  parsing-effects [ section "Foo" [] ]  
+  std.do! [ coq.env.begin-section "Foo", coq.env.end-section ]  
 }} lp:{{
   coq.env.begin-section "Foo",
   coq.env.add-section-variable "x" {{ nat }} X,

diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
@@ -57,7 +57,7 @@ End kwd.
 Elpi Command test.
 
 Elpi Query lp:{{
-  parsing-effects [section "xxxxx" []]
+  std.do! [coq.env.begin-section "xxxxx", coq.env.end-section]
 }} lp:{{
   coq.env.begin-section "xxxxx",
   coq.univ.new U,
@@ -604,7 +604,7 @@ Polymorphic Inductive tree (A : Type) :=
 Set Printing Universes.
 Print tree.
 Elpi Query lp:{{
-  parsing-effects [module_ "M" none [] _\_]  
+  std.do! [coq.env.begin-module "M" none, coq.env.end-module _]  
 }} lp:{{
 pglobal (indt I) _ = {{ tree }},
 coq.env.indt-decl I D,

diff --git a/tests/test_glob.v b/tests/test_glob.v
@@ -8,7 +8,7 @@ Module N1. End N1. Module M1 := N1.
 
 Elpi Command test.
 #[synterp] Elpi Accumulate lp:{{
-  main _ :- parsing-effects [ section "A" [], module_ "N2" none [] _\_ ].
+  main _ :- std.do! [ coq.env.begin-section "A", coq.env.end-section, coq.env.begin-module "N2" none, coq.env.end-module _].
 }}.
 Elpi Accumulate lp:{{
     main _ :-

diff --git a/tests/test_synterp.v b/tests/test_synterp.v
@@ -72,11 +72,11 @@ Fail Elpi err "C".
 Elpi Command module2.
 #[synterp] Elpi Accumulate lp:{{
   main [str X, str Y] :- 
-    parsing-effects [
-      module_ X none [] (m\[
+    std.do! [
+      coq.env.begin-module X none [] (m\[
       import-module m,
       ]),
-      module_ Y none [] (m\[]),
+      coq.env.begin-module Y none [] (m\[]),
     ].
 }}.
 Elpi Accumulate lp:{{
@@ -135,7 +135,7 @@ pr 1.
 Elpi Command test_data.
 #[synterp] Elpi Accumulate lp:{{
   type foo int.
-  main-synterp _ R :- R = foo. % parsing-effects.
+  main-synterp _ R :- R = foo. % std.do!.
 }}.
 #[interp] Elpi Accumulate lp:{{
   type foo int.

diff --git a/theories/elpi.v b/theories/elpi.v
@@ -8,7 +8,7 @@ Elpi Document Builtins.
 Elpi Checker "coq://elpi/coq-elpi-checker.elpi" "coq://elpi/coq-elpi-checker.elpi".
 
 Elpi Printer "elpi2html.elpi" "elpi2html.elpi". (* this one is from elpi *)
-Elpi Template Command "coq://elpi/elpi-command-template-parsing-phase.elpi" "coq://elpi/elpi-command-template.elpi".
+Elpi Template Command "coq://elpi/elpi-command-template-synterp.elpi" "coq://elpi/elpi-command-template.elpi".
 Elpi Template Tactic "coq://elpi/elpi-tactic-template.elpi".
 
 (* Special constant used for HOAS of holes, see coq-bultins.elpi *)