import { type CheckVerdict, type Judgment } from "./assumptions.js";
import type { Env } from "./eval.js";
import type { Equation } from "./expr.js";
import type { Rational } from "./rational.js";
import { type AnimationDiff, type BranchingRule, type Location, type Rule } from "./rule.js";
interface NodeBase {
    readonly id: string;
    readonly parentId: string | null;
    /** The full state AFTER this operation. */
    readonly judgment: Judgment;
    /** Append-only; mutated only by Derivation.commit. */
    readonly children: string[];
}
/**
 * One committed operation in the derivation tree. Rule applications are the
 * common case; pins, case-split branches, and solution checks are first-class
 * log entries too, so the whole story of a derivation is replayable and every
 * assumption's origin step is a real node.
 */
export type DerivationNode = NodeBase & ({
    readonly kind: "root";
} | {
    readonly kind: "rule";
    readonly ruleId: string;
    readonly location: Location;
    readonly params: unknown;
    readonly diff: AnimationDiff;
    readonly viaCaseSplit?: boolean;
} | {
    /** Branch B of a case split: the move was NOT applied; the variable is pinned instead. */
    readonly kind: "case-pin";
    readonly forRuleId: string;
    readonly variable: string;
    readonly value: Rational;
} | {
    /** One arm of a disjunctive rewrite; its siblings are the other arms. */
    readonly kind: "branch";
    readonly ruleId: string;
    readonly location: Location;
    readonly params: unknown;
    readonly label: string;
    readonly diff: AnimationDiff;
} | {
    readonly kind: "pin";
    readonly variable: string;
    readonly value: Rational;
} | {
    readonly kind: "unpin";
    readonly variable: string;
} | {
    readonly kind: "check-solution";
    readonly candidate: Env;
    readonly verdict: CheckVerdict;
});
/**
 * The derivation log: an append-only TREE of judgments. "Current state" is a
 * pointer into the tree; undo moves the pointer to the parent, and applying a
 * new operation while elsewhere simply grows a new branch — abandoned
 * branches stay live and navigable (goto). Nothing is ever rewritten.
 */
export declare class Derivation {
    private readonly nodes;
    readonly rootId: string;
    private currentId;
    constructor(initial: Equation | Judgment);
    node(id: string): DerivationNode;
    get currentNode(): DerivationNode;
    get current(): Judgment;
    childrenOf(id: string): readonly string[];
    /** Nodes from the root to the current pointer, inclusive. */
    get path(): DerivationNode[];
    private commit;
    /** Apply a rewrite rule at the current pointer; illegal moves throw and leave no node. */
    apply<P>(rule: Rule<P>, location: Location, params: P): DerivationNode;
    canUndo(): boolean;
    /** Move the pointer to the parent. The abandoned node stays in the tree. */
    undo(): Judgment;
    canRedo(): boolean;
    /** Move to the most recently created child; use goto() to pick a branch. */
    redo(): Judgment;
    /** Jump anywhere in the tree — every committed state stays live. */
    goto(id: string): Judgment;
    /**
     * User what-if: assume variable = value. Rejected (both directions of the
     * conflict check) when it decidably violates an existing Restriction.
     */
    pinVariable(variable: string, value: Rational): DerivationNode;
    /**
     * Remove a user pin. Restrictions that were discharged by this pin become
     * active again (the discharge pass re-decides them). Case-split pins are
     * structural to their branch and cannot be unpinned.
     */
    unpinVariable(variable: string): DerivationNode;
    /**
     * Apply a DISJUNCTIVE rewrite: all branches are committed as live sibling
     * children (the union of their solution sets equals the original's) and
     * the pointer lands on the first. Navigate the rest via goto.
     */
    applyBranching<P>(rule: BranchingRule<P>, location: Location, params: P): DerivationNode[];
    /**
     * Fork the current node on a Restriction-producing move whose restriction
     * targets a bare variable v ≠ c:
     *   - branch A ("restricted") applies the move and carries Restriction(v ≠ c);
     *   - branch B ("pinned") does NOT apply the move and pins v = c instead.
     * Both branches stay live; the pointer moves to branch A.
     */
    caseSplit<P>(rule: Rule<P>, location: Location, params: P): {
        restricted: DerivationNode;
        pinned: DerivationNode;
    };
    /**
     * Check a candidate solution against the original equation(s) carried by
     * the judgment's Extensions. Verified candidates discharge the Extensions;
     * extraneous ones are condemned in the log (the node records the verdict)
     * and change nothing else.
     */
    checkSolution(candidate: Env): {
        verdict: CheckVerdict;
        node: DerivationNode;
    };
}
export {};
//# sourceMappingURL=derivation.d.ts.map