From b3cf0ab72531cce0a7f74b819c43a67293268119 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 1 Dec 2023 14:08:10 +0100 Subject: [PATCH] w --- apps/derive/theories/derive.v | 4 +- elpi/elpi-command-template-parsing-phase.elpi | 62 ------------------- elpi/elpi-command-template-synterp.elpi | 3 + tests/test_API2.v | 22 +++---- tests/test_API_module.v | 48 ++++++++------ tests/test_API_section.v | 2 +- tests/test_HOAS.v | 4 +- tests/test_glob.v | 2 +- tests/test_synterp.v | 8 +-- theories/elpi.v | 2 +- 10 files changed, 54 insertions(+), 103 deletions(-) delete mode 100644 elpi/elpi-command-template-parsing-phase.elpi create mode 100644 elpi/elpi-command-template-synterp.elpi diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v index 78d9477c4..5d92cf97e 100644 --- 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 deleted file mode 100644 index 3cc0bb89e..000000000 --- a/elpi/elpi-command-template-parsing-phase.elpi +++ /dev/null @@ -1,62 +0,0 @@ -/* Loaded when Elpi Command is used */ -/* license: GNU Lesser General Public License Version 2.1 or later */ -/* ------------------------------------------------------------------------- */ - -typeabbrev effects list eff. - -kind eff type. -type module_ id -> option modtypath -> effects -> - (modpath -> effects) -> eff. -type module-functor id -> option modtypath -> peffects -> - (modpath -> effects) -> eff. -type module-type id -> effects -> - (modtypath -> effects) -> eff. -type module-type-functor id -> peffects -> - (modtypath -> effects) -> eff. -type apply-functor id -> option modtypath -> modpath -> list modpath -> coq.inline -> - (modpath -> effects) -> eff. -type apply-type-functor id -> modtypath -> list modpath -> coq.inline -> - (modtypath -> effects) -> eff. -type include-module modpath -> coq.inline -> eff. -type include-module-type modtypath -> coq.inline -> eff. -type import-module modpath -> eff. -type export-module modpath -> eff. -type section id -> effects -> eff. - - -kind peffects type. -type mparam id -> modtypath -> (modpath -> peffects) -> peffects. -type meffects effects -> peffects. - -pred parsing-effects i:effects. -parsing-effects []. -parsing-effects [X|XS] :- !, std.do! [ parsing-effect X, parsing-effects XS ]. -parsing-effects _. % allows to write (x\_) when there are no effects - - -pred peffects->params i:peffects, o:list (pair id modtypath). -peffects->params (mparam ID MT F) [pr ID MT|PS] :- - pi x\ peffects->params (F x) PS. -peffects->params (meffects _) []. -peffects->params _ []. - -pred interp-peffects i:peffects. -interp-peffects (mparam ID _ F) :- !, std.do! [ - coq.locate-module ID M, - interp-peffects (F M), -]. -interp-peffects (meffects ES) :- !, parsing-effects ES. -interp-peffects _. % allows to write (mparam X T x\_) when there are no effects - -pred parsing-effect i:eff. -parsing-effect (module_ ID TY IES ES) :- std.do! [ coq.env.begin-module ID TY, parsing-effects IES, coq.env.end-module O, parsing-effects (ES O) ]. -parsing-effect (module-functor ID TY PES ES) :- std.do! [ coq.env.begin-module-functor ID TY {peffects->params PES}, interp-peffects PES, coq.env.end-module O, parsing-effects (ES O) ]. -parsing-effect (module-type ID IES ES) :- std.do! [ coq.env.begin-module-type ID, parsing-effects IES, coq.env.end-module-type O, parsing-effects (ES O) ]. -parsing-effect (module-type-functor ID PES ES) :- std.do! [ coq.env.begin-module-type-functor ID {peffects->params PES}, interp-peffects PES, coq.env.end-module-type O, parsing-effects (ES O) ]. -parsing-effect (apply-functor ID TY MP PS I ES) :- std.do! [ coq.env.apply-module-functor ID TY MP PS I O, parsing-effects (ES O) ]. -parsing-effect (apply-type-functor ID MP PS I ES) :- std.do! [ coq.env.apply-module-type-functor ID MP PS I O, parsing-effects (ES O) ]. -parsing-effect (include-module MP I) :- std.do! [ coq.env.include-module MP I ]. -parsing-effect (include-module-type MP I) :- std.do! [ coq.env.include-module-type MP I ]. -parsing-effect (import-module MP) :- std.do! [ coq.env.import-module MP ]. -parsing-effect (export-module MP) :- std.do! [ coq.env.export-module MP ]. -parsing-effect (section ID ES) :- std.do! [ coq.env.begin-section ID, parsing-effects ES, coq.env.end-section ]. diff --git a/elpi/elpi-command-template-synterp.elpi b/elpi/elpi-command-template-synterp.elpi new file mode 100644 index 000000000..6cef3c560 --- /dev/null +++ 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 index 8715d10f1..8d28238c2 100644 --- 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 index 09c0a4de1..417def432 100644 --- 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,7 +142,7 @@ 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" } }}. @@ -141,10 +150,11 @@ 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 index ab3b8b540..7cfb32c0c 100644 --- 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 index 5c41a2e3d..889e97352 100644 --- 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 index 53e7f8268..9ee60ea74 100644 --- 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 index 64a440d2e..62f25de9b 100644 --- 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 index 3f4e9d5c5..3bff41c2f 100644 --- 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 *)