Support for prefix attribute.

LPCIC · Feb 16, 2024 · 11e1bf7 · 11e1bf7
1 parent 2c11713
commit 11e1bf7
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 2 deletions.
diff --git a/apps/derive/elpi/derive.elpi b/apps/derive/elpi/derive.elpi
@@ -107,7 +107,9 @@ main T P CL :- main1 T P CL.
 
 pred main1 i:gref, i:bool, o:list prop.
 main1 T P CL :-
-  if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = ""),
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = "")),
   std.findall (derivation T Prefix _ _) L,
   if (L = [])
      (coq.error "no derivation found, did you Import derive.std?")

diff --git a/apps/derive/elpi/derive_synterp.elpi b/apps/derive/elpi/derive_synterp.elpi
@@ -60,7 +60,9 @@ main T P :- main1 T P.
 
 pred main1 i:string, i:bool.
 main1 T P :-
-  if (P = tt) (Prefix is T ^ "_") (Prefix = ""),
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (if (P = tt) (Prefix is T ^ "_") (Prefix = "")),
   std.findall (derivation T Prefix _) L,
   std.map L (x\r\ x = derivation _ _ r) DL,
   toposort DL SortedDL,

diff --git a/apps/derive/theories/derive.v b/apps/derive/theories/derive.v
@@ -69,6 +69,7 @@ Elpi Db derive.with_attributes lp:{{
       att "verbose" bool,
       att "only" attmap,
       att "recursive" bool,
+      att "prefix" string,
     ] Opts, !,
     Opts => P.
 }}.