recursive derive

Author: gares

apps/derive/elpi/derive.elpi

@@ -10,7 +10,7 @@ exists-indc I P :-
   std.exists KL P.
 
 pred if-verbose i:prop.
-if-verbose P :- get-option "verbose" tt, !, P.
+if-verbose P :- (get-option "verbose" tt ; get-option "recursive" tt), !, P.
 if-verbose _.
 
 pred dep o:string, o:string.
@@ -22,38 +22,38 @@ selected Name :- get-option "only" Map, !,
   Map => (get-option Name _; (get-option X _, dep X Name)).
 selected _.
 
-pred validate-only i:list derive.
-validate-only LD :- get-option "only" Map, !, std.forall Map (known-option LD).
-validate-only _.
+pred validate-only i:gref, i:list derive.
+validate-only T LD :- get-option "only" Map, !, std.forall Map (known-option T LD).
+validate-only _ _.
 
-pred known-option i:list derive, i:prop.
-known-option L (get-option X _) :-
+pred known-option i:gref, i:list derive, i:prop.
+known-option T L (get-option X _) :-
   if (std.mem! L (derive X _ _)) true
-     (coq.error "Derivation" X "unknown or not applicable to the input").
-
-pred chain i:list derive, o:list prop.
-chain [] [].
-chain [derive Name _ _|FS] CL :- not(selected Name), !,
-  if-verbose (coq.say "Skipping derivation" Name "since the user did not select it"),
-  chain FS CL.
-chain [derive Name _ AlreadyDone|FS] CL :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
-  if-verbose (coq.say "Skipping derivation" Name "since it has been already run"),
-  chain FS CL.
-chain [derive Name F _|FS] CL :- get-option "only" _, !, % request this one
-  if-verbose (coq.say "Derivation" Name),
+     (coq.error "Derivation" X "unknown or not applicable to input" T).
+
+pred chain i:gref, i:list derive, o:list prop.
+chain _ [] [].
+chain T [derive Name _ _|FS] CL :- not(selected Name), !,
+  if-verbose (coq.say "Skipping derivation" Name "on" T "since the user did not select it"),
+  chain T FS CL.
+chain T [derive Name _ AlreadyDone|FS] CL :- (pi x\ stop x :- !, fail) => AlreadyDone, !,
+  if-verbose (coq.say "Skipping derivation" Name "on" T "since it has been already run"),
+  chain T FS CL.
+chain T [derive Name F _|FS] CL :- get-option "only" _, !, % request this one
+  if-verbose (coq.say "Derivation" Name "on" T),
   @dropunivs! => std.time (F C) Time,
-  if-verbose (coq.say "Derivation" Name "took" Time),
-  C => chain FS CS,
+  if-verbose (coq.say "Derivation" Name "on" T "took" Time),
+  C => chain T FS CS,
   std.append C CS CL.
-chain [derive Name F _|FS] CL :- % all are selected, we can fail
-  if-verbose (coq.say "Derivation" Name),
+chain T [derive Name F _|FS] CL :- % all are selected, we can fail
+  if-verbose (coq.say "Derivation" Name "on" T),
   (pi x\ stop x :- !, fail) => @dropunivs! => std.time (F C) Time, !,
-  if-verbose (coq.say "Derivation" Name "took" Time),
-  C => chain FS CS,
+  if-verbose (coq.say "Derivation" Name "on" T "took" Time),
+  C => chain T FS CS,
   std.append C CS CL.
-chain [derive F _ _|FS] CL :-
-  if-verbose (coq.say "Derivation" F "failed, continuing"),
-  chain FS CL.
+chain T [derive F _ _|FS] CL :-
+  if-verbose (coq.say "Derivation" F "on" T "failed, continuing"),
+  chain T FS CL.
 
 pred toposort i:list derive, o:list derive.
 toposort L SL :-
@@ -85,20 +85,36 @@ topo L Deps SL :-
 pred export? i:prop, o:prop.
 export? (export M) (coq.env.export-module M).
 
+pred indt-or-const i:gref.
+indt-or-const (indt _).
+indt-or-const (const _).
+
 pred main i:gref, i:string, o:list prop.
-main T Prefix CL :-
+main T Prefix CL :- get-option "recursive" tt, !,
+  coq.env.dependencies T _ AllDeps,
+  coq.gref.set.elements AllDeps AllDepsL,
+  std.filter AllDepsL indt-or-const Deps,
+  main.aux Deps Prefix [] CL1,
+  CL1 => main1 T Prefix CL2,
+  std.append CL1 CL2 CL.
+pred main.aux i:list gref, i:string, i:list prop, o:list prop.
+main.aux [] _ X X.
+main.aux [T|TS] Prefix Acc CL :-
+  (pi X\get-option "only" X :- !, fail) => Acc => main T Prefix CL1,
+  main.aux TS Prefix {std.append CL1 Acc} CL.
+
+main T Prefix CL :- main1 T Prefix CL.
+
+pred main1 i:gref, i:string, o:list prop.
+main1 T Prefix CL :-
   std.findall (derivation T 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 DL,
+  validate-only T DL,
   toposort DL SortedDL,
-  ModName is "Derive_Anonymous_" ^ {std.any->string {new_int}}, 
-  coq.env.begin-module ModName none,
-  chain SortedDL CL,
-  coq.env.end-module ModPath,
-  coq.env.import-module ModPath.
+  chain T SortedDL CL.
 
 pred decl+main i:indt-decl.
 decl+main DS :- std.do! [

apps/derive/examples/usage.v

@@ -3,22 +3,14 @@
 *)
 
 From Coq Require Import Bool.
-From elpi.apps Require Import derive.std derive.legacy.
+From elpi.apps Require Import derive.std.
 Set Uniform Inductive Parameters.
 
-(** The basic invocation is with just one argument, the inductive
-    type name *)
-derive nat.
-
-(** generated constants are prefixed with nat_ *)
-Check nat_eq_OK :
-  forall x y, reflect (x = y) (nat_eq x y).
-
-(** One can also prefix an Inductive declaration with derive. *)
+(** The best way to call derive is to prefix an Inductive declaration. *)
 derive
 Inductive tickle A := stop | more : A -> tickle -> tickle.
 
-(** In this case the command is elaborated to:
+(** The command is elaborated to something like:
 
   Module tickle.
     Inductive tickle A := stop | more : A -> tickle -> tickle.
@@ -27,23 +19,21 @@ Inductive tickle A := stop | more : A -> tickle -> tickle.
   Notation tickle := tickle.tickle.
   Notation stop := tickle.stop.
   Notation more := tickle.more.
+
 *)
 Check more :
   forall A, A -> tickle A -> tickle A.
 
 (** Some goodies *)
-Check tickle.eq : (* eq test *)
+Check tickle.eqb : (* eq test *)
   forall A, (A -> A -> bool) -> tickle A -> tickle A -> bool.
 
-Check tickle.eq_OK : (* eq test correctness proof *)
-  forall A f, (forall x y, reflect (x = y) (f x y)) -> forall x y, reflect (x = y) (tickle.eq A f x y).
+Check tickle.eqb_OK : (* eq test correctness proof *)
+  forall A f, (forall x y, reflect (x = y) (f x y)) -> forall x y, reflect (x = y) (tickle.eqb A f x y).
 
 Check tickle.map : (* map the container *)
   forall A B, (A -> B) -> tickle A -> tickle B.
 
-Check tickle.isk_stop : (* recognize a constructor *)
-  forall A, tickle A -> bool.
-
 Check tickle.tickle_R : (* relator (binary parametricity translation) *)
   forall A B, (A -> B -> Type) -> tickle A -> tickle B -> Type.
 
@@ -59,11 +49,8 @@ Check rtree.induction : (* this is the key *)
   (forall l, tickle.is_tickle (rtree A) P l -> P (Node A l)) ->
   forall x, rtree.is_rtree A PA x -> P x.
 
-Check rtree.eq_OK nat nat_eq nat_eq_OK : (* proofs compose *)
-  forall x y : rtree nat, reflect (x = y) (rtree.eq nat nat_eq x y).
-
 (** You can also select which derivations you like *)
-#[only(lens_laws, eq)] derive
+#[verbose, only(lens_laws, eqb)] derive
 Record Box A := { contents : A; tag : nat }.
 
 Check Box.eq :
@@ -81,3 +68,23 @@ Check Box._tag_contents_exchange : (* another one *)
   forall A (r : Box A) x y, set Box._tag x (set Box._contents y r) =
                             set Box._contents y (set Box._tag x r).
 
+(** Finally, one can derive an existing inductive typegenerated constants are
+    prefixed with nat_ but won't be in the right
+    place, which is where the type is defined. This means that two users
+    may run derive for the same type in different files, leading to
+    duplication. *)
+
+derive nat.
+
+Check nat_eq_OK :
+  forall x y, reflect (x = y) (nat_eq x y).
+
+(** Once can also run derive recursively, but this has the same bad effect,
+    all generated concepts will be out of place *)
+
+Inductive a := A.
+Inductive b := B : A -> B.
+
+#[recursive] derive b.
+
+Check b.eqb.

apps/derive/theories/derive.v

@@ -70,6 +70,7 @@ with-attributes P :-
   coq.parse-attributes A [
     att "verbose" bool,
     att "only" attmap,
+    att "recursive" bool,
   ] Opts, !,
   Opts => P.
 

apps/derive/theories/derive/std.v

@@ -17,8 +17,9 @@ From elpi.apps Require Export
   derive.tag
   derive.fields
   derive.eqb
+  derive.eqbcorrect
   derive.eqbOK
-.
+. 
 Elpi Typecheck derive.
 
 (* we derive the Coq prelude *)