Repository navigation
feat: cast validation → infer phase, shared for_each handler #365
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from 5 commits
a2c509f
09eaf7a
3f41fd9
23992f4
b8f6210
212720d
5520555
f060173
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -21,6 +21,7 @@ | |
| module v2.compiler.infer | ||
|
|
||
| import std.types { SourceSpan, container_param_name } | ||
| import std.coercion { dag_can_cast, is_numeric_cast_type } | ||
| import v2.std.core { | ||
| Node, | ||
| authored_name_at, NewlineIndex, has_child_named, | ||
|
|
@@ -593,6 +594,25 @@ fn categorized_error(message: String, span: SourceSpan, module_name: String, cat | |
| make_error_node(diagnostic: InternalError { message: message, span: span }, module_name: module_name) | ||
| } | ||
|
|
||
| // Validate a cast at the .dag level. Returns a diagnostic if the cast | ||
| // is invalid between numeric kernel types, or none if the cast is allowed. | ||
| fn validate_cast(source_inferred: InferredNode?, target_name: String, span: SourceSpan, source_index: NewlineIndex?, module_name: String) -> ErrorNode? { | ||
| match source_inferred { | ||
| Some { value: Resolved { node: src_node } } => | ||
| let source_name = authored_name_at(source_index: source_index, node: src_node) | ||
| if source_name == target_name { none } | ||
| else if !is_numeric_cast_type(name: source_name) { none } | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Invariant violation: |
||
| else if !is_numeric_cast_type(name: target_name) { none } | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
The new cast validator returns Useful? React with 👍 / 👎. |
||
| else if dag_can_cast(source_type: source_name, target_type: target_name) { none } | ||
| else { | ||
| let msg = concat("invalid cast: ", source_name, " as ", target_name) | ||
| let diag = InternalError { message: msg, span: span } | ||
| Some { value: make_error_node(diagnostic: diag, module_name: module_name) } | ||
| } | ||
| _ => none | ||
| } | ||
| } | ||
|
|
||
| fn type_variable_node(id: String) -> Node { | ||
| Node { name: "", span: make_span(start: 0, end: 0), ident_span: none, children: [], connective: NoConnective, params: [], inferred: Some { value: TypeVariable { id: id } }, return_cardinality: Required, uses: [], body: none, transport: none, properties: [], type_annotation: none, is_self_recursive: false, has_non_tail_self_call: false, match_pattern: none, expr_data: NoExprData } | ||
| } | ||
|
|
@@ -1873,10 +1893,20 @@ fn infer_expr(texpr: Node, scope: InferScope, expected: Node?) -> InferResult { | |
| let inner_result = infer_expr(texpr: cast_inner, scope: scope, expected: none) | ||
| let inner_typed = inner_result.typed | ||
| let inner_diags = inner_result.diagnostics | ||
| // Validate cast at .dag level: only check when both types are in the | ||
| // numeric cast domain (Int, Float, Bool). Alias casts and user types | ||
| // are allowed unconditionally — they resolve to identity at emit time. | ||
| let si = scope.type_env.source_index | ||
| let target_name = authored_name_at(source_index: si, node: target_type) | ||
| let cast_diag = validate_cast(source_inferred: inner_typed.inferred, target_name: target_name, span: span, source_index: si, module_name: scope.module_name) | ||
| let cast_diags = match cast_diag { | ||
| Some { value: d } => [d] | ||
| None => [] | ||
| } | ||
| let cast_texpr = make_expr_node(expr_data: ExprCast, children: [inner_typed, target_type], inferred: Some { value: Resolved { node: target_type } }, span: span) | ||
| InferResult { | ||
| typed: cast_texpr, | ||
| diagnostics: inner_diags | ||
| diagnostics: concat(inner_diags, cast_diags) | ||
| } | ||
|
|
||
| ExprForEach => | ||
|
|
||
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -60,7 +60,7 @@ import v2.std.core { | |
| import v2.compiler.infer_env { TypeEnv, TypeBinding } | ||
| import std.induction { InductiveField } | ||
| // NamingCase, PascalCase, SnakeCase imported via v2.compiler.languages (bootstrap-local mirror) | ||
| import v2.compiler.infer_types { resolved_type, child_type_node, emit_map_has, node_is_collection, node_is_keyed_collection, node_is_element_collection, normalize_access_type_node } | ||
| import v2.compiler.infer_types { resolved_type, child_type_node, emit_map_has, node_is_collection, node_is_keyed_collection, node_is_element_collection, normalize_access_type_node, for_each_element_type_node } | ||
| import std.types { is_container_type, container_to_algebra_name } | ||
| import v2.compiler.coercion { coerce_primitive_type, coerce_container_template, target_optional_template, target_callable, can_cast, render_cast, literal_suffix } | ||
| import v2.compiler.infer_sigs { ResolvedFuncSig, ResolvedFuncEnv } | ||
|
|
@@ -1878,17 +1878,13 @@ fn extract_string_interp_parts(expr: Node) -> List<StringPart> { | |
| } | ||
|
|
||
| // Shared ExprCast — data-driven, target-parameterized. | ||
| // Cast syntax and validity derive from CastSyntax in extdeps/languages/*/types.dag. | ||
| // Rust: `expr as type` (valid for numeric targets only, per Rust Reference §8.2.4). | ||
| // Python/Go: `type(expr)` (constructor call, always valid). | ||
| // Shared ExprCast — data-driven, target-parameterized. | ||
| // Cast syntax and validity derive from CastRule in extdeps/languages/*/types.dag. | ||
| // Cast syntax derives from CastSyntax in extdeps/languages/*/types.dag. | ||
| // Rust: `expr as type`, Python/Go: `type(expr)`. | ||
| // | ||
| // KNOWN VIOLATION (tracked): cast legality is checked here in emit, but the | ||
| // "emission is translation" invariant says emit should only render pre-validated | ||
| // constructs. The fix: .dag defines its own cast rules, infer validates against | ||
| // them, and emit renders unconditionally. Blocked on: .dag-level cast rule | ||
| // definitions (not yet modeled) and infer-phase cast validation. | ||
| // Numeric casts are validated early in infer (dag_can_cast). Emit retains | ||
| // the per-target can_cast guard as a fail-closed safety net for casts | ||
| // outside the numeric domain (String, user types, etc.) until structural | ||
| // cast modeling replaces the string-keyed tables. | ||
| fn emit_typed_cast_shared(expr: Node, cast_target_node: Node, target: RenderTarget, recurse: fn(Node) -> String, source_index: NewlineIndex?) -> String { | ||
| let expr_str = recurse(expr) | ||
| let ty_str = emit_node_type(n: cast_target_node, target: target, source_index: source_index) | ||
|
|
@@ -1902,12 +1898,31 @@ fn emit_typed_cast_shared(expr: Node, cast_target_node: Node, target: RenderTarg | |
| } else if can_cast(target: target, source_type: src_ty, target_type: ty_str) { | ||
| render_cast(expr_str: expr_str, type_str: ty_str, target: target) | ||
| } else { | ||
| // Unreachable in normal operation: all .dag casts are numeric and every | ||
| // target declares numeric cast rules. If reached, a CastRule is missing. | ||
| emit_error_expr(message: concat("unsupported cast from ", src_ty, " to ", ty_str), target: target) | ||
| } | ||
| } | ||
|
|
||
| // Shared ExprForEach — reads ForEachSyntax + BlockSyntax, no target branching. | ||
| // ForEachSyntax.prefix/separator declare the loop header; BlockSyntax declares | ||
| // block delimiters. Emit translates, does not decide. | ||
| fn emit_typed_for_each_shared(variable: String, collection: Node, body: Node, target: RenderTarget, depth: Int, source_index: NewlineIndex?, recurse: fn(Node, InferScope, Int) -> String, scope: InferScope) -> String { | ||
| let coll_str = recurse(collection, scope, depth) | ||
| let elem_type = for_each_element_type_node(n: resolved_type(n: collection)) | ||
|
Contributor
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Invariant violation: emit_typed_for_each_shared recomputes the loop binder type with resolved_type and for_each_element_type_node, so emit is still making a semantic binding decision instead of translating an infer-produced fact, violating Emission is translation, not decision-making. |
||
| let body_scope = extend_scope(scope: scope, name: variable, resolved: elem_type) | ||
| let body_str = recurse(body, body_scope, depth + 1) | ||
This comment was marked as resolved.
Sorry, something went wrong. |
||
| let var_str = emit_ident(name: variable, target: target) | ||
| let spec = language_spec(target: target) | ||
| let fes = spec.for_each_syntax | ||
| let bs = spec.block_syntax | ||
| let body_indent = make_indent(level: depth + 1) | ||
| if bs.significant_whitespace { | ||
| concat(fes.prefix, var_str, fes.separator, coll_str, bs.block_open, body_indent, body_str) | ||
| } else { | ||
| let close_indent = make_indent(level: depth) | ||
| concat(fes.prefix, var_str, fes.separator, coll_str, bs.block_open, body_indent, body_str, "\n", close_indent, bs.block_close) | ||
| } | ||
| } | ||
|
|
||
| // Shared ExprIndex — dispatches on string/map/list via LanguageSpec.indexing. | ||
| fn emit_typed_index_shared(base: Node, index: Node, target: RenderTarget, recurse: fn(Node) -> String, source_index: NewlineIndex?) -> String { | ||
| let spec = language_spec(target: target) | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Invariant violation:
dag_cast_rulesmakes.dagcast semantics depend on string type names instd/, which is the same identity-proxy pattern M4/M8 are trying to delete rather than a structural cast model.