import type { TCoreArgument, TCoreLogicalOperatorType, TCorePremise, TCorePropositionalExpression, TCorePropositionalVariable } from "../../schemata/index.js";
/**
 * Visitor callbacks for walking a premise's expression tree.
 * Each method handles one node type and returns a caller-defined result.
 */
export interface TFormulaTreeVisitor<T> {
    /** Called for each variable expression. */
    variable(symbol: string, variableId: string): T;
    /** Called for each operator. Receives the operator type and rendered children. */
    operator(type: TCoreLogicalOperatorType, children: T[]): T;
    /** Called for each formula (grouping). Receives the rendered child. */
    formula(child: T): T;
    /** Called when the premise has no root expression. */
    empty(): T;
}
import type { TCoreResolvedAssignment, TCorePremiseEvaluationResult, TCoreValidationResult } from "../../types/evaluation.js";
import type { TInvariantValidationResult } from "../../types/validation.js";
import type { TCoreMutationResult } from "../../types/mutation.js";
import type { TExpressionInput, TExpressionWithoutPosition, TExpressionUpdate } from "../expression-manager.js";
import type { TPremiseEngineSnapshot } from "../premise-engine.js";
/**
 * Single-premise expression tree mutations.
 */
export interface TExpressionMutations<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable> {
    /**
     * Adds an expression to this premise's tree.
     *
     * If the expression has `parentId: null` it becomes the root; only one
     * root is permitted per premise. All Structural rules (`implies`/`iff`
     * root-only, child limits, position uniqueness, derivation root
     * operator) are enforced at mutation time.
     *
     * As of v1.0 P-1 (non-not operator under operator) is **not**
     * enforced at mutation time — the AN-1 post-hook in assistive
     * behavior inserts the formula buffer; in permissive behavior the
     * un-buffered state stays and surfaces via
     * `engine.validate('presentable')`.
     *
     * @param expression - The expression to add, including position and
     *   parent assignment.
     * @returns The added expression (with checksum) and changeset.
     * @throws If the premise already has a root expression and this one is
     *   also a root.
     * @throws If the expression's parent does not exist in this premise.
     * @throws If the expression is a variable reference and the variable
     *   has not been registered.
     */
    addExpression(expression: TExpressionInput<TExpr>): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Adds an expression as the last child of the given parent, with
     * position computed automatically. If `parentId` is `null`, the
     * expression becomes the root.
     *
     * Composite-mutation behavior (spec §8 / S-9): sibling positions
     * are always shifted as part of the bundled op when the computed
     * position would collide with an existing sibling. Repositioned
     * siblings appear in `changes.expressions.modified`.
     *
     * @param parentId - The parent expression ID, or `null` for root.
     * @param expression - The expression to add (position is auto-assigned).
     * @returns The added expression (with checksum) and changeset.
     * @throws If the premise already has a root and `parentId` is `null`.
     * @throws If the expression is a variable reference and the variable
     *   has not been registered.
     */
    appendExpression(parentId: string | null, expression: TExpressionWithoutPosition<TExpr>): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Adds an expression immediately before or after an existing sibling,
     * with position computed automatically.
     *
     * Composite-mutation behavior (spec §8 / S-9): sibling positions
     * are always shifted as part of the bundled op when the computed
     * midpoint position would collide with an existing sibling. Only
     * the minimal set of nodes is repositioned. Repositioned siblings
     * appear in `changes.expressions.modified`.
     *
     * @param siblingId - The ID of the existing sibling expression.
     * @param relativePosition - Whether to insert `"before"` or `"after"`
     *   the sibling.
     * @param expression - The expression to add (position is auto-assigned).
     * @returns The added expression (with checksum) and changeset.
     * @throws If the sibling does not exist in this premise.
     * @throws If the expression is a variable reference and the variable
     *   has not been registered.
     */
    addExpressionRelative(siblingId: string, relativePosition: "before" | "after", expression: TExpressionWithoutPosition<TExpr>): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Updates mutable fields of an existing expression. Only `position`,
     * `variableId`, and `operator` may be updated.
     *
     * @param expressionId - The ID of the expression to update.
     * @param updates - The fields to update.
     * @returns The updated expression and changeset.
     * @throws If the expression does not exist in this premise.
     * @throws If `variableId` references a non-existent variable.
     */
    updateExpression(expressionId: string, updates: TExpressionUpdate): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Removes an expression and optionally its entire descendant subtree.
     *
     * As of v1.0 the pre-mutation 0/1-child collapse cascade is gone —
     * AN-3 (post-mutation hook in assistive mode) handles 0/1-child
     * operator/formula collapse on the surviving parent.
     *
     * @param expressionId - The ID of the expression to remove.
     * @param deleteSubtree - Whether to remove all descendants as well.
     * @returns The removed root expression, or `undefined` if not found.
     * @throws If `deleteSubtree` is false and the single surviving
     *   child is a root-only operator (`implies`/`iff`) that would be
     *   placed in a non-root position (S-5).
     */
    removeExpression(expressionId: string, deleteSubtree: boolean): TCoreMutationResult<TExpr | undefined, TExpr, TVar, TPremise, TArg>;
    /**
     * Splices a new expression between existing nodes in the tree. The new
     * expression inherits the tree slot of the anchor node
     * (`leftNodeId ?? rightNodeId`).
     *
     * As of v1.0 P-1 (non-not operator under operator) is **not**
     * enforced at mutation time — the AN-1 post-hook in assistive
     * behavior inserts the formula buffer; in permissive behavior the
     * un-buffered state stays and surfaces via
     * `engine.validate('presentable')`.
     *
     * @param expression - The expression to insert, including position and
     *   parent assignment.
     * @param leftNodeId - The existing node to become the left child of
     *   the new expression.
     * @param rightNodeId - The existing node to become the right child of
     *   the new expression.
     * @returns The inserted expression (with checksum) and changeset.
     * @throws If the expression is a variable reference and the variable
     *   has not been registered.
     */
    insertExpression(expression: TExpressionInput<TExpr>, leftNodeId?: string, rightNodeId?: string): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Wraps an existing expression with a new operator and a new sibling
     * in a single atomic operation.
     *
     * The operator takes the existing node's slot in the tree. Both the
     * existing node and the new sibling become children of the operator.
     * Exactly one of `leftNodeId` / `rightNodeId` must be provided — it
     * identifies the existing node and which child slot it occupies.
     *
     * As of v1.0 P-1 (non-not operator under operator) is **not**
     * enforced at mutation time — the AN-1 post-hook in assistive
     * behavior inserts the formula buffer; in permissive behavior the
     * un-buffered state stays and surfaces via
     * `engine.validate('presentable')`.
     *
     * @param operator - The new operator expression to wrap with.
     * @param newSibling - The new sibling expression to add alongside the
     *   existing node.
     * @param leftNodeId - The existing node to place as the left child.
     * @param rightNodeId - The existing node to place as the right child.
     * @returns The inserted operator (with checksum) and changeset.
     * @throws If the new sibling is a variable reference and the variable
     *   has not been registered.
     */
    wrapExpression(operator: TExpressionWithoutPosition<TExpr>, newSibling: TExpressionWithoutPosition<TExpr>, leftNodeId?: string, rightNodeId?: string): TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>;
    /**
     * Toggles negation on an expression. If the expression's parent is a
     * NOT operator, removes the NOT (promoting the expression). Otherwise,
     * wraps the expression with a new NOT operator.
     *
     * As of v1.0 P-1 (non-not operator under operator) and P-2
     * (NOT(NOT(x)) double-negation) are **not** enforced at mutation
     * time. The post-mutation AN hook handles them in assistive
     * behavior: AN-1 inserts the formula buffer between NOT and a
     * non-not operator child; AN-2 collapses NOT(NOT(x)) → x. In
     * permissive behavior both states stay and surface via
     * `engine.validate('presentable')`.
     *
     * @param expressionId - The ID of the expression to toggle negation on.
     * @param extraFields - Optional additional fields to merge into newly
     *   created expressions (NOT and formula nodes). Structural fields
     *   (id, type, operator, parentId, position, premiseId, argumentId,
     *   argumentVersion) cannot be overridden.
     * @returns The new NOT expression when adding negation, or `null` when
     *   removing it, along with the changeset.
     * @throws If the expression does not exist in this premise.
     */
    toggleNegation(expressionId: string, extraFields?: Partial<TExpr>): TCoreMutationResult<TExpr | null, TExpr, TVar, TPremise, TArg>;
    /**
     * Changes the operator type of an existing operator expression.
     *
     * Handles three structural cases automatically:
     * - **Simple change:** The operator has exactly 2 children and no merge
     *   condition. Updates the operator type in-place.
     * - **Merge:** The operator has exactly 2 children and its parent is the
     *   same type as `newOperator`. Dissolves the current operator and
     *   reparents its children under the parent.
     * - **Split:** The operator has >2 children. Extracts `sourceChildId` and
     *   `targetChildId` into a new sub-operator of type `newOperator`,
     *   inserting a formula buffer between the parent and the new
     *   sub-operator (the buffer is part of the bundled composite mutation
     *   so the resulting tree satisfies P-1 regardless of the engine's
     *   `behavior` setting).
     *
     * @param expressionId  The operator expression to change.
     * @param newOperator   The target operator type.
     * @param sourceChildId First child to include in a split (required when >2 children).
     * @param targetChildId Second child to include in a split (required when >2 children).
     * @param extraFields   Optional partial expression fields merged into any
     *                      newly created expressions (formula buffer, new sub-operator).
     *                      Structural fields (id, type, operator, parentId, position,
     *                      premiseId, argumentId, argumentVersion) cannot be overridden.
     * @returns result — For simple change: the updated operator expression.
     *                   For merge: null (operator was dissolved).
     *                   For split: the newly created sub-operator expression.
     *          changes — Full changeset with correct hierarchical checksums.
     * @throws If the expression does not exist, is not an operator, or is "not".
     * @throws If >2 children and sourceChildId/targetChildId not provided.
     * @throws If sourceChildId/targetChildId are not children of expressionId.
     */
    changeOperator(expressionId: string, newOperator: TCoreLogicalOperatorType, sourceChildId?: string, targetChildId?: string, extraFields?: Partial<TExpr>): TCoreMutationResult<TExpr | null, TExpr, TVar, TPremise, TArg>;
}
/**
 * Single-premise expression tree reads.
 */
export interface TExpressionQueries<TExpr extends TCorePropositionalExpression = TCorePropositionalExpression> {
    /**
     * Returns an expression by ID, or `undefined` if not found in this
     * premise.
     *
     * @param id - The expression ID to look up.
     * @returns The expression entity, or `undefined`.
     */
    getExpression(id: string): TExpr | undefined;
    /**
     * Returns the ID of the root expression, or `undefined` if the premise
     * is empty.
     *
     * @returns The root expression ID, or `undefined`.
     */
    getRootExpressionId(): string | undefined;
    /**
     * Returns the root expression, or `undefined` if the premise is empty.
     *
     * @returns The root expression entity, or `undefined`.
     */
    getRootExpression(): TExpr | undefined;
    /**
     * Returns all expressions in this premise.
     *
     * @returns An array of expression entities.
     */
    getExpressions(): TExpr[];
    /**
     * Returns the child expressions of the given parent, sorted by
     * position.
     *
     * @param parentId - The parent expression ID, or `null` for root-level
     *   children.
     * @returns An array of child expression entities.
     */
    getChildExpressions(parentId: string | null): TExpr[];
    /**
     * Returns the operator expressions a reviewer can accept or reject, in
     * pre-order depth-first tree order.
     *
     * Excludes `"not"` operators (NOT is flipped via a render-time flag,
     * not voted on) and skips formula nodes (they are traversed but never
     * emitted). Returns `[]` for empty premises and premises with no
     * operators.
     *
     * Order is stable across calls on the same `PremiseEngine` instance;
     * callers typically rely on index for step-queue construction.
     *
     * @returns An array of decidable operator expression entities.
     */
    getDecidableOperatorExpressions(): TExpr[];
}
/**
 * Variable reference queries and cascade deletion.
 */
export interface TVariableReferences<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable> {
    /**
     * Returns all argument-level variables (from the shared
     * VariableManager) sorted by ID. Since the VariableManager is shared
     * across all premises, this returns every registered variable — not
     * just those referenced by expressions in this premise.
     *
     * @returns An array of variable entities.
     */
    getVariables(): TVar[];
    /**
     * Returns the set of variable IDs referenced by expressions in this
     * premise. Only variables that appear in `type: "variable"` expression
     * nodes are included.
     *
     * @returns A Set of referenced variable ID strings.
     */
    getReferencedVariableIds(): Set<string>;
    /**
     * Deletes all expressions that reference the given variable ID,
     * including their subtrees. As of v1.0 the pre-mutation operator
     * collapse cascade is gone — AN-3 (post-mutation hook in assistive
     * behavior) handles 0/1-child operator/formula collapse on the
     * surviving parents.
     *
     * @param variableId - The variable ID whose referencing expressions
     *   should be removed.
     * @returns The removed expressions and changeset.
     */
    deleteExpressionsUsingVariable(variableId: string): TCoreMutationResult<TExpr[], TExpr, TVar, TPremise, TArg>;
}
/**
 * Premise type classification (inference vs constraint).
 */
export interface TPremiseClassification {
    /**
     * Returns `true` if the root expression is an `implies` or `iff`
     * operator, meaning this premise expresses a logical inference
     * relationship.
     *
     * @returns Whether this premise is an inference.
     */
    isInference(): boolean;
    /**
     * Returns `true` if this premise does not have an inference operator at
     * its root. Equivalent to `!isInference()`.
     *
     * @returns Whether this premise is a constraint.
     */
    isConstraint(): boolean;
}
/**
 * Premise-level evaluation: single-assignment evaluation and evaluability
 * validation.
 */
export interface TPremiseEvaluation {
    /**
     * Validates that this premise is structurally ready for evaluation.
     *
     * @returns A validation result with any issues found.
     */
    validateEvaluability(): TCoreValidationResult;
    /**
     * Evaluates the premise under an expression assignment.
     *
     * Variable values are looked up using the four-valued Belnap connectives
     * (`null` = unknown, `CONTESTED` = forced both true and false). Missing
     * variables default to `null`. For inference premises (`implies`/`iff`),
     * an `inferenceDiagnostic` is always computed.
     *
     * The parameter is the wider {@link TCoreResolvedAssignment} because
     * argument evaluation feeds its own constraint-closure output back
     * through here; a reader's `TCoreExpressionAssignment` is
     * assignable to it and stays three-valued.
     *
     * Operator decisions do not affect premise evaluation. A rejected
     * expression evaluates from its children like any other — a rejection is
     * a decision about a step, and its effect (striking the whole premise
     * from the evaluated set) belongs to argument-level evaluation.
     *
     * @param assignment - The variable assignment and the reader's operator
     *   decisions.
     * @param options - Optional evaluation options.
     * @param options.strictUnknownKeys - If `true`, unknown variable keys
     *   in the assignment cause an error.
     * @param options.requireExactCoverage - If `true`, the assignment must
     *   cover exactly the referenced variables.
     * @returns The premise evaluation result.
     */
    evaluate(assignment: TCoreResolvedAssignment, options?: {
        strictUnknownKeys?: boolean;
        requireExactCoverage?: boolean;
    }): TCorePremiseEvaluationResult;
}
/**
 * Premise snapshot and mutation callback lifecycle.
 * Static fromSnapshot factory is class-level only.
 */
export interface TPremiseLifecycle<TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression> {
    /**
     * Returns a serializable snapshot of the premise's owned state.
     *
     * @returns The premise engine snapshot.
     */
    snapshot(): TPremiseEngineSnapshot<TPremise, TExpr>;
    /**
     * Sets a callback invoked after every mutation, or `undefined` to
     * clear.
     *
     * @param callback - The mutation callback, or `undefined` to remove.
     */
    setOnMutate(callback: (() => void) | undefined): void;
    /**
     * Sets a callback that checks whether adding a variable-expression to a
     * premise would create a circular binding. Injected by `ArgumentEngine`
     * to enable cross-premise cycle detection. If not set, only the direct
     * check (within the premise itself) runs.
     *
     * @param check - A function that returns `true` if adding the variable
     *   to the premise would create a cycle, or `undefined` to clear.
     */
    setCircularityCheck(check: ((variableId: string, premiseId: string) => boolean) | undefined): void;
    /**
     * Sets a callback that checks whether a premise-bound variable's target
     * premise has an empty expression tree. Injected by `ArgumentEngine` to
     * enable cross-premise validation. Used during `validateEvaluability`.
     *
     * @param check - A function that returns `true` if the variable's bound
     *   premise has no root expression, or `undefined` to clear.
     */
    setEmptyBoundPremiseCheck(check: ((variableId: string) => boolean) | undefined): void;
    /**
     * Invalidates the cached checksum so the next call recomputes it.
     */
    markDirty(): void;
    /**
     * Run invariant validation on this premise and its expression tree.
     */
    validate(): TInvariantValidationResult;
    /**
     * Sets a callback that returns the full set of variable IDs registered
     * in the argument. Injected by `ArgumentEngine`.
     *
     * @param callback - A function returning the set of registered variable
     *   IDs, or `undefined` to clear.
     */
    setVariableIdsCallback(callback: (() => Set<string>) | undefined): void;
    /**
     * Sets a callback that runs full argument-level invariant validation.
     * Injected by `ArgumentEngine` so the premise can delegate to the
     * argument-level validator.
     *
     * @param callback - A function returning the invariant validation result,
     *   or `undefined` to clear.
     */
    setArgumentValidateCallback(callback: (() => TInvariantValidationResult) | undefined): void;
}
/**
 * Premise entity identity and metadata access.
 */
export interface TPremiseIdentity<TArg extends TCoreArgument = TCoreArgument, TPremise extends TCorePremise = TCorePremise, TExpr extends TCorePropositionalExpression = TCorePropositionalExpression, TVar extends TCorePropositionalVariable = TCorePropositionalVariable> {
    /**
     * Returns the premise ID.
     *
     * @returns The premise ID string.
     */
    getId(): string;
    /**
     * Returns a serializable premise representation containing only
     * identity/metadata and checksum. Use `getRootExpressionId()`,
     * `getExpressions()`, `getReferencedVariableIds()` for runtime state.
     *
     * @returns The premise data entity.
     */
    toPremiseData(): TPremise;
    /**
     * Returns the premise's extra metadata record.
     *
     * @returns The extras record.
     */
    getExtras(): Record<string, unknown>;
    /**
     * Replaces the premise's extra metadata record.
     *
     * @param extras - The new extras record.
     * @returns The new extras record and a changeset with the modified premise.
     */
    setExtras(extras: Record<string, unknown>): TCoreMutationResult<Record<string, unknown>, TExpr, TVar, TPremise, TArg>;
    /**
     * Shallow-merges updates into the premise's existing extras.
     *
     * @param updates - Key-value pairs to merge into the current extras.
     * @returns The merged extras record and a changeset with the modified premise.
     */
    updateExtras(updates: Record<string, unknown>): TCoreMutationResult<Record<string, unknown>, TExpr, TVar, TPremise, TArg>;
}
/**
 * Generic formula tree traversal via visitor pattern.
 */
export interface TFormulaTreeWalking {
    /**
     * Walks the premise's expression tree, invoking the visitor for each node,
     * and returns the visitor's result for the root. Returns the result of
     * `visitor.empty()` when the premise has no root expression.
     *
     * @param visitor - Callbacks for each expression node type.
     * @returns The visitor's result for the root node, or `visitor.empty()`
     *   if the premise is empty.
     */
    walkFormulaTree<T>(visitor: TFormulaTreeVisitor<T>): T;
}
//# sourceMappingURL=premise-engine.interfaces.d.ts.map