Support for module attribute.

apps/derive/elpi/derive.elpi

@@ -89,28 +89,38 @@ pred indt-or-const i:gref.
 indt-or-const (indt _).
 indt-or-const (const _).
 
-pred main i:gref, i:bool, o:list prop.
-main T P CL :- get-option "recursive" tt, !,
-  coq.env.dependencies T _ AllDeps,
+pred main i:gref, o:list prop.
+main GR CL :- get-option "module" M, !,
+  if (M = "") (coq.gref->id GR Mod) (Mod = M),
+  if-verbose (coq.say "Starting module" Mod),
+  coq.env.begin-module Mod none,
+  main-derive GR tt CL,
+  coq.env.end-module _.
+main GR CL :-
+  main-derive GR ff CL.
+
+pred main-derive i:gref, i:bool, o:list prop.
+main-derive GR InModule CL :- get-option "recursive" tt, !,
+  coq.env.dependencies GR _ AllDeps,
   coq.gref.set.elements AllDeps AllDepsL,
   std.filter AllDepsL indt-or-const Deps,
-  main.aux Deps [] CL1,
-  CL1 => main1 T P CL2,
+  main.aux InModule Deps [] CL1,
+  CL1 => main1 GR InModule CL2,
   std.append CL1 CL2 CL.
-pred main.aux i:list gref, i:list prop, o:list prop.
-main.aux [] X X.
-main.aux [T|TS] Acc CL :-
-  (pi X\get-option "only" X :- !, fail) => Acc => main T tt CL1,
-  main.aux TS {std.append CL1 Acc} CL.
+main-derive GR InModule CL :- main1 GR InModule CL.
 
-main T P CL :- main1 T P CL.
+pred main.aux i:bool, i:list gref, i:list prop, o:list prop.
+main.aux _ [] X X.
+main.aux InModule [GR|GRS] Acc CL :-
+  (pi X\get-option "only" X :- !, fail) => Acc => main-derive GR InModule CL1,
+  main.aux InModule GRS {std.append CL1 Acc} CL.
 
 pred main1 i:gref, i:bool, o:list prop.
-main1 T P CL :-
+main1 GR InModule CL :-
   if (get-option "prefix" PFX)
      (Prefix = PFX)
-     (if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = "")),
-  std.findall (derivation T Prefix _ _) L,
+     (if (InModule is ff) (Prefix is {coq.gref->id GR} ^ "_") (Prefix = "")),
+  std.findall (derivation GR Prefix _ _) L,
   if (L = [])
      (coq.error "no derivation found, did you Import derive.std?")
      true,
@@ -122,23 +132,33 @@ main1 T P CL :-
            true)
        (x = derivation _ _ _ r)
   ) DL,
-  validate-only T DL,
+  validate-only GR DL,
   toposort DL SortedDL,
-  chain T SortedDL CL.
-
-pred decl+main i:indt-decl.
-decl+main DS :- std.do! [
-  indt-decl-name DS ModName,
-  if-verbose (coq.say "Starting module" ModName),
-  coq.env.begin-module ModName none,
+  chain GR SortedDL CL.
+
+pred decl+main i:string, i:indt-decl.
+decl+main TypeName DS :- std.do! [
+  if (get-option "module" M)
+     (if (M = "") (ModName = TypeName) (ModName = M), HasModule = tt)
+     (HasModule = ff),
+  if (HasModule = tt)
+     (if-verbose (coq.say "Starting module" ModName),
+      coq.env.begin-module ModName none)
+     true,
   std.assert-ok! (coq.elaborate-indt-decl-skeleton DS D) "Inductive type declaration illtyped",
   if-verbose (coq.say "Declaring inductive" D),
   coq.env.add-indt D I,
   if-verbose (coq.say "Deriving"),
-  main (indt I) ff CL,
+  main-derive (indt I) HasModule CL,
   if-verbose (coq.say "Done"),
-  coq.env.end-module _,
+  if (HasModule = tt)
+     (coq.env.end-module _,
+      decl+main.post ModName I DS CL)
+     true
+].
 
+pred decl+main.post i:string, i:inductive, i:indt-decl, o:list prop. 
+decl+main.post ModName I DS CL :- std.do! [
   coq.env.indt I _ _ _ _ KS _,
   std.map KS (k\r\ r = indc k) KGRS,
   std.map KGRS coq.gref->id KNS,
@@ -162,10 +182,4 @@ decl+main DS :- std.do! [
 pred short-alias i:id, i:term.
 short-alias ID T :- @global! => coq.notation.add-abbreviation ID 0 T ff _.
 
-pred indt-decl-name i:indt-decl, o:string.
-indt-decl-name (parameter _ _ _ Decl) Name :-
-  pi x\ indt-decl-name (Decl x) Name.
-indt-decl-name (inductive Name _ _ _) Name.
-indt-decl-name (record Name _ _ _) Name.
-
 }

apps/derive/elpi/derive_synterp.elpi

@@ -55,17 +55,26 @@ topo L Deps SL :-
   topo Other NewDeps SOther,
   std.append LNoDeps SOther SL.
 
-pred main i:string, i:bool.
-main T P :- main1 T P.
+pred main i:string.
+main TypeName :- get-option "module" M, !,
+  if (M = "") (Mod = TypeName) (Mod = M),
+  coq.env.begin-module Mod none,
+  main-derive TypeName tt,
+  coq.env.end-module _.
+main TypeName :-
+  main-derive TypeName ff.
+
+pred main-derive i:string, i:bool.
+main-derive TypeName InModule :- main1 TypeName InModule.
 
 pred main1 i:string, i:bool.
-main1 T P :-
+main1 TypeName InModule :-
   if (get-option "prefix" PFX)
      (Prefix = PFX)
-     (if (P = tt) (Prefix is T ^ "_") (Prefix = "")),
-  std.findall (derivation T Prefix _) L,
+     (if (InModule is ff) (Prefix is TypeName ^ "_") (Prefix = "")),
+  std.findall (derivation TypeName Prefix _) L,
   std.map L (x\r\ x = derivation _ _ r) DL,
   toposort DL SortedDL,
-  chain T SortedDL.
+  chain TypeName SortedDL.
 
 }

apps/derive/examples/readme.v

@@ -1,7 +1,7 @@
-(* README *)                            
+(* README *)
 From elpi.apps Require Import derive.std.
- 
-derive Inductive peano := Zero | Succ (p : peano).
+
+#[module] derive Inductive peano := Zero | Succ (p : peano).
 
 (* Bug 8.16: About peano.peano.*)
 (* Notation peano := peano.peano *)
@@ -26,4 +26,4 @@ Check is_add. (*
 : forall n : nat, is_nat n ->
   forall m : nat, is_nat m ->
     is_nat (n + m)
-*)
+*)

apps/derive/examples/usage.v

@@ -7,7 +7,7 @@ From elpi.apps Require Import derive.std.
 Set Uniform Inductive Parameters.
 
 (** The best way to call derive is to prefix an Inductive declaration. *)
-derive
+#[module] derive
 Inductive tickle A := stop | more : A -> tickle -> tickle.
 
 (** The command is elaborated to something like:
@@ -40,7 +40,7 @@ Check tickle.tickle_R : (* relator (binary parametricity translation) *)
 (** This is a tricky case, since you need a good induction principle for the
     nested occurrence of tickle. #[verbose] prints all the derivations being
     run *)
-#[verbose] derive
+#[verbose,module] derive
 Inductive rtree A := Leaf (a : A) | Node (l : tickle rtree).
 
 Check rtree.induction : (* this is the key *)
@@ -50,7 +50,7 @@ Check rtree.induction : (* this is the key *)
   forall x, rtree.is_rtree A PA x -> P x.
 
 (** You can also select which derivations you like *)
-#[verbose, only(lens_laws, eqb)] derive
+#[verbose, only(lens_laws, eqb), module] derive
 Record Box A := { contents : A; tag : nat }.
 
 Check Box.eqb :

apps/derive/tests/test_derive.v

@@ -133,7 +133,7 @@ Check XXX.rtree_constructP : forall (A:Type) (l:rtree A), XXX.rtree_construct A
 Check XXX.rtree_eqb : forall (A:Type), (A -> A -> bool) -> rtree A -> rtree A -> bool.
 (* bug #270 *)
 
-derive
+#[module] derive
 Inductive triv : Coverage.unit -> Prop :=
 | one t : triv t | more x : triv x.
 
@@ -150,7 +150,7 @@ Inductive RoseTree : Type :=
 
 Elpi derive.param1 is_list.
 
-derive
+#[module] derive
 Inductive Pred : RoseTree -> Type :=
 | Pred_ctr branches :
     is_list _ Pred branches ->

apps/derive/theories/derive.v

@@ -59,8 +59,10 @@ From elpi.apps.derive Extra Dependency "derive_synterp.elpi" as derive_synterp.
 
 From elpi Require Import elpi.
 
+Elpi Command derive.
+
 #[phase="both"]
-Elpi Db derive.with_attributes lp:{{
+Elpi Accumulate lp:{{
   % runs P in a context where Coq #[attributes] are parsed
   pred with-attributes i:prop.
   with-attributes P :-
@@ -70,53 +72,45 @@ Elpi Db derive.with_attributes lp:{{
       att "only" attmap,
       att "recursive" bool,
       att "prefix" string,
+      att "module" string,
     ] Opts, !,
     Opts => P.
-}}.
-
-Elpi Command derive.
-Elpi Accumulate File derive_hook.
-Elpi Accumulate File derive.
-Elpi Accumulate Db derive.with_attributes.
-
-Elpi Accumulate lp:{{
-main [str I] :- !,
-  coq.locate I GR,
-  with-attributes (derive.main GR tt _).
-
-main [indt-decl D] :- !,
-  with-attributes (derive.decl+main D).
-
-main _ :- usage.
 
-usage :-
-  coq.error "Usage:  derive <inductive type/definition>\n\tderive Inductive name Params : Arity := Constructors.".
+  pred get_name i:indt-decl, o:string.
+  get_name (parameter _ _ _ F) N :- pi p\ get_name (F p) N.
+  get_name (inductive N _ _ _) N.
+  get_name (record N _ _ _) N.
 }}.
 
 #[synterp] Elpi Accumulate File derive_synterp_hook.
 #[synterp] Elpi Accumulate File derive_synterp.
-#[synterp] Elpi Accumulate Db derive.with_attributes.
-
 #[synterp] Elpi Accumulate lp:{{
-  main [str I] :- !,
-    with-attributes (derive.main I tt).
+  main [str TypeName] :- !,
+    with-attributes (derive.main TypeName).
 
   main [indt-decl D] :- !,
-    with-attributes (with_name D).
+    get_name D TypeName,
+    with-attributes (derive.main TypeName).
 
   main _.
+}}.
+
+Elpi Accumulate File derive_hook.
+Elpi Accumulate File derive.
+Elpi Accumulate lp:{{
+  main [str I] :- !,
+    coq.locate I GR,
+    with-attributes (derive.main GR _).
+
+  main [indt-decl D] :- !,
+    get_name D TypeName,
+    with-attributes (derive.decl+main TypeName D).
+
+  main _ :- usage.
 
-  pred with_name i:indt-decl.
-  with_name (parameter _ _ _ F) :-
-    pi p\ with_name (F p).
-  with_name (inductive N _ _ _) :-
-    coq.env.begin-module N none,
-    derive.main N tt,
-    coq.env.end-module _.
-  with_name (record N _ _ _) :-
-    coq.env.begin-module N none,
-    derive.main N tt,
-    coq.env.end-module _.
+  usage :-
+    coq.error "Usage:  derive <inductive type/definition>\n\tderive Inductive name Params : Arity := Constructors.".
 }}.
+
 Elpi Typecheck.
 Elpi Export derive.