import { PropositionalFormula, PropositionalOperator, PropositionalArgument } from '../types.js';
import { Loggers } from '../utils/logger.js';
import { EnhancedPropositionalParser } from './enhancedPropositionalParser.js';
const logger = Loggers.parser;
/**
* Parser for propositional logic formulas
*/
export class PropositionalParser {
/**
* Parse a string into a propositional formula
* @param input Input string to parse
* @returns Parsed propositional formula
*/
parse(input: string): PropositionalFormula | PropositionalArgument {
try {
logger.debug('parse called', { input });
// Check if this is an argument (contains 'therefore' or commas with conclusion)
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);
} catch (error) {
logger.error('Parse error', {
error: error instanceof Error ? error.message : String(error),
input
});
// Provide helpful error messages
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('∴') ||
(normalized.includes(',') && normalized.split(',').length > 1) ||
(normalized.includes('.') && normalized.split('.').filter(s => s.trim()).length > 2);
}
/**
* Parse an argument (premises and conclusion)
* @param input Input string
* @returns Parsed argument
*/
private parseArgument(input: string): PropositionalArgument {
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().replace(/^[,.\s]+/, '') // Remove leading punctuation;
// Check if premises contain periods - if so, split by periods first
if (premisesStr.includes('.')) {
parts = premisesStr.split('.').map(s => s.trim()).filter(s => s.length > 0);
logger.debug(`Split premises by period`, { premises: parts });
} else {
// Otherwise split by commas
parts = premisesStr.split(',').map(s => s.trim()).filter(s => s.length > 0);
logger.debug(`Split premises by comma`, { premises: parts });
}
logger.debug(`Split by '${indicator}'`, {
premisesStr,
premises: parts,
conclusion: conclusionPart
});
break;
}
}
}
// If no conclusion indicator found, try splitting by period
if (!conclusionPart && input.includes('.')) {
const sentences = input.split('.').map(s => s.trim()).filter(s => s.length > 0);
if (sentences.length >= 2) {
// Check if last sentence looks like a conclusion (contains "therefore", "thus", etc.)
const lastSentence = sentences[sentences.length - 1].toLowerCase();
if (lastSentence.includes('therefore') || lastSentence.includes('thus') || lastSentence.includes('hence')) {
// Extract conclusion from the sentence containing the indicator
for (const indicator of ['therefore', 'thus', 'hence']) {
if (lastSentence.includes(indicator)) {
const split = sentences[sentences.length - 1].split(new RegExp(indicator, 'i'));
if (split.length === 2) {
conclusionPart = split[1].trim();
parts = sentences.slice(0, -1);
logger.debug('Split by period with conclusion indicator', { premises: parts, conclusion: conclusionPart });
break;
}
}
}
} else {
// No indicator, treat last sentence as conclusion
conclusionPart = sentences[sentences.length - 1];
parts = sentences.slice(0, -1);
logger.debug('Split by period (no conclusion indicator)', { premises: parts, conclusion: conclusionPart });
}
}
}
// If still no conclusion, try splitting by comma
if (!conclusionPart && input.includes(',')) {
const allParts = input.split(',').map(s => s.trim());
if (allParts.length >= 2) {
conclusionPart = allParts[allParts.length - 1];
parts = allParts.slice(0, -1);
logger.debug('Split by comma (no conclusion indicator)', { premises: parts, conclusion: conclusionPart });
}
}
if (parts.length === 0 || !conclusionPart) {
throw new Error('Invalid argument format. Expected: "premise1, premise2, therefore conclusion"');
}
// Parse each premise using enhanced parser for natural language support
const enhancedParser = new EnhancedPropositionalParser();
const premises = parts.map((part, idx) => {
logger.debug(`Parsing premise ${idx + 1}`, { premise: part });
try {
const parseResult = enhancedParser.parse(part);
return parseResult.formula;
} catch (error) {
// Fallback to standard tokenization
logger.warn(`Enhanced parser failed for premise ${idx + 1}, using standard parser`, {
error: error instanceof Error ? error.message : String(error)
});
const tokens = this.tokenize(part);
logger.debug(`Tokens for premise ${idx + 1}`, { tokens });
return this.parseExpression(tokens);
}
});
// Parse conclusion using enhanced parser
logger.debug('Parsing conclusion', { conclusion: conclusionPart });
let conclusion: PropositionalFormula;
try {
const parseResult = enhancedParser.parse(conclusionPart);
conclusion = parseResult.formula;
} catch (error) {
// Fallback to standard tokenization
logger.warn(`Enhanced parser failed for conclusion, using standard parser`, {
error: error instanceof Error ? error.message : String(error)
});
const conclusionTokens = this.tokenize(conclusionPart);
logger.debug('Tokens for conclusion', { tokens: conclusionTokens });
conclusion = this.parseExpression(conclusionTokens);
}
return {
premises,
conclusion
};
}
/**
* Tokenize the input string
* @param input Input string
* @returns Array of tokens
*/
private tokenize(input: string): string[] {
// First, apply basic NLP preprocessing for common patterns
let processed = input;
// Handle "if X, then Y" or "if X, Y" → "X implies Y"
processed = processed.replace(/\b(if|when|whenever)\s+([^,]+),?\s+(then\s+)?([^,.;]+)/gi, '($2) implies ($4)');
// IMPORTANT: Add spaces around operators BEFORE replacing them
// This prevents "¬P" from becoming "notP" (which looks like a variable)
const normalized = processed
// First, add spaces around all operator symbols
.replace(/∧/g, ' ∧ ')
.replace(/∨/g, ' ∨ ')
.replace(/¬/g, ' ¬ ')
.replace(/→/g, ' → ')
.replace(/↔/g, ' ↔ ')
.replace(/⊕/g, ' ⊕ ')
.replace(/&&/g, ' && ')
.replace(/\|\|/g, ' || ')
// Then replace with text equivalents
.replace(/∧/g, 'and')
.replace(/∨/g, 'or')
.replace(/¬/g, 'not')
.replace(/→/g, 'implies')
.replace(/↔/g, 'iff')
.replace(/⊕/g, 'xor')
.replace(/&&/g, 'and')
.replace(/\|\|/g, 'or')
.replace(/:/g, ' implies ')
.replace(/->/g, 'implies')
.replace(/=/g, ' iff ');
// Split into tokens - add comma handling
return normalized
.replace(/\(/g, ' ( ')
.replace(/\)/g, ' ) ')
.replace(/,/g, ' , ') // Add spaces around commas
.split(/\s+/)
.filter(token => token.length > 0 && token !== ','); // Remove comma tokens
}
/**
* Parse an expression from tokens
* @param tokens Array of tokens
* @returns Parsed propositional formula
*/
private parseExpression(tokens: string[]): PropositionalFormula {
return this.parseImplication(tokens, 0).formula;
}
/**
* Parse an implication expression (lowest precedence)
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseImplication(tokens: string[], index: number): {
formula: PropositionalFormula;
nextIndex: number;
} {
let result = this.parseIff(tokens, index);
while (
result.nextIndex < tokens.length &&
(tokens[result.nextIndex] === 'implies' || tokens[result.nextIndex] === '→')
) {
const operator = this.getOperator(tokens[result.nextIndex]);
result.nextIndex++; // Skip operator
const right = this.parseImplication(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: operator as Exclude<PropositionalOperator, 'not' | '¬'>,
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: PropositionalFormula;
nextIndex: number;
} {
let result = this.parseOr(tokens, index);
while (
result.nextIndex < tokens.length &&
(
tokens[result.nextIndex] === 'iff' ||
tokens[result.nextIndex] === '↔' ||
tokens[result.nextIndex] === 'xor' ||
tokens[result.nextIndex] === '⊕'
)
) {
const operator = this.getOperator(tokens[result.nextIndex]);
result.nextIndex++; // Skip operator
const right = this.parseIff(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: operator as Exclude<PropositionalOperator, 'not' | '¬'>,
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: PropositionalFormula;
nextIndex: number;
} {
let result = this.parseAnd(tokens, index);
while (
result.nextIndex < tokens.length &&
(tokens[result.nextIndex] === 'or' || tokens[result.nextIndex] === '∨')
) {
const operator = this.getOperator(tokens[result.nextIndex]);
result.nextIndex++; // Skip operator
const right = this.parseOr(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: operator as Exclude<PropositionalOperator, 'not' | '¬'>,
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: PropositionalFormula;
nextIndex: number;
} {
let result = this.parseFactor(tokens, index);
while (
result.nextIndex < tokens.length &&
(tokens[result.nextIndex] === 'and' || tokens[result.nextIndex] === '∧')
) {
const operator = this.getOperator(tokens[result.nextIndex]);
result.nextIndex++; // Skip operator
const right = this.parseAnd(tokens, result.nextIndex);
result = {
formula: {
type: 'binary',
operator: operator as Exclude<PropositionalOperator, 'not' | '¬'>,
left: result.formula,
right: right.formula
},
nextIndex: right.nextIndex
};
}
return result;
}
/**
* Parse a factor (not, variable, or parenthesized expression)
* @param tokens Array of tokens
* @param index Current index
* @returns Parse result
*/
private parseFactor(tokens: string[], index: number): {
formula: PropositionalFormula;
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: this.getOperator(token) as 'not' | '¬',
operand: result.formula
},
nextIndex: result.nextIndex
};
}
// Handle parenthesized expression
if (token === '(') {
const result = this.parseExpression(tokens.slice(index + 1));
const closingIndex = index + 1 + this.findClosingParenthesis(tokens, index + 1);
if (tokens[closingIndex] !== ')') {
throw new Error('Mismatched parentheses');
}
return {
formula: result,
nextIndex: closingIndex + 1
};
}
// Handle variable
if (this.isVariable(token)) {
return {
formula: {
type: 'variable',
name: token
},
nextIndex: index + 1
};
}
throw new Error(`Unexpected token: ${token}`);
}
/**
* Find the index of the closing parenthesis
* @param tokens Array of tokens
* @param startIndex Starting index
* @returns Index of the closing parenthesis
*/
private findClosingParenthesis(tokens: string[], startIndex: number): number {
let depth = 1;
let index = startIndex;
while (depth > 0 && index < tokens.length) {
if (tokens[index] === '(') {
depth++;
} else if (tokens[index] === ')') {
depth--;
}
if (depth === 0) {
return index - startIndex;
}
index++;
}
throw new Error('Mismatched parentheses');
}
/**
* Check if a token is a variable name
* @param token Token to check
* @returns Whether the token is a variable
*/
private isVariable(token: string): boolean {
// Allow multi-character variables (letters, numbers, underscores)
return /^[A-Za-z][A-Za-z0-9_]*$/.test(token);
}
/**
* Get standardized operator
* @param token Operator token
* @returns Standardized operator
*/
private getOperator(token: string): PropositionalOperator {
switch (token.toLowerCase()) {
case 'and':
case '∧':
return 'and';
case 'or':
case '∨':
return 'or';
case 'not':
case '¬':
return 'not';
case 'implies':
case '→':
return 'implies';
case 'iff':
case '↔':
return 'iff';
case 'xor':
case '⊕':
return 'xor';
default:
throw new Error(`Unknown operator: ${token}`);
}
}
/**
* 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);
if (errorMessage.includes('Unexpected token')) {
const token = errorMessage.match(/Unexpected token: (.*)/)?.[1] || 'unknown';
return new Error(`Syntax error: "${token}" is not a valid propositional logic token.
Allowed tokens:
• Variables: Single letters (P, Q, R)
• Operators: and, or, not, implies, iff, xor
• Symbols: ∧, ∨, ¬, →, ↔, ⊕
• Parentheses: ( )
Valid examples:
✓ P and Q
✓ (P or Q) implies R
✓ not P and Q
Invalid examples:
✗ if rains then wet (use: rains implies wet)
✗ P && Q (use: P and Q)
✗ All men are mortal (use syllogistic logic)
Your input: "${input}"`);
}
if (errorMessage.includes('Mismatched parentheses')) {
return new Error(`Syntax error: Mismatched parentheses.
Check that each opening parenthesis '(' has a matching closing parenthesis ')'.
Your input: "${input}"`);
}
if (errorMessage.includes('Unexpected end of input')) {
return new Error(`Syntax error: Incomplete expression.
The expression appears to be incomplete. Check for:
• Missing operands (e.g., "P and" is incomplete)
• Unclosed parentheses
• Missing right-hand side of binary operators
Your input: "${input}"`);
}
// Default enhanced error
return new Error(`Syntax error: ${errorMessage}
Please check your input follows propositional logic syntax.
Use "P and Q", "P or Q", "not P", "P implies Q", etc.
Your input: "${input}"`);
}
}
