Something went wrong. Try again.
The Package Calculus
Something went wrong. Try again.
2.3 kB · 50 lines
at icfp
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051import PackageCalculus.Composition.FeatureConcurrent.Typesimport PackageCalculus.Extensions.Feature.Definitionimport PackageCalculus.Extensions.Concurrent.Definition
/-! # Feature-concurrent composition: definitions
`IsConcurrentFeatureResolution` combines the per-package feature support withconcurrent version handling: a single shared intermediate per `(parent, name)`plus per-feature secondary intermediates, all linked via π. -/
namespace PackageCalculus.Composition
open Classical
variable {N : Type*} [DecidableEq N] {V : Type*} [DecidableEq V] {F : Type*} [DecidableEq F] {G : Type*} [DecidableEq G]variable {N_FC : Type*} [DecidableEq N_FC] {V_FC : Type*} [DecidableEq V_FC]variable [hcnm : Concurrent.HasConcurrentNames (Feature.FeatureName N F) V G N_FC]variable [hcvr : Concurrent.HasConcurrentVersions V G V_FC]variable [hcfi : HasConcurrentFeatureIntermediate N V F G N_FC]
set_option linter.unusedSectionVars false
/-! ### Target resolution predicate -/
structure IsConcurrentFeatureResolution (R : Real N V) (support : Feature.Support N V F) (Δ_f : Feature.FeatDepRel N V F) (Δ_a : Feature.AddlDepRel N V F) (g : V → G) (r : Package N V) (S : Finset (Package N V × Finset F)) (π : Finset (Package N V × Package N V)) : Prop where no_root_support : ∀ f, (r, f) ∉ support subset : ∀ p fs, (p, fs) ∈ S → p ∈ R root_mem : (r, ∅) ∈ S feature_unification : ∀ n v fs fs', ((n, v), fs) ∈ S → ((n, v), fs') ∈ S → fs = fs' parent_closure : ∀ p fs_p, (p, fs_p) ∈ S → ∀ n vs fs, (p, n, vs, fs) ∈ Δ_f → ∃! v, v ∈ vs ∧ (∃ fs', fs ⊆ fs' ∧ ((n, v), fs') ∈ S) ∧ ((n, v), p) ∈ π parent_closure_addl : ∀ p fs_p, (p, fs_p) ∈ S → ∀ f ∈ fs_p, ∀ n vs fs, ((p, f), n, vs, fs) ∈ Δ_a → ∃! v, v ∈ vs ∧ (∃ fs', fs ⊆ fs' ∧ ((n, v), fs') ∈ S) ∧ ((n, v), p) ∈ π π_functional : ∀ n v v' p, ((n, v), p) ∈ π → ((n, v'), p) ∈ π → v = v' version_granularity : ∀ n v v' fs fs', ((n, v), fs) ∈ S → ((n, v'), fs') ∈ S → v ≠ v' → g v ≠ g v' support_mem : ∀ n v fs f, ((n, v), fs) ∈ S → f ∈ fs → ((n, v), f) ∈ support
end PackageCalculus.Composition