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
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ data algebra_structure_has_two_representations_with_no_declared_mapping: Recurri
"INVALID STATE: one algebraic structure is represented twice with no declared mapping between the representations (a DESIGN section 3 fork). HOME 1, std.algebra RECORD TYPES: `type OrderedRing<T> { add, sub, zero, negate, mul, .. compare, eq, lt .. }`, `BooleanAlgebra<T> { meet, join, complement, top, bottom }`, inhabited by std VALUES (v2.std.integer int_ordered_ring: OrderedRing<Int>, v2.std.logic bool_boolean_algebra: BooleanAlgebra<Bool>), which the language models' grounding rows cite (v2.extdeps.languages.cpp cpp_bool_grounding and its siblings). HOME 2, v2.std.algebra_structure_signature SIGNATURE NODES: ring_type_node, ordered_ring_type_node, lattice_type_node, boolean_algebra_type_node, whose operations are binder edges named ^ring_field_add, ^lattice_field_join, .. and which every language model's AlgebraInhabitanceDecl inhabits (v2.extdeps.languages.rust rust_integer_algebra_inhabitance, swift, java, lean). The OPERATOR vocabulary is home 2 (v2.std.compilers.target_model canonical_operation_op_add = AlgebraPrimitive { algebra_field: ^ring_field_add }), so a consumer that holds a home-1 instance cannot ask whether it carries an operator's field: nothing maps ^ring_field_add to OrderedRing.add.",
"HARM: every consumer bridging the two invents its own mapping, a second authority each time, or picks one home and ignores facts stated in the other. Found while making v2 infer derive `||` through one algebra-operator route (N7-1): the instance facts for Int and Bool lived in home 1 and the operator fields in home 2, so the dag language model states its primitives in home 2 with a WITNESS citing the home-1 value (v2.extdeps.languages.dag dag_algebra_inhabitance_decls) rather than restating the fact; that keeps one statement of the inhabitance but does not join the structures. RUNG FOUND AT: mitigatable (no wrong answer is produced; consumers refuse or are absent). CEILING: structurally impossible -- one structure model. NEXT-RUNG TRIGGER, NAMING THE CAPABILITY: one structure model consumed by both the language models and std.algebra -- each structure declared once, its operations named once, and the record form (if kept) derived from the signature or vice versa -- SUFFICIENT FOR an instance stated in either place to answer an operator-field query with no consumer-local mapping.",
"RECEIPT, XL-2 step 1 (collection concat), a DISPOSITION OF THE THIRD HOME, not a third coexisting one. The std.algebra template tables (free_monoid_collection_templates and siblings, AlgebraFieldTemplate rows) were a third representation of the collection operations. RULED SPLIT (calm-boar-904, msg_8e2338e7 and msg_702ad2cc): signature-world AlgebraInhabitanceDecl rows type OPERATORS only (v2.compiler.infer's binary-algebra arm, gunbc#13060); the std.algebra collection roster row is the SINGLE typing authority for collection operations (map, all, fold, concat), bound through v2.compiler.fold_lowering's ONE roster binder (collection_roster_rows) and typed from the row (collection_roster_signature_arrow), and nothing else reads the template tables a second time. That REVERSES the earlier joint ruling that a bare concat reaches its field only through an imported declaration and that infer never reads the template tables. REASON: the only writable declaration, a .dag body for std.algebra list_append, regresses every caller from the persistent carrier's log(n + m) to O(|left|) and makes v2.std.node's subtree-accumulating fold quadratic, and an operator-backed fn body has no writable surface (O5). CONSEQUENCE: the ^free_monoid_field_concat structure node and a FreeMonoid AlgebraInhabitanceDecl row were NOT built; nothing would consume them (DESIGN section 3c). The signature-world free-monoid node stays unbuilt until an operator names a free-monoid field.",
"RECEIPT, XL-2 kernel-String concat: the signature-world FREE-MONOID STRUCTURE is now BUILT, because it gained a consumer. v2.std.algebra_structure_signature free_monoid_structure_type_node bounds the collection roster's concat carrier through BinderStructureEdge. Infer admits the carrier only through dag_free_monoid_free_monoid_inhabitance (list_append) and dag_host_text_free_monoid_inhabitance (host_text_concatenation). Kernel host text inhabits with generator std.types Char (Ruling 3: inhabitance, not identity with FreeMonoid<Char>).",
],
evidence: [
DeclarationRef { module_path: "v2.std.algebra_structure_signature", decl_name: "ordered_ring_type_node", field: WholeDeclaration },
Expand All @@ -18,5 +19,7 @@ data algebra_structure_has_two_representations_with_no_declared_mapping: Recurri
DeclarationRef { module_path: "v2.extdeps.languages.dag", decl_name: "dag_algebra_inhabitance_decls", field: WholeDeclaration },
DeclarationRef { module_path: "v2.compiler.fold_lowering", decl_name: "collection_roster_signature_arrow", field: WholeDeclaration },
DeclarationRef { module_path: "std.algebra", decl_name: "collection_concat_shape", field: WholeDeclaration },
DeclarationRef { module_path: "v2.std.algebra_structure_signature", decl_name: "free_monoid_structure_type_node", field: WholeDeclaration },
DeclarationRef { module_path: "v2.compiler.infer", decl_name: "infer_application_structure_bounds", field: WholeDeclaration },
],
}
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ data string_interpolation_read_as_literal_text_by_v2: RecurringFailureMode = Rec

"ATTAINABLE CEILING: structurally guaranteed. Interpolation is decidable at lexing: the v2 string rule either lowers an interpolating literal to its parts (text segments and references the resolver sees) or refuses it, located, until it does. NEXT-RUNG TRIGGER: the v2 dag language model gains an interpolation arm in dag_string_body_element_pattern, plus a lowering of the parts. Discriminating red: a literal `\"\{x}\"` with x unbound refuses at resolution. Positive control: `\"\{x}\"` with x bound lowers to a reference to x, and the same literal with its brace escaped (backslash, brace) stays literal text. XL-2 PR3b (realization lowering) depends on it: until it lands, 3b refuses each interpolating transport string, located, rather than lowering its braces as text.",

"CLIMBED (XL-2 PR2b, sleek-stag-53): the v2 dag lexer now splits a string at every hole opener v1 opens (v1.compiler.tokenize should_start_interpolation), DISJOINTLY BY INPUT: v2.extdeps.languages.dag dag_string_body_element_pattern admits no hole opener, so dag_token_string_literal ends at its quote and dag_token_string_template_head at the opener, and the hole's ordinary tokens lex in a pushed mode. The grammar reads one ^dag_string_template node (dag_grammar_string_template_expr) whose holes are dag_production_expr; its one reader is string_template_parts_optional, and v2.compiler.body_lowering_fold body_lower_string_template rewrites it to a concat chain, so no template survives normalize and a hole is a reference the resolver sees. A hole whose value is not text refuses at the concat argument: there is no implicit to_string. Evidence: v2.test.claim.body_lowering.string_template (the real-route claim and the lexer controls) and the escaped-brace control, a hole-free literal lexing as one plain literal. RUNG NOW: structurally guaranteed -- every string with a hole opener is a template in both compilers.",
"RECOGNITION RULE: a v2 node's string literal value contains an unescaped `{` followed by an identifier and `}`, in source that v1 also compiles.",
],

Expand Down
39 changes: 38 additions & 1 deletion src/v2/compiler/02_parse.dag
Original file line number Diff line number Diff line change
Expand Up @@ -85,7 +85,9 @@ import v2.std.witness { Holds, Violates, Witness, witness_from_optional }
import v2.extdeps.languages.dag {
dag_float_literal_node_from_lexeme,
dag_int_literal_node_from_lexeme,
dag_string_literal_node_from_lexeme
dag_string_literal_node_from_lexeme,
dag_string_template_part_class,
dag_string_template_part_node_from_lexeme
}
import v2.std.compilers.lexing {
LineBreakAnswer,
Expand Down Expand Up @@ -3779,6 +3781,39 @@ fn parse_expr_string_literal_value(
}
}

fn parse_expr_string_template_part_value(
tok: Token,
remaining: List<Token>,
table: ParseTable,
prov: ParseProvenanceState
) -> ParseExprResult {
let minted = parse_mint_from_source(
prov: prov,
file: tok.file,
start: tok.start,
end: tok.end
)
match dag_string_template_part_node_from_lexeme(
token_class: tok.class,
lexeme: tok.lexeme,
occurrence_id: node_occurrence_identity_minted(id: minted.id)
) {
Accepted { value: captured, diagnostics: _ } =>
ParseExprAccepted {
remaining: remaining,
captured: captured,
diagnostics: std.algebra.Empty,
prov: minted.prov,
table: table
}
Rejected { diagnostics: d } =>
ParseExprRejected {
diagnostics: parse_non_empty_diagnostics_to_list(ned: d),
table: table
}
}
}

// THE INT-LITERAL WRAP IN THIS FUNCTION IS LOAD-BEARING. minted.id is a raw OccurrenceId;
// Node.occurrence_id is the NodeOccurrenceIdentity coproduct, so the mint has to be lifted into
// OccurrenceMinted before it can inhabit a Node. #8833 removed that lift, reading it as a spurious
Expand Down Expand Up @@ -3830,6 +3865,8 @@ fn parse_expr_terminal(
}
} else if token_class == ^dag_token_string_literal {
parse_expr_string_literal_value(tok: tok, remaining: remaining, table: table, prov: prov)
} else if dag_string_template_part_class(token_class: token_class) {
parse_expr_string_template_part_value(tok: tok, remaining: remaining, table: table, prov: prov)
} else if token_class == ^dag_token_float_literal {
let minted = parse_mint_from_source(
prov: prov,
Expand Down
8 changes: 6 additions & 2 deletions src/v2/compiler/03_resolve.dag
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ import v2.std.diagnostic {
outcome_with_diagnostics
}
import v2.compiler.primitive_authority { primitive_authority_path, primitive_authority_row_names_head }
import v2.compiler.fold_lowering { FoldRealization, FoldRealizesDeclaration, FoldRealizesRosterOperation, collection_roster_primitive_call_row_optional, fold_family_realization }
import v2.compiler.fold_lowering { FoldRealization, FoldRealizesDeclaration, FoldRealizesRosterOperation, collection_roster_primitive_call_row_by_declaration_optional, collection_roster_primitive_call_row_optional, fold_family_realization }
import v2.std.qualified_name {
QualifiedName,
qualified_name_from_dotted_string,
Expand Down Expand Up @@ -2294,7 +2294,11 @@ fn resolve_atom_unscoped(ctx: ResolveContext, n: Node, identity: Symbol, pending
Absent =>
match collection_roster_primitive_call_row_optional(head: identity) {
Present { value: r } => resolve_atom_bound(ctx: ctx, n: n, path: declaration_ref_path(r: r.row), pending: pending)
Absent => resolve_atom_primitive_authority(ctx: ctx, n: n, identity: identity, pending: pending)
Absent =>
match collection_roster_primitive_call_row_by_declaration_optional(decl_name: identity) {
Present { value: r } => resolve_atom_bound(ctx: ctx, n: n, path: declaration_ref_path(r: r.row), pending: pending)
Absent => resolve_atom_primitive_authority(ctx: ctx, n: n, identity: identity, pending: pending)
}
}
}
}
Expand Down
Loading