Merge pull request #758 from proux01/param2-register

Add derive.param2.register
LPCIC · Feb 2, 2025 · eea1606 · eea1606
2 parents cd0e0eb + 71daf5f
commit eea1606
Show file tree

Hide file tree

Showing 4 changed files with 58 additions and 1 deletion.
diff --git a/apps/derive/README.md b/apps/derive/README.md
@@ -120,6 +120,34 @@ Inductive is_nat : nat -> Type :=
 | is_S : forall n : nat, is_nat n -> is_nat (S n) *)
 ```
 
+### `param2`
+
+Binary parametricity translation.
+
+Main command is `derive.param2`
+```coq
+Elpi derive.param2 nat.
+Print nat_R. (*
+Inductive nat_R : nat -> nat -> Set :=
+| O_R : nat_R 0 0
+| S_R : forall H H0 : nat, nat_R H H0 -> nat_R (S H) (S H0).
+```
+
+The command `derive.param2.register` can be used to register
+handcrafted parametricity rules, so that they can be used by further
+`derive.param2` commands.
+```coq
+Definition fa := 0.
+Definition fb := fa.
+
+Fail Elpi derive.param2 fb.
+(* derive.param2: No binary parametricity translation for fa *)
+
+Definition fa_R := O_R.
+Elpi derive.param2.register fa fa_R.
+Elpi derive.param2 fb.
+```
+
 ### `param1_functor`
 
 ```coq

diff --git a/apps/derive/elpi/param2.elpi b/apps/derive/elpi/param2.elpi
@@ -193,7 +193,7 @@ dispatch (const GR as C) Suffix Clauses :- do! [
   C1 = (param Term Term (global (const TermR)) :- !),
   coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "param:fail") C1),
   C2 = (paramR Term Term (global (const TermR)) :- !),
-  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C1),
+  coq.elpi.accumulate _ "derive.param2.db" (clause _ (before "paramR:fail") C2),
   coq.elpi.accumulate _ "derive.param2.db" (clause _ _ (param-done C)),
   Clauses = [param-done C, C1, C2]
 ].
@@ -241,6 +241,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)).
+
 }
 
 /*

diff --git a/apps/derive/tests/test_param2.v b/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.
diff --git a/apps/derive/theories/derive/param2.v b/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.