diff --git a/src/v4/std/coercion.dag b/src/v4/std/coercion.dag new file mode 100644 index 00000000000..8b81f0e57e5 --- /dev/null +++ b/src/v4/std/coercion.dag @@ -0,0 +1,158 @@ +// src/v4/std/coercion.dag +// Scope: exact coercion-fold substrate boundary over canonical groundings. +// Owns: CoercionCandidate, CoercionCandidateSet, CoercionFoldPolicy, TargetSelectionPolicy, CoercionMismatchKind, CoercionDiagnostic, AcceptedLoss, CoercionQuality, CoercionWitness, CoercionResult, coercion_quality_compose, candidates_for_algebra, coercion_fold, verify_coercion_witness. +// Consumes: std constraints, std collection, std diagnostic, std node. +// Status: scaffold — TASKS T-9/T-10; exact-only coercion fold, no rewrites. +// Anchor: docs/design-v4-compiler-homomorphism.md P7. + + +module v4.std.coercion + + +import v4.std.collection { List } +import v4.std.constraints { CanonicalGrounding } +import v4.std.diagnostic { + Diagnostic, + ExternalContractUnknown, + Locus, + Outcome, + PortLocus, + Rejected, + Unavailable +} +import v4.std.node { Node, Symbol } + + +type CoercionCandidate { + target: CanonicalGrounding +} + + +type CoercionCandidateSet { + target_model: Node + algebra_instance: Node + candidates: List +} + + +type TargetSelectionPolicy + + +type CoercionFoldPolicy { + target_selection: TargetSelectionPolicy +} + + +// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. +type CoercionMismatchKind + = NoTargetCandidate + | AmbiguousTargetCandidate + | StructuralMismatch + + +type CoercionDiagnostic { + kind: CoercionMismatchKind + at: Locus +} + + +type AcceptedLoss { + declaration: Node +} + + +// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. +type CoercionQuality + = Identity + | Exact + | Lossy { accepted_loss: AcceptedLoss } + + +type CoercionWitness { + source: CanonicalGrounding + target: CanonicalGrounding +} + + +type CoercionResult { + witness: CoercionWitness + target: Node + quality: CoercionQuality +} + + +data coercion_fold_stage_locus_port: Symbol = coercion_fold_stage_locus_port +data no_target_candidate: Symbol = no_target_candidate +data ambiguous_target_candidate: Symbol = ambiguous_target_candidate +data structural_mismatch: Symbol = structural_mismatch +data coercion_fold_not_realized: Symbol = coercion_fold_not_realized +data coercion_candidates_not_realized: Symbol = coercion_candidates_not_realized +data coercion_witness_verification_not_realized: Symbol = coercion_witness_verification_not_realized + + +fn coercion_mismatch_reason(kind: CoercionMismatchKind) -> Symbol { + match kind { + NoTargetCandidate => no_target_candidate + AmbiguousTargetCandidate => ambiguous_target_candidate + StructuralMismatch => structural_mismatch + } +} + + +fn coercion_diagnostic(d: CoercionDiagnostic) -> Diagnostic { + Diagnostic { + reason: coercion_mismatch_reason(kind: d.kind), + at: d.at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn coercion_quality_compose(left: CoercionQuality, right: CoercionQuality) -> CoercionQuality { + match left { + Lossy { accepted_loss } => Lossy { accepted_loss: accepted_loss } + Identity => right + Exact => match right { + Lossy { accepted_loss } => Lossy { accepted_loss: accepted_loss } + Identity => Exact + Exact => Exact + } + } +} + + +fn candidates_for_algebra(target_model: Node, algebra_instance: Node) -> Outcome { + Rejected { + diagnostic: Diagnostic { + reason: coercion_candidates_not_realized, + at: PortLocus { port: coercion_fold_stage_locus_port }, + correction: Unavailable { reason: ExternalContractUnknown } + } + } +} + + +fn coercion_fold( + source: CanonicalGrounding, + candidates: CoercionCandidateSet, + policy: CoercionFoldPolicy, +) -> Outcome { + Rejected { + diagnostic: Diagnostic { + reason: coercion_fold_not_realized, + at: PortLocus { port: coercion_fold_stage_locus_port }, + correction: Unavailable { reason: ExternalContractUnknown } + } + } +} + + +fn verify_coercion_witness(witness: CoercionWitness) -> Outcome { + Rejected { + diagnostic: Diagnostic { + reason: coercion_witness_verification_not_realized, + at: PortLocus { port: coercion_fold_stage_locus_port }, + correction: Unavailable { reason: ExternalContractUnknown } + } + } +} diff --git a/src/v4/std/constraints.dag b/src/v4/std/constraints.dag new file mode 100644 index 00000000000..2fa62fc8608 --- /dev/null +++ b/src/v4/std/constraints.dag @@ -0,0 +1,126 @@ +// src/v4/std/constraints.dag +// Scope: constraint-solving substrate boundary for canonical source grounding. +// Owns: ConstraintKind, Constraint, ConstraintSource, ConstraintGraph, ConstraintSolvePolicy, CanonicalGrounding, CanonicalGroundingWitness, ConstraintSolveResult, AmbiguousGroundingDiagnostic, UnsatisfiedConstraintDiagnostic, solve_constraints. +// Consumes: std collection, std diagnostic, std node. +// Status: scaffold — TASKS T-9; exact canonical-grounding boundary only. +// Anchor: docs/design-v4-compiler-homomorphism.md P5. + + +module v4.std.constraints + + +import v4.std.collection { List } +import v4.std.diagnostic { + Diagnostic, + ExternalContractUnknown, + Locus, + Outcome, + PortLocus, + Rejected, + Unavailable +} +import v4.std.node { Hash, Node, Symbol } + + +// 🟡 coproduct dissolution — feature:t9-solve-constraints-consumer. +type ConstraintKind + = TypeShapeConstraint + | InhabitanceConstraint + | EqualityConstraint + | DependencyConstraint + + +// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL. +type ConstraintSource + = SourceNode { node: Node } + | SourceEdge { from: Node, to: Node } + | SourceStage { stage: Symbol } + + +type Constraint { + kind: ConstraintKind + source: ConstraintSource + left: Node + right: Node +} + + +type ConstraintGraph { + root: Node + constraints: List +} + + +type ConstraintSolvePolicy + + +type CanonicalGroundingWitness { + source_graph: ConstraintGraph + canonical_hash: Hash +} + + +type CanonicalGrounding { + root: Node + witness: CanonicalGroundingWitness +} + + +type ConstraintSolveResult = Outcome + + +type AmbiguousGroundingDiagnostic { + graph: ConstraintGraph + at: Locus +} + + +type UnsatisfiedConstraintDiagnostic { + constraint: Constraint + at: Locus +} + + +data constraint_solve_stage_locus_port: Symbol = constraint_solve_stage_locus_port +data ambiguous_grounding: Symbol = ambiguous_grounding +data unsatisfied_constraint: Symbol = unsatisfied_constraint +data constraint_solver_not_realized: Symbol = constraint_solver_not_realized + + +fn ambiguous_grounding_diagnostic(d: AmbiguousGroundingDiagnostic) -> Diagnostic { + Diagnostic { + reason: ambiguous_grounding, + at: d.at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn unsatisfied_constraint_diagnostic(d: UnsatisfiedConstraintDiagnostic) -> Diagnostic { + Diagnostic { + reason: unsatisfied_constraint, + at: d.at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn constraint_solver_not_realized_diagnostic(at: Locus) -> Diagnostic { + Diagnostic { + reason: constraint_solver_not_realized, + at: at, + correction: Unavailable { reason: ExternalContractUnknown } + } +} + + +fn solve_constraints( + graph: ConstraintGraph, + policy: ConstraintSolvePolicy, +) -> ConstraintSolveResult { + Rejected { + diagnostic: constraint_solver_not_realized_diagnostic( + at: PortLocus { port: constraint_solve_stage_locus_port } + ) + } +}