`nx_help_test.nx` source

1// nx_help_test.nx -- smoke for substrate-native S-class help.
2
3import "syscalls.nx"
4import "nx_axioms.nx"
5import "nx_jargon.nx"
6import "nx_qed_db.nx"
7import "nx_question_genealogy.nx"
8import "nx_help.nx"
9
10func main() -> i64 {
11    // Build the three substrate DBs.
12    let jd: *JargonDb = nx_jargon_db_alloc()
13    nx_jargon_seed_corpus(jd)
14
15    let qd: *QedDb = nx_qed_db_alloc()
16    let ax: *i64 = (sys_mmap(8)) as *i64
17    ax[0] = NX_AX_PEANO_PA1_ZERO_EXISTS
18    nx_qed_insert(qd, "Pythagorean.theorem" as *u8,
19                  NX_QED_SYS_NISHILANG_LOCAL,
20                  ax, 1, 12345, NX_QED_VERIFY_LOCAL_PROVED)
21    nx_qed_insert(qd, "Nat.add_comm" as *u8,
22                  NX_QED_SYS_LEAN_MATHLIB,
23                  ax, 1, 67890, NX_QED_VERIFY_TRUSTED_LEAN)
24
25    let qt: *QuestionTree = nx_qg_tree_alloc()
26    nx_qg_seed_corpus(qt)
27
28    let result: *HelpResult = nx_help_result_alloc()
29
30    // === Query 1: a jargon term (monoid) ===
31    let r1: i64 = nx_help_query(jd, qd, qt, "monoid" as *u8,
32                                NX_DISC_MATH, NX_TIER_BEGINNER, result)
33    if r1 != 1 { return 1 }
34    if result.kind != NX_HELP_KIND_JARGON_DEFINITION { return 2 }
35    // Should have 1 alternate (the EXPERT tier).
36    if result.n_alternates != 1 { return 3 }
37
38    nx_help_emit_result(2, result, "monoid" as *u8)
39
40    // === Query 2: a theorem name ===
41    let result2: *HelpResult = nx_help_result_alloc()
42    let r2: i64 = nx_help_query(jd, qd, qt, "Pythagorean.theorem" as *u8,
43                                NX_DISC_MATH, NX_TIER_BEGINNER, result2)
44    if r2 != 1 { return 10 }
45    if result2.kind != NX_HELP_KIND_THEOREM_CARD { return 11 }
46
47    nx_help_emit_result(2, result2, "Pythagorean.theorem" as *u8)
48
49    // === Query 3: a question (matches genealogy by prefix) ===
50    let result3: *HelpResult = nx_help_result_alloc()
51    let r3: i64 = nx_help_query(jd, qd, qt, "Is pi" as *u8,
52                                NX_DISC_MATH, NX_TIER_BEGINNER, result3)
53    if r3 != 1 { return 20 }
54    if result3.kind != NX_HELP_KIND_QUESTION_NARRATIVE { return 21 }
55
56    nx_help_emit_result(2, result3, "Is pi" as *u8)
57
58    // === Query 4: unknown term (no match) ===
59    let result4: *HelpResult = nx_help_result_alloc()
60    let r4: i64 = nx_help_query(jd, qd, qt, "definitely_not_a_term_xyz" as *u8,
61                                NX_DISC_MATH, NX_TIER_BEGINNER, result4)
62    if r4 != 0 { return 30 }
63    if result4.kind != NX_HELP_KIND_NONE { return 31 }
64
65    nx_help_emit_result(2, result4, "definitely_not_a_term_xyz" as *u8)
66
67    // === Query 5: expert-tier lookup of homeomorphism ===
68    let result5: *HelpResult = nx_help_result_alloc()
69    let r5: i64 = nx_help_query(jd, qd, qt, "homeomorphism" as *u8,
70                                NX_DISC_MATH, NX_TIER_EXPERT, result5)
71    if r5 != 1 { return 40 }
72    if result5.kind != NX_HELP_KIND_JARGON_DEFINITION { return 41 }
73    if result5.tier != NX_TIER_EXPERT { return 42 }
74
75    nx_help_emit_result(2, result5, "homeomorphism" as *u8)
76
77    return 0
78}
nx_help_test.nx source

`nx_help_test.nx` source
