1/**
2 * Context tracking for proof verification.
3 */
5import { Expression } from './expression.js';
7/**
8 * Context holds variables and their types, plus the current goal.
9 */
10export class Context {
11 private variables: Map<string, Expression>;
12 public goal: Expression | null;
14 constructor() {
15 this.variables = new Map();
16 this.goal = null;
17 }
19 /**
20 * Add a variable with its type to the context.
21 */
22 addVariable(name: string, varType: Expression): void {
23 this.variables.set(name, varType);
24 }
26 /**
27 * Check if a variable exists in the context.
28 */
29 hasVariable(name: string): boolean {
30 return this.variables.has(name);
31 }
33 /**
34 * Get the type of a variable.
35 */
36 getVariableType(name: string): Expression | undefined {
37 return this.variables.get(name);
38 }
40 /**
41 * Create a deep copy of this context.
42 */
43 copy(): Context {
44 const newContext = new Context();
45 newContext.variables = new Map(this.variables);
46 newContext.goal = this.goal ? this.goal.copy() : null;
47 return newContext;
48 }
50 /**
51 * String representation of the context.
52 */
53 toString(): string {
54 const vars = Array.from(this.variables.entries())
55 .map(([name, type]) => `${name}: ${type.toString()}`)
56 .join(', ');
57 const goalStr = this.goal ? this.goal.toString() : 'None';
58 return `Context(vars=[${vars}], goal=${goalStr})`;
59 }
60}