nx_rewrite.nx source
↩ module page · 77 lines · 3185 B
1// nx_rewrite.nx -- equational normaliser engine.
2//
3// Closes "no equational rewriter" gap. HOL Light has REWRITE_TAC,
4// Coq has rewrite, Lean has simp. Ours emits v2-kernel-checked
5// rewrite steps using the existing EQ_SYM / EQ_TRANS rules + a
6// substitution helper.
7//
8// Strategy: leftmost-outermost. Given a Term `goal` and a set of
9// orientation-tagged equations [(lhs == rhs)...], walk the term and
10// apply the first matching rewrite at each position, emitting an
11// EQ_TRANS chain. Bounded iterations to guarantee termination.
12
13// nx_safety_envelope:
14// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
15// sil_target: SIL1
16// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
17// verdict: NOT_YET_EVALUATED
18
19import "nx_kernel_v2.nx"
20
21const NX_REWRITE_MAX_ITER: nx_int = 32
22
23// Apply equation (a == b) at the current goal: if goal == a, return
24// idx of axiom (goal == b) -- which is just the equation itself.
25// More general rewriting (under contexts) would need SUBST + structural
26// recursion; this is the surface case that handles top-level rewrites.
27//
28// Returns chain idx of the rewritten-equality theorem (still goal == X
29// for some new X), or -1 if no equation matched.
30func nx_rewrite_step(ch: *K2Chain, eqs: *nx_int, n_eqs: nx_int, current: *Term) -> nx_int {
31 var i: nx_int = 0
32 while i < n_eqs {
33 let p: *nx_int = ((eqs as nx_int) + (i * 8)) as *nx_int
34 let eq_idx: nx_int = p[0]
35 let eq_thm: *K2Thm = nx_k2_at(ch, eq_idx)
36 let eq_stmt: *Term = eq_thm.stmt
37 if eq_stmt.kind == NX_TERM_APP {
38 if eq_stmt.sym == NX_K2_SYM_EQ {
39 let lhs: *Term = nx_term_arg(eq_stmt, 0)
40 if nx_term_eq(lhs, current) == 1 {
41 // Top-level match -- just return the equation.
42 return eq_idx
43 }
44 }
45 }
46 i = i + 1
47 }
48 return 0 - 1
49}
50
51// Normalize: keep applying rewrite_step until fixed point or iteration cap.
52// Each step that fires gets chained via EQ_TRANS so the final result
53// has shape (goal == fully_normalised). Returns chain idx of the final
54// equality theorem, or -1 if no rewriting occurred.
55func nx_rewrite_normalise(ch: *K2Chain, eqs: *nx_int, n_eqs: nx_int, start: *Term) -> nx_int {
56 var current_eq_idx: nx_int = 0 - 1
57 var current_term: *Term = start
58 var iters: nx_int = 0
59 while iters < NX_REWRITE_MAX_ITER {
60 let step_idx: nx_int = nx_rewrite_step(ch, eqs, n_eqs, current_term)
61 if step_idx < 0 { return current_eq_idx }
62 let step_thm: *K2Thm = nx_k2_at(ch, step_idx)
63 let new_term: *Term = nx_term_arg(step_thm.stmt, 1)
64 if current_eq_idx < 0 {
65 current_eq_idx = step_idx
66 } else {
67 // Chain (start == current) and (current == new) into
68 // (start == new) via EQ_TRANS.
69 let chained: nx_int = nx_k2_eq_trans(ch, current_eq_idx, step_idx)
70 if chained < 0 { return chained }
71 current_eq_idx = chained
72 }
73 current_term = new_term
74 iters = iters + 1
75 }
76 return current_eq_idx
77}