Merge pull request #576 from proux01/rocq21611

Adapt to rocq-prover/rocq#21611

Author: proux01

HB/common/phant-abbreviation.elpi

@@ -225,14 +225,14 @@ build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type".
 %         [find s_0 | t ~ s_0]
 %         [find c_0 | s_0 ~ SK q_1 .. q_l t c_0]
 %         [find m'_{i_0_0}, .., m'_{i_0_n0} | c_0 ~ CK m'_{i_0_0} .. m'_{i_0_n0}]
-%         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_0_n0} m'_{i_0_n0} =>
+%         fun & hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_0_n0} m'_{i_0_n0} =>
 %       ...
 %       fun q'_1 .. q'_l' =>
 %         [find t   | T ~ t]
 %         [find s_k | t ~ s_k]
 %         [find c_k | s_k ~ SK q'_1 .. q'_l' y c_k]
 %         [find m'_{i_k_0}, .., m'_{i_k_nk} | c_0 ~ CK m'_{i_k_0} .. m'_{i_k_nk}]
-%         fun of hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_k_nk} m'_{i_k_nk} =>
+%         fun & hb.unify m_{i_0_0} m'_{i_0_0} & ... & hb.unify m_{i_k_nk} m'_{i_k_nk} =>
 %       F p_1 ... p_k T m_i0_j0 .. m_il_jl}}
 func mk-phant-term.mixins term, term, classname, phant-term,
   list term, name, term, (term -> list (w-args mixinname)) -> phant-term.

HB/structures.v

@@ -439,7 +439,7 @@ Elpi Export HB.graph.
   with requirements [Factory1] .. [FactoryN]:
 
 [[
-HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
+HB.mixin Record MixinName T & Factory1 T & … & FactoryN T := {
    op : T -> …
    …
    property : forall x : T, op …
@@ -451,7 +451,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
   - [MixinName T] abbreviation for the type of the (degenerate) factory
   - [MixinName.Build T] abbreviation for the constructor of the factory
 
-  Note: [T of f1 T & … & fN T] is ssreflect syntax for [T (_ : f1 T) … (_ : fN T)]
+  Note: [T & f1 T & … & fN T] is syntactic sugar for [T (_ : f1 T) … (_ : fN T)]
 
   Supported attributes:
   - [#[primitive]] experimental attribute to make the mixin/factory primitive,
@@ -500,7 +500,7 @@ actions N :-
 main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
 
 main _ :-
-  coq.error "Usage: HB.mixin Record <MixinName> T of F A & … := { … }.".
+  coq.error "Usage: HB.mixin Record <MixinName> T & F A & … := { … }.".
 }}.
 Elpi Typecheck.
 Elpi Export HB.mixin.
@@ -857,7 +857,7 @@ main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
 main [const-decl N _ _] :- with-attributes (actions N).
 
 main _ :-
-  coq.error "Usage: HB.factory Record <FactoryName> T of F A & … := { … }.\nUsage: HB.factory Definition <FactoryName> T of F A := t.".
+  coq.error "Usage: HB.factory Record <FactoryName> T & F A & … := { … }.\nUsage: HB.factory Definition <FactoryName> T of F A := t.".
 }}.
 Elpi Typecheck.
 Elpi Export HB.factory.
@@ -1121,7 +1121,7 @@ This command populates the current section with canonical instances.
 
   Syntax:
 [[
-HB.declare Context (p1 : P1) ... (pn : Pn) (t : T) of F0 ... Fk.
+HB.declare Context (p1 : P1) ... (pn : Pn) (t : T) & F0 & ... & Fk.
 ]]
   Effect:
 [[

examples/GReTA_talk/V2.v

@@ -8,7 +8,7 @@ HB.mixin Record is_semigroup (S : Type) := {
 HB.structure Definition SemiGroup :=
   { S of is_semigroup S }.
 
-HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+HB.mixin Record semigroup_is_monoid M & is_semigroup M := {
   zero  : M;
   add0r : forall x, add zero x = x;
   addr0 : forall x, add x zero = x;

examples/GReTA_talk/V3.v

@@ -8,7 +8,7 @@ HB.mixin Record is_semigroup (S : Type) := {
 HB.structure Definition SemiGroup :=
   { S & is_semigroup S }.
 
-HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+HB.mixin Record semigroup_is_monoid M & is_semigroup M := {
   zero  : M;
   add0r : forall x, add zero x = x;
   addr0 : forall x, add x zero = x;

examples/GReTA_talk/V4.v

@@ -7,7 +7,7 @@ HB.mixin Record is_semigroup (S : Type) := {
 }.
 HB.structure Definition SemiGroup := { S & is_semigroup S }.
 
-HB.mixin Record semigroup_is_monoid M of is_semigroup M := {
+HB.mixin Record semigroup_is_monoid M & is_semigroup M := {
   zero  : M;
   add0r : forall x, add zero x = x;
   addr0 : forall x, add x zero = x;
@@ -20,14 +20,14 @@ HB.factory Record is_monoid M := {
   add0r : forall x, add zero x = x;
   addr0 : forall x, add x zero = x;
 }.
-HB.builders Context (M : Type) of is_monoid M.
+HB.builders Context (M : Type) & is_monoid M.
   HB.instance Definition _ := is_semigroup.Build M add addrA.
   HB.instance Definition _ := semigroup_is_monoid.Build M zero add0r addr0.
 HB.end.
 
 HB.structure Definition Monoid := { M & is_monoid M }.
 
-HB.mixin Record monoid_is_group G of is_monoid G := {
+HB.mixin Record monoid_is_group G & is_monoid G := {
   opp : G -> G;
   subrr : forall x, add x (opp x) = zero;
   addNr : forall x, add (opp x) x = zero;
@@ -43,7 +43,7 @@ HB.factory Record is_group G := {
   subrr : forall x, add x (opp x) = zero;
   addNr : forall x, add (opp x) x = zero;
 }.
-HB.builders Context G of is_group G.
+HB.builders Context G & is_group G.
   Let addr0 : forall x, add x zero = x.
   Proof. by move=> x; rewrite -(addNr x) addrA subrr add0r. Qed.
   HB.instance Definition _ := is_monoid.Build G zero add addrA add0r addr0.
@@ -53,4 +53,4 @@ HB.end.
 HB.instance Definition Z_is_group : is_group Z :=
   is_group.Build Z 0%Z Z.add Z.opp
     Z.add_assoc Z.add_0_l (* Z.add_0_r (*spurious *) *)
-    Z.sub_diag Z.add_opp_diag_l.
+    Z.sub_diag Z.add_opp_diag_l.

examples/cat/cat.v

@@ -40,7 +40,7 @@ Notation "a ~>_ C b" := (@hom C a b)
   (at level 99, C at level 0, only parsing) : cat_scope.
 
 (* precategories are quivers + id and comp *)
-HB.mixin Record Quiver_IsPreCat C of Quiver C := {
+HB.mixin Record Quiver_IsPreCat C & Quiver C := {
   idmap : forall (a : C), a ~> a;
   comp : forall (a b c : C), (a ~> b) -> (b ~> c) -> (a ~> c);
 }.
@@ -50,7 +50,7 @@ HB.factory Record IsPreCat C := {
   idmap : forall (a : C), hom a a;
   comp : forall (a b c : C), hom a b -> hom b c -> hom a c;
 }.
-HB.builders Context C of IsPreCat C.
+HB.builders Context C & IsPreCat C.
   HB.instance Definition _ := IsQuiver.Build C hom.
   HB.instance Definition _ := Quiver_IsPreCat.Build C idmap comp.
 HB.end.
@@ -70,7 +70,7 @@ Notation "f \; g" := (comp f g) : cat_scope.
 Notation "\idmap_ a" := (@idmap _ a) (only parsing, at level 0) : cat_scope.
 
 (* categories are precategories + laws *)
-HB.mixin Record PreCat_IsCat C of PreCat C := {
+HB.mixin Record PreCat_IsCat C & PreCat C := {
   comp1o : forall (a b : C) (f : a ~> b), idmap \; f = f;
   compo1 : forall (a b : C) (f : a ~> b), f \; idmap = f;
   compoA : forall (a b c d : C) (f : a ~> b) (g : b ~> c) (h : c ~> d),
@@ -144,7 +144,7 @@ Qed.
 
 (* a functor is a prefunctor + laws for id and comp *)
 HB.mixin Record PreFunctor_IsFunctor (C D : precat) (F : C -> D)
-     of @PreFunctor C D F := {
+     & @PreFunctor C D F := {
    F1 : forall (a : C), F <$> \idmap_a = idmap;
    Fcomp : forall (a b c : C) (f : a ~> b) (g : b ~> c),
       F <$> (f \; g) = F <$> f \; F <$> g;
@@ -227,7 +227,7 @@ HB.instance Definition _ := cat_cat.
 Check (cat : cat).
 
 (* concrete categories *)
-HB.mixin Record Quiver_IsPreConcrete T of Quiver T := {
+HB.mixin Record Quiver_IsPreConcrete T & Quiver T := {
   concrete : T -> U;
   concrete_fun : forall (a b : T), (a ~> b) -> concrete a -> concrete b;
 }.
@@ -238,7 +238,7 @@ HB.structure Definition PreConcreteQuiver : Set :=
 Set Universe Checking.
 Coercion concrete : PreConcreteQuiver.sort >-> Sortclass.
 
-HB.mixin Record PreConcrete_IsConcrete T of PreConcreteQuiver T := {
+HB.mixin Record PreConcrete_IsConcrete T & PreConcreteQuiver T := {
   concrete_fun_inj : forall (a b : T), injective (concrete_fun a b)
 }.
 Unset Universe Checking.
@@ -250,7 +250,7 @@ Set Universe Checking.
 HB.instance Definition _ (C : ConcreteQuiver.type) :=
   IsPreFunctor.Build _ _ (concrete : C -> U) concrete_fun.
 
-HB.mixin Record PreCat_IsConcrete T of ConcreteQuiver T & PreCat T := {
+HB.mixin Record PreCat_IsConcrete T & ConcreteQuiver T & PreCat T := {
   concrete1 : forall (a : T), concrete <$> \idmap_a = idfun;
   concrete_comp : forall (a b c : T) (f : a ~> b) (g : b ~> c),
     concrete <$> (f \; g) = ((concrete <$> g) \o (concrete <$> f))%function;
@@ -308,7 +308,7 @@ HB.instance Definition _ := PreCat_IsConcrete.Build cat
    (fun=> erefl) (fun _ _ _ _ _ => erefl).
 
 (* constant functor *)
-Definition cst (C D : quiver) (c : C) := fun of D => c.
+Definition cst (C D : quiver) (c : C) := fun & D => c.
 Arguments cst {C} D c.
 HB.instance Definition _ {C D : precat} (c : C) :=
   IsPreFunctor.Build D C (cst D c) (fun _ _ _ => idmap).
@@ -574,7 +574,7 @@ Lemma delta_functor {C D : cat} : PreFunctor_IsFunctor _ _ (delta C D).
 Proof. by constructor=> [a|a b c f g]; exact/natP. Qed.
 HB.instance Definition _ C D := @delta_functor C D.
 
-HB.mixin Record IsMonad (C : precat) (M : C -> C) of @PreFunctor C C M := {
+HB.mixin Record IsMonad (C : precat) (M : C -> C) & @PreFunctor C C M := {
   unit : idfun ~~> M;
   join : (M \o M)%function ~~> M;
   bind : forall (a b : C), (a ~> M b) -> (M a ~> M b);
@@ -591,19 +591,19 @@ HB.structure Definition PreMonad (C : precat) :=
 HB.structure Definition Monad (C : precat) :=
    {M of @Functor C C M & IsMonad C M}.
 
-HB.factory Record IsJoinMonad (C : precat) (M : C -> C) of @PreFunctor C C M := {
+HB.factory Record IsJoinMonad (C : precat) (M : C -> C) & @PreFunctor C C M := {
   unit : idfun ~~> M;
   join : (M \o M)%function ~~> M;
   unit_join : forall a, (M <$> unit a) \; join _ = idmap;
   join_unit : forall a, join _ \; (M <$> unit a) = idmap;
   join_square : forall a, M <$> join a \; join _ = join _ \; join _
 }.
-HB.builders Context C M of IsJoinMonad C M.
+HB.builders Context C M & IsJoinMonad C M.
   HB.instance Definition _ := IsMonad.Build C M
     (fun a b f => erefl) unit_join join_unit join_square.
 HB.end.
 
-HB.mixin Record IsCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := {
+HB.mixin Record IsCoMonad (C : precat) (M : C -> C) & @IsPreFunctor C C M := {
   counit : M ~~> idfun;
   cojoin : M ~~> (M \o M)%function;
   cobind : forall (a b : C), (M a ~> b) -> (M a ~> M b);
@@ -619,14 +619,14 @@ HB.structure Definition PreCoMonad (C : precat) :=
 HB.structure Definition CoMonad (C : precat) :=
    {M of @Functor C C M & IsCoMonad C M}.
 
-HB.factory Record IsJoinCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := {
+HB.factory Record IsJoinCoMonad (C : precat) (M : C -> C) & @IsPreFunctor C C M := {
   counit : M ~~> idfun;
   cojoin : M ~~> (M \o M)%function;
   unit_cojoin : forall a, (M <$> counit a) \; cojoin _ = idmap;
   join_counit : forall a, cojoin _ \; (M <$> counit a) = idmap;
   cojoin_square : forall a, cojoin _ \; M <$> cojoin a = cojoin _ \; cojoin _
 }.
-HB.builders Context C M of IsJoinCoMonad C M.
+HB.builders Context C M & IsJoinCoMonad C M.
   HB.instance Definition _ := IsCoMonad.Build C M
     (fun a b f => erefl) unit_cojoin join_counit cojoin_square.
 HB.end.
@@ -822,7 +822,7 @@ Definition feqsym {C : precat} {a b : C} : a = b -> b ~> a.
 Proof. by move<-; exact idmap. Defined.
 
 HB.mixin Record IsLeftAdjointOf (C D : cat) (R : D ~> C) L
-    of @Functor C D L := {
+    & @Functor C D L := {
   Lphi : forall c d, (L c ~> d) -> (c ~> R d);
   Lpsi : forall c d, (c ~> R d) -> (L c ~> d);
   (* there should be a monad and comonad structure wrappers instead *)
@@ -861,7 +861,7 @@ Arguments Lcounit {C D R s}.
 (* End LeftAdjointOf_Theory. *)
 
 HB.mixin Record IsRightAdjoint (D C : cat) (R : D -> C)
-    of @Functor D C R := {
+    & @Functor D C R := {
   (* we should have a wrapper instead *)
   left_adjoint : C ~> D;
   LLphi : forall c d, (left_adjoint c ~> d) -> (c ~> R d);
@@ -886,7 +886,7 @@ Arguments LLpsi {D C s} {c d}.
 Arguments LLunit {D C s}.
 Arguments LLcounit {D C s}.
 
-HB.mixin Record PreCat_IsMonoidal C of PreCat C := {
+HB.mixin Record PreCat_IsMonoidal C & PreCat C := {
   onec : C;
   prod : (C * C)%type ~>_precat C;
 }.
@@ -906,7 +906,7 @@ Definition hom_cast {C : quiver} {a a' : C} (eqa : a = a')
   (a ~> b) -> (a' ~> b').
 Proof. now elim: _ / eqa; elim: _ / eqb. Defined.
 
-HB.mixin Record PreFunctor_IsMonoidal (C D : premonoidal) F of
+HB.mixin Record PreFunctor_IsMonoidal (C D : premonoidal) F &
     @PreFunctor C D F := {
   fun_one : F 1 = 1;
   fun_prod : forall (x y : C), F (x * y) = F x * F y;
@@ -949,7 +949,7 @@ HB.instance Definition _ {C : premonoidal} :=
   IsPreFunctor.Build C C prod1l
    (fun (a b : C) (f : a ~> b) => f <*> \idmap_1).
 
-HB.mixin Record PreMonoidal_IsMonoidal C of PreMonoidal C := {
+HB.mixin Record PreMonoidal_IsMonoidal C & PreMonoidal C := {
   prodA  : prod3l ~~> prod3r;
   prod1c : prod1r ~~> idfun;
   prodc1 : prod1l ~~> idfun;
@@ -1070,7 +1070,7 @@ HB.mixin Record IsIdeal (R : ring) (I : R -> Prop) := {
 }.
 HB.structure Definition Ideal (R : ring) := { I of IsIdeal R I }.
 
-HB.mixin Record Ideal_IsPrime (R : ring) (I : R -> Prop) of IsIdeal R I := {
+HB.mixin Record Ideal_IsPrime (R : ring) (I : R -> Prop) & IsIdeal R I := {
   ideal_prime : forall x y : R, I (x * y)%A -> I x \/ I y
 }.
 #[short(type="spectrum")]

examples/demo3/hierarchy_0.v

@@ -10,7 +10,7 @@ HB.mixin Record MulMonoid_of_Type A := {
 }.
 HB.structure Definition MulMonoid := { A of MulMonoid_of_Type A }.
 
-HB.mixin Record Ring_of_MulMonoid A of MulMonoid A := {
+HB.mixin Record Ring_of_MulMonoid A & MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;

examples/demo3/hierarchy_1.v

@@ -19,7 +19,7 @@ HB.mixin Record AddMonoid_of_Type A := {
 }.
 HB.structure Definition AddMonoid := { A of AddMonoid_of_Type A }.
 
-HB.mixin Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
+HB.mixin Record Ring_of_AddMulMonoid A & MulMonoid A & AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
@@ -28,7 +28,7 @@ HB.mixin Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
 }.
 HB.structure Definition Ring := { A of MulMonoid A & AddMonoid A & Ring_of_AddMulMonoid A }.
 
-HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
+HB.factory Record Ring_of_MulMonoid A & MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;

examples/demo3/hierarchy_2.v

@@ -19,20 +19,20 @@ HB.mixin Record AddMonoid_of_Type A := {
 }.
 HB.structure Definition AddMonoid := { A of AddMonoid_of_Type A }.
 
-HB.mixin Record AbGroup_of_AddMonoid A of AddMonoid A := {
+HB.mixin Record AbGroup_of_AddMonoid A & AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
 }.
 HB.structure Definition AbGroup := { A of AddMonoid A & AbGroup_of_AddMonoid A }.
 
-HB.mixin Record Ring_of_AbGroupMulMonoid A of MulMonoid A & AbGroup A := {
+HB.mixin Record Ring_of_AbGroupMulMonoid A & MulMonoid A & AbGroup A := {
   mulrDl : left_distributive mul (add : A -> A -> A);
   mulrDr : right_distributive mul (add : A -> A -> A);
 }.
 HB.structure Definition Ring := { A of MulMonoid A & AbGroup A & Ring_of_AbGroupMulMonoid A }.
 
-HB.factory Record Ring_of_AddMulMonoid A of MulMonoid A & AddMonoid A := {
+HB.factory Record Ring_of_AddMulMonoid A & MulMonoid A & AddMonoid A := {
   opp : A -> A;
   addrC : commutative (add : A -> A -> A);
   addNr : left_inverse zero opp add;
@@ -52,7 +52,7 @@ HB.builders Context A (a : Ring_of_AddMulMonoid A).
 
 HB.end.
 
-HB.factory Record Ring_of_MulMonoid A of MulMonoid A := {
+HB.factory Record Ring_of_MulMonoid A & MulMonoid A := {
   zero : A;
   add : A -> A -> A;
   addrA : associative add;

examples/demo4/hierarchy_0.v

@@ -16,7 +16,7 @@ Check (refl_equal _ : @inhab _ _ = 7).
 HB.instance Definition list_m1 A := m1.Build (option A) (list nat) (cons 7 nil) None.
 Check (refl_equal _ : @inhab _ _ = (cons 7 nil)).
 
-HB.mixin Record m2 (T : Type) (A : Type) of m1 T A := {
+HB.mixin Record m2 (T : Type) (A : Type) & m1 T A := {
   inj : T -> A;
 }.
 
@@ -25,4 +25,4 @@ HB.structure Definition s2 T :=
 
 Check fun X : s2.type nat => inhab : X.
 Check fun X : s2.type nat => inj : nat -> X.
-About s2_to_s1.
+About s2_to_s1.