more fresh names

Author: eponier

apps/derive/elpi/param1.elpi

@@ -108,7 +108,8 @@ reali-store N X XR :- !,
   Args = [_, _, X, XR],
   T1 = app [{{ lib:@param1.store_reali }}|Args],
   std.assert-ok! (coq.typecheck T1 T2) "reali-store: T1 illtyped",
-  coq.env.add-const Nreali T1 T2 _ GR,
+  coq.ensure-fresh-global-id Nreali FNreali,
+  coq.env.add-const FNreali T1 T2 _ GR,
   @global! => coq.TC.declare-instance (const GR) 0.
 
 pred reali-store-indc i:string, i:constructor, i:constructor.
@@ -134,7 +135,8 @@ dispatch (const GR) Prefix Clauses :- !, do! [
   std.assert-ok! (coq.typecheck VR VRTy) "param1: illtyped constant",
   std.assert-ok! (coq.unify-leq VRTy TyRV) "param1: constant does not have the right type",
 
-  coq.env.add-const Name VR TyRV _ TermR,
+  coq.ensure-fresh-global-id Name FName,
+  coq.env.add-const FName VR TyRV _ TermR,
 
   reali-store Name Term (global (const TermR)),
 
@@ -166,8 +168,9 @@ dispatch (indt GR) Prefix Clauses :- !, do! [
 
     NewName is Prefix ^ {coq.gref->id (indt GR)},
 
+    coq.ensure-fresh-global-id NewName FNewName,
     coq.build-indt-decl
-      (pr new_name NewName) tt LnoR LnoR {coq.subst-fun [Ind] TyR} KnamesR KtypesR DeclR
+      (pr new_name FNewName) tt LnoR LnoR {coq.subst-fun [Ind] TyR} KnamesR KtypesR DeclR
   ),
 
   std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param1 generates illtyped inductive",
@@ -176,7 +179,8 @@ dispatch (indt GR) Prefix Clauses :- !, do! [
 
   reali-store NewName Ind (global (indt GRR)),
   coq.env.indt GRR _ _ _ _ RealNamesR _,
-  forall2 Knames RealNamesR (reali-store-indc NewName),
+  Prefix1 is NewName ^ "_",
+  forall2 Knames RealNamesR (reali-store-indc Prefix1),
   C1 = (reali Ind (global (indt GRR)) :- !),
   coq.elpi.accumulate _ "derive.param1.db" (clause _ (before "reali:fail") C1),
   C2 = (realiR Ind (global (indt GRR)) :- !),
@@ -192,7 +196,8 @@ dispatch (indc _) _ _ :-
   coq.error "derive.param1: cannot translate a constructor".
 
 pred main i:gref, i:string, o:list prop.
-main T Out Clauses :- dispatch T Out Clauses.
+main T _ Clauses :-
+  dispatch T "is_" Clauses.
 
 }
 

apps/derive/elpi/param2.elpi

@@ -133,7 +133,8 @@ store-param N X X1 XR :- !,
   Args = [_, _, _, X, X1, XR],
   T1 = app [{{ lib:@param2.store_param }}|Args],
   std.assert-ok! (coq.typecheck T1 T2) "store-param: T1 illtyped",
-  coq.env.add-const Nparam T1 T2 _ C,
+  coq.ensure-fresh-global-id Nparam FNparam,
+  coq.env.add-const FNparam T1 T2 _ C,
   @global! => coq.TC.declare-instance (const C) 0.
 
 pred store-param-indc i:string, i:constructor, i:constructor.
@@ -159,7 +160,8 @@ dispatch (const GR as C) Suffix Clauses :- do! [
   std.assert-ok! (coq.typecheck XR XRTy) "param2: illtyped constant",
   std.assert-ok! (coq.unify-leq XRTy TyRTermTerm) "param2: constant does not have the right type",
 
-  coq.env.add-const NameR XR TyRTermTerm _ TermR,
+  coq.ensure-fresh-global-id NameR FNameR,
+  coq.env.add-const FNameR XR TyRTermTerm _ TermR,
 
   store-param NameR Term Term (global (const TermR)),
 
@@ -175,14 +177,15 @@ dispatch (indt I as GR) Suffix Clauses :- do! [
   Ind = global GR,
   coq.env.indt I IsInd Lno Luno Ty Knames Ktypes,
   NameR is {coq.gref->id GR} ^ Suffix,
+  coq.ensure-fresh-global-id NameR FNameR,
   map Knames (rename-indc Suffix) KnamesR,
 
   std.map Knames (k\r\ r = global (indc k)) Ks,
   pi new_name\ sigma KtypesR TyR\ (
       (param-indt I IsInd Lno Luno Ty Ks Ktypes
  	    	 new_name IsIndR LnoR LunoR TyR KtypesR),
     coq.build-indt-decl
-      (pr new_name NameR) IsIndR LnoR LunoR {coq.subst-fun [Ind, Ind] TyR} KnamesR KtypesR DeclR
+      (pr new_name FNameR) IsIndR LnoR LunoR {coq.subst-fun [Ind, Ind] TyR} KnamesR KtypesR DeclR
   ),
 
   std.assert-ok! (coq.typecheck-indt-decl DeclR) "derive.param2 generates illtyped term",
@@ -210,7 +213,8 @@ dispatch (indc _) _ _ :-
   coq.error "derive.param2: cannot translate a constructor".
 
 pred main i:gref, i:string, o:list prop.
-main T Out Clauses :- dispatch T Out Clauses.
+main T _ Clauses :-
+  dispatch T "_R" Clauses.
 
 }
 

apps/derive/theories/derive/param1.v

@@ -83,11 +83,10 @@ Elpi Accumulate File paramX.
 Elpi Accumulate File param1.
 Elpi Accumulate Db derive.param1.db.
 Elpi Accumulate lp:{{
-  main [str I, str O] :- !, coq.locate I GR, derive.param1.main GR O _.
-  main [str I] :- !, coq.locate I GR, derive.param1.main GR "is_" _.
+  main [str I] :- !, coq.locate I GR, derive.param1.main GR "" _.
   main _ :- usage.
 
-  usage :- coq.error "Usage: derive.param1 <object name> [<output prefix>]".
+  usage :- coq.error "Usage: derive.param1 <object name>".
 }}. 
 Elpi Typecheck.
 
@@ -106,6 +105,6 @@ Elpi Accumulate derive lp:{{
 pred derive.on_param1 i:inductive, i:(inductive -> string -> list prop -> prop), i:string, o:list prop.
 derive.on_param1 T F N C :- reali (global (indt T)) (global (indt P)), !, F P N C.
 
-derivation T Prefix (derive "param1" (derive.param1.main T N ) (reali-done T)) :- N is Prefix ^ "is_".
+derivation T N (derive "param1" (derive.param1.main T N ) (reali-done T)).
 
 }}.

apps/derive/theories/derive/param2.v

@@ -46,11 +46,10 @@ Elpi Accumulate File paramX.
 Elpi Accumulate File param2.
 Elpi Accumulate Db derive.param2.db.
 Elpi Accumulate lp:{{
-  main [str I, str O] :- !, coq.locate I GR, derive.param2.main GR O _.
-  main [str I] :- !, coq.locate I GR, derive.param2.main GR "_R" _.
+  main [str I] :- !, coq.locate I GR, derive.param2.main GR "" _.
   main _ :- usage.
 
-  usage :- coq.error "Usage: derive.param2 <object name> [<output suffix>]".
+  usage :- coq.error "Usage: derive.param2 <object name>".
 }}. 
 Elpi Typecheck.
 
@@ -59,7 +58,7 @@ Elpi Accumulate derive Db derive.param2.db.
 Elpi Accumulate derive File param2.
 Elpi Accumulate derive lp:{{
 
-derivation T Prefix (derive "param2" (derive.param2.main T N) (param-done T)) :- N is Prefix ^ "_R".
+derivation T N (derive "param2" (derive.param2.main T N) (param-done T)).
 
 }}.