Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
158 changes: 158 additions & 0 deletions src/v4/std/coercion.dag
Original file line number Diff line number Diff line change
@@ -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<CoercionCandidate>
}


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

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: CoercionResult.target can disagree with witness.target.root, allowing the result to expose a target Node not tied to the verified target grounding (INVARIANTS P2).

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 }

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Composing Lossy with any later Lossy returns only the left AcceptedLoss, so accepted-loss evidence from the right branch is silently dropped across the T-9 quality boundary (INVARIANTS P2 facts-flow-forward).

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<CoercionCandidateSet> {
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<CoercionResult> {
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<CoercionWitness> {
Rejected {
diagnostic: Diagnostic {
reason: coercion_witness_verification_not_realized,
at: PortLocus { port: coercion_fold_stage_locus_port },
correction: Unavailable { reason: ExternalContractUnknown }
}
}
}
126 changes: 126 additions & 0 deletions src/v4/std/constraints.dag
Original file line number Diff line number Diff line change
@@ -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<Constraint>
}


type ConstraintSolvePolicy


type CanonicalGroundingWitness {
source_graph: ConstraintGraph
canonical_hash: Hash
}


type CanonicalGrounding {
root: Node

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: CanonicalGrounding.root can disagree with witness.source_graph.root, so the canonical grounding boundary has two authorities for the grounded Node (INVARIANTS P2).

witness: CanonicalGroundingWitness
}


type ConstraintSolveResult = Outcome<CanonicalGrounding>


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 }
)
}
}
Loading