Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
7.5 kB · 165 lines
at dev
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166import PackageCalculus.Core.Definitionimport Mathlib.Logic.Embedding.Basic
/-! # Virtual extension: definitions
Virtual packages selecting concrete providers, encoded through a `provides`relation and the `IsVirtualResolution` structure. -/
namespace PackageCalculus.Virtual
open Function
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V]
/-- A version or top (wildcard). -/inductive VTop (V : Type*) where | val : V → VTop V | top : VTop V deriving DecidableEq
/-- Provides relation: (provider-package, virtual-name, version-or-top). -/abbrev ProvidesRel (N V : Type*) [DecidableEq N] [DecidableEq V] := Finset (Package N V × N × VTop V)
/-- v matches vs; top matches anything. -/def memTop (v : VTop V) (vs : Finset V) : Prop := match v with | .top => True | .val v' => v' ∈ vs
instance decidableMemTop (v : VTop V) (vs : Finset V) : Decidable (memTop v vs) := match v with | .top => Decidable.isTrue trivial | .val v' => Finset.decidableMem v' vs
structure IsVirtualResolution (R : Real N V) (Delta : DepRel N V) (prov : ProvidesRel N V) (r : Package N V) (S : Finset (Package N V)) (rho : Finset (Package N V × N × Package N V)) : Prop where subset : S ⊆ R root_mem : r ∈ S /-- Either a direct version is selected, or exactly one provider satisfies the dep via rho. -/ virtual_dep_closure : ∀ p ∈ S, ∀ n : N, ∀ vs : Finset V, (p, n, vs) ∈ Delta → (∃ v ∈ vs, (n, v) ∈ S) ∨ (∃! q, q ∈ S ∧ ∃ v, memTop v vs ∧ (q, n, v) ∈ prov ∧ (q, n, p) ∈ rho) version_unique : VersionUnique S /-- rho ⊆ S × N × S: every provider edge relates members of the resolution. -/ provider_subset : ∀ q : Package N V, ∀ n : N, ∀ p : Package N V, (q, n, p) ∈ rho → q ∈ S ∧ p ∈ S
class HasVirtualNames (N V : Type*) (N' : outParam Type*) where origN : N ↪ N' /-- Synthetic selector name for a (package, dep-name) pair. -/ selectorN : Package N V → N → N' selectorN_injective : Injective2 selectorN origN_ne_selectorN : ∀ n p m, origN n ≠ selectorN p m selectorN_ne_origN : ∀ p m n, selectorN p m ≠ origN n /-- Decidable partial inverse of `origN`. -/ tryOrigN : N' → Option N tryOrigN_origN : ∀ n, tryOrigN (origN n) = some n tryOrigN_some : ∀ n' n, tryOrigN n' = some n → origN n = n' /-- Decidable partial inverse of `selectorN`. -/ trySelectorN : N' → Option (Package N V × N) trySelectorN_selectorN : ∀ p n, trySelectorN (selectorN p n) = some (p, n) trySelectorN_some : ∀ n' q, trySelectorN n' = some q → selectorN q.1 q.2 = n'
attribute [simp] HasVirtualNames.origN_ne_selectorN HasVirtualNames.selectorN_ne_origN
class HasVirtualVersions (N V : Type*) (V' : outParam Type*) where origV : V ↪ V' /-- Synthetic provider version indexed by (name, version). -/ providerV : N → V → V' providerV_injective : Injective2 providerV origV_ne_providerV : ∀ v n w, origV v ≠ providerV n w providerV_ne_origV : ∀ n w v, providerV n w ≠ origV v /-- Decidable partial inverse of `origV`. -/ tryOrigV : V' → Option V tryOrigV_origV : ∀ v, tryOrigV (origV v) = some v tryOrigV_some : ∀ v' v, tryOrigV v' = some v → origV v = v' /-- Decidable partial inverse of `providerV`. -/ tryProviderV : V' → Option (N × V) tryProviderV_providerV : ∀ n w, tryProviderV (providerV n w) = some (n, w) tryProviderV_some : ∀ v' q, tryProviderV v' = some q → providerV q.1 q.2 = v'
attribute [simp] HasVirtualVersions.origV_ne_providerV HasVirtualVersions.providerV_ne_origV
/-- **No self-provides.** No package provides its own name: provided names areproperly virtual. The reduction routes a dependency on a virtual name throughselector packages whose versions mirror the chosen provider; a self-provider`⟨⟨n,w⟩, n, v⟩` would make its selector→provider edge structurally identical tothe selector→direct edge for the real version `w` of `n`, so the direct versionset could not be separated from the providers in the reduced problem. This isthe condition under which the dependency relation is recoverable up to`restrictReal` (transpiling retraction). -/def ProvidesRel.NoSelfProvides (prov : ProvidesRel N V) : Prop := ∀ q n v, (q, n, v) ∈ prov → q.1 ≠ n
/-- The instantiation of a provides relation on a dependency relation: theadmissible (provider, name, depender) triples, mirroring the shape of ρ.Guards are consulted only against the version sets Δ actually contains, sothis is the normal form of `prov` that resolution semantics observes(`instantiate_resolution_congr`). -/def ProvidesRel.instantiate (prov : ProvidesRel N V) (Δ : DepRel N V) : Finset (Package N V × N × Package N V) := Δ.biUnion fun e => prov.biUnion fun t => if t.2.1 = e.2.1 ∧ memTop t.2.2 e.2.2 then {(t.1, e.2.1, e.1)} else ∅
theorem ProvidesRel.mem_instantiate {prov : ProvidesRel N V} {Δ : DepRel N V} {q p : Package N V} {n : N} : (q, n, p) ∈ prov.instantiate Δ ↔ ∃ vs, (p, n, vs) ∈ Δ ∧ ∃ v, memTop v vs ∧ (q, n, v) ∈ prov := by simp only [ProvidesRel.instantiate, Finset.mem_biUnion] constructor · rintro ⟨⟨p₁, n₁, vs⟩, hdep, ⟨q₁, n₂, v⟩, hprov, hif⟩ split at hif · rename_i hc simp only at hc obtain ⟨hn, hm⟩ := hc rw [Finset.mem_singleton] at hif obtain ⟨rfl, rfl, rfl⟩ := hif subst hn exact ⟨vs, hdep, v, hm, hprov⟩ · exact absurd hif (Finset.notMem_empty _) · rintro ⟨vs, hdep, v, hv, hprov⟩ refine ⟨(p, n, vs), hdep, (q, n, v), hprov, ?_⟩ rw [if_pos ⟨rfl, hv⟩] exact Finset.mem_singleton_self _
/-- Resolutions consult the provides relation only through its instantiation:provides relations with the same instantiation on Δ admit the sameresolutions. -/theorem instantiate_resolution_congr {R : Real N V} {Δ : DepRel N V} {prov prov' : ProvidesRel N V} {r : Package N V} {S : Finset (Package N V)} {rho : Finset (Package N V × N × Package N V)} (hfn : Δ.FunctionalInName) (h : prov.instantiate Δ = prov'.instantiate Δ) : IsVirtualResolution R Δ prov r S rho ↔ IsVirtualResolution R Δ prov' r S rho := by suffices aux : ∀ {P P' : ProvidesRel N V}, P.instantiate Δ = P'.instantiate Δ → IsVirtualResolution R Δ P r S rho → IsVirtualResolution R Δ P' r S rho from ⟨aux h, aux h.symm⟩ intro P P' h hres refine ⟨hres.subset, hres.root_mem, ?_, hres.version_unique, hres.provider_subset⟩ intro p hp n vs hdep rcases hres.virtual_dep_closure p hp n vs hdep with hdir | ⟨q, ⟨hqS, v, hv, hP, hrho⟩, huniq⟩ · exact Or.inl hdir · have hq : (q, n, p) ∈ P'.instantiate Δ := by rw [← h] exact ProvidesRel.mem_instantiate.mpr ⟨vs, hdep, v, hv, hP⟩ obtain ⟨vs', hdep', v', hv', hP'⟩ := ProvidesRel.mem_instantiate.mp hq obtain rfl := hfn p n vs vs' hdep hdep' refine Or.inr ⟨q, ⟨hqS, v', hv', hP', hrho⟩, ?_⟩ rintro q₂ ⟨hq₂S, v₂, hv₂, hP₂, hrho₂⟩ apply huniq q₂ have hq₂ : (q₂, n, p) ∈ P.instantiate Δ := by rw [h] exact ProvidesRel.mem_instantiate.mpr ⟨vs, hdep, v₂, hv₂, hP₂⟩ obtain ⟨vs₂, hdep₂, v₀, hv₀, hP₀⟩ := ProvidesRel.mem_instantiate.mp hq₂ obtain rfl := hfn p n vs vs₂ hdep hdep₂ exact ⟨hq₂S, v₀, hv₀, hP₀, hrho₂⟩
end PackageCalculus.Virtual