2 * Verification logic for calculate blocks.
3 */
5import { Block } from './block.js';
6import { Expression } from './expression.js';
7import { Context } from './context.js';
8import { VerificationError } from './errors.js';
9import { simplify } from './simplifier.js';
11/**
12 * Verify a calculate block and return true if goal is resolved.
13 */
14export function verifyCalculate(
15 step: Block,
16 context: Context,
17 axiomsAndTheorems: Map<string, Block>
18): boolean {
19 // 1. Validate that the goal is an equality
20 if (context.goal === null) {
21 throw new VerificationError(`Line ${step.lineNum}: No goal for calculate`);
22 }
24 if (context.goal.name !== 'eq' || context.goal.children.length !== 2) {
25 throw new VerificationError(
26 `Line ${step.lineNum}: Goal must be eq(a, b), got ${context.goal}`
27 );
28 }
30 const initialExpr = context.goal.children[0];
31 const finalExpr = context.goal.children[1];
33 // 2. Validate calculate structure
34 if (step.args.length !== 1) {
35 throw new VerificationError(
36 `Line ${step.lineNum}: 'calculate' must have exactly one argument (initial expression)`
37 );
38 }
40 const calcInitial = step.args[0];
41 if (!calcInitial.equals(initialExpr)) {
42 throw new VerificationError(
43 `Line ${step.lineNum}: Calculate initial expression ${calcInitial} does not match goal LHS ${initialExpr}`
44 );
45 }
47 if (step.children.length === 0) {
48 throw new VerificationError(
49 `Line ${step.lineNum}: Calculate block must have at least one step`
50 );
51 }
53 // 3. Process each calculation step
54 let currentExpr = initialExpr;
56 for (const child of step.children) {
57 if (child.blockType !== '=') {
58 throw new VerificationError(
59 `Line ${child.lineNum}: Calculate children must be '=' blocks, got '${child.blockType}'`
60 );
61 }
63 currentExpr = verifyCalcStep(child, currentExpr, context, axiomsAndTheorems);
64 }
66 // 4. Final check: current expression should equal goal's RHS
67 if (!currentExpr.equals(finalExpr)) {
68 throw new VerificationError(
69 `Line ${step.lineNum}: Calculate final expression ${currentExpr} does not match goal RHS ${finalExpr}`
70 );
71 }
73 return true; // Goal resolved
74}
76/**
77 * Verify a single calculation step and return the new expression.
78 */
79function verifyCalcStep(
80 step: Block,
81 prevExpr: Expression,
82 context: Context,
83 axiomsAndTheorems: Map<string, Block>
84): Expression {
85 if (step.args.length < 2) {
86 throw new VerificationError(
87 `Line ${step.lineNum}: '=' must have at least 2 arguments (new_expr and justification)`
88 );
89 }
91 const newExpr = step.args[0];
92 const justificationType = step.args[1].name;
94 if (step.args[1].children.length > 0) {
95 throw new VerificationError(
96 `Line ${step.lineNum}: Justification type must be a simple identifier (by-lhs or by-rhs)`
97 );
98 }
100 // Get the equation (lhs, rhs) based on justification
101 const remainingArgs = step.args.slice(2);
102 let lhs: Expression, rhs: Expression;
104 if (justificationType === 'by-lhs') {
105 [lhs, rhs] = getEquationForJustification(step, context, axiomsAndTheorems, remainingArgs);
106 // by-lhs: verify that prevExpr can be transformed to newExpr by replacing lhs with rhs where needed
107 if (!verifyTransformation(prevExpr, newExpr, lhs, rhs)) {
108 throw new VerificationError(
109 `Line ${step.lineNum}: Cannot transform ${prevExpr} to ${newExpr} using by-lhs ${lhs} = ${rhs}`
110 );
111 }
112 } else if (justificationType === 'by-rhs') {
113 [lhs, rhs] = getEquationForJustification(step, context, axiomsAndTheorems, remainingArgs);
114 // by-rhs: verify that prevExpr can be transformed to newExpr by replacing rhs with lhs where needed
115 if (!verifyTransformation(prevExpr, newExpr, rhs, lhs)) {
116 throw new VerificationError(
117 `Line ${step.lineNum}: Cannot transform ${prevExpr} to ${newExpr} using by-rhs ${lhs} = ${rhs}`
118 );
119 }
120 } else {
121 throw new VerificationError(
122 `Line ${step.lineNum}: Unknown justification type '${justificationType}', expected 'by-lhs' or 'by-rhs'`
123 );
124 }
126 return newExpr;
127}
129/**
130 * Get the (lhs, rhs) equation from either a variable or axiom/theorem.
131 */
132function getEquationForJustification(
133 step: Block,
134 context: Context,
135 axiomsAndTheorems: Map<string, Block>,
136 args: Expression[]
137): [Expression, Expression] {
138 if (args.length === 0) {
139 throw new VerificationError(
140 `Line ${step.lineNum}: Justification requires at least one argument`
141 );
142 }
144 const firstArg = args[0];
146 // First argument must be a simple identifier
147 if (firstArg.children.length > 0) {
148 throw new VerificationError(
149 `Line ${step.lineNum}: First justification argument must be a simple identifier (variable or axiom name)`
150 );
151 }
153 const name = firstArg.name;
155 // Check if it's a variable in context (with only one arg total)
156 if (args.length === 1 && context.hasVariable(name)) {
157 // This is a variable reference
158 return getEquationFromVariable(step, name, context);
159 }
161 // Otherwise, treat it as an axiom/theorem
162 const axiomArgs = args.slice(1); // Remaining args are the axiom arguments
163 return getEquationFromAxiom(step, name, axiomArgs, context, axiomsAndTheorems);
164}
166/**
167 * Extract (lhs, rhs) from a variable with type eq(lhs, rhs).
168 */
169function getEquationFromVariable(
170 step: Block,
171 varName: string,
172 context: Context
173): [Expression, Expression] {
174 if (!context.hasVariable(varName)) {
175 throw new VerificationError(
176 `Line ${step.lineNum}: Variable '${varName}' not in context`
177 );
178 }
180 const varType = context.getVariableType(varName)!;
182 if (varType.name !== 'eq' || varType.children.length !== 2) {
183 throw new VerificationError(
184 `Line ${step.lineNum}: Variable '${varName}' must have type eq(a, b), got ${varType}`
185 );
186 }
188 return [varType.children[0], varType.children[1]];
189}
191/**
192 * Extract (lhs, rhs) from an axiom/theorem after substituting arguments.
193 */
194function getEquationFromAxiom(
195 step: Block,
196 axiomName: string,
197 args: Expression[],
198 context: Context,
199 axiomsAndTheorems: Map<string, Block>
200): [Expression, Expression] {
201 if (!axiomsAndTheorems.has(axiomName)) {
202 throw new VerificationError(
203 `Line ${step.lineNum}: Axiom or theorem '${axiomName}' not found`
204 );
205 }
207 const axiomBlock = axiomsAndTheorems.get(axiomName)!;
209 // Extract suppose blocks
210 const supposeBlocks: Block[] = [];
211 let concludeBlock: Block | null = null;
213 for (const child of axiomBlock.children) {
214 if (child.blockType === 'suppose') {
215 supposeBlocks.push(child);
216 } else if (child.blockType === 'conclude') {
217 concludeBlock = child;
218 }
219 }
221 if (concludeBlock === null) {
222 throw new VerificationError(
223 `Line ${step.lineNum}: Axiom '${axiomName}' has no conclude block`
224 );
225 }
227 // Verify number of arguments matches
228 if (args.length !== supposeBlocks.length) {
229 throw new VerificationError(
230 `Line ${step.lineNum}: Axiom '${axiomName}' expects ${supposeBlocks.length} arguments, got ${args.length}`
231 );
232 }
234 // Build substitution map
235 const substitutions = new Map<string, Expression>();
237 for (let i = 0; i < supposeBlocks.length; i++) {
238 const suppose = supposeBlocks[i];
239 const arg = args[i];
241 // Parse suppose: suppose name : type
242 if (suppose.args.length !== 1) {
243 throw new VerificationError(
244 `Line ${step.lineNum}: Invalid suppose block in axiom '${axiomName}'`
245 );
246 }
248 const supposeArg = suppose.args[0];
249 if (supposeArg.name !== 'var' || supposeArg.children.length !== 2) {
250 throw new VerificationError(
251 `Line ${step.lineNum}: Invalid suppose format in axiom '${axiomName}'`
252 );
253 }
255 const varName = supposeArg.children[0].name;
256 substitutions.set(varName, arg);
257 }
259 // Get the conclusion and verify it's an equation
260 let conclusion = concludeBlock.args[0];
262 // Apply substitutions to the conclusion
263 for (const [varName, argExpr] of substitutions) {
264 conclusion = conclusion.substitute(varName, argExpr);
265 }
267 if (conclusion.name !== 'eq' || conclusion.children.length !== 2) {
268 throw new VerificationError(
269 `Line ${step.lineNum}: Axiom '${axiomName}' conclusion must be eq(a, b), got ${conclusion}`
270 );
271 }
273 return [conclusion.children[0], conclusion.children[1]];
274}
276/**
277 * Verify that prevExpr can be transformed to targetExpr by replacing fromExpr with toExpr where needed.
278 */
279function verifyTransformation(
280 prevExpr: Expression,
281 targetExpr: Expression,
282 fromExpr: Expression,
283 toExpr: Expression
284): boolean {
285 // If they're already equal, no substitution needed
286 if (prevExpr.equals(targetExpr)) {
287 return true;
288 }
290 // Try substituting at the root level
291 if (prevExpr.equals(fromExpr)) {
292 return toExpr.equals(targetExpr);
293 }
295 // If names don't match or different number of children, can't transform
296 if (prevExpr.name !== targetExpr.name || prevExpr.children.length !== targetExpr.children.length) {
297 return false;
298 }
300 // Recursively check all children
301 return prevExpr.children.every((pc, i) =>
302 verifyTransformation(pc, targetExpr.children[i], fromExpr, toExpr)
303 );
304}