Add of the expose grafting + test

_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

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.

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.

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 "<todo>");
   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";

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

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.