Commit e3760751 authored by Ralf Jung's avatar Ralf Jung

WIP: Make uPred, OFE and CMRAs use primitive projections

Compilation still fails
parent e7578e2d
From iris.algebra Require Export ofe.
Set Primitive Projections.
Class PCore (A : Type) := pcore : A option A.
Instance: Params (@pcore) 2.
......@@ -67,7 +69,7 @@ Structure cmraT := CMRAT' {
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CMRAMixin cmra_car;
_ : Type
cmra_car' : Type
}.
Arguments CMRAT' _ {_ _ _ _ _ _} _ _ _.
Notation CMRAT A m m' := (CMRAT' A m m' A).
......@@ -88,6 +90,8 @@ Hint Extern 0 (ValidN _) => eapply (@cmra_validN _) : typeclass_instances.
Coercion cmra_ofeC (A : cmraT) : ofeT := OfeT A (cmra_ofe_mixin A).
Canonical Structure cmra_ofeC.
Unset Primitive Projections.
(** Lifting properties from the mixin *)
Section cmra_mixin.
Context {A : cmraT}.
......
......@@ -10,6 +10,8 @@ From iris.algebra Require Export base.
*)
(** Unbundeled version *)
Set Primitive Projections.
Class Dist A := dist : nat relation A.
Instance: Params (@dist) 3.
Notation "x ≡{ n }≡ y" := (dist n x y)
......@@ -42,7 +44,7 @@ Structure ofeT := OfeT' {
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car;
_ : Type
ofe_car' : Type
}.
Arguments OfeT' _ {_ _} _ _.
Notation OfeT A m := (OfeT' A m A).
......@@ -54,6 +56,8 @@ Arguments ofe_equiv : simpl never.
Arguments ofe_dist : simpl never.
Arguments ofe_mixin : simpl never.
Unset Primitive Projections.
(** Lifting properties from the mixin *)
Section ofe_mixin.
Context {A : ofeT}.
......@@ -339,7 +343,10 @@ Section ofe_fun.
Next Obligation. intros c x n i ?. by apply (chain_cauchy c). Qed.
Global Program Instance ofe_fun_cofe `{Cofe B} : Cofe ofe_funC :=
{ compl c x := compl (ofe_fun_chain c x) }.
Next Obligation. intros ? n c x. apply (conv_compl n (ofe_fun_chain c x)). Qed.
Next Obligation. intros ? n c.
intro x. (* This fails. *)
hnf. unfold ofe_dist. intro x. (* This works. *)
apply (conv_compl n (ofe_fun_chain c x)). Qed.
End ofe_fun.
Arguments ofe_funC : clear implicits.
......
......@@ -79,7 +79,7 @@ Lemma nnupd_ownM_updateP x (Φ : M → Prop) :
x ~~>: Φ uPred_ownM x =n=> y, ⌜Φ y uPred_ownM y.
Proof.
intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
intros n y ? Hown a.
intros n y ? Hown. unfold uPred_holds. intros a.
red; rewrite //= => n' yf ??.
inversion Hown as (x'&Hequiv).
edestruct (Hbupd n' (Some (x' yf))) as (y'&?&?); eauto.
......
From iris.algebra Require Export cmra.
Set Primitive Projections.
Record uPred (M : ucmraT) : Type := IProp {
uPred_holds :> nat M Prop;
uPred_mono n x1 x2 : uPred_holds n x1 x1 {n} x2 uPred_holds n x2;
......@@ -8,6 +9,7 @@ Record uPred (M : ucmraT) : Type := IProp {
Arguments uPred_holds {_} _ _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Unset Primitive Projections.
Delimit Scope uPred_scope with I.
Bind Scope uPred_scope with uPred.
......
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