/**
 * Context tracking for proof verification.
 */

import { Expression } from './expression.js';

/**
 * Context holds variables and their types, plus the current goal.
 */
export class Context {
    private variables: Map<string, Expression>;
    public goal: Expression | null;

    constructor() {
        this.variables = new Map();
        this.goal = null;
    }

    /**
     * Add a variable with its type to the context.
     */
    addVariable(name: string, varType: Expression): void {
        this.variables.set(name, varType);
    }

    /**
     * Check if a variable exists in the context.
     */
    hasVariable(name: string): boolean {
        return this.variables.has(name);
    }

    /**
     * Get the type of a variable.
     */
    getVariableType(name: string): Expression | undefined {
        return this.variables.get(name);
    }

    /**
     * Create a deep copy of this context.
     */
    copy(): Context {
        const newContext = new Context();
        newContext.variables = new Map(this.variables);
        newContext.goal = this.goal ? this.goal.copy() : null;
        return newContext;
    }

    /**
     * String representation of the context.
     */
    toString(): string {
        const vars = Array.from(this.variables.entries())
            .map(([name, type]) => `${name}: ${type.toString()}`)
            .join(', ');
        const goalStr = this.goal ? this.goal.toString() : 'None';
        return `Context(vars=[${vars}], goal=${goalStr})`;
    }
}