From 86d81407308916b706495b0aeeca80be98d50c80 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:35:25 +0000 Subject: [PATCH 01/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/grammar.dag | 279 +++++++++++++++++++++++++++++++++++++++++ src/v4/std/lexing.dag | 90 +++++++++++++ 2 files changed, 369 insertions(+) create mode 100644 src/v4/std/grammar.dag create mode 100644 src/v4/std/lexing.dag diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag new file mode 100644 index 00000000000..3d7a73938ae --- /dev/null +++ b/src/v4/std/grammar.dag @@ -0,0 +1,279 @@ +// src/v4/std/grammar.dag +// Scope: canonical grammar model shared by compiler stages and target-language specs. +// Anchor: THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-7. +// Status: T-7 grammar data carriers; parser implementation remains in v4.compiler.parse. + +module v4.std.grammar + +import v4.std.algebra { Empty, fold_list, list_snoc_item } +import v4.std.collection { List, Set } +import v4.std.lexing { LexRules } +import v4.std.logic { Bool } +import v4.std.node { Atom, Conj, Edge, Named, Node, NodeFold, Symbol, TypeNode, fold_node } + +// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: GrammarExpr converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. +type GrammarExpr + = Terminal { token_class: Symbol } + | Nonterminal { production: Symbol } + | Sequence { left: GrammarExpr, right: GrammarExpr } + | Choice { left: GrammarExpr, right: GrammarExpr } + | Optional { element: GrammarExpr } + | Repeat { element: GrammarExpr } + + +type GrammarProduction { + name: Symbol + expression: GrammarExpr + emitted: Node +} + + +// 🟑 gated β€” feature: T-8 parse error-recovery trigger β€” sync_tokens present; parse_skip_to_sync +// is structurally correct but unreachable until parse_expr emits non-empty diagnostics on +// committed Terminal mismatches. Dissolve-on: T-8. +type GrammarRoot { + start: Symbol + productions: List + sync_tokens: Set +} + + +// Parse-table entrypoint carrier: produced only after undefined/duplicate/left-recursion gates pass. +type ValidatedGrammarRoot { + root: GrammarRoot +} + + +// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: Grammar converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. +type Grammar + = VoidGrammar + | ModeledGrammar { root: GrammarRoot } + + +type GrammarSchema { + lex: LexRules + grammar: Grammar +} + + +type GrammarSymbolFoldState { + found: Bool +} + + +data grammar_terminal_token_class_node_projection: Symbol = grammar_terminal_token_class_node_projection +data grammar_nonterminal_production_node_projection: Symbol = grammar_nonterminal_production_node_projection +data grammar_sequence_left_node_projection: Symbol = grammar_sequence_left_node_projection +data grammar_sequence_right_node_projection: Symbol = grammar_sequence_right_node_projection +data grammar_choice_left_node_projection: Symbol = grammar_choice_left_node_projection +data grammar_choice_right_node_projection: Symbol = grammar_choice_right_node_projection +data grammar_optional_element_node_projection: Symbol = grammar_optional_element_node_projection +data grammar_repeat_element_node_projection: Symbol = grammar_repeat_element_node_projection +data grammar_production_name_node_projection: Symbol = grammar_production_name_node_projection +data grammar_production_expression_node_projection: Symbol = grammar_production_expression_node_projection +data grammar_production_emitted_node_projection: Symbol = grammar_production_emitted_node_projection +data grammar_root_start_production_node_projection: Symbol = grammar_root_start_production_node_projection +data grammar_root_productions_node_projection: Symbol = grammar_root_productions_node_projection +data grammar_root_sync_tokens_node_projection: Symbol = grammar_root_sync_tokens_node_projection + + +fn grammar_atom(identity: Symbol) -> Node { + Node { + kind: TypeNode { + connective: Atom { identity: identity } + }, + children: [] + } +} + + +fn grammar_named_edge(name: Symbol, target: Node) -> Edge { + Edge { + label: Named { name: name }, + target: target + } +} + + +fn grammar_empty_sync_tokens() -> Set { + Set { member: fn(_) { false } } +} + + +fn grammar_empty_node() -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: [] + } +} + + +fn grammar_expr_to_node(expr: GrammarExpr) -> Node { + match expr { + Terminal { token_class: token_class } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_terminal_token_class_node_projection, target: grammar_atom(identity: token_class)) + ] + } + Nonterminal { production: production } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_nonterminal_production_node_projection, target: grammar_atom(identity: production)) + ] + } + Sequence { left: left, right: right } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_sequence_left_node_projection, target: grammar_expr_to_node(expr: left)), + grammar_named_edge(name: grammar_sequence_right_node_projection, target: grammar_expr_to_node(expr: right)) + ] + } + Choice { left: left, right: right } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_choice_left_node_projection, target: grammar_expr_to_node(expr: left)), + grammar_named_edge(name: grammar_choice_right_node_projection, target: grammar_expr_to_node(expr: right)) + ] + } + Optional { element: element } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_optional_element_node_projection, target: grammar_expr_to_node(expr: element)) + ] + } + Repeat { element: element } => + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_repeat_element_node_projection, target: grammar_expr_to_node(expr: element)) + ] + } + } +} + + +fn grammar_production_to_node(production: GrammarProduction) -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_production_name_node_projection, target: grammar_atom(identity: production.name)), + grammar_named_edge(name: grammar_production_expression_node_projection, target: grammar_expr_to_node(expr: production.expression)), + grammar_named_edge(name: grammar_production_emitted_node_projection, target: production.emitted) + ] + } +} + + +fn grammar_production_to_list_step(acc: List, production: GrammarProduction) -> List { + list_snoc_item( + xs: acc, + item: grammar_named_edge( + name: production.name, + target: grammar_production_to_node(production: production) + ) + ) +} + + +fn grammar_productions_to_node(productions: List) -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: fold_list( + xs: productions, + empty: Empty, + cons: fn(acc, production) { + grammar_production_to_list_step(acc: acc, production: production) + } + ) + } +} + + +// 🟑 gated T-8 β€” P2-boundary interim β€” feature: grammar-root-node-projection-completeness β€” +// bind TASKS.md T-8 β€” GrammarRoot.sync_tokens: Set is a predicate closure +// { member: fn(Symbol) -> Bool }; the Node substrate has no edge kind for function values, so +// sync_tokens cannot be materialized as a Node child here. grammar_root_sync_tokens_node_projection +// names the intended edge. Dissolve-on: T-8, when Set is reified as an explicit membership +// list type (or substrate gains literal-value edge support), enabling the edge to be emitted. +fn grammar_root_to_node(root: GrammarRoot) -> Node { + Node { + kind: TypeNode { + connective: Conj + }, + children: [ + grammar_named_edge(name: grammar_root_start_production_node_projection, target: grammar_atom(identity: root.start)), + grammar_named_edge(name: grammar_root_productions_node_projection, target: grammar_productions_to_node(productions: root.productions)) + ] + } +} + + +fn grammar_to_node(grammar: Grammar) -> Node { + match grammar { + VoidGrammar => grammar_empty_node() + ModeledGrammar { root: root } => grammar_root_to_node(root: root) + } +} + + +fn grammar_symbol_fold(sym: Symbol) -> NodeFold { + NodeFold { + init: fn(n0) { + grammar_symbol_fold_init(n: n0, sym: sym) + }, + step: grammar_symbol_fold_step + } +} + + +fn grammar_symbol_fold_init(n: Node, sym: Symbol) -> GrammarSymbolFoldState { + match n.kind { + TypeNode { connective: Atom { identity: id } } => + GrammarSymbolFoldState { found: id == sym } + _ => + GrammarSymbolFoldState { found: false } + } +} + + +fn grammar_symbol_fold_step( + acc: GrammarSymbolFoldState, + edge: Edge, + child_has_symbol: GrammarSymbolFoldState +) -> GrammarSymbolFoldState { + GrammarSymbolFoldState { found: acc.found || child_has_symbol.found } +} + + +fn grammar_symbol_fold_state(n: Node, sym: Symbol) -> GrammarSymbolFoldState { + fold_node(n: n, algebra: grammar_symbol_fold(sym: sym)) +} + + +fn grammar_carries_symbol(grammar: Grammar, sym: Symbol) -> Bool { + grammar_symbol_fold_state(n: grammar_to_node(grammar: grammar), sym: sym).found +} diff --git a/src/v4/std/lexing.dag b/src/v4/std/lexing.dag new file mode 100644 index 00000000000..37c95ae8c24 --- /dev/null +++ b/src/v4/std/lexing.dag @@ -0,0 +1,90 @@ +// src/v4/std/lexing.dag +// Scope: canonical lexical model shared by compiler stages and target-language specs. +// Anchor: THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-6. +// Status: T-6 lexical data carriers; lexer implementation remains in v4.compiler.tokenize. + +module v4.std.lexing + +import v4.std.algebra { fold_list } +import v4.std.collection { List } +import v4.std.logic { Bool } +import v4.std.node { Symbol } +import v4.std.text { Char, String } + +// 🟑 coproduct dissolution β€” CP-1b item 13a; lexical data is modeled, per-arm lexer morphism witness remains gated. +type LexCharClass + = WhitespaceChar + | DigitChar + | HexDigitChar + | IdentStartChar + | IdentContinueChar + | StringTextChar + | LineCommentTextChar + | BlockCommentTextChar + + +// 🟑 coproduct dissolution β€” CP-1b item 13b; declarative parse/emit pattern data is modeled, bidirectional grammar carrier convergence remains gated. +type LexPattern + = EmptyPattern + | LiteralPattern { text: String } + | KeywordPattern { text: String } + | CharPattern { char: Char } + | CharClassPattern { class: LexCharClass } + | SequencePattern { left: LexPattern, right: LexPattern } + | ChoicePattern { left: LexPattern, right: LexPattern } + | OptionalPattern { element: LexPattern } + | RepeatPattern { element: LexPattern } + | OneOrMorePattern { element: LexPattern } + | DelimitedPattern { open: LexPattern, body: LexPattern, close: LexPattern } + + +// 🟑 coproduct dissolution β€” CP-1b item 13c; token/trivia rule data is modeled, per-arm lexer morphism witness remains gated. +type LexRule + = TokenRule { token_class: Symbol, pattern: LexPattern } + | TriviaRule { pattern: LexPattern } + + +// Maximal munch: compiler tokenization selects the accepting rule with the longest lexeme; +// equal-length ties prefer the later rule (specific literals/keywords after ident). +type LexRuleSet { + rules: List +} + + +// 🟑 coproduct dissolution β€” CP-1b item 13d; modeled rule data is present, generic lexical walk realized. +type LexRules + = VoidLexRules + | ModeledLexRules { root: LexRuleSet } + + +type Token { + class: Symbol + lexeme: String + file: Symbol + start: Int + end: Int +} + + +type TokenStream { + tokens: List +} + + +fn lex_rule_token_class_member(rule: LexRule, token_class: Symbol) -> Bool { + match rule { + TokenRule { token_class: c, pattern: _ } => c == token_class + TriviaRule { pattern: _ } => false + } +} + + +fn lex_rule_set_token_class_member(rules: LexRuleSet, token_class: Symbol) -> Bool { + fold_list( + xs: rules.rules, + empty: false, + cons: fn(acc, rule) { + acc || lex_rule_token_class_member(rule: rule, token_class: token_class) + } + ) +} From 149b50b7c807d9e70449f1e177f5120be3149618 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:37:03 +0000 Subject: [PATCH 02/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/01_tokenize.dag | 106 ++----- src/v4/compiler/02_parse.dag | 283 ++---------------- src/v4/compiler/03_normalize.dag | 2 +- src/v4/compiler/06_translate.dag | 2 +- src/v4/compiler/07_target_carriers.dag | 2 +- src/v4/extdeps/formats/sql.dag | 2 +- src/v4/extdeps/languages/cpp.dag | 4 +- src/v4/extdeps/languages/dag.dag | 4 +- src/v4/extdeps/languages/go.dag | 4 +- src/v4/extdeps/languages/java.dag | 4 +- src/v4/extdeps/languages/kotlin.dag | 4 +- src/v4/extdeps/languages/python.dag | 4 +- src/v4/extdeps/languages/rust.dag | 4 +- src/v4/extdeps/languages/swift.dag | 4 +- src/v4/extdeps/languages/typescript.dag | 4 +- src/v4/extdeps/languages/wasm.dag | 4 +- .../claim/manual/dag_ingest_round_trip.dag | 2 +- .../manual/infer_emit_compile_anchor.dag | 2 +- .../manual/java_wave2_grammar_structure.dag | 4 +- .../validate_then_compile_public_terminal.dag | 2 +- 20 files changed, 78 insertions(+), 369 deletions(-) diff --git a/src/v4/compiler/01_tokenize.dag b/src/v4/compiler/01_tokenize.dag index 1013f975069..99ecf90fec3 100644 --- a/src/v4/compiler/01_tokenize.dag +++ b/src/v4/compiler/01_tokenize.dag @@ -16,62 +16,37 @@ import v4.std.algebra { Cons, Empty, ListTailResult, TailAbsent, TailFound, fold import v4.std.text { Char, CharAbsent, CharFound, String, string_head, string_is_empty, string_tail } import v4.std.nat { Nat, nat_lte, nat_gte } import v4.std.logic { Bool } - -// 🟑 coproduct dissolution β€” CP-1b item 13a; lexical data is modeled, per-arm lexer morphism witness remains gated. -type LexCharClass - = WhitespaceChar - | DigitChar - | HexDigitChar - | IdentStartChar - | IdentContinueChar - | StringTextChar - | LineCommentTextChar - | BlockCommentTextChar - - -// 🟑 coproduct dissolution β€” CP-1b item 13b; declarative parse/emit pattern data is modeled, bidirectional grammar carrier convergence remains gated. -type LexPattern - = EmptyPattern - | LiteralPattern { text: String } - | KeywordPattern { text: String } - | CharPattern { char: Char } - | CharClassPattern { class: LexCharClass } - | SequencePattern { left: LexPattern, right: LexPattern } - | ChoicePattern { left: LexPattern, right: LexPattern } - | OptionalPattern { element: LexPattern } - | RepeatPattern { element: LexPattern } - | OneOrMorePattern { element: LexPattern } - | DelimitedPattern { open: LexPattern, body: LexPattern, close: LexPattern } - - -// 🟑 coproduct dissolution β€” CP-1b item 13c; token/trivia rule data is modeled, per-arm lexer morphism witness remains gated. -type LexRule - = TokenRule { token_class: Symbol, pattern: LexPattern } - | TriviaRule { pattern: LexPattern } - - -// Maximal munch: lex_try_rules selects the accepting rule with the longest lexeme; -// equal-length ties prefer the later rule (specific literals/keywords after ident). -type LexRuleSet { - rules: List -} - - -// 🟑 coproduct dissolution β€” CP-1b item 13d; modeled rule data is present, generic lexical walk realized. -type LexRules - = VoidLexRules - | ModeledLexRules { root: LexRuleSet } - - -type Token { - class: Symbol - lexeme: String - file: Symbol - start: Int - end: Int -} -type TokenStream { - tokens: List +import v4.std.lexing { + BlockCommentTextChar, + CharClassPattern, + CharPattern, + ChoicePattern, + DelimitedPattern, + DigitChar, + EmptyPattern, + HexDigitChar, + IdentContinueChar, + IdentStartChar, + KeywordPattern, + LexCharClass, + LexPattern, + LexRule, + LexRuleSet, + LexRules, + LineCommentTextChar, + LiteralPattern, + ModeledLexRules, + OneOrMorePattern, + OptionalPattern, + RepeatPattern, + SequencePattern, + StringTextChar, + Token, + TokenRule, + TokenStream, + TriviaRule, + VoidLexRules, + WhitespaceChar } // 🟑 coproduct dissolution β€” CP-1b item 13e; per-pattern match result; dissolves when LexPattern converges with GrammarExpr on single bidirectional grammar carrier. @@ -89,25 +64,6 @@ data tokenize_lex_e0_source_not_exhausted: Symbol = tokenize_lex_e0_source_not_e data tokenize_lex_e1_unrecognized_char: Symbol = tokenize_lex_e1_unrecognized_char -fn lex_rule_token_class_member(rule: LexRule, token_class: Symbol) -> Bool { - match rule { - TokenRule { token_class: c, pattern: _ } => c == token_class - TriviaRule { pattern: _ } => false - } -} - - -fn lex_rule_set_token_class_member(rules: LexRuleSet, token_class: Symbol) -> Bool { - fold_list( - xs: rules.rules, - empty: false, - cons: fn(acc, rule) { - acc || lex_rule_token_class_member(rule: rule, token_class: token_class) - } - ) -} - - fn tokenize_lex_e0_source_not_exhausted_diagnostic(at: Locus) -> Diagnostic { Diagnostic { reason: tokenize_lex_e0_source_not_exhausted, diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 338b1a2f71d..0801023a350 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -11,56 +11,29 @@ module v4.compiler.parse -import v4.compiler.tokenize { LexRules, Token, TokenStream } import v4.std.diagnostic { Accepted, Diagnostic, Diagnostics, ExternalContractUnknown, Locus, NonEmptyDiagnostics, None, Outcome, Some, Unavailable, UserInputBoundary, diagnostics_singleton, port_locus } -import v4.std.node { Atom, Conj, Edge, Named, Node, NodeFold, Symbol, TypeNode, fold_node, well_formed } +import v4.std.node { Conj, Edge, Named, Node, Symbol, TypeNode, well_formed } import v4.std.collection { List, Map, Set, empty_map, map_insert } import v4.std.algebra { Cons, Empty, TailAbsent, TailFound, contains, fold_list, fold_list_right, is_empty, length, list_append, list_snoc_item, list_tail } import v4.std.logic { Bool } import v4.std.witness { Holds, Violates, Witness } - - -// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: GrammarExpr converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. -type GrammarExpr - = Terminal { token_class: Symbol } - | Nonterminal { production: Symbol } - | Sequence { left: GrammarExpr, right: GrammarExpr } - | Choice { left: GrammarExpr, right: GrammarExpr } - | Optional { element: GrammarExpr } - | Repeat { element: GrammarExpr } - - -type GrammarProduction { - name: Symbol - expression: GrammarExpr - emitted: Node -} - - -// 🟑 gated β€” feature: T-8 parse error-recovery trigger β€” sync_tokens present; parse_skip_to_sync -// is structurally correct but unreachable until parse_expr emits non-empty diagnostics on -// committed Terminal mismatches. Dissolve-on: T-8. -type GrammarRoot { - start: Symbol - productions: List - sync_tokens: Set -} - -// Parse-table entrypoint carrier: produced only after undefined/duplicate/left-recursion gates pass. -type ValidatedGrammarRoot { - root: GrammarRoot -} - - -// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: Grammar converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. -type Grammar - = VoidGrammar - | ModeledGrammar { root: GrammarRoot } - - -type GrammarSchema { - lex: LexRules - grammar: Grammar +import v4.std.lexing { Token, TokenStream } +import v4.std.grammar { + Choice, + Grammar, + GrammarExpr, + GrammarProduction, + GrammarRoot, + ModeledGrammar, + Nonterminal, + Optional, + Repeat, + Sequence, + Terminal, + ValidatedGrammarRoot, + VoidGrammar, + grammar_named_edge, + grammar_to_node } @@ -105,10 +78,6 @@ type ParsePositionKey { // Memoized (position, production) β†’ parse_expr result for production.expression at that offset. type ParseTable = Map -type GrammarSymbolFoldState { - found: Bool -} - type TokensAtPositionAcc { skipped: Int target: Int @@ -116,20 +85,6 @@ type TokensAtPositionAcc { } -data grammar_terminal_token_class_node_projection: Symbol = grammar_terminal_token_class_node_projection -data grammar_nonterminal_production_node_projection: Symbol = grammar_nonterminal_production_node_projection -data grammar_sequence_left_node_projection: Symbol = grammar_sequence_left_node_projection -data grammar_sequence_right_node_projection: Symbol = grammar_sequence_right_node_projection -data grammar_choice_left_node_projection: Symbol = grammar_choice_left_node_projection -data grammar_choice_right_node_projection: Symbol = grammar_choice_right_node_projection -data grammar_optional_element_node_projection: Symbol = grammar_optional_element_node_projection -data grammar_repeat_element_node_projection: Symbol = grammar_repeat_element_node_projection -data grammar_production_name_node_projection: Symbol = grammar_production_name_node_projection -data grammar_production_expression_node_projection: Symbol = grammar_production_expression_node_projection -data grammar_production_emitted_node_projection: Symbol = grammar_production_emitted_node_projection -data grammar_root_start_production_node_projection: Symbol = grammar_root_start_production_node_projection -data grammar_root_productions_node_projection: Symbol = grammar_root_productions_node_projection -data grammar_root_sync_tokens_node_projection: Symbol = grammar_root_sync_tokens_node_projection data grammar_production_identity_node_projection: Symbol = grammar_production_identity_node_projection data grammar_production_captured_node_projection: Symbol = grammar_production_captured_node_projection @@ -202,208 +157,6 @@ fn parse_e1_syntax_error_diagnostic(at: Locus) -> Diagnostic { } -fn grammar_atom(identity: Symbol) -> Node { - Node { - kind: TypeNode { - connective: Atom { identity: identity } - }, - children: [] - } -} - - -fn grammar_named_edge(name: Symbol, target: Node) -> Edge { - Edge { - label: Named { name: name }, - target: target - } -} - - -fn grammar_empty_sync_tokens() -> Set { - Set { member: fn(_) { false } } -} - - -fn grammar_empty_node() -> Node { - Node { - kind: TypeNode { - connective: Conj - }, - children: [] - } -} - - -fn grammar_expr_to_node(expr: GrammarExpr) -> Node { - match expr { - Terminal { token_class: token_class } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_terminal_token_class_node_projection, target: grammar_atom(identity: token_class)) - ] - } - Nonterminal { production: production } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_nonterminal_production_node_projection, target: grammar_atom(identity: production)) - ] - } - Sequence { left: left, right: right } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_sequence_left_node_projection, target: grammar_expr_to_node(expr: left)), - grammar_named_edge(name: grammar_sequence_right_node_projection, target: grammar_expr_to_node(expr: right)) - ] - } - Choice { left: left, right: right } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_choice_left_node_projection, target: grammar_expr_to_node(expr: left)), - grammar_named_edge(name: grammar_choice_right_node_projection, target: grammar_expr_to_node(expr: right)) - ] - } - Optional { element: element } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_optional_element_node_projection, target: grammar_expr_to_node(expr: element)) - ] - } - Repeat { element: element } => - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_repeat_element_node_projection, target: grammar_expr_to_node(expr: element)) - ] - } - } -} - - -fn grammar_production_to_node(production: GrammarProduction) -> Node { - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_production_name_node_projection, target: grammar_atom(identity: production.name)), - grammar_named_edge(name: grammar_production_expression_node_projection, target: grammar_expr_to_node(expr: production.expression)), - grammar_named_edge(name: grammar_production_emitted_node_projection, target: production.emitted) - ] - } -} - - -fn grammar_production_to_list_step(acc: List, production: GrammarProduction) -> List { - list_snoc_item( - xs: acc, - item: grammar_named_edge( - name: production.name, - target: grammar_production_to_node(production: production) - ) - ) -} - - -fn grammar_productions_to_node(productions: List) -> Node { - Node { - kind: TypeNode { - connective: Conj - }, - children: fold_list( - xs: productions, - empty: Empty, - cons: fn(acc, production) { - grammar_production_to_list_step(acc: acc, production: production) - } - ) - } -} - - -// 🟑 gated T-8 β€” P2-boundary interim β€” feature: grammar-root-node-projection-completeness β€” -// bind TASKS.md T-8 β€” GrammarRoot.sync_tokens: Set is a predicate closure -// { member: fn(Symbol) -> Bool }; the Node substrate has no edge kind for function values, so -// sync_tokens cannot be materialized as a Node child here. grammar_root_sync_tokens_node_projection -// names the intended edge. Dissolve-on: T-8, when Set is reified as an explicit membership -// list type (or substrate gains literal-value edge support), enabling the edge to be emitted. -fn grammar_root_to_node(root: GrammarRoot) -> Node { - Node { - kind: TypeNode { - connective: Conj - }, - children: [ - grammar_named_edge(name: grammar_root_start_production_node_projection, target: grammar_atom(identity: root.start)), - grammar_named_edge(name: grammar_root_productions_node_projection, target: grammar_productions_to_node(productions: root.productions)) - ] - } -} - - -fn grammar_to_node(grammar: Grammar) -> Node { - match grammar { - VoidGrammar => grammar_empty_node() - ModeledGrammar { root: root } => grammar_root_to_node(root: root) - } -} - - -fn grammar_symbol_fold(sym: Symbol) -> NodeFold { - NodeFold { - init: fn(n0) { - grammar_symbol_fold_init(n: n0, sym: sym) - }, - step: grammar_symbol_fold_step - } -} - - -fn grammar_symbol_fold_init(n: Node, sym: Symbol) -> GrammarSymbolFoldState { - match n.kind { - TypeNode { connective: Atom { identity: id } } => - GrammarSymbolFoldState { found: id == sym } - _ => - GrammarSymbolFoldState { found: false } - } -} - - -fn grammar_symbol_fold_step( - acc: GrammarSymbolFoldState, - edge: Edge, - child_has_symbol: GrammarSymbolFoldState -) -> GrammarSymbolFoldState { - GrammarSymbolFoldState { found: acc.found || child_has_symbol.found } -} - - -fn grammar_symbol_fold_state(n: Node, sym: Symbol) -> GrammarSymbolFoldState { - fold_node(n: n, algebra: grammar_symbol_fold(sym: sym)) -} - - -fn grammar_carries_symbol(grammar: Grammar, sym: Symbol) -> Bool { - grammar_symbol_fold_state(n: grammar_to_node(grammar: grammar), sym: sym).found -} - - fn grammar_lookup_production_step( acc: Witness, production: GrammarProduction, diff --git a/src/v4/compiler/03_normalize.dag b/src/v4/compiler/03_normalize.dag index 60875a064ec..1c112668d34 100644 --- a/src/v4/compiler/03_normalize.dag +++ b/src/v4/compiler/03_normalize.dag @@ -8,7 +8,7 @@ module v4.compiler.normalize import v4.std.algebra { list_snoc_item } -import v4.compiler.parse { ParseTree } +import v4.std.grammar { ParseTree } import v4.extdeps.languages.dag { dag_c3_surface_sugar_fn, dag_c3_surface_sugar_operation, diff --git a/src/v4/compiler/06_translate.dag b/src/v4/compiler/06_translate.dag index f113e7c0f81..49a0442524d 100644 --- a/src/v4/compiler/06_translate.dag +++ b/src/v4/compiler/06_translate.dag @@ -52,7 +52,7 @@ import v4.std.node { fold_node, well_formed } -import v4.compiler.tokenize { +import v4.std.lexing { LexRules, LexRule, LexPattern, diff --git a/src/v4/compiler/07_target_carriers.dag b/src/v4/compiler/07_target_carriers.dag index c28cebd83d8..4478e696298 100644 --- a/src/v4/compiler/07_target_carriers.dag +++ b/src/v4/compiler/07_target_carriers.dag @@ -7,7 +7,7 @@ module v4.compiler.target_carriers -import v4.compiler.tokenize { LexRules, VoidLexRules } +import v4.std.lexing { LexRules, VoidLexRules } import v4.std.collection { Map, empty_map } import v4.std.node { Node, Symbol } import v4.std.text { String } diff --git a/src/v4/extdeps/formats/sql.dag b/src/v4/extdeps/formats/sql.dag index 655c212fc0d..456c441ece6 100644 --- a/src/v4/extdeps/formats/sql.dag +++ b/src/v4/extdeps/formats/sql.dag @@ -6,7 +6,7 @@ module v4.extdeps.formats.sql -import v4.compiler.parse { GrammarSchema } +import v4.std.grammar { GrammarSchema } import v4.std.algebra { fold_list, list_append } import v4.std.collection { List, Map, Optional } import v4.std.nat { Nat } diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index 3b48355aaa9..8f6cc8699a5 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -5,14 +5,14 @@ module v4.extdeps.languages.cpp -import v4.compiler.parse { +import v4.std.grammar { GrammarExpr, GrammarProduction, Sequence, Terminal, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { LexRule, LexRuleSet, LexRules, diff --git a/src/v4/extdeps/languages/dag.dag b/src/v4/extdeps/languages/dag.dag index 2c0e47f93b4..d032318e830 100644 --- a/src/v4/extdeps/languages/dag.dag +++ b/src/v4/extdeps/languages/dag.dag @@ -8,7 +8,7 @@ module v4.extdeps.languages.dag import v4.std.collection { List, Set } -import v4.compiler.parse { +import v4.std.grammar { Grammar, GrammarExpr, GrammarProduction, @@ -23,7 +23,7 @@ import v4.compiler.parse { VoidGrammar, grammar_carries_symbol } -import v4.compiler.tokenize { +import v4.std.lexing { BlockCommentTextChar, CharClassPattern, CharPattern, diff --git a/src/v4/extdeps/languages/go.dag b/src/v4/extdeps/languages/go.dag index 5a527d27938..23c53b22715 100644 --- a/src/v4/extdeps/languages/go.dag +++ b/src/v4/extdeps/languages/go.dag @@ -5,14 +5,14 @@ module v4.extdeps.languages.go -import v4.compiler.parse { +import v4.std.grammar { GrammarExpr, GrammarProduction, Sequence, Terminal, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { LexRule, LexRuleSet, LexRules, diff --git a/src/v4/extdeps/languages/java.dag b/src/v4/extdeps/languages/java.dag index 2790c94f9ec..1e75bb5873d 100644 --- a/src/v4/extdeps/languages/java.dag +++ b/src/v4/extdeps/languages/java.dag @@ -5,7 +5,7 @@ module v4.extdeps.languages.java -import v4.compiler.parse { +import v4.std.grammar { Choice, Grammar, GrammarExpr, @@ -21,7 +21,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, IdentContinueChar, IdentStartChar, diff --git a/src/v4/extdeps/languages/kotlin.dag b/src/v4/extdeps/languages/kotlin.dag index b019db9e440..a8178998d42 100644 --- a/src/v4/extdeps/languages/kotlin.dag +++ b/src/v4/extdeps/languages/kotlin.dag @@ -5,7 +5,7 @@ module v4.extdeps.languages.kotlin -import v4.compiler.parse { +import v4.std.grammar { Grammar, GrammarExpr, GrammarProduction, @@ -16,7 +16,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, IdentContinueChar, IdentStartChar, diff --git a/src/v4/extdeps/languages/python.dag b/src/v4/extdeps/languages/python.dag index d6549192877..b6bf424473e 100644 --- a/src/v4/extdeps/languages/python.dag +++ b/src/v4/extdeps/languages/python.dag @@ -9,14 +9,14 @@ module v4.extdeps.languages.python -import v4.compiler.parse { +import v4.std.grammar { GrammarProduction, GrammarExpr, Sequence, Terminal, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { LexRule, LexRuleSet, LexRules, diff --git a/src/v4/extdeps/languages/rust.dag b/src/v4/extdeps/languages/rust.dag index 9a8ece0c7a7..d88fcbad62f 100644 --- a/src/v4/extdeps/languages/rust.dag +++ b/src/v4/extdeps/languages/rust.dag @@ -5,7 +5,7 @@ module v4.extdeps.languages.rust -import v4.compiler.parse { +import v4.std.grammar { Grammar, GrammarExpr, GrammarProduction, @@ -16,7 +16,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, IdentContinueChar, IdentStartChar, diff --git a/src/v4/extdeps/languages/swift.dag b/src/v4/extdeps/languages/swift.dag index 98414e77d73..40ad8f6f1bb 100644 --- a/src/v4/extdeps/languages/swift.dag +++ b/src/v4/extdeps/languages/swift.dag @@ -9,7 +9,7 @@ module v4.extdeps.languages.swift -import v4.compiler.parse { +import v4.std.grammar { Choice, Grammar, GrammarExpr, @@ -25,7 +25,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, ChoicePattern, DelimitedPattern, diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag index d93ecf920b0..e3e44971181 100644 --- a/src/v4/extdeps/languages/typescript.dag +++ b/src/v4/extdeps/languages/typescript.dag @@ -9,7 +9,7 @@ module v4.extdeps.languages.typescript -import v4.compiler.parse { +import v4.std.grammar { Grammar, GrammarExpr, GrammarProduction, @@ -20,7 +20,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, IdentContinueChar, IdentStartChar, diff --git a/src/v4/extdeps/languages/wasm.dag b/src/v4/extdeps/languages/wasm.dag index 008d7b90882..95be4ef0887 100644 --- a/src/v4/extdeps/languages/wasm.dag +++ b/src/v4/extdeps/languages/wasm.dag @@ -9,7 +9,7 @@ module v4.extdeps.languages.wasm -import v4.compiler.parse { +import v4.std.grammar { Choice, Grammar, GrammarExpr, @@ -24,7 +24,7 @@ import v4.compiler.parse { grammar_empty_sync_tokens, grammar_production_to_node } -import v4.compiler.tokenize { +import v4.std.lexing { CharClassPattern, ChoicePattern, DigitChar, diff --git a/src/v4/test/claim/manual/dag_ingest_round_trip.dag b/src/v4/test/claim/manual/dag_ingest_round_trip.dag index f47bbfcb010..39e52765ad3 100644 --- a/src/v4/test/claim/manual/dag_ingest_round_trip.dag +++ b/src/v4/test/claim/manual/dag_ingest_round_trip.dag @@ -19,7 +19,7 @@ import v4.extdeps.languages.dag { dag_token_kw_module, dag_wave1_lex_token_symbol } -import v4.compiler.parse { grammar_carries_symbol } +import v4.std.grammar { grammar_carries_symbol } import v4.std.logic { Bool } import v4.std.node { Atom, Conj, Edge, Named, Node, Symbol, TypeNode } import v4.std.verification { diff --git a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag index b3916d49dec..f4398deac84 100644 --- a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag +++ b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag @@ -16,7 +16,7 @@ import v4.compiler.compile { compile_ingest_staging } import v4.compiler.target_carriers { TargetModel, TargetSource } -import v4.compiler.tokenize { VoidLexRules } +import v4.std.lexing { VoidLexRules } import v4.compiler.emit { emit } import v4.compiler.infer { InferredFacts, diff --git a/src/v4/test/claim/manual/java_wave2_grammar_structure.dag b/src/v4/test/claim/manual/java_wave2_grammar_structure.dag index 74e66370b9b..de3019b257f 100644 --- a/src/v4/test/claim/manual/java_wave2_grammar_structure.dag +++ b/src/v4/test/claim/manual/java_wave2_grammar_structure.dag @@ -21,8 +21,8 @@ import v4.extdeps.languages.java { java_token_kw_void, java_wave2_lex_rules } -import v4.compiler.parse { grammar_carries_symbol } -import v4.compiler.tokenize { lex_rule_set_token_class_member } +import v4.std.grammar { grammar_carries_symbol } +import v4.std.lexing { lex_rule_set_token_class_member } import v4.std.logic { Bool } fn java_wave2_grammar_structure_satisfied(lm: JavaLanguageModel) -> Bool { diff --git a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag index c6bce4e7357..d1584f54e70 100644 --- a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag +++ b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag @@ -20,7 +20,7 @@ import v4.compiler.compile { } import v4.compiler.infer { InferredTree } import v4.compiler.target_carriers { TargetModel } -import v4.compiler.tokenize { VoidLexRules } +import v4.std.lexing { VoidLexRules } import v4.test.claim.manual.infer_ground_add_mvp { fixture_add_resolved_tree } import v4.std.diagnostic { Accepted, From 337200b682e6c41a56b9fc178aec32dc66f06f26 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:38:21 +0000 Subject: [PATCH 03/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/02_parse.dag | 3 +-- src/v4/extdeps/formats/csv.dag | 2 +- src/v4/extdeps/formats/json.dag | 2 +- src/v4/extdeps/formats/toml.dag | 2 +- src/v4/extdeps/formats/yaml.dag | 2 +- src/v4/extdeps/languages/kotlin.dag | 18 +----------------- src/v4/std/grammar.dag | 3 +++ .../empty_required_lenses_skip_gate.dag | 2 +- .../claim/manual/kotlin_mvp1_grammar_claim.dag | 17 ++++++++++++----- src/v4/test/claim/parse/grammar_validation.dag | 10 ++++++---- src/v4/test/claim/parse/swift_wave2a.dag | 6 ++++-- 11 files changed, 32 insertions(+), 35 deletions(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 0801023a350..63523225071 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -27,6 +27,7 @@ import v4.std.grammar { ModeledGrammar, Nonterminal, Optional, + ParseTree, Repeat, Sequence, Terminal, @@ -37,8 +38,6 @@ import v4.std.grammar { } -type ParseTree = Node - // 🟑 coproduct dissolution β€” feature:T-8-parse-result-projection; per-expression walk result; dissolves when parse-walk result carrier unifies with Outcome via T-8 projection (remaining/captured consolidates; List accumulator lifts into standard Diagnostics). type ParseExprResult = ParseExprAccepted { remaining: List, captured: Node, diagnostics: List } diff --git a/src/v4/extdeps/formats/csv.dag b/src/v4/extdeps/formats/csv.dag index bb51cc5fcc0..732c4eacdb3 100644 --- a/src/v4/extdeps/formats/csv.dag +++ b/src/v4/extdeps/formats/csv.dag @@ -5,7 +5,7 @@ module v4.extdeps.formats.csv -import v4.compiler.parse { GrammarSchema } +import v4.std.grammar { GrammarSchema } import v4.std.collection { Optional } diff --git a/src/v4/extdeps/formats/json.dag b/src/v4/extdeps/formats/json.dag index 0953cc7759b..89a34dfefb2 100644 --- a/src/v4/extdeps/formats/json.dag +++ b/src/v4/extdeps/formats/json.dag @@ -6,7 +6,7 @@ module v4.extdeps.formats.json -import v4.compiler.parse { GrammarSchema } +import v4.std.grammar { GrammarSchema } // 🟒 coproduct dissolution β€” CP-3229-GREEN-TERMINAL. diff --git a/src/v4/extdeps/formats/toml.dag b/src/v4/extdeps/formats/toml.dag index 437e5315135..7892d473951 100644 --- a/src/v4/extdeps/formats/toml.dag +++ b/src/v4/extdeps/formats/toml.dag @@ -6,7 +6,7 @@ module v4.extdeps.formats.toml -import v4.compiler.parse { GrammarSchema } +import v4.std.grammar { GrammarSchema } import v4.std.datetime { LocalDate, LocalDateTime, LocalTime, OffsetDateTime } diff --git a/src/v4/extdeps/formats/yaml.dag b/src/v4/extdeps/formats/yaml.dag index f0a30ae3b77..59730d73a5f 100644 --- a/src/v4/extdeps/formats/yaml.dag +++ b/src/v4/extdeps/formats/yaml.dag @@ -6,7 +6,7 @@ module v4.extdeps.formats.yaml -import v4.compiler.parse { GrammarSchema } +import v4.std.grammar { GrammarSchema } // 🟒 coproduct dissolution β€” CP-3229-GREEN-TERMINAL. diff --git a/src/v4/extdeps/languages/kotlin.dag b/src/v4/extdeps/languages/kotlin.dag index a8178998d42..0371935f651 100644 --- a/src/v4/extdeps/languages/kotlin.dag +++ b/src/v4/extdeps/languages/kotlin.dag @@ -28,12 +28,9 @@ import v4.std.lexing { ModeledLexRules, RepeatPattern, SequencePattern, - Token, TokenRule, - lex_rule_set_token_class_member, - tokenize + lex_rule_set_token_class_member } -import v4.std.diagnostic { Accepted, Outcome, Rejected } import v4.std.collection { List, Map, Set, empty_map, map_insert } import v4.std.model_core { EffectSemanticsDecl, @@ -1223,19 +1220,6 @@ fn kotlin_wave1_lex() -> LexRules { ModeledLexRules { root: kotlin_wave1_lex_rules() } } -// Parse-fixture tokens: lexer output from MVP authority source (lexeme + spans via tokenize). -fn kotlin_mvp1_parse_tokens() -> Outcome> { - match tokenize( - text: kotlin_mvp1_source_text, - file: kotlin_mvp1_parse_fixture_file, - rules: kotlin_wave1_lex() - ) { - Accepted { value: stream, diagnostics: diags } => - Accepted { value: stream.tokens, diagnostics: diags } - Rejected { diagnostics: diags } => Rejected { diagnostics: diags } - } -} - fn kotlin_wave1_grammar_root() -> GrammarRoot { let start = kotlin_grammar_production_mvp1_fn_add() GrammarRoot { diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index 3d7a73938ae..31908614cc2 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -56,6 +56,9 @@ type GrammarSchema { } +type ParseTree = Node + + type GrammarSymbolFoldState { found: Bool } diff --git a/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag b/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag index 6ff5a94fa59..ed5f715d201 100644 --- a/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag +++ b/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag @@ -13,7 +13,7 @@ import v4.compiler.compile { validate_then_compile } import v4.compiler.target_carriers { TargetModel } -import v4.compiler.tokenize { VoidLexRules } +import v4.std.lexing { VoidLexRules } import v4.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } import v4.std.logic { Bool } import v4.std.algebra { Empty } diff --git a/src/v4/test/claim/manual/kotlin_mvp1_grammar_claim.dag b/src/v4/test/claim/manual/kotlin_mvp1_grammar_claim.dag index 6fcb5452a23..12f36f358d0 100644 --- a/src/v4/test/claim/manual/kotlin_mvp1_grammar_claim.dag +++ b/src/v4/test/claim/manual/kotlin_mvp1_grammar_claim.dag @@ -7,17 +7,20 @@ module v4.test.claim.manual.kotlin_mvp1_grammar_claim import v4.compiler.parse { - ParseTree, grammar_validate_for_parse, parse_production, parse_stage_locus_port } +import v4.compiler.tokenize { tokenize } import v4.extdeps.languages.kotlin { - kotlin_mvp1_parse_tokens, + kotlin_mvp1_parse_fixture_file, kotlin_production_mvp1_fn_add, + kotlin_mvp1_source_text, + kotlin_wave1_lex, kotlin_wave1_grammar_root } import v4.std.diagnostic { Accepted, Outcome, Rejected, port_locus } +import v4.std.grammar { ParseTree } import v4.std.node { Atom, Node, Symbol, TypeNode } import v4.std.logic { Bool } import v4.std.verification { @@ -60,14 +63,18 @@ fn kotlin_mvp1_grammar_parse_accepted() -> Bool { fn kotlin_mvp1_grammar_parse_fixture() -> Outcome { let at = port_locus(port: parse_stage_locus_port) - match kotlin_mvp1_parse_tokens() { + match tokenize( + text: kotlin_mvp1_source_text, + file: kotlin_mvp1_parse_fixture_file, + rules: kotlin_wave1_lex() + ) { Rejected { diagnostics: diags } => Rejected { diagnostics: diags } - Accepted { value: tokens, diagnostics: _ } => + Accepted { value: stream, diagnostics: _ } => match grammar_validate_for_parse(root: kotlin_wave1_grammar_root(), at: at) { Rejected { diagnostics: diags } => Rejected { diagnostics: diags } Accepted { value: validated, diagnostics: _ } => parse_production( - tokens: tokens, + tokens: stream.tokens, validated: validated, production_name: kotlin_production_mvp1_fn_add ) diff --git a/src/v4/test/claim/parse/grammar_validation.dag b/src/v4/test/claim/parse/grammar_validation.dag index 276459bad5e..f5c3e602ff7 100644 --- a/src/v4/test/claim/parse/grammar_validation.dag +++ b/src/v4/test/claim/parse/grammar_validation.dag @@ -8,18 +8,20 @@ module v4.test.claim.parse.grammar_validation -import v4.compiler.tokenize { Token } -import v4.compiler.parse { +import v4.std.lexing { Token } +import v4.std.grammar { GrammarProduction, GrammarRoot, Nonterminal, Optional, - ParseSyncState, ParseTree, Sequence, Terminal, grammar_atom, - grammar_empty_sync_tokens, + grammar_empty_sync_tokens +} +import v4.compiler.parse { + ParseSyncState, grammar_has_duplicate_productions, grammar_has_left_recursion, grammar_has_undefined_nonterminals, diff --git a/src/v4/test/claim/parse/swift_wave2a.dag b/src/v4/test/claim/parse/swift_wave2a.dag index a974c210224..d84ced4181f 100644 --- a/src/v4/test/claim/parse/swift_wave2a.dag +++ b/src/v4/test/claim/parse/swift_wave2a.dag @@ -5,8 +5,10 @@ module v4.test.claim.parse.swift_wave2a -import v4.compiler.tokenize { TokenStream, tokenize } -import v4.compiler.parse { ParseTree, parse } +import v4.std.lexing { TokenStream } +import v4.std.grammar { ParseTree } +import v4.compiler.tokenize { tokenize } +import v4.compiler.parse { parse } import v4.extdeps.languages.swift { swift_wave1_lex, swift_wave1_grammar } import v4.std.diagnostic { Accepted, Outcome, Rejected } import v4.std.node { Atom, Node, Symbol, TypeNode } From 574438113c53bb758f5bef26b8c962d6ecc810bb Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:39:58 +0000 Subject: [PATCH 04/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/extdeps/languages/swift.dag | 2 +- src/v4/extdeps/languages/typescript.dag | 2 +- src/v4/extdeps/languages/wasm.dag | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/v4/extdeps/languages/swift.dag b/src/v4/extdeps/languages/swift.dag index 40ad8f6f1bb..d6f4175a67d 100644 --- a/src/v4/extdeps/languages/swift.dag +++ b/src/v4/extdeps/languages/swift.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/swift.dag // Scope: Swift language/standard-library scalar fact-bundles and ModelCore wave-1. // Owns: SwiftIntWidth, SwiftIntSignedness, SwiftFloatWidth, SwiftStringRepresentation, SwiftCharacterRepresentation, SwiftUnitRepresentation, SwiftBoolRepresentation, SwiftIntegerOverflowSemantics, SwiftScalar, SwiftIntegerPrimitiveFacts, SwiftFloatPrimitiveFacts, SwiftNonNumericPrimitiveFacts, SwiftLanguageModel, SwiftConcreteSyntaxToken, SwiftGrammarRelationRow, swift_language_model_surface_id, swift_surface_spelling_int, swift_surface_spelling_int8, swift_surface_spelling_int16, swift_surface_spelling_int32, swift_surface_spelling_int64, swift_surface_spelling_uint, swift_surface_spelling_uint8, swift_surface_spelling_uint16, swift_surface_spelling_uint32, swift_surface_spelling_uint64, swift_surface_spelling_float, swift_surface_spelling_double, swift_surface_spelling_bool, swift_surface_spelling_character, swift_surface_spelling_string, swift_surface_spelling_void, swift_facts_field_surface_spelling, swift_facts_field_signedness, swift_facts_field_width, swift_facts_field_overflow, swift_facts_field_ieee754_binary, swift_facts_field_scalar, swift_facts_field_value_fact, swift_primitive_fact_axis_scalar_classifier, swift_tag_signed, swift_tag_unsigned, swift_tag_bits8, swift_tag_bits16, swift_tag_bits32, swift_tag_bits64, swift_tag_pointer_word, swift_tag_trap_on_overflow, swift_tag_ieee754_binary32, swift_tag_ieee754_binary64, swift_tag_bool_representation, swift_tag_character_extended_grapheme_cluster, swift_tag_string_unicode_text, swift_tag_void_empty_tuple, swift_tag_scalar_int, swift_tag_scalar_float, swift_tag_scalar_bool, swift_tag_scalar_character, swift_tag_scalar_string, swift_tag_scalar_void, swift_inhabitant_int32, swift_inhabitant_field_int32, swift_inhabitant_field_atom, swift_inhabitant_field_facts, swift_token_kw_func, swift_token_kw_return, swift_token_kw_let, swift_token_kw_var, swift_token_kw_if, swift_token_kw_else, swift_token_kw_while, swift_token_kw_for, swift_token_kw_in, swift_token_kw_struct, swift_token_kw_class, swift_token_kw_enum, swift_token_kw_protocol, swift_token_kw_extension, swift_token_kw_import, swift_token_kw_true, swift_token_kw_false, swift_token_ident, swift_token_int_literal, swift_token_string_literal, swift_token_operator, swift_token_arrow, swift_token_equal, swift_token_lbrace, swift_token_rbrace, swift_token_lparen, swift_token_rparen, swift_token_lbracket, swift_token_rbracket, swift_token_comma, swift_token_colon, swift_token_dot, swift_token_semicolon, swift_production_mvp1_fn_add, swift_production_fn_decl, swift_production_typed_param, swift_production_param_list, swift_production_type_expr, swift_production_block, swift_production_stmt, swift_production_return_stmt, swift_production_let_stmt, swift_production_if_stmt, swift_production_while_stmt, swift_production_expr, swift_production_binary_expr, swift_production_call_expr, swift_production_primary_expr, swift_surface_fn_item, swift_surface_typed_param, swift_surface_param_list, swift_surface_type_expr, swift_surface_block, swift_surface_stmt, swift_surface_return_stmt, swift_surface_let_stmt, swift_surface_if_stmt, swift_surface_while_stmt, swift_surface_expr, swift_surface_binary_expr, swift_surface_call_expr, swift_surface_primary_expr, swift_surface_type_int32, swift_surface_bin_add, swift_binding_fn_add, swift_binding_param_x, swift_binding_param_y, swift_binding_ty_int32, swift_binding_op_plus, swift_relation_rule_mvp1_fn_add, swift_mvp1_source_literal, swift_mvp1_source_text_field, swift_mvp1_source_grammar_field, swift_mvp1_concrete_tokens, swift_mvp1_source_text, swift_integer_overflow_trap, swift_bool_representation, swift_character_representation, swift_string_representation, swift_unit_representation, swift_facts_int, swift_facts_int8, swift_facts_int16, swift_facts_int32, swift_facts_int64, swift_facts_uint, swift_facts_uint8, swift_facts_uint16, swift_facts_uint32, swift_facts_uint64, swift_facts_float, swift_facts_double, swift_facts_bool, swift_facts_character, swift_facts_string, swift_facts_void, swift_integer_facts_catalog, swift_float_facts_catalog, swift_nonnumeric_facts_catalog, swift_bool_grounding, swift_atom, swift_named_edge, swift_signedness_node, swift_width_node, swift_float_width_node, swift_overflow_node, swift_scalar_node, swift_nonnumeric_representation_node, swift_nonnumeric_scalar_classifier_node, swift_integer_facts_node, swift_float_facts_node, swift_nonnumeric_surface_spelling, swift_nonnumeric_facts_node, swift_integer_inhabitant_node, swift_inhabitant_int32_node, swift_declared_inhabitants_root, swift_mvp1_selection_policy_node, swift_mvp1_emitted_add_fn_node, swift_mvp1_source_text_authority, swift_concrete_token_class, swift_concrete_token_node, swift_mvp1_positional_token_edge, swift_mvp1_positional_edges_from_token_classes, swift_mvp1_serialize_source_prefix_edges, swift_mvp1_serialize_source_children, swift_mvp1_serialize_source_node, swift_grammar_terminal, swift_grammar_sequence_fold_step, swift_grammar_sequence_from_token_classes, swift_mvp1_grammar_relation_row, swift_relation_token_edges, swift_grammar_relation_row_node, swift_mvp1_translation_rules_node, swift_mvp1_target_model_node, swift_mvp1_binding_spellings, swift_mvp1_target_model, swift_lex_rule, swift_keyword_lex_rule, swift_whitespace_trivia_rule, swift_ident_lex_pattern, swift_ident_lex_rule, swift_int_literal_lex_rule, swift_string_literal_lex_rule, swift_infix_operator_lex_pattern, swift_infix_operator_lex_rule, swift_wave1_lex_rules, swift_wave1_lex, swift_grammar_atom, swift_grammar_nonterminal, swift_grammar_sequence, swift_grammar_choice, swift_grammar_optional, swift_grammar_repeat, swift_grammar_type_expr, swift_grammar_typed_param_expr, swift_grammar_param_list_expr, swift_grammar_binary_operator_expr, swift_grammar_expr_list_expr, swift_grammar_primary_expr, swift_grammar_call_expr, swift_grammar_binary_expr, swift_grammar_expr_expr, swift_grammar_return_stmt_expr, swift_grammar_let_stmt_expr, swift_grammar_if_stmt_expr, swift_grammar_while_stmt_expr, swift_grammar_stmt_expr, swift_grammar_block_stmt_separator_expr, swift_grammar_block_expr, swift_grammar_fn_decl_expr, swift_grammar_production_mvp1_fn_add, swift_grammar_production_fn_decl, swift_grammar_production_typed_param, swift_grammar_production_param_list, swift_grammar_production_type_expr, swift_grammar_production_block, swift_grammar_production_stmt, swift_grammar_production_return_stmt, swift_grammar_production_let_stmt, swift_grammar_production_if_stmt, swift_grammar_production_while_stmt, swift_grammar_production_expr, swift_grammar_production_binary_expr, swift_grammar_production_call_expr, swift_grammar_production_primary_expr, swift_wave1_grammar_root, swift_wave1_grammar, swift_wave1_lex_token_symbol, swift_empty_primitive_spec_facts, swift_primitive_fact_map_4, swift_primitive_fact_map_3, swift_primitive_fact_map_2, swift_primitive_bundle_from_integer_facts, swift_primitive_bundle_from_float_facts, swift_primitive_bundle_from_nonnumeric_facts, swift_primitive_bundles_from_integer_catalog, swift_primitive_bundles_from_float_catalog, swift_primitive_bundles_from_nonnumeric_catalog, swift_wave1_primitive_fact_bundles, swift_integer_catalog_surface_symbol_step, swift_float_catalog_surface_symbol_step, swift_nonnumeric_catalog_surface_symbol_step, swift_integer_catalog_surface_symbol, swift_float_catalog_surface_symbol, swift_nonnumeric_catalog_surface_symbol, swift_catalog_surface_symbol, swift_language_model_canonical_symbols, swift_model_core_wave1, swift_language_model_wave1 -// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text. +// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text. // Status: T-4 Swift wave-1; fixed-width integer spellings are explicit, Int/UInt stay platform-word-width facts, Float/Double carry IEEE-754 precision; canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 grammar/token substrate for T-11; bool canonical-B decl-ref is E-6(b) staging. // Anchor: https://docs.swift.org/swift-book/documentation/the-swift-programming-language/thebasics/ // Ledger: CP-3229-GREEN-TERMINAL. diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag index e3e44971181..29da0b7d51d 100644 --- a/src/v4/extdeps/languages/typescript.dag +++ b/src/v4/extdeps/languages/typescript.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/typescript.dag // Scope: TypeScript 5.9 + ECMA-262 ES2025 numeric primitive fact-bundles and ModelCore wave-1. // Owns: TsNumberPrimitiveFacts, TsBigIntPrimitiveFacts, TsBooleanPrimitiveFacts, TsEcma262NumericPrimitiveFactsUnion, TsLanguageModel, TsConcreteSyntaxToken, TsGrammarRelationRow, ts_language_model_surface_id, ts_std_projection_float64, ts_std_projection_bigint, ts_std_projection_bool, ts_surface_spelling_number, ts_surface_spelling_bigint, ts_surface_spelling_boolean, ts_ieee754_binary64, ts_repr_bigint_exact_unbounded, ts_repr_boolean_ecma_boolean, ts_inhabitant_number, ts_inhabitant_bigint, ts_inhabitant_boolean, ts_inhabitant_field_number, ts_inhabitant_field_bigint, ts_inhabitant_field_boolean, ts_inhabitant_field_atom, ts_inhabitant_field_facts, ts_facts_field_surface_spelling, ts_facts_field_arithmetic_semantics, ts_facts_field_bitwise_semantics, ts_facts_field_operation_semantics, ts_facts_field_width, ts_facts_field_ieee754_binary, ts_facts_field_std_projection, ts_facts_field_encoding, ts_tag_bits64, ts_tag_number_ieee754_binary64, ts_tag_number_bitwise_int32_uint32, ts_tag_bigint_exact_unbounded, ts_witness_number_approximate_field, ts_witness_bigint_ordered_ring, ts_witness_bool_boolean_algebra, ts_token_kw_function, ts_token_kw_return, ts_token_ident, ts_token_ty_number, ts_token_plus, ts_token_lbrace, ts_token_rbrace, ts_token_lparen, ts_token_rparen, ts_token_comma, ts_token_colon, ts_token_semicolon, ts_production_mvp1_fn_add, ts_surface_fn_item, ts_surface_type_number, ts_surface_bin_add, ts_binding_fn_add, ts_binding_param_x, ts_binding_param_y, ts_relation_rule_mvp1_fn_add, ts_mvp1_source_literal, ts_mvp1_source_text_field, ts_mvp1_source_grammar_field, ts_mvp1_concrete_tokens, ts_mvp1_source_text, ts_facts_number, ts_facts_bigint, ts_facts_boolean, ts_bool_grounding, ts_numeric_facts_catalog, ts_inhabitant_atom, ts_named_edge, ts_number_arithmetic_semantics_node, ts_number_bitwise_semantics_node, ts_bigint_operation_semantics_node, ts_bool_operation_semantics_node, ts_number_facts_node, ts_bigint_facts_node, ts_bool_facts_node, ts_number_inhabitant_node, ts_bigint_inhabitant_node, ts_bool_inhabitant_node, ts_inhabitant_number_node, ts_inhabitant_bigint_node, ts_inhabitant_boolean_node, ts_declared_inhabitants_root, ts_mvp1_selection_policy_node, ts_mvp1_emitted_add_fn_node, ts_mvp1_source_text_authority, ts_concrete_token_class, ts_concrete_token_node, ts_mvp1_positional_token_edge, ts_mvp1_positional_edges_from_token_classes, ts_mvp1_serialize_source_prefix_edges, ts_mvp1_serialize_source_children, ts_mvp1_serialize_source_node, ts_grammar_terminal, TsGramBuild1State, ts_grammar_sequence_from_token_classes, ts_mvp1_grammar_relation_row, ts_relation_token_edges, ts_grammar_relation_row_node, ts_mvp1_translation_rules_node, ts_mvp1_target_model_node, ts_mvp1_binding_spellings, ts_mvp1_target_model, ts_wave1_target_model, ts_lex_rule, ts_ident_lex_pattern, ts_ident_lex_rule, ts_wave1_lex_rules, ts_wave1_lex, ts_grammar_atom, ts_grammar_production_mvp1_fn_add, ts_wave1_grammar_root, ts_wave1_grammar, ts_wave1_lex_token_symbol, ts_catalog_surface_symbol_step, ts_catalog_surface_symbol, ts_language_model_canonical_symbols, ts_number_spec_facts, ts_bigint_spec_facts, ts_bool_spec_facts, ts_primitive_bundle_from_number_facts, ts_primitive_bundle_from_bigint_facts, ts_primitive_bundle_from_bool_facts, ts_primitive_bundles_from_catalog_step, ts_numeric_primitive_fact_bundles, ts_wave1_primitive_fact_bundles, ts_number_algebra_witness_node, ts_bigint_algebra_witness_node, ts_bool_algebra_witness_node, ts_number_algebra_inhabitance, ts_bigint_algebra_inhabitance, ts_bool_algebra_inhabitance, ts_numeric_algebra_inhabitance_step, ts_numeric_algebra_inhabitance_decls, ts_bool_algebra_inhabitance_decls, ts_model_core_inhabitance_decls, ts_model_core_wave1, ts_language_model_wave1 -// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.model_core, v4.std.target_model, v4.std.text. +// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.model_core, v4.std.target_model, v4.std.text. // Status: T-4 typescript slice β€” ECMA `number` (IEEE-754 binary64) + `bigint` (exact unbounded β„€) fact-bundles; `core: ModelCore` primitives from `ts_numeric_facts_catalog` via fold; canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 grammar/token substrate for T-11; bool canonical-B decl-ref β€” 🟑 E-6(b) staging. // Anchor: https://www.typescriptlang.org/docs/handbook/2/everyday-types.html β€” ECMA-262 https://tc39.es/ecma262/2025/multipage/ // Ledger: CP-3229-GREEN-TERMINAL, SL-T11-GRAMMAR-FROM-TOKEN-ROW. diff --git a/src/v4/extdeps/languages/wasm.dag b/src/v4/extdeps/languages/wasm.dag index 95be4ef0887..7d56deca074 100644 --- a/src/v4/extdeps/languages/wasm.dag +++ b/src/v4/extdeps/languages/wasm.dag @@ -1,7 +1,7 @@ // src/v4/extdeps/languages/wasm.dag // Scope: WebAssembly Core numeric value types β€” LanguageModel fact-bundles (Shape A). // Owns: WasmIntWidth, WasmFloatWidth, WasmScalar, WasmIntegerPrimitiveFacts, WasmFloatPrimitiveFacts, WasmLanguageModel, WasmConcreteSyntaxToken, WasmGrammarRelationRow, wasm_language_model_surface_id, wasm_std_projection_i32, wasm_std_projection_i64, wasm_std_projection_f32, wasm_std_projection_f64, wasm_surface_spelling_i32, wasm_surface_spelling_i64, wasm_surface_spelling_f32, wasm_surface_spelling_f64, wasm_ieee754_binary32, wasm_ieee754_binary64, wasm_repr_sign_agnostic_modular, wasm_repr_modular_wrap, wasm_inhabitant_i32, wasm_inhabitant_i64, wasm_inhabitant_f32, wasm_inhabitant_f64, wasm_inhabitant_field_i32, wasm_inhabitant_field_i64, wasm_inhabitant_field_f32, wasm_inhabitant_field_f64, wasm_facts_field_surface_spelling, wasm_facts_field_width, wasm_facts_field_std_projection, wasm_facts_field_scalar_classifier, wasm_facts_field_ieee754_binary, wasm_scalar_field_classifier, wasm_scalar_field_width, wasm_tag_sign_agnostic_modular, wasm_tag_bits32, wasm_tag_bits64, wasm_tag_modular_wrap, wasm_tag_scalar_int, wasm_tag_scalar_float, wasm_inhabitant_field_atom, wasm_inhabitant_field_facts, wasm_token_lparen, wasm_token_rparen, wasm_token_kw_module, wasm_token_kw_func, wasm_token_ident, wasm_token_kw_param, wasm_token_kw_result, wasm_token_local_get, wasm_token_type_i32, wasm_token_type_i64, wasm_token_type_f32, wasm_token_type_f64, wasm_token_int_numeric_literal, wasm_token_float_numeric_literal, wasm_token_localidx_literal, wasm_token_i32_numeric_literal, wasm_token_i64_numeric_literal, wasm_token_f32_numeric_literal, wasm_token_f64_numeric_literal, wasm_token_i32_const, wasm_token_i32_add, wasm_token_i32_sub, wasm_token_i32_mul, wasm_token_i32_div_s, wasm_token_i32_div_u, wasm_token_i32_rem_s, wasm_token_i32_rem_u, wasm_token_i32_and, wasm_token_i32_or, wasm_token_i32_xor, wasm_token_i32_shl, wasm_token_i32_shr_s, wasm_token_i32_shr_u, wasm_token_i32_rotl, wasm_token_i32_rotr, wasm_token_i64_const, wasm_token_i64_add, wasm_token_i64_sub, wasm_token_i64_mul, wasm_token_i64_div_s, wasm_token_i64_div_u, wasm_token_i64_rem_s, wasm_token_i64_rem_u, wasm_token_i64_and, wasm_token_i64_or, wasm_token_i64_xor, wasm_token_i64_shl, wasm_token_i64_shr_s, wasm_token_i64_shr_u, wasm_token_i64_rotl, wasm_token_i64_rotr, wasm_token_f32_const, wasm_token_f32_add, wasm_token_f32_sub, wasm_token_f32_mul, wasm_token_f32_div, wasm_token_f32_min, wasm_token_f32_max, wasm_token_f32_copysign, wasm_token_f64_const, wasm_token_f64_add, wasm_token_f64_sub, wasm_token_f64_mul, wasm_token_f64_div, wasm_token_f64_min, wasm_token_f64_max, wasm_token_f64_copysign, wasm_production_mvp1_fn_add, wasm_production_text_fragment, wasm_production_mvp1_module, wasm_production_value_type, wasm_production_i32_numeric_literal, wasm_production_i64_numeric_literal, wasm_production_f32_numeric_literal, wasm_production_f64_numeric_literal, wasm_production_numeric_const_instr, wasm_production_numeric_binop_instr, wasm_production_localidx, wasm_surface_fn_item, wasm_surface_text_fragment, wasm_surface_mvp1_module_item, wasm_surface_type_i32, wasm_surface_value_type, wasm_surface_bin_add, wasm_surface_i32_numeric_literal, wasm_surface_i64_numeric_literal, wasm_surface_f32_numeric_literal, wasm_surface_f64_numeric_literal, wasm_surface_numeric_const_instr, wasm_surface_numeric_binop_instr, wasm_surface_localidx, wasm_binding_fn_add, wasm_binding_localidx_0, wasm_binding_localidx_1, wasm_numeric_immediate_field_token_class, wasm_numeric_immediate_field_width, wasm_numeric_immediate_field_validation, wasm_numeric_immediate_validation_i32_range, wasm_numeric_immediate_validation_i64_range, wasm_numeric_immediate_validation_f32_payload, wasm_numeric_immediate_validation_f64_payload, wasm_localidx_validation_u32_range, wasm_relation_rule_mvp1_fn_add, wasm_mvp1_source_literal, wasm_mvp1_source_text_field, wasm_mvp1_source_grammar_field, wasm_mvp1_concrete_tokens, wasm_mvp1_source_text, wasm_facts_i32, wasm_facts_i64, wasm_facts_f32, wasm_facts_f64, wasm_integer_facts_catalog, wasm_float_facts_catalog, wasm_inhabitant_atom, wasm_int_width_node, wasm_float_width_node, wasm_scalar_node, wasm_integer_facts_node, wasm_float_facts_node, wasm_integer_inhabitant_node, wasm_float_inhabitant_node, wasm_inhabitant_i32_node, wasm_inhabitant_i64_node, wasm_inhabitant_f32_node, wasm_inhabitant_f64_node, wasm_named_edge, wasm_int_numeric_immediate_node, wasm_float_numeric_immediate_node, wasm_i32_numeric_literal_node, wasm_i64_numeric_literal_node, wasm_f32_numeric_literal_node, wasm_f64_numeric_literal_node, wasm_localidx_node, wasm_localidx_operand_node, wasm_declared_inhabitants_root, wasm_mvp1_selection_policy_node, wasm_mvp1_emitted_add_fn_node, wasm_mvp1_source_text_authority, wasm_concrete_token_class, wasm_concrete_token_node, wasm_mvp1_positional_token_edge, wasm_mvp1_positional_edges_from_token_classes, wasm_mvp1_serialize_source_prefix_edges, wasm_mvp1_serialize_source_children, wasm_mvp1_serialize_source_node, wasm_grammar_terminal, wasm_grammar_choice, wasm_grammar_optional, wasm_grammar_repeat, wasm_grammar_choice_fold_step, wasm_grammar_choice_from_token_classes, wasm_grammar_sequence, wasm_grammar_sequence_fold_step, wasm_grammar_sequence_from_token_classes, wasm_mvp1_grammar_relation_row, wasm_relation_token_edges, wasm_grammar_relation_row_node, wasm_mvp1_translation_rules_node, wasm_mvp1_target_model_node, wasm_mvp1_binding_spellings, wasm_mvp1_target_model, wasm_lex_rule, wasm_dollar_ident_lex_pattern, wasm_ident_lex_rule, wasm_lex_choice, wasm_lex_sequence, wasm_optional_sign_lex_pattern, wasm_digit_run_lex_pattern, wasm_hex_digit_run_lex_pattern, wasm_decimal_exponent_lex_pattern, wasm_hex_exponent_lex_pattern, wasm_decimal_integer_lex_pattern, wasm_hex_integer_lex_pattern, wasm_decimal_float_lex_pattern, wasm_hex_float_lex_pattern, wasm_nan_payload_lex_pattern, wasm_float_special_lex_pattern, wasm_u32_lex_pattern, wasm_wat_int_literal_lex_pattern, wasm_wat_float_literal_lex_pattern, wasm_numeric_literal_lex_rule, wasm_int_numeric_literal_lex_rule, wasm_float_numeric_literal_lex_rule, wasm_localidx_literal_lex_rule, wasm_i32_numeric_literal_lex_rule, wasm_i64_numeric_literal_lex_rule, wasm_f32_numeric_literal_lex_rule, wasm_f64_numeric_literal_lex_rule, wasm_wave1_lex_rules, wasm_wave1_lex, wasm_grammar_atom, wasm_grammar_mvp1_fn_add_expr, wasm_grammar_production_mvp1_fn_add, wasm_grammar_value_type_expr, wasm_grammar_localidx_expr, wasm_grammar_numeric_const_instr_expr, wasm_grammar_numeric_binop_instr_expr, wasm_grammar_mvp1_module_expr, wasm_grammar_text_fragment_expr, wasm_grammar_production_text_fragment, wasm_grammar_production_mvp1_module, wasm_grammar_production_value_type, wasm_grammar_production_i32_numeric_literal, wasm_grammar_production_i64_numeric_literal, wasm_grammar_production_f32_numeric_literal, wasm_grammar_production_f64_numeric_literal, wasm_grammar_production_localidx, wasm_grammar_production_numeric_const_instr, wasm_grammar_production_numeric_binop_instr, wasm_wave1_grammar_root, wasm_wave1_grammar, wasm_wave1_lex_token_symbol, wasm_integer_catalog_surface_symbol_step, wasm_float_catalog_surface_symbol_step, wasm_integer_catalog_surface_symbol, wasm_float_catalog_surface_symbol, wasm_catalog_surface_symbol, wasm_language_model_canonical_symbols, wasm_integer_spec_facts, wasm_float_spec_facts, wasm_primitive_bundle_from_integer_facts, wasm_primitive_bundle_from_float_facts, wasm_primitive_bundles_from_integer_catalog, wasm_primitive_bundles_from_float_catalog, wasm_wave1_primitive_fact_bundles, wasm_model_core_wave1, wasm_language_model_wave1 -// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text. +// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text. // Status: T-4 wasm slice β€” Core Β§2.3.1 number types (i32/i64/f32/f64 wave-1); `core: ModelCore` (#3474); canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 WAT grammar/token substrate for T-11; v128/funcref/externref 🟑 wave-2; integer sign-agnostic per spec (width + modular wrap, not signed/unsigned partition). // Anchor: https://webassembly.github.io/spec/core/types.html#number-types // Ledger: CP-3229-GREEN-TERMINAL. From 3d9362b687bc2ad4446afa707ad28942a6427910 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:44:20 +0000 Subject: [PATCH 05/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/02_parse.dag | 1 - 1 file changed, 1 deletion(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 63523225071..41884cc0d52 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -26,7 +26,6 @@ import v4.std.grammar { GrammarRoot, ModeledGrammar, Nonterminal, - Optional, ParseTree, Repeat, Sequence, From c470fb0ef73fa331046c8c870a5307de08ce8b84 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 13:54:53 +0000 Subject: [PATCH 06/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- scripts/strict_deprose_dag.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/strict_deprose_dag.py b/scripts/strict_deprose_dag.py index 258d0205c12..f9e3d9db93b 100644 --- a/scripts/strict_deprose_dag.py +++ b/scripts/strict_deprose_dag.py @@ -652,7 +652,7 @@ def main() -> None: "src/v4/extdeps/languages/typescript.dag", "// Scope: TypeScript 5.9 + ECMA-262 ES2025 numeric primitive fact-bundles and ModelCore wave-1.", "// Anchor: https://www.typescriptlang.org/docs/handbook/2/everyday-types.html β€” ECMA-262 https://tc39.es/ecma262/2025/multipage/", - "// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.model_core, v4.std.target_model, v4.std.text.", + "// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.model_core, v4.std.target_model, v4.std.text.", "// Status: T-4 typescript slice β€” ECMA `number` (IEEE-754 binary64) + `bigint` (exact unbounded β„€) fact-bundles; `core: ModelCore` primitives from `ts_numeric_facts_catalog` via fold; canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 grammar/token substrate for T-11; bool canonical-B decl-ref β€” 🟑 E-6(b) staging.", "// 🟑", ), @@ -660,7 +660,7 @@ def main() -> None: "src/v4/extdeps/languages/swift.dag", "// Scope: Swift language/standard-library scalar fact-bundles and ModelCore wave-1.", "// Anchor: https://docs.swift.org/swift-book/documentation/the-swift-programming-language/thebasics/", - "// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text.", + "// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text.", "// Status: T-4 Swift wave-1; fixed-width integer spellings are explicit, Int/UInt stay platform-word-width facts, Float/Double carry IEEE-754 precision; canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 grammar/token substrate for T-11; bool canonical-B decl-ref is E-6(b) staging.", "// 🟑", ), @@ -668,7 +668,7 @@ def main() -> None: "src/v4/extdeps/languages/wasm.dag", "// Scope: WebAssembly Core numeric value types β€” LanguageModel fact-bundles (Shape A).", "// Anchor: https://webassembly.github.io/spec/core/types.html#number-types", - "// Consumes: v4.compiler.parse, v4.compiler.tokenize, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text.", + "// Consumes: v4.std.grammar, v4.std.lexing, v4.std.collection, v4.std.model_core, v4.std.target_model, v4.std.node, v4.std.logic, v4.std.algebra, v4.std.text.", "// Status: T-4 wasm slice β€” Core Β§2.3.1 number types (i32/i64/f32/f64 wave-1); `core: ModelCore` (#3474); canonical_symbols = catalog surface spellings + wave-1 lex/grammar/MVP; target_model edge keys from std/target_model.dag; MVP-1 WAT grammar/token substrate for T-11; v128/funcref/externref 🟑 wave-2; integer sign-agnostic per spec (width + modular wrap, not signed/unsigned partition).", "// 🟑", ), From 4266c0aa58e323c50a8c3e33b655e4a93bf07e53 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 14:11:24 +0000 Subject: [PATCH 07/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/lexing.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/src/v4/std/lexing.dag b/src/v4/std/lexing.dag index 37c95ae8c24..d7b95fd8cf2 100644 --- a/src/v4/std/lexing.dag +++ b/src/v4/std/lexing.dag @@ -71,6 +71,7 @@ type TokenStream { } +// 🟑 gated β€” predicate-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: lex-rule-token-class-query β€” bind TASKS.md T-6/T-7 β€” dissolve-on-arrival: substrate-derived LexRule token-class membership query over the lexical rule coproduct; forbidden: duplicating LexRule arm matches outside this std query. fn lex_rule_token_class_member(rule: LexRule, token_class: Symbol) -> Bool { match rule { TokenRule { token_class: c, pattern: _ } => c == token_class From 341df4e5f956d8ea75f3fb0e9f38881feb9f49ab Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 14:26:20 +0000 Subject: [PATCH 08/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/grammar.dag | 2 +- src/v4/std/lexing.dag | 10 +++++----- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index 31908614cc2..6c8df5e894a 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -1,6 +1,6 @@ // src/v4/std/grammar.dag // Scope: canonical grammar model shared by compiler stages and target-language specs. -// Anchor: THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-7. +// Anchor: https://en.wikipedia.org/wiki/Formal_grammar + https://en.wikipedia.org/wiki/Parsing + THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-7. // Status: T-7 grammar data carriers; parser implementation remains in v4.compiler.parse. module v4.std.grammar diff --git a/src/v4/std/lexing.dag b/src/v4/std/lexing.dag index d7b95fd8cf2..cd5f6660b6d 100644 --- a/src/v4/std/lexing.dag +++ b/src/v4/std/lexing.dag @@ -1,6 +1,6 @@ // src/v4/std/lexing.dag // Scope: canonical lexical model shared by compiler stages and target-language specs. -// Anchor: THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-6. +// Anchor: https://en.wikipedia.org/wiki/Lexical_analysis + THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-6. // Status: T-6 lexical data carriers; lexer implementation remains in v4.compiler.tokenize. module v4.std.lexing @@ -11,7 +11,7 @@ import v4.std.logic { Bool } import v4.std.node { Symbol } import v4.std.text { Char, String } -// 🟑 coproduct dissolution β€” CP-1b item 13a; lexical data is modeled, per-arm lexer morphism witness remains gated. +// 🟑 coproduct dissolution β€” feature:t6-lex-char-class-morphism β€” consumer:v4.compiler.tokenize.char_in_class β€” bind TASKS.md T-6 β€” dissolve-on-arrival: substrate-derived LexCharClass membership morphism replaces per-arm character-range predicates; forbidden: adding LexCharClass arms without the morphism consumer. type LexCharClass = WhitespaceChar | DigitChar @@ -23,7 +23,7 @@ type LexCharClass | BlockCommentTextChar -// 🟑 coproduct dissolution β€” CP-1b item 13b; declarative parse/emit pattern data is modeled, bidirectional grammar carrier convergence remains gated. +// 🟑 coproduct dissolution β€” feature:CP-1b-bidirectional-grammar-carrier β€” consumer:v4.compiler.tokenize.lex_match_pattern/v4.compiler.translate.lex_rules_literal_for_class β€” bind TASKS.md T-6/T-7/T-10 β€” dissolve-on-arrival: LexPattern converges with GrammarExpr on one declarative bidirectional concrete-syntax model; forbidden: parallel lexical and grammar production algebras without explicit structural justification. type LexPattern = EmptyPattern | LiteralPattern { text: String } @@ -38,7 +38,7 @@ type LexPattern | DelimitedPattern { open: LexPattern, body: LexPattern, close: LexPattern } -// 🟑 coproduct dissolution β€” CP-1b item 13c; token/trivia rule data is modeled, per-arm lexer morphism witness remains gated. +// 🟑 coproduct dissolution β€” feature:t6-lex-rule-morphism β€” consumer:v4.compiler.tokenize.lex_try_rule/std.lexing.lex_rule_token_class_member β€” bind TASKS.md T-6 β€” dissolve-on-arrival: substrate-derived LexRule fold/projection covers token/trivia rule consumers; forbidden: duplicating LexRule arm matches outside this std query and tokenizer walk. type LexRule = TokenRule { token_class: Symbol, pattern: LexPattern } | TriviaRule { pattern: LexPattern } @@ -51,7 +51,7 @@ type LexRuleSet { } -// 🟑 coproduct dissolution β€” CP-1b item 13d; modeled rule data is present, generic lexical walk realized. +// 🟑 coproduct dissolution β€” feature:t6-lex-rules-language-projection β€” consumer:v4.compiler.tokenize.tokenize/v4.compiler.target_carriers.TargetModel.lex β€” bind TASKS.md T-6/T-11 β€” dissolve-on-arrival: LanguageModel lexical projection carries explicit non-empty rule-set or void-language evidence, replacing VoidLexRules staging; forbidden: treating VoidLexRules as an unbounded default. type LexRules = VoidLexRules | ModeledLexRules { root: LexRuleSet } From c5eb82481fb6308a582e117c4eb45a97503f9fa3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 14:30:58 +0000 Subject: [PATCH 09/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/grammar.dag | 1 + 1 file changed, 1 insertion(+) diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index 6c8df5e894a..a63a6f5d6c7 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -113,6 +113,7 @@ fn grammar_empty_node() -> Node { } +// 🟑 gated β€” walker-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: grammar-expr-node-projection β€” bind TASKS.md T-7/T-10 β€” dissolve-on-arrival: substrate-derived GrammarExpr fold/projection to Node replaces this recursive coproduct walker; forbidden: duplicating GrammarExpr arm re-encoders outside this std projection. fn grammar_expr_to_node(expr: GrammarExpr) -> Node { match expr { Terminal { token_class: token_class } => From 8a4dc2f62dba8d0ab836e86d2f6f84d387d24510 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 14:44:15 +0000 Subject: [PATCH 10/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/grammar.dag | 2 +- src/v4/std/lexing.dag | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index a63a6f5d6c7..65214fcb410 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -113,7 +113,7 @@ fn grammar_empty_node() -> Node { } -// 🟑 gated β€” walker-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: grammar-expr-node-projection β€” bind TASKS.md T-7/T-10 β€” dissolve-on-arrival: substrate-derived GrammarExpr fold/projection to Node replaces this recursive coproduct walker; forbidden: duplicating GrammarExpr arm re-encoders outside this std projection. +// 🟑 gated β€” walker-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: grammar-expr-node-projection β€” bind node://adhoc-2145db6b-69a β€” dissolve-on-arrival: substrate-derived GrammarExpr fold/projection to Node replaces this recursive coproduct walker; forbidden: duplicating GrammarExpr arm re-encoders outside this std projection. fn grammar_expr_to_node(expr: GrammarExpr) -> Node { match expr { Terminal { token_class: token_class } => diff --git a/src/v4/std/lexing.dag b/src/v4/std/lexing.dag index cd5f6660b6d..ac0a78ae1e1 100644 --- a/src/v4/std/lexing.dag +++ b/src/v4/std/lexing.dag @@ -71,7 +71,7 @@ type TokenStream { } -// 🟑 gated β€” predicate-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: lex-rule-token-class-query β€” bind TASKS.md T-6/T-7 β€” dissolve-on-arrival: substrate-derived LexRule token-class membership query over the lexical rule coproduct; forbidden: duplicating LexRule arm matches outside this std query. +// 🟑 gated β€” predicate-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: lex-rule-token-class-query β€” bind node://adhoc-2145db6b-69a β€” dissolve-on-arrival: substrate-derived LexRule token_class projection + TokenRule discriminant query; forbidden: duplicating LexRule arm matches outside this std query or laundering through local folds. fn lex_rule_token_class_member(rule: LexRule, token_class: Symbol) -> Bool { match rule { TokenRule { token_class: c, pattern: _ } => c == token_class From b7f569d3591cb0872af6a32806b88a48c6395d33 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 15:03:30 +0000 Subject: [PATCH 11/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/02_parse.dag | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 41884cc0d52..6d9d91784f2 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -32,7 +32,10 @@ import v4.std.grammar { Terminal, ValidatedGrammarRoot, VoidGrammar, + grammar_empty_node, grammar_named_edge, + grammar_sequence_left_node_projection, + grammar_sequence_right_node_projection, grammar_to_node } From 77a19f34757e55217c92f12265e86670328eeee3 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 15:10:59 +0000 Subject: [PATCH 12/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/std/grammar.dag | 146 +++++++++++++++++++---------------------- 1 file changed, 69 insertions(+), 77 deletions(-) diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index 55860ca3a70..11d272f7080 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -1,7 +1,6 @@ // src/v4/std/grammar.dag -<<<<<<< HEAD +// Grounds in: https://en.wikipedia.org/wiki/Formal_grammar, https://en.wikipedia.org/wiki/Context-free_grammar, https://en.wikipedia.org/wiki/Parsing // Scope: canonical grammar model shared by compiler stages and target-language specs. -// Anchor: https://en.wikipedia.org/wiki/Formal_grammar + https://en.wikipedia.org/wiki/Parsing + THESIS.md "Compiler-std consolidation" + src/v4/TASKS.md T-7. // Status: T-7 grammar data carriers; parser implementation remains in v4.compiler.parse. module v4.std.grammar @@ -12,6 +11,69 @@ import v4.std.lexing { LexRules } import v4.std.logic { Bool } import v4.std.node { Atom, Conj, Edge, Named, Node, NodeFold, Symbol, TypeNode, fold_node } +// "What is a terminal symbol?" +// Ref: https://en.wikipedia.org/wiki/Terminal_and_nonterminal_symbols +// A terminal is a symbol drawn from the terminal alphabet Ξ£. It cannot appear +// as the left-hand side of any production rule; it represents an atomic +// input token that terminates a derivation. +type FormalTerminal { + identity: Symbol +} + + +// "What is a nonterminal symbol?" +// A nonterminal is a symbol drawn from the nonterminal set N. It may appear +// as the left-hand side of a production rule; it represents a syntactic +// category subject to rewriting. +type FormalNonterminal { + identity: Symbol +} + + +// 🟒 coproduct dissolution β€” CP-3229-GREEN-TERMINAL. +// "What is an element of the grammar vocabulary (N βˆͺ Ξ£)?" +// Ref: https://en.wikipedia.org/wiki/Formal_grammar#Formal_definition +// A grammar symbol is either a terminal or a nonterminal. Sequences of +// grammar symbols form the right-hand sides of production rules. +type FormalGrammarSymbol + = FormalTerminalOccurrence { terminal: FormalTerminal } + | FormalNonterminalOccurrence { nonterminal: FormalNonterminal } + + +// "What is a production rule?" +// Ref: https://en.wikipedia.org/wiki/Production_(computer_science) +// In a context-free grammar: A β†’ Ξ± where A ∈ N and Ξ± ∈ (N βˆͺ Ξ£)*. +// The left-hand side is a single nonterminal; the right-hand side is +// a (possibly empty) sequence of grammar symbols. +type FormalProduction { + lhs: FormalNonterminal + rhs: List +} + + +// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: v4.compiler.parse operational grammar types (ParseGrammar, GrammarExpr, GrammarProduction) converge onto this canonical substrate; this file is the dissolution destination, parse.dag operational types dissolve into it. +// 🟑 gated β€” feature:grammar-well-formed-witness β€” FormalGrammar carries four representable invalid states: (1) start βˆ‰ nonterminals, (2) FormalProduction.lhs not in N, (3) FormalProduction.rhs symbols not drawn from NβˆͺΞ£, (4) N∩Σ overlap (FormalTerminal and FormalNonterminal both carry identity: Symbol). Dissolve-on: consumers require WellFormedFormalGrammar (below) not bare FormalGrammar; bare FormalGrammar becomes internal construction only. +// "What is a formal grammar?" +// Ref: https://en.wikipedia.org/wiki/Formal_grammar +// G = (N, Ξ£, P, S) β€” the four-component definition of a formal language: +// N (nonterminals): finite set of nonterminal symbols +// Ξ£ (terminals): finite set of terminal symbols, disjoint from N +// P (productions): finite collection of production rules +// S (start): designated start symbol, S ∈ N +type FormalGrammar { + nonterminals: Set + terminals: Set + productions: List + start: FormalNonterminal +} + + +// 🟑 gated β€” feature:grammar-well-formed-witness β€” witness that a FormalGrammar value satisfies all four invariants: (1) start∈N, (2) each FormalProduction.lhs∈N, (3) each FormalProduction.rhs symbol∈NβˆͺΞ£, (4) N∩Σ=βˆ…. Dissolve-on: validate_grammar(g: FormalGrammar) -> Witness is the only constructor; sub-invariant checks require set-membership fold over grammar alphabets. +type WellFormedFormalGrammar { + grammar: FormalGrammar +} + + // 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: GrammarExpr converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. type GrammarExpr = Terminal { token_class: Symbol } @@ -45,15 +107,15 @@ type ValidatedGrammarRoot { } -// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: Grammar converges with LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. -type Grammar +// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: ParseGrammar converges with FormalGrammar/LexPattern on single declarative bidirectional grammar model; forbidden: parallel production algebras without explicit structural justification. +type ParseGrammar = VoidGrammar | ModeledGrammar { root: GrammarRoot } type GrammarSchema { lex: LexRules - grammar: Grammar + grammar: ParseGrammar } @@ -237,7 +299,7 @@ fn grammar_root_to_node(root: GrammarRoot) -> Node { } -fn grammar_to_node(grammar: Grammar) -> Node { +fn grammar_to_node(grammar: ParseGrammar) -> Node { match grammar { VoidGrammar => grammar_empty_node() ModeledGrammar { root: root } => grammar_root_to_node(root: root) @@ -279,76 +341,6 @@ fn grammar_symbol_fold_state(n: Node, sym: Symbol) -> GrammarSymbolFoldState { } -fn grammar_carries_symbol(grammar: Grammar, sym: Symbol) -> Bool { +fn grammar_carries_symbol(grammar: ParseGrammar, sym: Symbol) -> Bool { grammar_symbol_fold_state(n: grammar_to_node(grammar: grammar), sym: sym).found } -======= -// Grounds in: https://en.wikipedia.org/wiki/Formal_grammar, https://en.wikipedia.org/wiki/Context-free_grammar -// Scope: canonical formal grammar types β€” Terminal, Nonterminal, Production, Grammar -// Owns: Terminal, Nonterminal, GrammarSymbol, Production, Grammar, WellFormedGrammar -// Consumes: v4.std.node, v4.std.collection -// Status: substrate canonical declaration; v4.compiler.parse operational grammar types -// gate to converge here under feature:CP-1b-bidirectional-grammar-carrier (TASKS.md T-6/T-7). - -module v4.std.grammar - -import v4.std.node { Symbol } -import v4.std.collection { List, Set } - -// "What is a terminal symbol?" -// Ref: https://en.wikipedia.org/wiki/Terminal_and_nonterminal_symbols -// A terminal is a symbol drawn from the terminal alphabet Ξ£. It cannot appear -// as the left-hand side of any production rule; it represents an atomic -// input token that terminates a derivation. -type Terminal { - identity: Symbol -} - -// "What is a nonterminal symbol?" -// A nonterminal is a symbol drawn from the nonterminal set N. It may appear -// as the left-hand side of a production rule; it represents a syntactic -// category subject to rewriting. -type Nonterminal { - identity: Symbol -} - -// 🟒 coproduct dissolution β€” CP-3229-GREEN-TERMINAL. -// "What is an element of the grammar vocabulary (N βˆͺ Ξ£)?" -// Ref: https://en.wikipedia.org/wiki/Formal_grammar#Formal_definition -// A grammar symbol is either a terminal or a nonterminal. Sequences of -// grammar symbols form the right-hand sides of production rules. -type GrammarSymbol - = TerminalOccurrence { terminal: Terminal } - | NonterminalOccurrence { nonterminal: Nonterminal } - -// "What is a production rule?" -// Ref: https://en.wikipedia.org/wiki/Production_(computer_science) -// In a context-free grammar: A β†’ Ξ± where A ∈ N and Ξ± ∈ (N βˆͺ Ξ£)*. -// The left-hand side is a single nonterminal; the right-hand side is -// a (possibly empty) sequence of grammar symbols. -type Production { - lhs: Nonterminal - rhs: List -} - -// 🟑 gated β€” feature:CP-1b-bidirectional-grammar-carrier β€” bind TASKS.md T-6/T-7 β€” dissolve-on: v4.compiler.parse grammar types (Grammar, GrammarExpr, GrammarProduction) converge onto this canonical substrate; this file is the dissolution destination, parse.dag operational types dissolve into it. -// 🟑 gated β€” feature:grammar-well-formed-witness β€” Grammar carries four representable invalid states: (1) start βˆ‰ nonterminals, (2) Production.lhs not in N, (3) Production.rhs symbols not drawn from NβˆͺΞ£, (4) N∩Σ overlap (Terminal and Nonterminal both carry identity: Symbol). Dissolve-on: consumers require WellFormedGrammar (below) not bare Grammar; bare Grammar becomes internal construction only. -// "What is a formal grammar?" -// Ref: https://en.wikipedia.org/wiki/Formal_grammar -// G = (N, Ξ£, P, S) β€” the four-component definition of a formal language: -// N (nonterminals): finite set of nonterminal symbols -// Ξ£ (terminals): finite set of terminal symbols, disjoint from N -// P (productions): finite collection of production rules -// S (start): designated start symbol, S ∈ N -type Grammar { - nonterminals: Set - terminals: Set - productions: List - start: Nonterminal -} - -// 🟑 gated β€” feature:grammar-well-formed-witness β€” witness that a Grammar value satisfies all four invariants: (1) start∈N, (2) each Production.lhs∈N, (3) each Production.rhs symbol∈NβˆͺΞ£, (4) N∩Σ=βˆ…. Dissolve-on: validate_grammar(g: Grammar) -> Witness is the only constructor; sub-invariant checks require set-membership fold over grammar alphabets. -type WellFormedGrammar { - grammar: Grammar -} ->>>>>>> origin/main From bdf1c09a67326be807ffb6b1bf95ed9cad456797 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 15:12:26 +0000 Subject: [PATCH 13/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/02_parse.dag | 4 ++-- src/v4/extdeps/languages/dag.dag | 8 ++++---- src/v4/extdeps/languages/java.dag | 8 ++++---- src/v4/extdeps/languages/kotlin.dag | 8 ++++---- src/v4/extdeps/languages/rust.dag | 6 +++--- src/v4/extdeps/languages/swift.dag | 4 ++-- src/v4/extdeps/languages/typescript.dag | 4 ++-- src/v4/extdeps/languages/wasm.dag | 6 +++--- 8 files changed, 24 insertions(+), 24 deletions(-) diff --git a/src/v4/compiler/02_parse.dag b/src/v4/compiler/02_parse.dag index 6d9d91784f2..7568f590098 100644 --- a/src/v4/compiler/02_parse.dag +++ b/src/v4/compiler/02_parse.dag @@ -20,7 +20,7 @@ import v4.std.witness { Holds, Violates, Witness } import v4.std.lexing { Token, TokenStream } import v4.std.grammar { Choice, - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -868,7 +868,7 @@ fn parse_production(tokens: List, validated: ValidatedGrammarRoot, produc } -fn parse(tokens: TokenStream, grammar: Grammar) -> Outcome { +fn parse(tokens: TokenStream, grammar: ParseGrammar) -> Outcome { let at = port_locus(port: parse_stage_locus_port) let ntok = length(xs: tokens.tokens) let grammar_node = grammar_to_node(grammar: grammar) diff --git a/src/v4/extdeps/languages/dag.dag b/src/v4/extdeps/languages/dag.dag index d032318e830..a425944333a 100644 --- a/src/v4/extdeps/languages/dag.dag +++ b/src/v4/extdeps/languages/dag.dag @@ -9,7 +9,7 @@ module v4.extdeps.languages.dag import v4.std.collection { List, Set } import v4.std.grammar { - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -196,7 +196,7 @@ data dag_surface_fn_literal: Symbol = dag_surface_fn_literal type DagLanguageModel { lex: LexRules - grammar: Grammar + grammar: ParseGrammar language_identity: Symbol canonical_symbols: Set } @@ -1667,12 +1667,12 @@ fn dag_wave1_grammar_root() -> GrammarRoot { } -fn dag_wave1_g0_void_grammar() -> Grammar { +fn dag_wave1_g0_void_grammar() -> ParseGrammar { VoidGrammar } -fn dag_wave1_grammar() -> Grammar { +fn dag_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: dag_wave1_grammar_root() } } diff --git a/src/v4/extdeps/languages/java.dag b/src/v4/extdeps/languages/java.dag index 1e75bb5873d..ebc59a13afb 100644 --- a/src/v4/extdeps/languages/java.dag +++ b/src/v4/extdeps/languages/java.dag @@ -7,7 +7,7 @@ module v4.extdeps.languages.java import v4.std.grammar { Choice, - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -144,7 +144,7 @@ type OverflowAction type JavaLanguageModel { lex: LexRules - grammar: Grammar + grammar: ParseGrammar language_identity: Symbol canonical_symbols: Set core: ModelCore @@ -1030,7 +1030,7 @@ fn java_wave1_grammar_root() -> GrammarRoot { GrammarRoot { start: java_production_mvp1_method_add, productions: [start], sync_tokens: grammar_empty_sync_tokens() } } -fn java_wave1_grammar() -> Grammar { +fn java_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: java_wave1_grammar_root() } } @@ -1450,7 +1450,7 @@ fn java_wave2_grammar_root() -> GrammarRoot { } } -fn java_wave2_grammar() -> Grammar { +fn java_wave2_grammar() -> ParseGrammar { ModeledGrammar { root: java_wave2_grammar_root() } } diff --git a/src/v4/extdeps/languages/kotlin.dag b/src/v4/extdeps/languages/kotlin.dag index 0371935f651..1e1f0ae721e 100644 --- a/src/v4/extdeps/languages/kotlin.dag +++ b/src/v4/extdeps/languages/kotlin.dag @@ -6,7 +6,7 @@ module v4.extdeps.languages.kotlin import v4.std.grammar { - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -148,7 +148,7 @@ type KotlinNonNumericPrimitiveFacts { type KotlinLanguageModel { lex: LexRules - grammar: Grammar + grammar: ParseGrammar language_identity: Symbol canonical_symbols: Set core: ModelCore @@ -891,7 +891,7 @@ fn kotlin_mvp1_return_add_expr_node() -> Node { } } -// Grammar-as-data function item: name, param bindings, Int signature, return `x + y` expression facts. +// ParseGrammar-as-data function item: name, param bindings, Int signature, return `x + y` expression facts. fn kotlin_mvp1_emitted_add_fn_node() -> Node { Node { kind: TypeNode { connective: Conj }, @@ -1229,7 +1229,7 @@ fn kotlin_wave1_grammar_root() -> GrammarRoot { } } -fn kotlin_wave1_grammar() -> Grammar { +fn kotlin_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: kotlin_wave1_grammar_root() } } diff --git a/src/v4/extdeps/languages/rust.dag b/src/v4/extdeps/languages/rust.dag index d88fcbad62f..1593c200ce2 100644 --- a/src/v4/extdeps/languages/rust.dag +++ b/src/v4/extdeps/languages/rust.dag @@ -6,7 +6,7 @@ module v4.extdeps.languages.rust import v4.std.grammar { - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -224,7 +224,7 @@ type OverflowDisposition { type RustLanguageModel { lex: LexRules - grammar: Grammar + grammar: ParseGrammar language_identity: Symbol canonical_symbols: Set core: ModelCore @@ -1429,7 +1429,7 @@ fn rust_wave1_grammar_root() -> GrammarRoot { GrammarRoot { start: rust_production_mvp1_fn_add, productions: [start], sync_tokens: grammar_empty_sync_tokens() } } -fn rust_wave1_grammar() -> Grammar { +fn rust_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: rust_wave1_grammar_root() } } diff --git a/src/v4/extdeps/languages/swift.dag b/src/v4/extdeps/languages/swift.dag index d6f4175a67d..30c8636fce4 100644 --- a/src/v4/extdeps/languages/swift.dag +++ b/src/v4/extdeps/languages/swift.dag @@ -11,7 +11,7 @@ module v4.extdeps.languages.swift import v4.std.grammar { Choice, - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -1472,7 +1472,7 @@ fn swift_wave1_grammar_root() -> GrammarRoot { } } -fn swift_wave1_grammar() -> Grammar { +fn swift_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: swift_wave1_grammar_root() } } diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag index 29da0b7d51d..664baedc420 100644 --- a/src/v4/extdeps/languages/typescript.dag +++ b/src/v4/extdeps/languages/typescript.dag @@ -10,7 +10,7 @@ module v4.extdeps.languages.typescript import v4.std.grammar { - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -733,7 +733,7 @@ fn ts_wave1_grammar_root() -> GrammarRoot { GrammarRoot { start: ts_production_mvp1_fn_add, productions: [start], sync_tokens: grammar_empty_sync_tokens() } } -fn ts_wave1_grammar() -> Grammar { +fn ts_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: ts_wave1_grammar_root() } } diff --git a/src/v4/extdeps/languages/wasm.dag b/src/v4/extdeps/languages/wasm.dag index 7d56deca074..5fc37e36a42 100644 --- a/src/v4/extdeps/languages/wasm.dag +++ b/src/v4/extdeps/languages/wasm.dag @@ -11,7 +11,7 @@ module v4.extdeps.languages.wasm import v4.std.grammar { Choice, - Grammar, + ParseGrammar, GrammarExpr, GrammarProduction, GrammarRoot, @@ -125,7 +125,7 @@ type WasmFloatPrimitiveFacts { // 🟒 grounded. type WasmLanguageModel { lex: LexRules - grammar: Grammar + grammar: ParseGrammar language_identity: Symbol canonical_symbols: Set core: ModelCore @@ -1558,7 +1558,7 @@ fn wasm_wave1_grammar_root() -> GrammarRoot { } } -fn wasm_wave1_grammar() -> Grammar { +fn wasm_wave1_grammar() -> ParseGrammar { ModeledGrammar { root: wasm_wave1_grammar_root() } } From de2edcbe6d45e96facdc00b63299834a69dbfd35 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 15:29:05 +0000 Subject: [PATCH 14/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/compiler/00_compile.dag | 3 ++- src/v4/compiler/05_emit.dag | 3 ++- src/v4/compiler/06_translate.dag | 3 ++- src/v4/compiler/07_target_carriers.dag | 16 +++------------- src/v4/extdeps/languages/cpp.dag | 2 +- src/v4/extdeps/languages/go.dag | 2 +- src/v4/extdeps/languages/java.dag | 2 +- src/v4/extdeps/languages/kotlin.dag | 2 +- src/v4/extdeps/languages/python.dag | 2 +- src/v4/extdeps/languages/rust.dag | 2 +- src/v4/extdeps/languages/swift.dag | 2 +- src/v4/extdeps/languages/typescript.dag | 2 +- src/v4/extdeps/languages/wasm.dag | 2 +- src/v4/std/target_model.dag | 15 +++++++++++++-- .../empty_required_lenses_skip_gate.dag | 2 +- .../rejecting_lens_blocks_before_compile.dag | 2 +- .../claim/manual/infer_emit_compile_anchor.dag | 3 ++- .../claim/manual/mvp1_rust_add_translate.dag | 3 ++- .../validate_then_compile_public_terminal.dag | 2 +- src/v4/workflow/bootstrap.dag | 3 ++- 20 files changed, 40 insertions(+), 33 deletions(-) diff --git a/src/v4/compiler/00_compile.dag b/src/v4/compiler/00_compile.dag index cc174999f58..40c0e816c84 100644 --- a/src/v4/compiler/00_compile.dag +++ b/src/v4/compiler/00_compile.dag @@ -20,7 +20,8 @@ import v4.compiler.normalize { normalize } import v4.compiler.parse { parse } import v4.compiler.resolve { resolve } import v4.compiler.tokenize { tokenize } -import v4.compiler.target_carriers { TargetModel, TargetSource } +import v4.compiler.target_carriers { TargetSource } +import v4.std.target_model { TargetModel } import v4.extdeps.languages.dag { dag_language_model_wave1, qualified_name_from_module_node } import v4.lens.fact_density { fact_density_hollow_alias_gate } import v4.std.algebra { Cons, Empty, FreeMonoid, list_append, list_snoc_item } diff --git a/src/v4/compiler/05_emit.dag b/src/v4/compiler/05_emit.dag index c6b7bf5d621..df9e646abe8 100644 --- a/src/v4/compiler/05_emit.dag +++ b/src/v4/compiler/05_emit.dag @@ -8,7 +8,8 @@ module v4.compiler.emit -import v4.compiler.target_carriers { TargetModel, TargetSource } +import v4.compiler.target_carriers { TargetSource } +import v4.std.target_model { TargetModel } import v4.compiler.infer { InferredTree } import v4.compiler.translate { TargetNodeTree, diff --git a/src/v4/compiler/06_translate.dag b/src/v4/compiler/06_translate.dag index 49a0442524d..4220b69f7e2 100644 --- a/src/v4/compiler/06_translate.dag +++ b/src/v4/compiler/06_translate.dag @@ -12,7 +12,8 @@ module v4.compiler.translate -import v4.compiler.target_carriers { TargetModel, TargetSource } +import v4.compiler.target_carriers { TargetSource } +import v4.std.target_model { TargetModel } import v4.compiler.infer { InferredTree, canonical_grounding_for_node } import v4.std.coercion { CoercionCandidateSet, diff --git a/src/v4/compiler/07_target_carriers.dag b/src/v4/compiler/07_target_carriers.dag index 4478e696298..52ffb3d56ff 100644 --- a/src/v4/compiler/07_target_carriers.dag +++ b/src/v4/compiler/07_target_carriers.dag @@ -1,25 +1,15 @@ // src/v4/compiler/07_target_carriers.dag -// Scope: Shared compile-stage language/target carriers β€” breaks compile ↔ emit import cycle. -// Status: Wave-5-A β€” single authority for target projection carriers. +// Scope: Shared compile-stage language/source aliases β€” breaks compile ↔ emit import cycle. +// Status: Wave-5-A β€” TargetModel authority lives in v4.std.target_model. // Anchor: docs/design-v4-compiler-homomorphism.md module v4.compiler.target_carriers -import v4.std.lexing { LexRules, VoidLexRules } -import v4.std.collection { Map, empty_map } -import v4.std.node { Node, Symbol } +import v4.std.node { Node } import v4.std.text { String } type LanguageModel = Node -type TargetModelBundle { - bundle: Node - lex: LexRules - binding_spellings: Map - authority_source_text: String -} -type TargetModel = TargetModelBundle - type TargetSource = String diff --git a/src/v4/extdeps/languages/cpp.dag b/src/v4/extdeps/languages/cpp.dag index 8f6cc8699a5..64589e1a490 100644 --- a/src/v4/extdeps/languages/cpp.dag +++ b/src/v4/extdeps/languages/cpp.dag @@ -20,7 +20,7 @@ import v4.std.lexing { ModeledLexRules, TokenRule } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.logic { Bool, bool_boolean_algebra } import v4.std.algebra { BooleanAlgebra, diff --git a/src/v4/extdeps/languages/go.dag b/src/v4/extdeps/languages/go.dag index 23c53b22715..92bf5eda2a7 100644 --- a/src/v4/extdeps/languages/go.dag +++ b/src/v4/extdeps/languages/go.dag @@ -20,7 +20,7 @@ import v4.std.lexing { ModeledLexRules, TokenRule } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.collection { List, Map, empty_map, map_insert } import v4.std.model_core { AlgebraInhabitanceDecl, diff --git a/src/v4/extdeps/languages/java.dag b/src/v4/extdeps/languages/java.dag index ebc59a13afb..f99c8c55ee3 100644 --- a/src/v4/extdeps/languages/java.dag +++ b/src/v4/extdeps/languages/java.dag @@ -50,7 +50,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/extdeps/languages/kotlin.dag b/src/v4/extdeps/languages/kotlin.dag index 1e1f0ae721e..d4f6a418a9f 100644 --- a/src/v4/extdeps/languages/kotlin.dag +++ b/src/v4/extdeps/languages/kotlin.dag @@ -44,7 +44,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/extdeps/languages/python.dag b/src/v4/extdeps/languages/python.dag index b6bf424473e..8673a57aaec 100644 --- a/src/v4/extdeps/languages/python.dag +++ b/src/v4/extdeps/languages/python.dag @@ -24,7 +24,7 @@ import v4.std.lexing { ModeledLexRules, TokenRule } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.collection { List, Map, empty_map, map_insert } import v4.std.model_core { AlgebraInhabitanceDecl, diff --git a/src/v4/extdeps/languages/rust.dag b/src/v4/extdeps/languages/rust.dag index 1593c200ce2..13497c9424e 100644 --- a/src/v4/extdeps/languages/rust.dag +++ b/src/v4/extdeps/languages/rust.dag @@ -54,7 +54,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/extdeps/languages/swift.dag b/src/v4/extdeps/languages/swift.dag index 30c8636fce4..6b127470b03 100644 --- a/src/v4/extdeps/languages/swift.dag +++ b/src/v4/extdeps/languages/swift.dag @@ -62,7 +62,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/extdeps/languages/typescript.dag b/src/v4/extdeps/languages/typescript.dag index 664baedc420..d954886d4bb 100644 --- a/src/v4/extdeps/languages/typescript.dag +++ b/src/v4/extdeps/languages/typescript.dag @@ -47,7 +47,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/extdeps/languages/wasm.dag b/src/v4/extdeps/languages/wasm.dag index 5fc37e36a42..c0f1d5451e2 100644 --- a/src/v4/extdeps/languages/wasm.dag +++ b/src/v4/extdeps/languages/wasm.dag @@ -60,7 +60,7 @@ import v4.std.model_core { primitive_fact_axis_width } import v4.std.witness { Holds, Violates } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.target_model { concrete_syntax_token_field_binding, concrete_syntax_token_field_class, diff --git a/src/v4/std/target_model.dag b/src/v4/std/target_model.dag index 3d943971919..7b3de81c4f5 100644 --- a/src/v4/std/target_model.dag +++ b/src/v4/std/target_model.dag @@ -1,10 +1,21 @@ // src/v4/std/target_model.dag -// Scope: TargetModel Conj-bundle edge keys + grammar-relation protocol symbols. +// Scope: TargetModel carrier + Conj-bundle edge keys + grammar-relation protocol symbols. // Status: single authority per INVARIANTS P2 β€” consumers import; do not redeclare. module v4.std.target_model -import v4.std.node { Symbol } +import v4.std.collection { Map } +import v4.std.lexing { LexRules } +import v4.std.node { Node, Symbol } +import v4.std.text { String } + +type TargetModelBundle { + bundle: Node + lex: LexRules + binding_spellings: Map + authority_source_text: String +} +type TargetModel = TargetModelBundle data target_model_edge_selection_policy: Symbol = target_model_edge_selection_policy data target_model_edge_declared_inhabitants: Symbol = target_model_edge_declared_inhabitants diff --git a/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag b/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag index ed5f715d201..9ad91056a36 100644 --- a/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag +++ b/src/v4/test/claim/lens_application/empty_required_lenses_skip_gate.dag @@ -12,7 +12,7 @@ import v4.compiler.compile { compile_lens_gate_rejected, validate_then_compile } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.lexing { VoidLexRules } import v4.std.diagnostic { Accepted, NonEmptyDiagnostics, Outcome, Rejected } import v4.std.logic { Bool } diff --git a/src/v4/test/claim/lens_application/rejecting_lens_blocks_before_compile.dag b/src/v4/test/claim/lens_application/rejecting_lens_blocks_before_compile.dag index 4d5c7dfef37..1822169d5d7 100644 --- a/src/v4/test/claim/lens_application/rejecting_lens_blocks_before_compile.dag +++ b/src/v4/test/claim/lens_application/rejecting_lens_blocks_before_compile.dag @@ -14,7 +14,7 @@ import v4.compiler.compile { validate_then_compile } import v4.compiler.infer { InferredTree } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.diagnostic { Accepted, Outcome, PortLocus, Rejected, outcome_rejected } import v4.std.logic { Bool } import v4.std.algebra { Empty } diff --git a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag index f4398deac84..582265388d9 100644 --- a/src/v4/test/claim/manual/infer_emit_compile_anchor.dag +++ b/src/v4/test/claim/manual/infer_emit_compile_anchor.dag @@ -15,7 +15,8 @@ import v4.compiler.compile { compile_inferred, compile_ingest_staging } -import v4.compiler.target_carriers { TargetModel, TargetSource } +import v4.compiler.target_carriers { TargetSource } +import v4.std.target_model { TargetModel } import v4.std.lexing { VoidLexRules } import v4.compiler.emit { emit } import v4.compiler.infer { diff --git a/src/v4/test/claim/manual/mvp1_rust_add_translate.dag b/src/v4/test/claim/manual/mvp1_rust_add_translate.dag index 7d08ea6f04f..5f342451dfe 100644 --- a/src/v4/test/claim/manual/mvp1_rust_add_translate.dag +++ b/src/v4/test/claim/manual/mvp1_rust_add_translate.dag @@ -56,7 +56,8 @@ import v4.extdeps.languages.rust { rust_tag_two_complement_wrap } import v4.compiler.infer { InferredFacts, InferredTree } -import v4.compiler.target_carriers { TargetModel, TargetSource } +import v4.compiler.target_carriers { TargetSource } +import v4.std.target_model { TargetModel } import v4.test.claim.lens_common.infer_fixture { claim_inferred_facts_witness } import v4.test.claim.manual.infer_ground_add_mvp { claim_hash_placeholder, diff --git a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag index d1584f54e70..4eafcd594d7 100644 --- a/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag +++ b/src/v4/test/claim/manual/validate_then_compile_public_terminal.dag @@ -19,7 +19,7 @@ import v4.compiler.compile { validate_then_compile } import v4.compiler.infer { InferredTree } -import v4.compiler.target_carriers { TargetModel } +import v4.std.target_model { TargetModel } import v4.std.lexing { VoidLexRules } import v4.test.claim.manual.infer_ground_add_mvp { fixture_add_resolved_tree } import v4.std.diagnostic { diff --git a/src/v4/workflow/bootstrap.dag b/src/v4/workflow/bootstrap.dag index 72141288977..1bbc5b6a7a2 100644 --- a/src/v4/workflow/bootstrap.dag +++ b/src/v4/workflow/bootstrap.dag @@ -9,7 +9,8 @@ import v4.std.node { Atom, Conj, Edge, Hash, Named, Node, Symbol, TypeNode, cont import v4.std.algebra { bag_eq } -import v4.compiler.target_carriers { LanguageModel, TargetModel } +import v4.compiler.target_carriers { LanguageModel } +import v4.std.target_model { TargetModel } import v4.extdeps.languages.rust { rust_mvp1_target_model } import v4.extdeps.runtimes.v4_evaluator { V4EvaluatorRuntime, v4_evaluator_runtime_wave1 } import v4.std.diagnostic {Correction, Diagnostic, Extent, Locus, NoCorrectionReason, Outcome, Accepted, None, diagnostics_singleton} From d85a22c294a8af5c53dcf959473702384810713e Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Thu, 28 May 2026 15:42:19 +0000 Subject: [PATCH 15/15] WIP: Author std/lexing.dag + std/grammar.dag: move LexRule/Grammar/Production --- src/v4/TASKS.md | 33 +++++++++++++++++++++++++++++++++ src/v4/std/grammar.dag | 2 +- src/v4/std/lexing.dag | 2 +- 3 files changed, 35 insertions(+), 2 deletions(-) diff --git a/src/v4/TASKS.md b/src/v4/TASKS.md index 6d301cc43f9..4b6b2146e8a 100644 --- a/src/v4/TASKS.md +++ b/src/v4/TASKS.md @@ -492,6 +492,22 @@ conceptual `(Source, LanguageModel)` spelling. - merged: `src/v4/compiler/01_tokenize.dag` (B2-OMNI, E0 contract) - v3 L2.5 design: `docs/r3-path-b-tokenize-parse-brief-set.md` PB-2 +#### T-6.1: LexRule token-class query dissolution + +**Owner/lane:** T-6 std lexing substrate follow-up. + +**Missing primitive:** substrate-derived `LexRule` token-class projection plus +`TokenRule` discriminant query in `src/v4/std/lexing.dag`. + +**Interim surface:** `lex_rule_token_class_member` / `lex_rule_set_token_class_member` +are allowed only as the shared std query while language slices need canonical symbol +membership and no derived `LexRule` projection exists. + +**Dissolve-on-arrival:** the first PR that lands the projection/query primitive +must delete the hand-written `LexRule` arm match in `lex_rule_token_class_member` +and make `lex_rule_set_token_class_member` consume the substrate query in the same +commit train. No extdeps/compiler-local duplicate predicate may be added meanwhile. + --- ### T-7: compiler/02_parse.dag @@ -515,6 +531,23 @@ syntax-side projection of the landed `LanguageModel = Node` authority in - merged: `src/v4/compiler/02_parse.dag` (B2-OMNI, G0 contract) - v3 L2.5 design: `docs/r3-path-b-tokenize-parse-brief-set.md` PB-3 +#### T-7.1: GrammarExpr node projection dissolution + +**Owner/lane:** T-7 std grammar substrate follow-up. + +**Missing primitive:** substrate-derived `GrammarExpr` fold/projection to canonical +`Node` edges in `src/v4/std/grammar.dag`. + +**Interim surface:** `grammar_expr_to_node` is allowed only as the shared std +projection used by `grammar_to_node` and symbol-membership checks while no +substrate fold exists for `GrammarExpr`. + +**Dissolve-on-arrival:** the first PR that lands the `GrammarExpr` fold/projection +primitive must delete the recursive hand-written coproduct walker in +`grammar_expr_to_node` and route `grammar_to_node` through the substrate projection +in the same commit train. No compiler/extdeps-local `GrammarExpr` re-encoder may +be added meanwhile. + --- ### T-8: compiler/03_normalize.dag + 03_resolve.dag diff --git a/src/v4/std/grammar.dag b/src/v4/std/grammar.dag index a87b4c44209..2c48e40f913 100644 --- a/src/v4/std/grammar.dag +++ b/src/v4/std/grammar.dag @@ -176,7 +176,7 @@ fn grammar_empty_node() -> Node { } -// 🟑 gated β€” walker-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: grammar-expr-node-projection β€” bind node://adhoc-2145db6b-69a β€” dissolve-on-arrival: substrate-derived GrammarExpr fold/projection to Node replaces this recursive coproduct walker; forbidden: duplicating GrammarExpr arm re-encoders outside this std projection. +// 🟑 gated β€” walker-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature:grammar-expr-node-projection β€” bound task: src/v4/TASKS.md Β§T-7.1 (owner/lane: T-7 std grammar substrate follow-up) β€” dissolve-on-arrival: first PR landing substrate-derived GrammarExpr fold/projection to canonical Node edges deletes this recursive coproduct walker and routes grammar_to_node through that projection in the same commit train; forbidden: duplicating GrammarExpr arm re-encoders outside this std projection. fn grammar_expr_to_node(expr: GrammarExpr) -> Node { match expr { Terminal { token_class: token_class } => diff --git a/src/v4/std/lexing.dag b/src/v4/std/lexing.dag index eb88625da07..43199c6192a 100644 --- a/src/v4/std/lexing.dag +++ b/src/v4/std/lexing.dag @@ -73,7 +73,7 @@ type TokenStream { } -// 🟑 gated β€” predicate-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature: lex-rule-token-class-query β€” bind node://adhoc-2145db6b-69a β€” dissolve-on-arrival: substrate-derived LexRule token_class projection + TokenRule discriminant query; forbidden: duplicating LexRule arm matches outside this std query or laundering through local folds. +// 🟑 gated β€” predicate-dissolution interim (docs/modeling-discipline.md Practice 10) β€” feature:lex-rule-token-class-query β€” bound task: src/v4/TASKS.md Β§T-6.1 (owner/lane: T-6 std lexing substrate follow-up) β€” dissolve-on-arrival: first PR landing substrate-derived LexRule token_class projection + TokenRule discriminant query deletes this hand-written arm match and routes lex_rule_set_token_class_member through that query in the same commit train; forbidden: duplicating LexRule arm matches outside this std query or laundering through local folds. fn lex_rule_token_class_member(rule: LexRule, token_class: Symbol) -> Bool { match rule { TokenRule { token_class: c, pattern: _ } => c == token_class