W0.1: unify algebraic-composition classifier quartet

src/v2/lens/common/algebraic_composition.dag

@@ -0,0 +1,101 @@
+module v2.lens.common.algebraic_composition
+
+import v2.compiler.infer { InferredFacts }
+import v2.std.dependency { DependencyKindClassifier }
+import v2.std.diagnostic { Diagnostic }
+import v2.std.witness { Witness }
+
+type EffectClassification {}
+
+type IdempotencyVerdict
+  = AlgebraicIdempotenceProven { law: Witness<InferredFacts> }
+  | RequiresAlgebraWitness
+
+type OwnershipMode
+  = OwnedContainment
+  | SharedRead
+  | RequiresAccessWitness
+  | BorrowedDependency
+  | UnknownOwnership
+
+type ParallelismRelation
+  = DataDependent
+  | EffectCoupled
+  | BarrierCoupled
+  | UnresolvedCoupling { diagnostic: Diagnostic }
+
+type ParallelismKindPolicy
+  = KnownParallelismRelation { relation: ParallelismRelation }
+  | ReadsParallelismFacts
+
+data effect_classifier: DependencyKindClassifier<EffectClassification> = DependencyKindClassifier {
+  contains: EffectClassification {},
+  binds_to: EffectClassification {},
+  type_depends_on: EffectClassification {},
+  data_depends_on: EffectClassification {},
+  effect_depends_on: EffectClassification {},
+  resource_depends_on: EffectClassification {},
+  module_depends_on: EffectClassification {},
+  barrier_before: EffectClassification {},
+  placement_depends_on: EffectClassification {},
+  model_depends_on: EffectClassification {},
+  projection_depends_on: EffectClassification {},
+  generated_from: EffectClassification {},
+  verified_by: EffectClassification {},
+  promoted_by: EffectClassification {},
+  bootstrap_depends_on: EffectClassification {}
+}
+
+data idempotency_classifier: DependencyKindClassifier<IdempotencyVerdict> = DependencyKindClassifier {
+  contains: RequiresAlgebraWitness,
+  binds_to: RequiresAlgebraWitness,
+  type_depends_on: RequiresAlgebraWitness,
+  data_depends_on: RequiresAlgebraWitness,
+  effect_depends_on: RequiresAlgebraWitness,
+  resource_depends_on: RequiresAlgebraWitness,
+  module_depends_on: RequiresAlgebraWitness,
+  barrier_before: RequiresAlgebraWitness,
+  placement_depends_on: RequiresAlgebraWitness,
+  model_depends_on: RequiresAlgebraWitness,
+  projection_depends_on: RequiresAlgebraWitness,
+  generated_from: RequiresAlgebraWitness,
+  verified_by: RequiresAlgebraWitness,
+  promoted_by: RequiresAlgebraWitness,
+  bootstrap_depends_on: RequiresAlgebraWitness
+}
+
+data ownership_classifier: DependencyKindClassifier<OwnershipMode> = DependencyKindClassifier {
+  contains: OwnedContainment,
+  binds_to: BorrowedDependency,
+  type_depends_on: UnknownOwnership,
+  data_depends_on: SharedRead,
+  effect_depends_on: RequiresAccessWitness,
+  resource_depends_on: RequiresAccessWitness,
+  module_depends_on: UnknownOwnership,
+  barrier_before: UnknownOwnership,
+  placement_depends_on: UnknownOwnership,
+  model_depends_on: UnknownOwnership,
+  projection_depends_on: UnknownOwnership,
+  generated_from: UnknownOwnership,
+  verified_by: UnknownOwnership,
+  promoted_by: UnknownOwnership,
+  bootstrap_depends_on: UnknownOwnership
+}
+
+data parallelism_classifier: DependencyKindClassifier<ParallelismKindPolicy> = DependencyKindClassifier {
+  contains: KnownParallelismRelation { relation: DataDependent },
+  binds_to: KnownParallelismRelation { relation: DataDependent },
+  type_depends_on: ReadsParallelismFacts,
+  data_depends_on: KnownParallelismRelation { relation: DataDependent },
+  effect_depends_on: KnownParallelismRelation { relation: EffectCoupled },
+  resource_depends_on: KnownParallelismRelation { relation: EffectCoupled },
+  module_depends_on: ReadsParallelismFacts,
+  barrier_before: KnownParallelismRelation { relation: BarrierCoupled },
+  placement_depends_on: ReadsParallelismFacts,
+  model_depends_on: ReadsParallelismFacts,
+  projection_depends_on: ReadsParallelismFacts,
+  generated_from: ReadsParallelismFacts,
+  verified_by: ReadsParallelismFacts,
+  promoted_by: ReadsParallelismFacts,
+  bootstrap_depends_on: ReadsParallelismFacts
+}

src/v2/lens/effect.dag

@@ -1,5 +1,6 @@
 module v2.lens.effect
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import v2.lens.common.algebraic_composition { EffectClassification, effect_classifier }
 import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredFacts, InferredTree }
@@ -15,6 +16,7 @@ import v2.std.collection {
 import v2.std.dependency {
   ClassifiedDependencyView,
   DependencyView,
+  classify_dependency_view,
   classified_dependency_view_eq
 }
 import v2.std.diagnostic {
@@ -28,8 +30,6 @@ import v2.std.logic { Bool }
 import v2.std.node { Node, Symbol }
 import v2.std.witness { Holds, Violates, Witness }
 
-type EffectClassification {}
-
 type EffectFact {
   dependencies: List<ClassifiedDependencyView<EffectClassification>>
 }
@@ -38,10 +38,7 @@ fn effect_classify(
   tree: InferredTree,
   view: DependencyView
 ) -> ClassifiedDependencyView<EffectClassification> {
-  ClassifiedDependencyView {
-    dependency: view,
-    classification: EffectClassification {}
-  }
+  classify_dependency_view(classifier: effect_classifier, view: view)
 }
 
 fn effect_fact(tree: InferredTree, dependencies: List<DependencyView>) -> EffectFact {

src/v2/lens/idempotency.dag

@@ -1,5 +1,11 @@
 module v2.lens.idempotency
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import v2.lens.common.algebraic_composition {
+  AlgebraicIdempotenceProven,
+  IdempotencyVerdict,
+  RequiresAlgebraWitness,
+  idempotency_classifier
+}
 import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredFacts, InferredTree }
@@ -14,7 +20,6 @@ import v2.std.collection {
 }
 import v2.std.dependency {
   ClassifiedDependencyView,
-  DependencyKindClassifier,
   DependencyView,
   classify_dependency_view,
   classified_dependency_view_eq
@@ -30,36 +35,12 @@ import v2.std.logic { Bool }
 import v2.std.node { Symbol }
 import v2.std.witness { Holds, Violates, Witness }
 
-type IdempotencyVerdict
-  = AlgebraicIdempotenceProven { law: Witness<InferredFacts> }
-  | RequiresAlgebraWitness
-
 type IdempotencyFact {
   dependencies: List<ClassifiedDependencyView<IdempotencyVerdict>>
 }
 
-fn idempotency_dependency_kind_classifier() -> DependencyKindClassifier<IdempotencyVerdict> {
-  DependencyKindClassifier {
-    contains: RequiresAlgebraWitness,
-    binds_to: RequiresAlgebraWitness,
-    type_depends_on: RequiresAlgebraWitness,
-    data_depends_on: RequiresAlgebraWitness,
-    effect_depends_on: RequiresAlgebraWitness,
-    resource_depends_on: RequiresAlgebraWitness,
-    module_depends_on: RequiresAlgebraWitness,
-    barrier_before: RequiresAlgebraWitness,
-    placement_depends_on: RequiresAlgebraWitness,
-    model_depends_on: RequiresAlgebraWitness,
-    projection_depends_on: RequiresAlgebraWitness,
-    generated_from: RequiresAlgebraWitness,
-    verified_by: RequiresAlgebraWitness,
-    promoted_by: RequiresAlgebraWitness,
-    bootstrap_depends_on: RequiresAlgebraWitness
-  }
-}
-
 fn idempotency_classify(view: DependencyView) -> ClassifiedDependencyView<IdempotencyVerdict> {
-  classify_dependency_view(classifier: idempotency_dependency_kind_classifier(), view: view)
+  classify_dependency_view(classifier: idempotency_classifier, view: view)
 }
 
 fn idempotency_fact(tree: InferredTree, dependencies: List<DependencyView>) -> IdempotencyFact {

src/v2/lens/ownership.dag

@@ -1,13 +1,21 @@
 module v2.lens.ownership
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import v2.lens.common.algebraic_composition {
+  BorrowedDependency,
+  OwnedContainment,
+  OwnershipMode,
+  RequiresAccessWitness,
+  SharedRead,
+  UnknownOwnership,
+  ownership_classifier
+}
 import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredTree }
 import v2.std.algebra { bag_eq, list_snoc_item }
 import v2.std.collection { List }
 import v2.std.dependency {
   ClassifiedDependencyView,
-  DependencyKindClassifier,
   DependencyView,
   classify_dependency_view,
   classified_dependency_view_eq
@@ -23,39 +31,12 @@ import v2.std.logic { Bool }
 import v2.std.node { Symbol }
 import v2.std.witness { Holds, Violates, Witness }
 
-type OwnershipMode
-  = OwnedContainment
-  | SharedRead
-  | RequiresAccessWitness
-  | BorrowedDependency
-  | UnknownOwnership
-
 type OwnershipFact {
   dependencies: List<ClassifiedDependencyView<OwnershipMode>>
 }
 
-fn ownership_dependency_kind_classifier() -> DependencyKindClassifier<OwnershipMode> {
-  DependencyKindClassifier {
-    contains: OwnedContainment,
-    binds_to: BorrowedDependency,
-    type_depends_on: UnknownOwnership,
-    data_depends_on: SharedRead,
-    effect_depends_on: RequiresAccessWitness,
-    resource_depends_on: RequiresAccessWitness,
-    module_depends_on: UnknownOwnership,
-    barrier_before: UnknownOwnership,
-    placement_depends_on: UnknownOwnership,
-    model_depends_on: UnknownOwnership,
-    projection_depends_on: UnknownOwnership,
-    generated_from: UnknownOwnership,
-    verified_by: UnknownOwnership,
-    promoted_by: UnknownOwnership,
-    bootstrap_depends_on: UnknownOwnership
-  }
-}
-
 fn ownership_classify(view: DependencyView) -> ClassifiedDependencyView<OwnershipMode> {
-  classify_dependency_view(classifier: ownership_dependency_kind_classifier(), view: view)
+  classify_dependency_view(classifier: ownership_classifier, view: view)
 }
 
 fn ownership_fact(tree: InferredTree, dependencies: List<DependencyView>) -> OwnershipFact {

src/v2/lens/parallelism.dag

@@ -1,5 +1,16 @@
 module v2.lens.parallelism
 import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
+import v2.lens.common.algebraic_composition {
+  BarrierCoupled,
+  DataDependent,
+  EffectCoupled,
+  KnownParallelismRelation,
+  ParallelismKindPolicy,
+  ParallelismRelation,
+  ReadsParallelismFacts,
+  UnresolvedCoupling,
+  parallelism_classifier
+}
 import std.disposition { SingleAuthority }
 
 import v2.compiler.infer { InferredFacts, InferredTree, inferred_facts_descent }
@@ -14,7 +25,6 @@ import v2.std.collection {
 }
 import v2.std.dependency {
   ClassifiedDependencyView,
-  DependencyKindClassifier,
   DependencyView,
   classify_dependency_kind,
   classified_dependency_view_eq
@@ -31,38 +41,22 @@ import v2.std.logic { Bool }
 import v2.std.node { Symbol }
 import v2.std.witness { Holds, Violates, Witness }
 
-type ParallelismRelation
-  = DataDependent
-  | EffectCoupled
-  | BarrierCoupled
-  | UnresolvedCoupling { diagnostic: Diagnostic }
-
-type ParallelismKindPolicy
-  = KnownParallelismRelation { relation: ParallelismRelation }
-  | ReadsParallelismFacts
-
 type ParallelismFact {
   dependencies: List<ClassifiedDependencyView<ParallelismRelation>>
 }
 
-fn parallelism_dependency_kind_classifier() -> DependencyKindClassifier<ParallelismKindPolicy> {
-  DependencyKindClassifier {
-    contains: KnownParallelismRelation { relation: DataDependent },
-    binds_to: KnownParallelismRelation { relation: DataDependent },
-    type_depends_on: ReadsParallelismFacts,
-    data_depends_on: KnownParallelismRelation { relation: DataDependent },
-    effect_depends_on: KnownParallelismRelation { relation: EffectCoupled },
-    resource_depends_on: KnownParallelismRelation { relation: EffectCoupled },
-    module_depends_on: ReadsParallelismFacts,
-    barrier_before: KnownParallelismRelation { relation: BarrierCoupled },
-    placement_depends_on: ReadsParallelismFacts,
-    model_depends_on: ReadsParallelismFacts,
-    projection_depends_on: ReadsParallelismFacts,
-    generated_from: ReadsParallelismFacts,
-    verified_by: ReadsParallelismFacts,
-    promoted_by: ReadsParallelismFacts,
-    bootstrap_depends_on: ReadsParallelismFacts
-  }
+fn parallelism_relation_for_view(
+  tree: InferredTree,
+  view: DependencyView
+) -> ParallelismRelation {
+  parallelism_relation_for_policy(
+    tree: tree,
+    view: view,
+    policy: classify_dependency_kind(
+      classifier: parallelism_classifier,
+      kind: view.kind
+    )
+  )
 }
 
 fn parallelism_witness_diagnostic() -> Diagnostic {
@@ -121,20 +115,6 @@ fn parallelism_relation_for_policy(
   }
 }
 
-fn parallelism_relation_for_view(
-  tree: InferredTree,
-  view: DependencyView
-) -> ParallelismRelation {
-  parallelism_relation_for_policy(
-    tree: tree,
-    view: view,
-    policy: classify_dependency_kind(
-      classifier: parallelism_dependency_kind_classifier(),
-      kind: view.kind
-    )
-  )
-}
-
 fn parallelism_classify(
   tree: InferredTree,
   view: DependencyView