Add derive.param2.register

apps/derive/elpi/param2.elpi

@@ -222,6 +222,15 @@ pred main i:gref, i:string, o:list prop.
 main T _ Clauses :-
   dispatch T "_R" Clauses.
 
+pred main_register i:gref, i:gref.
+main_register I R :-
+  GI = global I, GR = global R,
+  C1 = (param GI GI GR :- !),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
+  C2 = (paramR GI GI GR :- !),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C2),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ _ (param-done I)).
+
 }
 
 /*

apps/derive/tests/test_param2.v

@@ -92,3 +92,12 @@ Definition size_seq (A : Type) : size_of (list A) := fun _ => 0.
 Elpi derive.param2 size_of.
 
 Elpi derive.param2 size_seq.  (* Fixed by https://github.com/LPCIC/coq-elpi/pull/754 *)
+
+Definition fa := 0.
+Definition fb := fa.
+
+Fail Elpi derive.param2 fb.
+
+Definition fa_R := O_R.
+Elpi derive.param2.register fa fa_R.
+Elpi derive.param2 fb.

apps/derive/theories/derive/param2.v

@@ -54,6 +54,17 @@ Elpi Accumulate lp:{{
   usage :- coq.error "Usage: derive.param2 <object name>".
 }}. 
 
+Elpi Command derive.param2.register.
+Elpi Accumulate File param2.
+Elpi Accumulate Db derive.param2.db.
+Elpi Accumulate lp:{{
+  main [str I, str R] :- !, coq.locate I GRI, coq.locate R GRR,
+    derive.param2.main_register GRI GRR.
+  main _ :- usage.
+
+  usage :- coq.error "Usage: derive.param2.register <name> <name_R>".
+}}.
+
 
 (* hook into derive *)
 Elpi Accumulate derive File param2.