nx_lex.nx source
↩ module page · 104 lines · 4537 B
1// nx_lex.nx -- canonical lexer primitives (source-code whitespace).
2//
3// Distinct from nx_ascii.nx by design: nx_ascii follows POSIX
4// isspace() / isalpha() semantics (broad, including VT and FF for
5// whitespace). nx_lex provides STRICT source-code-oriented variants
6// used by parsers that need precise control over what counts as
7// whitespace.
8//
9// CONSOLIDATION TRAIL (verified via nx_func_compare 2026-05-13):
10//
11// nx_lex_is_ws (4-char: space, tab, LF, CR) replaces 9 byte-identical
12// adapter-local variants:
13// - nx_coq_is_ws (hash 5493497725180460624)
14// - nx_extract_is_ws (hash 5493497725180460624)
15// - nx_hol_is_ws (hash 5493497725180460624)
16// - nx_isa_is_ws (hash 5493497725180460624)
17// - nx_lean_is_ws (hash 5493497725180460624)
18// - nx_mizar_is_ws (hash 5493497725180460624)
19// - nx_mm_is_ws (hash 5493497725180460624)
20// - nx_json_is_ws (semantically equivalent; hex-vs-decimal literals)
21// Why distinct from nx_ascii_is_space: nx_ascii_is_space also accepts
22// 0x0B (vertical tab) and 0x0C (form feed); adapter is_ws was strict
23// to the 4 source-code chars. Preserving the strict semantics here.
24//
25// nx_lex_is_intraline_ws (2-char: space, tab) replaces:
26// - nx_kv_is_ws (record-separator parsers must NOT treat
27// newline as whitespace)
28//
29// genealogy_id: ascii_1968_standard + posix_isspace_traditions
30// + source_code_lexer_conventions
31// lineage_id: character_class_predicate
32// axioms: NX_AX_LOGIC_EXCLUDED_MIDDLE (each c is or is not ws,
33// no third state)
34
35// nx_safety_envelope:
36// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
37// sil_target: SIL1
38// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
39// verdict: NOT_YET_EVALUATED
40
41import "syscalls.nx"
42import "nx_axioms.nx"
43import "nx_ascii.nx"
44
45// Source-code whitespace: SP HT LF CR. Strict 4-character set used by
46// most adapters; deliberately excludes VT/FF (which nx_ascii_is_space
47// accepts).
48func nx_lex_is_ws(c: i64) -> i64 {
49 if c == 32 { return 1 } // ' '
50 if c == 9 { return 1 } // '\t'
51 if c == 10 { return 1 } // '\n'
52 if c == 13 { return 1 } // '\r'
53 return 0
54}
55
56// Intra-line whitespace ONLY: space + tab. Used when newline is a
57// record/statement separator that must be preserved. E.g., KV parsers
58// where each line is one key=value pair.
59func nx_lex_is_intraline_ws(c: i64) -> i64 {
60 if c == 32 { return 1 }
61 if c == 9 { return 1 }
62 return 0
63}
64
65// ===== identifier-continuation variants ================================
66//
67// Many proof-assistant languages allow ' (prime) and / or . (qualified
68// path) in identifier names. These primitives capture two common
69// flavors; the C-style (no prime) lives in nx_ascii_is_id_cont.
70//
71// CONSOLIDATION TRAIL (verified via nx_func_compare 2026-05-13):
72//
73// nx_lex_is_id_cont_math (alpha + _ + digit + ')
74// - nx_hol_is_alnum (hash -3686892484023463762)
75// - nx_isa_is_alnum (hash -3686892484023463762)
76//
77// nx_lex_is_id_cont_qualified (alpha + _ + digit + ' + .)
78// - nx_coq_is_alnum (hash 5501640346889821503)
79// - nx_lean_is_alnum (hash 5501640346889821503)
80//
81// Why distinct from nx_ascii_is_id_cont: that's strict C-style
82// (alpha + digit + _ only), used by C / NishiLang / most modern
83// programming languages. Mathematical proof languages need primes
84// and qualified paths.
85
86// Math-style: alpha + _ + digit + ' (prime). Used by HOL Light and
87// Isabelle/HOL where 'x' or 'helper'' is a valid identifier.
88func nx_lex_is_id_cont_math(c: i64) -> i64 {
89 if nx_ascii_is_id_start(c) == 1 { return 1 }
90 if c >= 48 { if c <= 57 { return 1 } } // 0-9
91 if c == 39 { return 1 } // '
92 return 0
93}
94
95// Qualified-path style: alpha + _ + digit + ' + . (module path).
96// Used by Coq (Nat.add) and Lean (Mathlib.Data.Nat.add_comm) where
97// dots separate qualified module-path components inside one token.
98func nx_lex_is_id_cont_qualified(c: i64) -> i64 {
99 if nx_ascii_is_id_start(c) == 1 { return 1 }
100 if c >= 48 { if c <= 57 { return 1 } } // 0-9
101 if c == 39 { return 1 } // '
102 if c == 46 { return 1 } // .
103 return 0
104}