Commit 95c486ef authored by Ralf Jung's avatar Ralf Jung

add the infrastructure for Coq to automatically infer the "inG" instances

I added a new typeclass "inGF" to witness that a particular *functor* is part of \Sigma. inG, in contrast, witnesses a particular *CMRA* to be in there, after applying the functor to "\later iProp".
inGF can be inferred if that functor is consed to the head of \Sigma, and it is preserved by consing a new functor to \Sigma. This is not the case for inG since the recursive occurence of \Sigma also changes.
For evry construction (auth, sts, saved_prop), there is an instance infering the respective authG, stsG, savedPropG from an inGF. There is also a global inG_inGF, but Coq is unable to use it.

I tried to instead have *only* inGF, since having both typeclasses seemed weird. However, then the actual type that e.g. "own" is about is the result of applying a functor, and Coq entirely fails to infer anything.

I had to add a few type annotations in heap.v, because Coq tried to use the "authG_inGF" instance before the A got fixed, and ended up looping and expanding endlessly on that proof of timelessness.
This does not seem entirely unreasonable, I was honestly surprised Coq was able to infer the types previously.
parent dcaea50a
......@@ -28,19 +28,10 @@ Section client.
End client.
Section ClosedProofs.
Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: authF (constF heapRA)
Definition Σ : iFunctorG := agreeF .:: constF (stsRA barrier_proto.sts) .:: heapF
.:: (λ _, constF unitRA) : iFunctorG.
Notation iProp := (iPropG heap_lang Σ).
Instance: authG heap_lang Σ heapRA.
Proof. split; try apply _. by exists 2%nat. Qed.
Instance: stsG heap_lang Σ barrier_proto.sts.
Proof. split; try apply _. by exists 1%nat. Qed.
Instance: savedPropG heap_lang Σ.
Proof. by exists 0%nat. Qed.
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
Proof.
apply ht_alt. rewrite (heap_alloc (ndot nroot "Barrier")); last first.
......
......@@ -8,6 +8,7 @@ Import uPred.
predicates over finmaps instead of just ownP. *)
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
Definition heapF := authF heapRA.
Class heapG Σ := HeapG {
heap_inG : inG heap_lang Σ (authRA heapRA);
......@@ -20,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
Definition of_heap : heapRA state := omap (maybe Excl).
Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := Excl v ]}.
auth_own heap_name ({[ l := Excl v ]} : heapRA).
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
ownP (of_heap h).
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
......@@ -103,7 +104,7 @@ Section heap.
P || Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
trans (|={E}=> auth_own heap_name P)%I.
trans (|={E}=> auth_own heap_name ( : heapRA) P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
......
......@@ -76,12 +76,9 @@ Section LiftingTests.
End LiftingTests.
Section ClosedProofs.
Definition Σ : iFunctorG := λ _, authF (constF heapRA).
Definition Σ : iFunctorG := heapF .:: endF.
Notation iProp := (iPropG heap_lang Σ).
Instance: authG heap_lang Σ heapRA.
Proof. split; try apply _. by exists 1%nat. Qed.
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
Proof.
apply ht_alt. rewrite (heap_alloc nroot); last by rewrite nclose_nroot.
......
......@@ -9,6 +9,13 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_timeless (a : A) :> Timeless a;
}.
(* TODO: This shadows algebra.auth.authF. *)
Definition authF (A : cmraT) := constF (authRA A).
Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{ a : A, Timeless a}
`{inGF Λ Σ (authF A)} : authG Λ Σ A.
Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
Section definitions.
Context `{authG Λ Σ A} (γ : gname).
(* TODO: Once we switched to RAs, it is no longer necessary to remember that a
......
......@@ -145,3 +145,22 @@ Proof.
apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
Qed.
End global.
(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
the functor breaks badly because Coq is unable to infer the correct
typeclasses, it does not unfold the functor. *)
Class inGF (Λ : language) (Σ : gid iFunctor) (F : iFunctor) := InGF {
inGF_id : gid;
inGF_prf : F = Σ inGF_id;
}.
Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
Proof. exists 0. done. Qed.
Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
Proof. exists (S inGF_id). apply inGF_prf. Qed.
Definition endF : gid iFunctor := const (constF unitRA).
......@@ -5,6 +5,9 @@ Import uPred.
Notation savedPropG Λ Σ :=
(inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed.
Definition saved_prop_own `{savedPropG Λ Σ}
(γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
own γ (to_agree (Next (iProp_unfold P))).
......
......@@ -8,6 +8,12 @@ Class stsG Λ Σ (sts : stsT) := StsG {
}.
Coercion sts_inG : stsG >-> inG.
Definition stsF (sts : stsT) := constF (stsRA sts).
Instance stsG_inGF sts `{Inhabited (sts.state sts)}
`{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts.
Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
Section definitions.
Context `{i : stsG Λ Σ sts} (γ : gname).
Import sts.
......
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