Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.9 kB · 38 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839import PackageCalculus.Extensions.Concurrent.Definition
/-! # Peer-dependency extension: definitions
A `PeerRel` lets a parent constrain which version of a peer name its childrenmay use. Builds on the concurrent extension via `IsPeerResolution`. -/
namespace PackageCalculus.PeerDep
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {G : Type*}
/-- p Θ (n, vs) means a parent of p can only depend on peer n with a version in vs. -/abbrev PeerRel (N V : Type*) [DecidableEq N] [DecidableEq V] := Finset (Package N V × N × Finset V)
/-- **Groundedness of a peer relation.** Every peer constraint`⟨⟨o,u⟩, m, ws⟩ ∈ Θ` is *witnessed* by a package `⟨n,v⟩` that depends both on thepeer name `o` (with a version set containing `u`) and on the constrained name`m`. The reduction only emits a core edge for a peer constraint through such awitness, so this is exactly the condition under which the peer relation isrecoverable from the reduced problem (transpiling retraction). -/def PeerRel.GroundedIn (Θ : PeerRel N V) (Δ : DepRel N V) : Prop := ∀ o u m ws, ((o, u), m, ws) ∈ Θ → ∃ n v us, ((n, v), o, us) ∈ Δ ∧ u ∈ us ∧ ∃ ws', ((n, v), m, ws') ∈ Δ
structure IsPeerResolution (R : Real N V) (Δ : DepRel N V) (Θ : PeerRel N V) (g : V → G) (r : Package N V) (S : Finset (Package N V)) (π : Finset (Package N V × Package N V)) : Prop where concurrent : Concurrent.IsConcurrentResolution R Δ g r S π /-- If p has peer dep on n, and p's parent q depends on n, the version selected by q via π must be in the peer constraint. -/ peer_satisfaction : ∀ p ∈ S, ∀ n : N, ∀ vs : Finset V, (p, n, vs) ∈ Θ → ∀ q, (p, q) ∈ π → ∀ us : Finset V, (q, n, us) ∈ Δ → ∀ v, v ∈ us → ((n, v), q) ∈ π → v ∈ vs
end PackageCalculus.PeerDep