Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
1.9 kB · 55 lines
at dev
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556import PackageCalculus.Core.Definitionimport Mathlib.Data.Finset.Image
namespace PackageCalculus
variable (V : Type*)
inductive CmpOp where | ge | gt | le | lt | eq | ne deriving DecidableEq
inductive VersionFormula (V : Type*) where | top : VersionFormula V | bot : VersionFormula V | conj : VersionFormula V → VersionFormula V → VersionFormula V | disj : VersionFormula V → VersionFormula V → VersionFormula V | cmp : CmpOp → V → VersionFormula V deriving DecidableEq
variable {V : Type*} [DecidableEq V] {N : Type*} [DecidableEq N]
def CmpOp.eval [LT V] [DecidableRel (· < · : V → V → Prop)] (ω : CmpOp) (v c : V) : Bool := match ω with | .ge => !decide (v < c) | .gt => decide (c < v) | .le => !decide (c < v) | .lt => decide (v < c) | .eq => decide (v = c) | .ne => !decide (v = c)
/-- The versions in `Vn` that satisfy `φ`. -/def VersionFormula.eval [LT V] [DecidableRel (· < · : V → V → Prop)] (φ : VersionFormula V) (Vn : Finset V) : Finset V := match φ with | .top => Vn | .bot => ∅ | .conj φ₁ φ₂ => φ₁.eval Vn ∩ φ₂.eval Vn | .disj φ₁ φ₂ => φ₁.eval Vn ∪ φ₂.eval Vn | .cmp ω c => Vn.filter (fun v => ω.eval v c)
abbrev VFDepRel (N V : Type*) [DecidableEq N] [DecidableEq V] := Finset (Package N V × N × VersionFormula V)
/-- Like IsResolution but dependency closure uses formula semantics. -/structure IsVFResolution [LT V] [DecidableRel (· < · : V → V → Prop)] (R : Real N V) (Δ_Φ : VFDepRel N V) (r : Package N V) (S : Finset (Package N V)) : Prop where subset : S ⊆ R root_mem : r ∈ S dep_closure : ∀ p ∈ S, ∀ m : N, ∀ φ : VersionFormula V, (p, m, φ) ∈ Δ_Φ → ∃ v ∈ φ.eval (repoVersions R m), (m, v) ∈ S version_unique : VersionUnique S
end PackageCalculus