proposit-core
    Preparing search index...

    Class PremiseEngine<TArg, TPremise, TExpr, TVar>

    Single-premise expression tree mutations.

    Type Parameters

    Hierarchy (View Summary)

    Implements

    Index

    Constructors

    • Type Parameters

      • TArg extends {
            checksum: string;
            combinedChecksum: string;
            descendantChecksum: string | null;
            id: string;
            version: number;
        } = {
            checksum: string;
            combinedChecksum: string;
            descendantChecksum: string | null;
            id: string;
            version: number;
        }
      • TPremise extends
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "freeform";
            }
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                derivedClaimId: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "derivation";
            } =
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "freeform";
            }
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                derivedClaimId: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "derivation";
            }
      • TExpr extends TCorePropositionalExpression = TCorePropositionalExpression
      • TVar extends
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                claimId: string;
                claimVersion: number;
                id: string;
                symbol: string;
            }
            | {
                argumentId: string;
                argumentVersion: number;
                boundArgumentId: string;
                boundArgumentVersion: number;
                boundPremiseId: string;
                checksum: string;
                id: string;
                symbol: string;
            } =
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                claimId: string;
                claimVersion: number;
                id: string;
                symbol: string;
            }
            | {
                argumentId: string;
                argumentVersion: number;
                boundArgumentId: string;
                boundArgumentVersion: number;
                boundPremiseId: string;
                checksum: string;
                id: string;
                symbol: string;
            }

      Parameters

      Returns PremiseEngine<TArg, TPremise, TExpr, TVar>

    Properties

    expressions: ExpressionManager<TExpr>
    grammarConfig: TGrammarConfig
    rootExpressionId: string | undefined
    variables: VariableManager<TVar>

    Methods

    • 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) are enforced.

      When the wrapInsertFormula flag is enabled (either directly via TAutoNormalizeConfig or via autoNormalize: true), operator nesting violations are auto-corrected by inserting a formula buffer between the parent operator and the non-not operator child, rather than throwing. The same flag also controls auto-insertion in insertExpression and wrapExpression.

      Parameters

      Returns TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>

      The added expression (with checksum) and changeset.

      If the premise already has a root expression and this one is also a root.

      If the expression's parent does not exist in this premise.

      If the expression is a variable reference and the variable has not been registered.

      If a non-not operator would become a direct child of another operator expression (when wrapInsertFormula is disabled).

    • Adds an expression immediately before or after an existing sibling, with position computed automatically.

      When the repositionOnCollision auto-normalize flag is enabled, sibling positions are automatically redistributed if 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.

      Parameters

      • siblingId: string

        The ID of the existing sibling expression.

      • relativePosition: "before" | "after"

        Whether to insert "before" or "after" the sibling.

      • expression: TExpressionWithoutPosition<TExpr>

        The expression to add (position is auto-assigned).

      Returns TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>

      The added expression (with checksum) and changeset.

      If the sibling does not exist in this premise.

      If the expression is a variable reference and the variable has not been registered.

      If a non-not operator would become a direct child of another operator expression.

    • Adds an expression as the last child of the given parent, with position computed automatically. If parentId is null, the expression becomes the root.

      When the repositionOnCollision auto-normalize flag is enabled, sibling positions are automatically redistributed if the computed position would collide with an existing sibling. Repositioned siblings appear in changes.expressions.modified.

      Parameters

      • parentId: string | null

        The parent expression ID, or null for root.

      • expression: TExpressionWithoutPosition<TExpr>

        The expression to add (position is auto-assigned).

      Returns TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>

      The added expression (with checksum) and changeset.

      If the premise already has a root and parentId is null.

      If the expression is a variable reference and the variable has not been registered.

      If a non-not operator would become a direct child of another operator expression.

    • 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 if required by grammar enforcement.

      Parameters

      • expressionId: string

        The operator expression to change.

      • newOperator: "not" | "and" | "or" | "implies" | "iff"

        The target operator type.

      • OptionalsourceChildId: string

        First child to include in a split (required when >2 children).

      • OptionaltargetChildId: string

        Second child to include in a split (required when >2 children).

      • OptionalextraFields: Partial<TExpr>

        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 TCoreMutationResult<TExpr | null, TExpr, TVar, TPremise, TArg>

      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.

      If the expression does not exist, is not an operator, or is "not".

      If >2 children and sourceChildId/targetChildId not provided.

      If sourceChildId/targetChildId are not children of expressionId.

    • Evaluates the premise under a three-valued expression assignment.

      Variable values are looked up using Kleene three-valued logic (null = unknown). Missing variables default to null. For inference premises (implies/iff), an inferenceDiagnostic is computed with three-valued fields unless the root is rejected.

      Parameters

      • assignment: TCoreExpressionAssignment

        The variable assignment and optional rejected expression IDs.

      • Optionaloptions: {
            requireExactCoverage?: boolean;
            resolver?: (variableId: string) => boolean | null;
            strictUnknownKeys?: boolean;
        }

        Optional evaluation options.

        • OptionalrequireExactCoverage?: boolean

          If true, the assignment must cover exactly the referenced variables.

        • Optionalresolver?: (variableId: string) => boolean | null
        • OptionalstrictUnknownKeys?: boolean

          If true, unknown variable keys in the assignment cause an error.

      Returns TCorePremiseEvaluationResult

      The premise evaluation result.

    • 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 TExpr[]

      An array of decidable operator expression entities.

    • 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 TVar[]

      An array of variable entities.

    • Splices a new expression between existing nodes in the tree. The new expression inherits the tree slot of the anchor node (leftNodeId ?? rightNodeId).

      Parameters

      • expression: TExpressionInput<TExpr>

        The expression to insert, including position and parent assignment.

      • OptionalleftNodeId: string

        The existing node to become the left child of the new expression.

      • OptionalrightNodeId: string

        The existing node to become the right child of the new expression.

      Returns TCoreMutationResult<TExpr, TExpr, TVar, TPremise, TArg>

      The inserted expression (with checksum) and changeset.

      If the expression is a variable reference and the variable has not been registered.

      If a non-not operator would become a direct child of another operator expression.

    • 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.

      Parameters

      • check: ((variableId: string, premiseId: string) => boolean) | undefined

        A function that returns true if adding the variable to the premise would create a cycle, or undefined to clear.

      Returns 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.

      Parameters

      • check: ((variableId: string) => boolean) | undefined

        A function that returns true if the variable's bound premise has no root expression, or undefined to clear.

      Returns void

    • Overrides the grammar config for both this premise engine and its internal expression manager. Used by restoration paths when the caller's grammar config should override the snapshot's config.

      Parameters

      Returns void

    • Sets a callback invoked after every mutation, or undefined to clear.

      Parameters

      • callback: (() => void) | undefined

        The mutation callback, or undefined to remove.

      Returns void

    • Sets a callback that returns the full set of variable IDs registered in the argument. Injected by ArgumentEngine.

      Parameters

      • callback: (() => Set<string>) | undefined

        A function returning the set of registered variable IDs, or undefined to clear.

      Returns void

    • 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.

      When the target is already a NOT expression and collapseDoubleNegation is enabled, removes the existing NOT (promoting its child) instead of wrapping in another NOT — preventing NOT(NOT(x)).

      When the target is a non-not operator and negationInsertFormula is enabled, auto-inserts a formula buffer between the new NOT and the target to satisfy the operator nesting restriction. Throws if the flag is disabled and enforceFormulaBetweenOperators is true.

      Parameters

      • expressionId: string

        The ID of the expression to toggle negation on.

      • OptionalextraFields: Partial<TExpr>

        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 TCoreMutationResult<TExpr | null, TExpr, TVar, TPremise, TArg>

      The new NOT expression when adding negation, or null when removing it, along with the changeset.

      If the expression does not exist in this premise.

      If negationInsertFormula is disabled and the target is a non-not operator (would create operator-under-operator).

    • Creates a new PremiseEngine from a previously captured snapshot.

      Type Parameters

      • TArg extends {
            checksum: string;
            combinedChecksum: string;
            descendantChecksum: string | null;
            id: string;
            version: number;
        } = {
            checksum: string;
            combinedChecksum: string;
            descendantChecksum: string | null;
            id: string;
            version: number;
        }
      • TPremise extends
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "freeform";
            }
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                derivedClaimId: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "derivation";
            } =
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "freeform";
            }
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                combinedChecksum: string;
                derivedClaimId: string;
                descendantChecksum: string
                | null;
                id: string;
                type: "derivation";
            }
      • TExpr extends TCorePropositionalExpression = TCorePropositionalExpression
      • TVar extends
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                claimId: string;
                claimVersion: number;
                id: string;
                symbol: string;
            }
            | {
                argumentId: string;
                argumentVersion: number;
                boundArgumentId: string;
                boundArgumentVersion: number;
                boundPremiseId: string;
                checksum: string;
                id: string;
                symbol: string;
            } =
            | {
                argumentId: string;
                argumentVersion: number;
                checksum: string;
                claimId: string;
                claimVersion: number;
                id: string;
                symbol: string;
            }
            | {
                argumentId: string;
                argumentVersion: number;
                boundArgumentId: string;
                boundArgumentVersion: number;
                boundPremiseId: string;
                checksum: string;
                id: string;
                symbol: string;
            }

      Parameters

      Returns PremiseEngine<TArg, TPremise, TExpr, TVar>