Merge pull request #562 from math-comp/rename-class

avoid type name collision: class -> hbclass

Author: gares

.github/workflows/nix-action-coq-8.20.yml

@@ -1 +1 @@
-"a1bfc972fc850d935b8a38c8d901c54299b8df41"
+"7af8a21e712b7665447bea5189ce3ff83fcfeac8"

.github/workflows/nix-action-coq-9.0.yml

@@ -23,10 +23,10 @@ mixin-src_src (mixin-src _ _ S) S.
 func local-canonical-gref prop -> constant.
 local-canonical-gref (local-canonical C) C.
 
-func class_name class -> classname.
+func class_name hbclass -> classname.
 class_name (class N _ _) N.
 
-func class_structure class -> structure.
+func class_structure hbclass -> structure.
 class_structure (class _ S _) S.
 
 func class-def_name prop -> classname.
@@ -38,7 +38,7 @@ mixin-class_class (mixin-class _ C) C.
 func mixin-class_mixin prop -> mixinname.
 mixin-class_mixin (mixin-class M _) M.
 
-func classname->def classname -> class.
+func classname->def classname -> hbclass.
 classname->def CN (class CN S ML) :- class-def (class CN S ML), !.
 
 func classname->mixins classname -> mixins.
@@ -70,7 +70,7 @@ extract-builder (builder-decl B) B.
 func leq-builder builder, builder ->.
 leq-builder (builder N _ _ _) (builder M _ _ _) :- N =< M.
 
-func sub-class? class, class ->.
+func sub-class? hbclass, hbclass ->.
 sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :-
   not (C1 = C2),
   list-w-params_list ML1P ML1,
@@ -187,7 +187,7 @@ toposort-classes In Out :- std.do! [
   std.gref.toposort ES In Out,
 ].
 
-func findall-classes -> list class.
+func findall-classes -> list hbclass.
 findall-classes CLSortedDef :- std.do! [
   std.findall (class-def C_) All,
   std.map All class-def_name CL,
@@ -204,7 +204,7 @@ findall-classes-for.unsorted [M|ML] CLAcc Out :- std.do! [
   findall-classes-for.unsorted ML {std.append CL CLAcc} Out
 ].
 
-func findall-classes-for list mixinname -> list class.
+func findall-classes-for list mixinname -> list hbclass.
 findall-classes-for ML CLSortedDef :- std.do! [
   findall-classes-for.unsorted ML [] CL,
   toposort-classes CL CLSorted,
@@ -252,7 +252,7 @@ findall-local-canonical CL :-
 %
 % [findall-newjoins C AllSuper] finds all C1 and C2 such that C is a (new) join for
 % them
-pred distinct-pairs-below i:class, i:list class, o:class, o:class.
+pred distinct-pairs-below i:hbclass, i:list hbclass, o:hbclass, o:hbclass.
 distinct-pairs-below CurrentClass AllSuper C1 C2 :-
   std.mem AllSuper C1, std.mem AllSuper C2,
   % no cut until here, since we don't know which C1 and C2 to pick
@@ -267,7 +267,7 @@ distinct-pairs-below CurrentClass AllSuper C1 C2 :-
        true, % no join, valid pair
   ].
 
-pred assert-building-bottom-up i:class, i:classname, i:classname, i:classname.
+pred assert-building-bottom-up i:hbclass, i:classname, i:classname, i:classname.
 assert-building-bottom-up CurrentClass C3n C1n C2n :-
   class-def (class C3n X Y),
   CurrentClass = class CC _ _,
@@ -284,10 +284,10 @@ assert-building-bottom-up CurrentClass C3n C1n C2n :-
        Msg2)
      true.
 
-func distinct-pairs_pair prop -> pair class class.
+func distinct-pairs_pair prop -> pair hbclass hbclass.
 distinct-pairs_pair (distinct-pairs-below _ _ X Y) (pr X Y).
 
-func findall-newjoins class, list class -> list (pair class class).
+func findall-newjoins hbclass, list hbclass -> list (pair hbclass hbclass).
 findall-newjoins CurrentClass AllSuper TodoJoins :-
   std.findall (distinct-pairs-below CurrentClass AllSuper C1_ C2_) JoinOf,
   std.map JoinOf distinct-pairs_pair TodoJoins.

.github/workflows/nix-action-coq-9.1.yml

@@ -88,7 +88,7 @@ declare-const Name BodySkel TyWPSkel CFL CSL :- std.do! [
 ].
 
 % [not-subclass-of X C] holds if C does not inherit from X
-func not-subclass-of classname, class ->.
+func not-subclass-of classname, hbclass ->.
 not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _).
 
 % [declare-all T CL MCSTL] given a type T and a list of class definition
@@ -97,7 +97,7 @@ not-subclass-of HasNoInstance (class C _ _) :- not(sub-class C HasNoInstance _ _
 % rest. For each fulfilled class it declares a local constant inhabiting the
 % corresponding structure and declares it canonical.
 % Each mixin used in order to fulfill a class is returned together with its name.
-func declare-all term, list class -> list (pair id constant).
+func declare-all term, list hbclass -> list (pair id constant).
 declare-all _ [] [].
 declare-all T [class _ Struct _|Rest] L :- has-instance T Struct, !,
   declare-all T Rest L.
@@ -114,7 +114,7 @@ declare-all T [class HasNoInstance _ _|Rest] L :-
 % for generic types, we need first to instantiate them by giving them holes,
 % so they can be used to instantiate the classes
 :index (_ 2)
-func declare-all-on-type-constructor term, list class -> list (pair id constant).
+func declare-all-on-type-constructor term, list hbclass -> list (pair id constant).
 declare-all-on-type-constructor _ [] [].
 declare-all-on-type-constructor TK [class _ Struct _|Rest] L :- saturate-type-constructor TK T, has-instance T Struct, !,
   declare-all-on-type-constructor TK Rest L.
@@ -268,7 +268,7 @@ saturate-instances Filter :- std.do! [
     declare-all-on-type-constructor t Classes _),
 ].
 
-func no-instance-for cs-pattern, class ->.
+func no-instance-for cs-pattern, hbclass ->.
 no-instance-for K (class _ S _) :-
   get-structure-sort-projection S (global Proj),
   coq.CS.db-for Proj K [].

.github/workflows/nix-action-coq-master.yml

@@ -330,7 +330,7 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
 
 % [declare-coercion P1 P2 C1 C2] declares a structure and a class coercion
 % from C1 to C2 given P1 P2 the two projections from the structure of C1
-pred declare-coercion i:term, i:term, i:class, i:class.
+pred declare-coercion i:term, i:term, i:hbclass, i:hbclass.
 declare-coercion SortProjection ClassProjection
     (class FC StructureF FMLwP) (class TC StructureT TMLwP) :- std.do! [
 
@@ -386,7 +386,7 @@ join-body N1 N2 S3 S2_Pack S1_sort S3_to_S1 S2_class S3_to_S2
     mk-app S2_Pack {std.append Holes2 [S1_sortS3Ps, S2_classS3Ps]} (Pack s)
   ].
 
-pred declare-join i:class, i:pair class class, o:prop.
+pred declare-join i:hbclass, i:pair hbclass hbclass, o:prop.
 declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C2 C3) :-
   Name is "join_" ^ {gref->modname S3 2 "_"} ^
     "_between_" ^ {gref->modname S1 2 "_"} ^ "_and_" ^ {gref->modname S2 2 "_"},
@@ -414,7 +414,7 @@ declare-join (class C3 S3 MLwP3) (pr (class C1 S1 _) (class C2 S2 _)) (join C1 C
 % in the middle of existing ones. Possible fix: always declare all intermediate
 % possibilities but without proper names (requires the previous TODO about
 % aliasing already existing stuff).
-pred declare-unification-hints i:term, i:term, i:class, o:list prop.
+pred declare-unification-hints i:term, i:term, i:hbclass, o:list prop.
 declare-unification-hints SortProj ClassProj CurrentClass NewJoins :- std.do! [
   findall-classes All,
 
@@ -495,7 +495,7 @@ declare-sort-coercion CoeClass StructureName (global Proj) :-
 
   log.coq.coercion.declare (coercion Proj 0 StructureName CoeClass).
 
-pred if-class-already-exists-error i:id, i:list class, i:list mixinname.
+pred if-class-already-exists-error i:id, i:list hbclass, i:list mixinname.
 if-class-already-exists-error _ [] _.
 if-class-already-exists-error N [class _ S ML1wP|CS] ML2 :-
   list-w-params_list ML1wP ML1,

.nix/coq-nix-toolbox.nix

@@ -100,11 +100,11 @@ typeabbrev (w-mixins A) (pair mixins (w-params A)).
 % instances by calls to `S.Pack T {{lib:elpi.hole}}`, and extending the reconstruction
 % mecanism of mixins to also reinfer these holes.
 
-kind class type.
-type class classname -> structure -> mixins -> class.
+kind hbclass type.
+type class classname -> structure -> mixins -> hbclass.
 
 % class-def contains all the classes ever declared
-pred class-def o:class.
+pred class-def o:hbclass.
 
 %%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%