fix collision by generating a fresh name

Author: gares

Changelog.md

@@ -12,6 +12,7 @@
 - New `coq.env.term-dependencies` computing all the `grefs` occurring in a term.
 - New `coq.redflag` and `coq.redflags` types for `@redflags!` option understood
   by `coq.reduction.lazy.*` `and coq.reduction.cbv.norm`
+- New `coq.env.fresh-global-id`
 
 ### APPS
 - Change `derive` usage.

apps/derive/elpi/bcongr.elpi

@@ -110,8 +110,9 @@ main-constructor Lno Prefix K Kt Clause :- do! [
   % we build the comparison function
   bo-param Lno Kn Kt R,
   std.assert-ok! (coq.typecheck R RT) "derive.bcongr generates illtyped term",
-  Name is Prefix ^ {coq.gref->id (indc K)},
-  coq.env.add-const Name R RT @opaque! Cong,
+  Name is Prefix ^ "bcongr_" ^ {coq.gref->id (indc K)},
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName R RT @opaque! Cong,
 
   % we register it as a clause
   Clause = (bcongr-db K (global (const Cong)) :- !),

apps/derive/elpi/derive.elpi

@@ -89,24 +89,25 @@ 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 :- get-option "recursive" tt, !,
+pred main i:gref, i:bool, o:list prop.
+main T P 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,
+  main.aux Deps [] CL1,
+  CL1 => main1 T P 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.
+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 Prefix CL :- main1 T Prefix CL.
+main T P CL :- main1 T P CL.
 
-pred main1 i:gref, i:string, o:list prop.
-main1 T Prefix CL :-
+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,
   if (L = [])
      (coq.error "no derivation found, did you Import derive.std?")
@@ -125,7 +126,7 @@ decl+main DS :- std.do! [
   if-verbose (coq.say "Declaring inductive" D),
   coq.env.add-indt D I,
   if-verbose (coq.say "Deriving"),
-  main (indt I) "" CL,
+  main (indt I) ff CL,
   if-verbose (coq.say "Done"),
   coq.env.end-module _,
 

apps/derive/elpi/eqb.elpi

@@ -12,13 +12,15 @@ derive.eqb.main (indt I) Prefix CL :- std.do! [
   derive.eqb.eqbf.main FI FI [] [] R,
   std.assert-ok! (coq.typecheck R Rty) "derive.eqbf generates illtyped term",
   Name is Prefix ^ "eqb_fields",
-  coq.env.add-const Name R Rty ff C,
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName R Rty ff C,
   EQBF = global (const C),
 
   derive.eqb.eqb.main FI FI [] [] EQBF R1Skel,
   std.assert-ok! (coq.elaborate-skeleton R1Skel R1ty R1) "derive.eqb generates illtyped term", % need elaborate for prim record
   Name1 is Prefix ^ "eqb",
-  coq.env.add-const Name1 R1 R1ty ff C1,
+  coq.ensure-fresh-global-id Name1 FName1,
+  coq.env.add-const FName1 R1 R1ty ff C1,
   EQB = global (const C1),
 
   % populate dbs
@@ -31,8 +33,9 @@ derive.eqb.main (const C) Prefix CL :- std.do! [
   coq.env.const C (some T) _,
   std.assert! (eqb-for T T EQB) "cannot derive eqb",
   Name is Prefix ^ "eqb",
+  coq.ensure-fresh-global-id Name FName,
   X = global (const C),
-  coq.env.add-const Name EQB {{ lp:X -> lp:X -> bool }} @transparent! EQBC,
+  coq.env.add-const FName EQB {{ lp:X -> lp:X -> bool }} @transparent! EQBC,
   CL = [eqb-done (const C), eqb-for (global (const C)) (global (const C)) (global (const EQBC))],
   std.forall CL (x\ coq.elpi.accumulate _ "derive.eqb.db" (clause _ (before "eqb-for:whd") x)),
 ].

apps/derive/elpi/eqbcorrect.elpi

@@ -33,7 +33,8 @@ main (indt I) Prefix CLs :- std.do! [
   %std.assert! (ground_term R) "ww",
   std.assert-ok! (coq.typecheck R Ty) "derive.eqbcorrect: common/correct generates ill typed term", 
   Name is Prefix ^ "eqb_correct",
-  coq.env.add-const Name R Ty @opaque! Correct,
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName R Ty @opaque! Correct,
 
   if (has-params? FI) (
 
@@ -42,7 +43,8 @@ main (indt I) Prefix CLs :- std.do! [
 
     std.assert-ok! (coq.typecheck Rx Tyx) "derive.eqbcorrect: common-aux/corect generates ill typed term", 
     Namex is Prefix ^ "eqb_correct_aux",
-    coq.env.add-const Namex Rx Tyx @opaque! Correctx,
+    coq.ensure-fresh-global-id Namex FNamex,
+    coq.env.add-const FNamex Rx Tyx @opaque! Correctx,
     CL_CORRECT = [correct-lemma-for (global (indt I)) (global (const Correctx))]
 
   ) (CL_CORRECT = [correct-lemma-for (global (indt I)) (global (const Correct))]),
@@ -54,7 +56,8 @@ main (indt I) Prefix CLs :- std.do! [
 
   std.assert-ok! (coq.typecheck Rr Tyr) "derive.eqbcorrect: common/refl generates ill typed term", 
   Namer is Prefix ^ "eqb_refl",
-  coq.env.add-const Namer Rr Tyr @opaque! Refl,
+  coq.ensure-fresh-global-id Namer FNamer,
+  coq.env.add-const FNamer Rr Tyr @opaque! Refl,
 
   if (has-params? FI) (
 
@@ -63,7 +66,8 @@ main (indt I) Prefix CLs :- std.do! [
 
     std.assert-ok! (coq.typecheck Rrx Tyrx) "derive.eqbcorrect: common-aux/refl generates ill typed term", 
     Namerx is Prefix ^ "eqb_refl_aux",
-    coq.env.add-const Namerx Rrx Tyrx @opaque! Reflx,
+    coq.ensure-fresh-global-id Namerx FNamerx,
+    coq.env.add-const FNamerx Rrx Tyrx @opaque! Reflx,
     CL_REFL = [refl-lemma-for (global (indt I)) (global (const Reflx))]
 
   ) (CL_REFL = [refl-lemma-for (global (indt I)) (global (const Refl))]),
@@ -83,8 +87,10 @@ main (const C) Prefix [Clause] :- std.do! [
   NameR is Prefix ^ "eqb_refl",
   NameC is Prefix ^ "eqb_correct",
   X = global (const C),
-  coq.env.add-const NameC Correct {{ @eqb_correct  lp:X lp:F }} @transparent! CC,
-  coq.env.add-const NameR Refl   {{ @eqb_reflexive lp:X lp:F }} @transparent! CR,
+  coq.ensure-fresh-global-id NameR FNameR,
+  coq.ensure-fresh-global-id NameC FNameC,
+  coq.env.add-const FNameC Correct {{ @eqb_correct  lp:X lp:F }} @transparent! CC,
+  coq.env.add-const FNameR Refl   {{ @eqb_reflexive lp:X lp:F }} @transparent! CR,
   Clause = (eqcorrect-for (const C) CC CR),
   coq.elpi.accumulate _ "derive.eqbcorrect.db" (clause _ _ Clause),
 ].

apps/derive/elpi/fields.elpi

@@ -29,23 +29,27 @@ main I Prefix AllCL :- std.do! [
   CLB => fields_t.main FI (global (indt I)) Body_t,
   std.assert-ok! (coq.typecheck Body_t Ty_t) "derive.fields generates illtyped fields_t",
   Name_t is Prefix ^ "fields_t",
-  coq.env.add-const Name_t Body_t Ty_t ff Fields_t, 
+  coq.ensure-fresh-global-id Name_t FName_t,
+  coq.env.add-const FName_t Body_t Ty_t ff Fields_t, 
 
   CLB => fields.main FI (global (indt I)) (global (const Fields_t)) (global (const Tag)) BodySkel,
   % we elaborate only for primitive records...
   std.assert-ok! (coq.elaborate-skeleton BodySkel Ty Body) "derive.fields generates illtyped fields",
   Name is Prefix ^ "fields",
-  coq.env.add-const Name Body Ty ff Fields, 
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName Body Ty ff Fields, 
 
   CLB => construct.main FI (global (indt I)) Fields_t Body_c,
   std.assert-ok! (coq.typecheck Body_c Ty_c) "derive.fields generates illtyped construct",
   Name_c is Prefix ^ "construct",
-  coq.env.add-const Name_c Body_c Ty_c ff Construct, 
+  coq.ensure-fresh-global-id Name_c FName_c,
+  coq.env.add-const FName_c Body_c Ty_c ff Construct, 
 
   coq.bind-ind-arity (global (indt I)) Arity (case-refl Tag Fields Construct) Body_PSkel,
   std.assert-ok! (coq.elaborate-skeleton Body_PSkel Ty_P Body_P) "derive.fields generates illtyped constructP",
   Name_P is Prefix ^ "constructP",
-  coq.env.add-const Name_P Body_P Ty_P @opaque! ConstructP, 
+  coq.ensure-fresh-global-id Name_P FName_P,
+  coq.env.add-const FName_P Body_P Ty_P @opaque! ConstructP, 
 
   AllCL = [fields-for I Fields_t Fields Construct ConstructP|CLB],
   std.forall AllCL (x\ coq.elpi.accumulate _ "derive.fields.db" (clause _ _ x)),

apps/derive/elpi/induction.elpi

@@ -117,7 +117,7 @@ params 0 Ity K KT Arity (fun `P` Pty p\ Bo p) :-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 pred main i:inductive, i:string, o:list prop.
-main GR Name [Clause] :- do! [
+main GR Prefix [Clause] :- do! [
   T = global (indt GR),
 
   if (coq.env.informative? GR) (Informative = [informative]) (Informative = []),
@@ -134,7 +134,9 @@ main GR Name [Clause] :- do! [
   % coq.say {coq.term->string R},
   std.assert-ok! (coq.typecheck R RT) "derive.induction generates illtyped term",
 
-  coq.env.add-const Name R RT _ I,
+  Name is Prefix ^ "induction",
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName R RT _ I,
 
   % we register it as a clause
   Clause = (induction-db GR (global (const I)) :- !),

apps/derive/elpi/map.elpi

@@ -170,15 +170,17 @@ mk-clause N Lno Ity1 Ity2 X Todo Map C :- whd1 X X1, !,
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 pred main i:inductive, i:string, o:list prop.
-main GR Name C :- do! [
+main GR Prefix C :- do! [
   T = global (indt GR),
   coq.env.indt GR _Ind Lno Luno Arity _ _,
   assert! (Lno = Luno) "derive.map: Non-uniform parameters not supported",
 
   % generate map and add to the env
   bo-params 0 Lno T T Arity Arity [] RSkel,
   std.assert-ok! (coq.elaborate-skeleton RSkel Rty R) "derive.map generates illtyped term",
-  coq.env.add-const Name R Rty @transparent! Funct,
+  Name is Prefix ^ "map",
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName R Rty @transparent! Funct,
 
   % generate clause and add to the db
   mk-clause 0 Lno T T Arity [] (global (const Funct)) Clause,

apps/derive/elpi/tag.elpi

@@ -23,7 +23,7 @@ main I Prefix CL :- do! [
   std.assert-ok! (elaborate-skeleton BodyR Ty Body) "derive.tag generates illtyped code",
 
   % save constant
-  Name is Prefix ^ "tag",
+  coq.ensure-fresh-global-id (Prefix ^ "tag") Name,
   coq.env.add-const Name Body Ty ff C,
 
   % store in the DB the tag function, so that other Elpi commands can find it

apps/derive/examples/usage.v

@@ -53,7 +53,7 @@ Check rtree.induction : (* this is the key *)
 #[verbose, only(lens_laws, eqb)] derive
 Record Box A := { contents : A; tag : nat }.
 
-Check Box.eq :
+Check Box.eqb :
   forall A, (A -> A -> bool) -> Box A -> Box A -> bool.
 
 Import lens.
@@ -76,15 +76,16 @@ Check Box._tag_contents_exchange : (* another one *)
 
 derive nat.
 
-Check nat_eq_OK :
-  forall x y, reflect (x = y) (nat_eq x y).
+Check nat_eqb_OK :
+  forall x y, reflect (x = y) (nat_eqb 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.
+Inductive b := B : a -> b.
 
-#[recursive] derive b.
+#[recursive, only(eqbOK)] derive b.
 
-Check b.eqb.
+Check a_eqb.
+Check b_eqb.