Merge pull request #597 from rlepigre/br/derive-synterp

Add synterp phase support for derive plugins.

Author: gares

apps/derive/README.md

@@ -7,33 +7,47 @@ given an inductive type declaration.
 
 ```coq
 From elpi.apps Require Import derive.std.
- 
-derive Inductive peano := Zero | Succ (p : peano).
 
-Print peano.
-(* Notation peano := peano.peano *)
+#[module] derive Inductive peano := Zero | Succ (p : peano).
+
 Print peano.peano.
-(* Inductive peano : Type :=  Zero : peano | Succ : peano -> peano *)
+(* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano. *)
 
 Eval compute in peano.eqb Zero (Succ Zero).
 (* = false : bool *)
 
 About peano.eqb_OK.
 (*
-peano.eqb_OK : forall x1 x2 : peano, Bool.reflect (x1 = x2) (peano.eqb x1 x2)
+peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2)
 
 peano.eqb_OK is not universe polymorphic
 Arguments peano.eqb_OK x1 x2
 peano.eqb_OK is opaque
+Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK
 *)
 ```
 
-See also [examples/usage.v](examples/usage.v)
+See also [examples/usage.v](examples/usage.v) and [tests/test_readme.v](tests/test_readme.v).
 
 :warning: The line `From elpi.apps Require Import derive.std.` sets globally 
 `Uniform Inductive Parameters`.
 See the [documentation of that option in the Coq reference manual](https://coq.inria.fr/refman/language/core/inductive.html#coq:flag.Uniform-Inductive-Parameters).
 
+## Usage and attributes
+
+Using `derive Inductive ty := ...` produces the inductive `ty`, together with
+derivations, all in the current scope. The `#[module=<string>]` attriute can
+be used to specify that the inductive and the derivations should be wrapped
+in a module of the given name (the name of the inductive is used if no name
+is specified).
+
+When a wrapper module is generated, an alias (i.e., a notation) is generated
+for the inductive to be accessible with its name, outside of the module scope.
+This behaviour can be disabled by using the `#[no_alias]` boolean attribute.
+
+The `#[prefix=<string>]` attribute can be used to specify a prefix for all the
+derived definitions/lemmas.
+
 ## Documentation
 
 Elpi's `derive` app is a little framework to register derivations.

apps/derive/_CoqProject.test

@@ -6,6 +6,7 @@
 -R tests    elpi.apps.derive.tests
 -R examples elpi.apps.derive.examples
 
+tests/test_readme.v
 tests/test_derive_stdlib.v
 tests/test_bcongr.v
 tests/test_derive.v

apps/derive/elpi/derive.elpi

@@ -89,53 +89,84 @@ 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 T P CL :- main1 T P CL.
-
+main-derive GR InModule CL :- main1 GR InModule 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 validate-recursive i:prop, o:derive.
+validate-recursive (derivation _ _ tt _) _ :- get-option "recursive" tt,
+  coq.error "Synterp actions not supported in recursive derive.".
+validate-recursive (derivation _ _ _ R) R.
 pred main1 i:gref, i:bool, o:list prop.
-main1 T P CL :-
-  if (P = tt) (Prefix is {coq.gref->id T} ^ "_") (Prefix = ""),
-  std.findall (derivation T Prefix _) L,
+main1 GR InModule CL :-
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (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,
-  std.map L (x\r\ x = derivation _ _ r) DL,
-  validate-only T DL,
+  std.map L validate-recursive 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 TypeName I DS CL)
+     check-no-no-alias
+].
+
+pred check-no-no-alias.
+check-no-no-alias :- get-option "no_alias" tt, !,
+  coq.error "The no_alias attribute only has an effect when a wrapper module is generated.".
+check-no-no-alias.
 
+pred decl+main.post i:string, i:inductive, i:indt-decl, o:list prop.
+decl+main.post TypeName 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,
   std.map KGRS (gr\r\ r = global gr) KTS,
 
-  std.forall2 [ModName|KNS] [global (indt I)|KTS] short-alias,
+  std.forall2 [TypeName|KNS] [global (indt I)|KTS] short-alias,
 
   coq.indt-decl->implicits DS IndImpls KsImpls,
   if (coq.any-implicit? IndImpls)
@@ -151,12 +182,7 @@ decl+main DS :- std.do! [
 ].
 
 pred short-alias i:id, i:term.
+short-alias _ _ :- get-option "no_alias" tt, !, true.
 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_hook.elpi

@@ -2,7 +2,7 @@
 /* license: GNU Lesser General Public License Version 2.1 or later           */
 /* ------------------------------------------------------------------------- */
 
-pred derivation i:gref, i:string, o:derive.
+pred derivation i:gref, i:string, o:bool, o:derive.
 pred export i:modpath.
 pred dep1 o:string, o:string.
 kind derive type.

apps/derive/elpi/derive_synterp.elpi

@@ -0,0 +1,80 @@
+/* Entry point for all derivations                                           */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+namespace derive {
+
+pred dep o:string, o:string.
+dep X Y :- dep1 X Y.
+dep X Y :- dep1 X Z, dep Z Y.
+
+pred selected i:string.
+selected Name :- get-option "only" Map, !,
+  Map => (get-option Name _; (get-option X _, dep X Name)).
+selected _.
+
+pred chain i:string, i:list derive.
+chain _ [].
+chain T [derive Name _ _|FS] :- not(selected Name), !,
+  chain T FS.
+chain T [derive _ _ AlreadyDone|FS] :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+  chain T FS.
+chain T [derive _ F _|FS] :- get-option "only" _, !, % request this one
+  F _,
+  chain T FS.
+chain T [derive _ F _|FS] :- % all are selected, we can fail
+  (pi x\ stop x :- !, fail) => F _, !,
+  chain T FS.
+chain T [derive _ _ _|FS] :-
+  chain T FS.
+
+pred toposort i:list derive, o:list derive.
+toposort L SL :-
+  std.findall (dep1 _ _) Deps,
+  topo L Deps SL.
+
+pred std.partition i:list A, i:(A -> prop), o:list A, o:list A.
+std.partition [] _ [] [].
+std.partition [X|XS] P [X|R] L :- P X, !, std.partition XS P R L.
+std.partition [X|XS] P R [X|L] :- std.partition XS P R L.
+
+pred not-a-src i:list prop, i:derive.
+not-a-src Deps (derive A _ _) :- not(std.mem! Deps (dep1 A _)).
+
+pred tgt-is-not-in i:list derive, i:prop.
+tgt-is-not-in [] _.
+tgt-is-not-in [derive Tgt _ _|_] (dep1 _ Tgt) :- !, fail.
+tgt-is-not-in [_|L] D :- tgt-is-not-in L D.
+
+pred topo i:list derive, i:list prop, o:list derive.
+topo [] _ [] :- !.
+topo L Deps SL :-
+  std.partition L (not-a-src Deps) LNoDeps Other,
+  if (LNoDeps = []) (coq.error "derive: no topological order:" L Deps) true,
+  std.filter Deps (tgt-is-not-in LNoDeps) NewDeps,
+  topo Other NewDeps SOther,
+  std.append LNoDeps SOther SL.
+
+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 TypeName InModule :-
+  if (get-option "prefix" PFX)
+     (Prefix = PFX)
+     (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 TypeName SortedDL.
+
+}

apps/derive/elpi/derive_synterp_hook.elpi

@@ -0,0 +1,9 @@
+/* Entry point for derive extensions                                         */
+/* license: GNU Lesser General Public License Version 2.1 or later           */
+/* ------------------------------------------------------------------------- */
+
+pred derivation i:string, i:string, o:derive.
+pred export i:modpath.
+pred dep1 o:string, o:string.
+kind derive type.
+type derive string -> (list prop -> prop) -> prop -> derive.

apps/derive/examples/readme.v

@@ -1,29 +1,27 @@
-(* README *)                            
+(* README *)
 From elpi.apps Require Import derive.std.
- 
-derive Inductive peano := Zero | Succ (p : peano).
 
-(* Bug 8.16: About peano.peano.*)
-(* Notation peano := peano.peano *)
+#[module] derive Inductive peano := Zero | Succ (p : peano).
 
 Print peano.peano.
-(* Inductive peano : Type :=  Zero : peano | Succ : peano -> peano *)
+(* Inductive peano : Set :=  Zero : peano | Succ : peano -> peano. *)
 
 Eval compute in peano.eqb Zero (Succ Zero).
 (* = false : bool *)
 
 About peano.eqb_OK.
 (*
-peano.eqb_OK : forall x1 x2 : peano, Bool.reflect (x1 = x2) (peano.eqb x1 x2)
+peano.eqb_OK : forall x1 x2 : peano, reflect (x1 = x2) (peano.eqb x1 x2)
 
 peano.eqb_OK is not universe polymorphic
 Arguments peano.eqb_OK x1 x2
 peano.eqb_OK is opaque
+Expands to: Constant elpi.apps.derive.examples.readme.peano.eqb_OK
 *)
 
 #[verbose] derive Nat.add.
 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 ->