import { PredicateFormula, PredicateArgument, Quantifier } from '../types.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.parser;
/**
* Parser for predicate logic formulas
*/
export class PredicateParser {
/**
* Parse a string into a predicate formula or argument
* @param input Input string to parse
* @returns Parsed predicate formula or argument
*/
parse(input: string): PredicateFormula | PredicateArgument {
try {
logger.debug('parse called', { input });
// Check if this is an argument (contains 'therefore' or conclusion indicators)
const isArg = this.isArgument(input);
logger.debug('isArgument check', { input, isArgument: isArg });
if (isArg) {
return this.parseArgument(input);
}
// Otherwise parse as a single formula
const tokens = this.tokenize(input);
logger.debug('Parsing as single formula', { tokens });
return this.parseExpression(tokens, 0).formula;
} catch (error) {
logger.error('Parse error', {
error: error instanceof Error ? error.message : String(error),
input
});
throw this.enhanceError(error, input);
}
}
/**
* Check if input represents an argument
* @param input Input string
* @returns True if it's an argument
*/
private isArgument(input: string): boolean {
const normalized = input.toLowerCase();
return normalized.includes('therefore') ||
normalized.includes('thus') ||
normalized.includes('hence') ||
normalized.includes('∴');
}
/**
* Parse an argument (premises and conclusion)
* @param input Input string
* @returns Parsed argument
*/
private parseArgument(input: string): PredicateArgument {
logger.debug('parseArgument called', { input });
// Split by 'therefore' or similar conclusion indicators
const conclusionIndicators = ['therefore', 'thus', 'hence', '∴'];
let parts: string[] = [];
let conclusionPart = '';
for (const indicator of conclusionIndicators) {
if (input.toLowerCase().includes(indicator)) {
logger.debug(`Found indicator '${indicator}' in input`);
const regex = new RegExp(`\\s*${indicator}\\s*`, 'i');
const split = input.split(regex);
logger.debug(`Split result`, { splitLength: split.length, split });
if (split.length === 2) {
const premisesStr = split[0].trim();
conclusionPart = split[1].trim();
parts = premisesStr.split(',').map(s => s.trim()).filter(s => s.length > 0);
logger.debug(`Split by '${indicator}'`, {
premisesStr,
premises: parts,
conclusion: conclusionPart
});
break;
}
}
}
if (parts.length === 0 || !conclusionPart) {
throw new Error('Invalid argument format. Expected: "premise1, premise2, therefore conclusion"');
}
// Parse each premise
const premises = parts.map((part, idx) => {
logger.debug(`Parsing premise ${idx + 1}`, { premise: part });
const tokens = this.tokenize(part);
logger.debug(`Tokens for premise ${idx + 1}`, { tokens });
return this.parseExpression(tokens, 0).formula;
});
// Parse conclusion
logger.debug('Parsing conclusion', { conclusion: conclusionPart });
const conclusionTokens = this.tokenize(conclusionPart);
logger.debug('Tokens for conclusion', { tokens: conclusionTokens });
const conclusion = this.parseExpression(conclusionTokens, 0).formula;
return {
premises,
conclusion
};
}
/**
* Tokenize the input string
* @param input Input string
* @returns Array of tokens
*/
private tokenize(input: string): string[] {
// Replace Unicode symbols with text equivalents (with spaces)
const normalized = input
.replace(/∀/g, ' forall ')
.replace(/∃/g, ' exists ')
.replace(/∧/g, ' and ')
.replace(/∨/g, ' or ')
.replace(/¬/g, ' not ')
.replace(/→/g, ' implies ')
.replace(/↔/g, ' iff ')
.replace(/⊕/g, ' xor ')
.replace(/->/g, ' implies ')
.replace(/<->/g, ' iff ');
// Split into tokens
return normalized
.replace(/\(/g, ' ( ')
.replace(/\)/g, ' ) ')
.replace(/,/g, ' , ')
.replace(/\./g, ' . ')
.split(/\s+/)
.filter(token => token.length > 0);
}
/**
* Parse an expression from tokens
* @param tokens Array of tokens
* @param index Starting index
* @returns Parse result with formula and next index
*/
private parseExpression(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
// Try to parse quantified formula
if (index < tokens.length && this.isQuantifier(tokens[index])) {
return this.parseQuantified(tokens, index);
}
// Otherwise parse as implication (lowest precedence)
return this.parseImplication(tokens, index);
}
/**
* Parse a quantified formula
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseQuantified(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
if (index >= tokens.length) {
throw new Error('Unexpected end of input');
}
const quantifier = this.normalizeQuantifier(tokens[index]);
index++; // Skip quantifier
// Get variable name
if (index >= tokens.length) {
throw new Error('Expected variable after quantifier');
}
const variable = tokens[index];
if (!this.isVariable(variable)) {
throw new Error(`Expected variable after quantifier, got: ${variable}`);
}
index++; // Skip variable
// Skip optional dot or space
if (index < tokens.length && tokens[index] === '.') {
index++; // Skip dot
}
// Parse the body formula
const body = this.parseExpression(tokens, index);
return {
formula: {
type: 'quantified',
quantifier,
variable,
formula: body.formula
},
nextIndex: body.nextIndex
};
}
/**
* Parse an implication expression
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseImplication(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
let result = this.parseIff(tokens, index);
while (
result.nextIndex < tokens.length &&
(tokens[result.nextIndex] === 'implies' || tokens[result.nextIndex] === '→')
) {
result.nextIndex++; // Skip operator
const right = this.parseImplication(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: 'implies',
left: result.formula,
right: right.formula
},
nextIndex: right.nextIndex
};
}
return result;
}
/**
* Parse an iff/xor expression
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseIff(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
let result = this.parseOr(tokens, index);
while (
result.nextIndex < tokens.length &&
(tokens[result.nextIndex] === 'iff' || tokens[result.nextIndex] === 'xor')
) {
const operator = tokens[result.nextIndex] as 'iff' | 'xor';
result.nextIndex++; // Skip operator
const right = this.parseIff(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator,
left: result.formula,
right: right.formula
},
nextIndex: right.nextIndex
};
}
return result;
}
/**
* Parse an or expression
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseOr(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
let result = this.parseAnd(tokens, index);
while (
result.nextIndex < tokens.length &&
tokens[result.nextIndex] === 'or'
) {
result.nextIndex++; // Skip operator
const right = this.parseOr(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: 'or',
left: result.formula,
right: right.formula
},
nextIndex: right.nextIndex
};
}
return result;
}
/**
* Parse an and expression
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseAnd(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
let result = this.parseFactor(tokens, index);
while (
result.nextIndex < tokens.length &&
tokens[result.nextIndex] === 'and'
) {
result.nextIndex++; // Skip operator
const right = this.parseAnd(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: 'and',
left: result.formula,
right: right.formula
},
nextIndex: right.nextIndex
};
}
return result;
}
/**
* Parse a factor (not, predicate, or parenthesized expression)
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseFactor(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
if (index >= tokens.length) {
throw new Error('Unexpected end of input');
}
const token = tokens[index];
// Handle negation
if (token === 'not' || token === '¬') {
const result = this.parseFactor(tokens, index + 1);
return {
formula: {
type: 'unary',
operator: 'not',
operand: result.formula
},
nextIndex: result.nextIndex
};
}
// Handle parenthesized expression
if (token === '(') {
const result = this.parseExpression(tokens, index + 1);
if (result.nextIndex >= tokens.length || tokens[result.nextIndex] !== ')') {
throw new Error('Mismatched parentheses');
}
return {
formula: result.formula,
nextIndex: result.nextIndex + 1
};
}
// Handle predicate or variable
return this.parsePredicateOrVariable(tokens, index);
}
/**
* Parse a predicate or variable
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parsePredicateOrVariable(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
if (index >= tokens.length) {
throw new Error('Unexpected end of input');
}
const name = tokens[index];
// Check if next token is '(' - indicates a predicate or function
if (index + 1 < tokens.length && tokens[index + 1] === '(') {
// Parse arguments
const args: PredicateFormula[] = [];
let currentIndex = index + 2; // Skip name and '('
// Find matching closing parenthesis first
let parenDepth = 1;
let endIndex = currentIndex;
while (endIndex < tokens.length && parenDepth > 0) {
if (tokens[endIndex] === '(') parenDepth++;
if (tokens[endIndex] === ')') parenDepth--;
if (parenDepth > 0) endIndex++;
}
if (parenDepth !== 0) {
throw new Error('Mismatched parentheses in predicate');
}
// Now parse arguments between currentIndex and endIndex
while (currentIndex < endIndex) {
// Skip commas
if (tokens[currentIndex] === ',') {
currentIndex++;
continue;
}
// Parse argument
const arg = this.parseArgument2(tokens, currentIndex);
args.push(arg.formula);
currentIndex = arg.nextIndex;
}
currentIndex = endIndex + 1; // Skip ')'
// Determine if it's a predicate (uppercase) or function (lowercase first char)
const isPredicate = /^[A-Z]/.test(name);
return {
formula: {
type: isPredicate ? 'predicate' : 'function',
name,
args
} as PredicateFormula,
nextIndex: currentIndex
};
}
// Check if it's a constant (lowercase) or variable (depends on context)
if (this.isConstant(name)) {
return {
formula: {
type: 'constant',
name
},
nextIndex: index + 1
};
}
// Otherwise it's a variable
return {
formula: {
type: 'variable',
name
},
nextIndex: index + 1
};
}
/**
* Parse an argument (term inside predicate)
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseArgument2(tokens: string[], index: number): {
formula: PredicateFormula;
nextIndex: number;
} {
if (index >= tokens.length) {
throw new Error('Unexpected end of input');
}
const token = tokens[index];
// Check if it's a function call
if (index + 1 < tokens.length && tokens[index + 1] === '(') {
return this.parsePredicateOrVariable(tokens, index);
}
// Check if it's a constant
if (this.isConstant(token)) {
return {
formula: {
type: 'constant',
name: token
},
nextIndex: index + 1
};
}
// Otherwise it's a variable
return {
formula: {
type: 'variable',
name: token
},
nextIndex: index + 1
};
}
/**
* Check if token is a quantifier
* @param token Token to check
* @returns Whether token is a quantifier
*/
private isQuantifier(token: string): boolean {
return token === 'forall' || token === 'exists' ||
token === '∀' || token === '∃';
}
/**
* Normalize quantifier to standard form
* @param token Quantifier token
* @returns Normalized quantifier
*/
private normalizeQuantifier(token: string): Quantifier {
if (token === 'forall' || token === '∀') {
return 'forall';
}
if (token === 'exists' || token === '∃') {
return 'exists';
}
throw new Error(`Invalid quantifier: ${token}`);
}
/**
* Check if token is a variable
* @param token Token to check
* @returns Whether token is a variable
*/
private isVariable(token: string): boolean {
// Variables are typically single lowercase letters or lowercase words
return /^[a-z]$/.test(token);
}
/**
* Check if token is a constant
* @param token Token to check
* @returns Whether token is a constant
*/
private isConstant(token: string): boolean {
// Constants are lowercase words (not single letters)
// But 'a', 'b', 'c' etc at the beginning of alphabet are treated as constants
return (/^[a-e]$/.test(token)) || (/^[a-z][a-z0-9_]*$/.test(token) && token.length > 1);
}
/**
* Enhance error messages with helpful information
* @param error Original error
* @param input Original input
* @returns Enhanced error
*/
private enhanceError(error: any, input: string): Error {
const errorMessage = error instanceof Error ? error.message : String(error);
return new Error(`Syntax error in predicate logic: ${errorMessage}
Predicate logic syntax:
• Quantifiers: ∀x (for all x), ∃x (exists x)
• Predicates: P(x), Human(x), Loves(x,y)
• Constants: a, b, socrates, john
• Variables: x, y, z
• Operators: and, or, not, implies, iff
• Symbols: ∧, ∨, ¬, →, ↔
Valid examples:
✓ ∀x P(x)
✓ ∀x (P(x) implies Q(x))
✓ ∃x (Human(x) and Mortal(x))
Your input: "${input}"`);
}
}
