Commit 8c77aa2f authored by Robbert Krebbers's avatar Robbert Krebbers

Put the carrier also in the back of canonical structures.

This is inspired by ssr, and makes unification faster if it goes
right-to-left.

See https://sympa.inria.fr/sympa/arc/ssreflect/2013-11/msg00010.html
parent 6615248b
Pipeline #1436 passed with stage
...@@ -52,7 +52,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := { ...@@ -52,7 +52,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
}. }.
(** Bundeled version *) (** Bundeled version *)
Structure cmraT := CMRAT { Structure cmraT := CMRAT' {
cmra_car :> Type; cmra_car :> Type;
cmra_equiv : Equiv cmra_car; cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car; cmra_dist : Dist cmra_car;
...@@ -62,9 +62,11 @@ Structure cmraT := CMRAT { ...@@ -62,9 +62,11 @@ Structure cmraT := CMRAT {
cmra_valid : Valid cmra_car; cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car; cmra_validN : ValidN cmra_car;
cmra_cofe_mixin : CofeMixin cmra_car; cmra_cofe_mixin : CofeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car cmra_mixin : CMRAMixin cmra_car;
cmra_car' : Type
}. }.
Arguments CMRAT _ {_ _ _ _ _ _ _} _ _. Arguments CMRAT' _ {_ _ _ _ _ _ _} _ _ _.
Notation CMRAT A m m' := (CMRAT' A m m' A).
Arguments cmra_car : simpl never. Arguments cmra_car : simpl never.
Arguments cmra_equiv : simpl never. Arguments cmra_equiv : simpl never.
Arguments cmra_dist : simpl never. Arguments cmra_dist : simpl never.
...@@ -150,7 +152,7 @@ Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := { ...@@ -150,7 +152,7 @@ Record UCMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, Empty A} := {
mixin_ucmra_pcore_unit : pcore Some mixin_ucmra_pcore_unit : pcore Some
}. }.
Structure ucmraT := UCMRAT { Structure ucmraT := UCMRAT' {
ucmra_car :> Type; ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car; ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car; ucmra_dist : Dist ucmra_car;
...@@ -162,9 +164,11 @@ Structure ucmraT := UCMRAT { ...@@ -162,9 +164,11 @@ Structure ucmraT := UCMRAT {
ucmra_empty : Empty ucmra_car; ucmra_empty : Empty ucmra_car;
ucmra_cofe_mixin : CofeMixin ucmra_car; ucmra_cofe_mixin : CofeMixin ucmra_car;
ucmra_cmra_mixin : CMRAMixin ucmra_car; ucmra_cmra_mixin : CMRAMixin ucmra_car;
ucmra_mixin : UCMRAMixin ucmra_car ucmra_mixin : UCMRAMixin ucmra_car;
ucmra_car' : Type;
}. }.
Arguments UCMRAT _ {_ _ _ _ _ _ _ _} _ _ _. Arguments UCMRAT' _ {_ _ _ _ _ _ _ _} _ _ _ _.
Notation UCMRAT A m m' m'' := (UCMRAT' A m m' m'' A).
Arguments ucmra_car : simpl never. Arguments ucmra_car : simpl never.
Arguments ucmra_equiv : simpl never. Arguments ucmra_equiv : simpl never.
Arguments ucmra_dist : simpl never. Arguments ucmra_dist : simpl never.
......
...@@ -58,14 +58,16 @@ Class Contractive `{Dist A, Dist B} (f : A → B) := ...@@ -58,14 +58,16 @@ Class Contractive `{Dist A, Dist B} (f : A → B) :=
contractive n x y : ( i, i < n x {i} y) f x {n} f y. contractive n x y : ( i, i < n x {i} y) f x {n} f y.
(** Bundeled version *) (** Bundeled version *)
Structure cofeT := CofeT { Structure cofeT := CofeT' {
cofe_car :> Type; cofe_car :> Type;
cofe_equiv : Equiv cofe_car; cofe_equiv : Equiv cofe_car;
cofe_dist : Dist cofe_car; cofe_dist : Dist cofe_car;
cofe_compl : Compl cofe_car; cofe_compl : Compl cofe_car;
cofe_mixin : CofeMixin cofe_car cofe_mixin : CofeMixin cofe_car;
cofe_car' : Type
}. }.
Arguments CofeT _ {_ _ _} _. Arguments CofeT' _ {_ _ _} _ _.
Notation CofeT A m := (CofeT' A m A).
Add Printing Constructor cofeT. Add Printing Constructor cofeT.
Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances. Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances.
Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances. Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment