Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
5.1 kB · 102 lines
at icfp
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103import PackageCalculus.Core.Definitionimport Mathlib.Logic.Embedding.Basicimport Mathlib.Data.Finset.Image
/-! # Feature extension: definitions
Per-package feature flags drawn from `F`, together with feature-leveldependency (`FeatDepRel`) and additional-dependency (`AddlDepRel`) relationsand the `IsFeatureResolution` structure. -/
namespace PackageCalculus.Feature
open Function
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {F : Type*} [DecidableEq F]
/-- (p, f) in support means package p supports feature f. -/abbrev Support (N V : Type*) [DecidableEq N] [DecidableEq V] (F : Type*) [DecidableEq F] := Finset (Package N V × F)
/-- Feature dependency relation: (package, name, versions, required-features). -/abbrev FeatDepRel (N V : Type*) [DecidableEq N] [DecidableEq V] (F : Type*) [DecidableEq F] := Finset (Package N V × N × Finset V × Finset F)
/-- Additional dependency relation: ((package, feature), name, versions, required-features). -/abbrev AddlDepRel (N V : Type*) [DecidableEq N] [DecidableEq V] (F : Type*) [DecidableEq F] := Finset ((Package N V × F) × N × Finset V × Finset F)
/-- **Groundedness of a support relation.** Every supported package is real.The reduction only materialises feature packages (and their base back-edges)for real packages, so support facts over non-repository packages leave notrace in the reduced problem; this is the condition under which the supportrelation is recoverable (transpiling retraction). -/def Support.GroundedIn (support : Support N V F) (R : Real N V) : Prop := ∀ p f, (p, f) ∈ support → p ∈ R
/-- The standing Functional-in-Name normalisation (Def 3.1.2), extended tofeature dependencies: a package depends on a given name with at most oneversion set and required-feature set. -/def FeatDepRel.FunctionalInName (Δ_f : FeatDepRel N V F) : Prop := ∀ p n vs₁ fs₁ vs₂ fs₂, (p, n, vs₁, fs₁) ∈ Δ_f → (p, n, vs₂, fs₂) ∈ Δ_f → vs₁ = vs₂ ∧ fs₁ = fs₂
/-- The standing Functional-in-Name normalisation (Def 3.1.2), extended toadditional dependencies: a (package, feature) pair depends on a given namewith at most one version set and required-feature set. -/def AddlDepRel.FunctionalInName (Δ_a : AddlDepRel N V F) : Prop := ∀ pf m vs₁ fs₁ vs₂ fs₂, (pf, m, vs₁, fs₁) ∈ Δ_a → (pf, m, vs₂, fs₂) ∈ Δ_a → vs₁ = vs₂ ∧ fs₁ = fs₂
/-- **Base-requirement irredundancy.** No additional dependency restates theautomatic base requirement `⟨⟨n,v⟩,f⟩ → n ∋ {v}` that feature activationalready enforces for a supported real package. The reduction emits exactlythis edge for every grounded support fact, so a redundant `Δ_a` entry of thisshape is indistinguishable from it in the reduced problem; irredundancy is thecondition under which the additional-dependency relation is recoverable on thenose (without it, recovery is exact up to thebase-requirement closure). -/def AddlDepRel.BaseIrredundant (Δ_a : AddlDepRel N V F) (R : Real N V) (support : Support N V F) : Prop := ∀ n v f, ((n, v), f) ∈ support → (n, v) ∈ R → (((n, v), f), n, {v}, ∅) ∉ Δ_a
structure IsFeatureResolution (R : Real N V) (support : Support N V F) (Δ_f : FeatDepRel N V F) (Δ_a : AddlDepRel N V F) (r : Package N V) (S : Finset (Package N V × Finset F)) : Prop where no_root_support : ∀ f, (r, f) ∉ support subset : ∀ p fs, (p, fs) ∈ S → p ∈ R root_mem : (r, ∅) ∈ S feat_dep_closure : ∀ p fs_p, (p, fs_p) ∈ S → ∀ n vs fs, (p, n, vs, fs) ∈ Δ_f → ∃ v ∈ vs, ∃ fs', fs ⊆ fs' ∧ ((n, v), fs') ∈ S addl_dep_closure : ∀ p fs_p, (p, fs_p) ∈ S → ∀ f ∈ fs_p, ∀ n vs fs, ((p, f), n, vs, fs) ∈ Δ_a → ∃ v ∈ vs, ∃ fs', fs ⊆ fs' ∧ ((n, v), fs') ∈ S feature_unification : ∀ n v v' fs fs', ((n, v), fs) ∈ S → ((n, v'), fs') ∈ S → fs = fs' version_unique : ∀ n v v' fs fs', ((n, v), fs) ∈ S → ((n, v'), fs') ∈ S → v = v' support_mem : ∀ n v fs f, ((n, v), fs) ∈ S → f ∈ fs → ((n, v), f) ∈ support
class HasFeatureNames (N F : Type*) (N' : outParam Type*) where origN : N ↪ N' /-- Synthetic name for a (name, feature) pair. -/ featuredN : N → F → N' featuredN_injective : Injective2 featuredN origN_ne_featuredN : ∀ n₁ n₂ f, origN n₁ ≠ featuredN n₂ f featuredN_ne_origN : ∀ n₁ f n₂, featuredN n₁ f ≠ 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 `featuredN`. -/ tryFeaturedN : N' → Option (N × F) tryFeaturedN_featuredN : ∀ n f, tryFeaturedN (featuredN n f) = some (n, f) tryFeaturedN_some : ∀ n' p, tryFeaturedN n' = some p → featuredN p.1 p.2 = n'
attribute [simp] HasFeatureNames.origN_ne_featuredN HasFeatureNames.featuredN_ne_origN
end PackageCalculus.Feature