diff --git a/src/v2/lens/common/algebraic_composition.dag b/src/v2/lens/common/algebraic_composition.dag new file mode 100644 index 00000000000..d8ffc24e3bc --- /dev/null +++ b/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 } + | 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 = 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 = 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 = 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 = 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 +} diff --git a/src/v2/lens/effect.dag b/src/v2/lens/effect.dag index d5cfd505c27..567ab3dfd92 100644 --- a/src/v2/lens/effect.dag +++ b/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> } @@ -38,10 +38,7 @@ fn effect_classify( tree: InferredTree, view: DependencyView ) -> ClassifiedDependencyView { - ClassifiedDependencyView { - dependency: view, - classification: EffectClassification {} - } + classify_dependency_view(classifier: effect_classifier, view: view) } fn effect_fact(tree: InferredTree, dependencies: List) -> EffectFact { diff --git a/src/v2/lens/idempotency.dag b/src/v2/lens/idempotency.dag index e066e3222c7..93250b1d49f 100644 --- a/src/v2/lens/idempotency.dag +++ b/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 } - | RequiresAlgebraWitness - type IdempotencyFact { dependencies: List> } -fn idempotency_dependency_kind_classifier() -> DependencyKindClassifier { - 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 { - 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) -> IdempotencyFact { diff --git a/src/v2/lens/ownership.dag b/src/v2/lens/ownership.dag index 1f7aa2a8548..ac567f51c12 100644 --- a/src/v2/lens/ownership.dag +++ b/src/v2/lens/ownership.dag @@ -1,5 +1,14 @@ 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 } @@ -7,7 +16,6 @@ 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> } -fn ownership_dependency_kind_classifier() -> DependencyKindClassifier { - 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 { - 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) -> OwnershipFact { diff --git a/src/v2/lens/parallelism.dag b/src/v2/lens/parallelism.dag index 438465a65e0..4677dc40b61 100644 --- a/src/v2/lens/parallelism.dag +++ b/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> } -fn parallelism_dependency_kind_classifier() -> DependencyKindClassifier { - 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