From d24585827177970442f86d86c6aecc5ef45ed468 Mon Sep 17 00:00:00 2001 From: Davide Fissore Date: Thu, 11 Jan 2024 16:43:40 +0100 Subject: [PATCH] Add of the expose grafting + test --- _CoqProject.test | 1 + coq-builtin-synterp.elpi | 6 ++++- coq-builtin.elpi | 6 ++++- src/coq_elpi_builtins_synterp.ml | 9 ++++++-- src/coq_elpi_builtins_synterp.mli | 4 ++-- tests/test_grafting.v | 37 +++++++++++++++++++++++++++++++ 6 files changed, 57 insertions(+), 6 deletions(-) create mode 100644 tests/test_grafting.v diff --git a/_CoqProject.test b/_CoqProject.test index 71e43c409..8510ba804 100644 --- a/_CoqProject.test +++ b/_CoqProject.test @@ -55,3 +55,4 @@ tests/test_link_order_import3.v tests/test_query_extra_dep.v tests/test_toposort.v tests/test_synterp.v +tests/test_grafting.v \ No newline at end of file diff --git a/coq-builtin-synterp.elpi b/coq-builtin-synterp.elpi index 7a2904b9a..41e0b7381 100644 --- a/coq-builtin-synterp.elpi +++ b/coq-builtin-synterp.elpi @@ -306,10 +306,14 @@ external pred coq.env.current-section-path o:list string. kind clause type. type clause id -> grafting -> prop -> clause. -% Specify if the clause has to be grafted before or after a named clause +% Specify if the clause has to replace or to be grafted before or after a +% +% named clause. +% Note: replace is only possible for unnamed clauses kind grafting type. type before id -> grafting. type after id -> grafting. +type replace id -> grafting. % Specify to which module the clause should be attached to kind scope type. diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 3ab751e67..5a69a27ad 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1711,10 +1711,14 @@ external pred coq.extra-dep i:id, o:option id. kind clause type. type clause id -> grafting -> prop -> clause. -% Specify if the clause has to be grafted before or after a named clause +% Specify if the clause has to replace or to be grafted before or after a +% +% named clause. +% Note: replace is only possible for unnamed clauses kind grafting type. type before id -> grafting. type after id -> grafting. +type replace id -> grafting. % Specify to which module the clause should be attached to kind scope type. diff --git a/src/coq_elpi_builtins_synterp.ml b/src/coq_elpi_builtins_synterp.ml index 6ea44f15d..0ee6123fb 100644 --- a/src/coq_elpi_builtins_synterp.ml +++ b/src/coq_elpi_builtins_synterp.ml @@ -53,7 +53,9 @@ let scope = let open Conv in let open API.AlgebraicData in declare { let grafting = let open Conv in let open API.AlgebraicData in declare { ty = TyName "grafting"; - doc = "Specify if the clause has to be grafted before or after a named clause"; + doc = {|Specify if the clause has to replace or to be grafted before or after a +named clause. +Note: replace is only possible for unnamed clauses |}; pp = (fun fmt _ -> Format.fprintf fmt ""); constructors = [ K("before","",A(id,N), @@ -62,10 +64,13 @@ let grafting = let open Conv in let open API.AlgebraicData in declare { K("after","",A(id,N), B (fun x -> (`After,x)), M (fun ~ok ~ko -> function (`After,x) -> ok x | _ -> ko ())); + K("replace","",A(id,N), + B (fun x -> (`Replace,x)), + M (fun ~ok ~ko -> function (`Replace,x) -> ok x | _ -> ko ())); ] } |> CConv.(!<) -type clause = string option * ([ `After | `Before ] * string) option * API.Data.term +type clause = string option * ([ `After | `Before | `Replace ] * string) option * API.Data.term let clause = let open Conv in let open API.AlgebraicData in declare { ty = TyName "clause"; diff --git a/src/coq_elpi_builtins_synterp.mli b/src/coq_elpi_builtins_synterp.mli index 0d94104b0..309834e62 100644 --- a/src/coq_elpi_builtins_synterp.mli +++ b/src/coq_elpi_builtins_synterp.mli @@ -52,14 +52,14 @@ val set_accumulate_to_db_synterp : val prop : Data.term Conversion.t val id : string Conversion.t -type clause = string option * ([ `After | `Before ] * string) option * Data.term +type clause = string option * ([ `After | `Before | `Replace ] * string) option * Data.term val clause : clause Conversion.t type scope = ExecutionSite | CurrentModule | Library val scope : scope Conversion.t -val grafting : ([ `After | `Before ] * string) Conversion.t +val grafting : ([ `After | `Before | `Replace ] * string) Conversion.t val options : (Coq_elpi_HOAS.options, Data.constraints) ContextualConversion.ctx_readback val locate_module : BuiltIn.declaration val locate_module_type : BuiltIn.declaration diff --git a/tests/test_grafting.v b/tests/test_grafting.v new file mode 100644 index 000000000..4a536edb0 --- /dev/null +++ b/tests/test_grafting.v @@ -0,0 +1,37 @@ +From elpi Require Import elpi. + +Elpi Db my_db lp:{{ + pred graft_me o:int. + + :name "graft_me0" + graft_me 0. +}}. + +Elpi Command test_wanted_order. +Elpi Accumulate Db my_db. +Elpi Accumulate lp:{{ + main L1 :- + std.findall (graft_me _) L2, + std.forall2 L1 L2 (x\y\ sigma X\ graft_me X = y, int X = x). +}}. +Elpi Typecheck. + +Elpi test_wanted_order 0. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause "graft_me2" (after "graft_me0") (graft_me 2)). +}}. + +Elpi test_wanted_order 0 2. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause "graft_me1" (before "graft_me2") (graft_me 1)). +}}. + +Elpi test_wanted_order 0 1 2. + +Elpi Query lp:{{ + coq.elpi.accumulate _ "my_db" (clause _ (replace "graft_me2") (graft_me 3)). +}}. + +Elpi test_wanted_order 0 1 3.