import { ModalFormula, ModalOperator, ModalArgument, ModalSystem } from '../types.js';
import { PropositionalParser } from './propositionalParser.js';
import { Loggers } from '../utils/logger.js';
const logger = Loggers.modal;
export class ModalParser {
private propParser: PropositionalParser;
constructor() {
this.propParser = new PropositionalParser();
}
parse(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'symbolic'): ModalFormula {
logger.debug(`Parsing modal formula: ${input} (format: ${format})`);
if (format === 'natural') {
return this.parseNatural(input);
}
// For symbolic and mixed, use symbolic parser
return this.parseSymbolic(input);
}
private parseNatural(input: string): ModalFormula {
const normalized = input.toLowerCase().trim();
// Enhanced necessity patterns
const necessityPatterns = [
/it is necessary that (.+)/,
/necessarily (.+)/,
/it must be that (.+)/,
/it must be the case that (.+)/,
/must be that (.+)/,
/has to be that (.+)/,
/has to be the case that (.+)/,
/it is required that (.+)/,
/it is certain that (.+)/
];
for (const pattern of necessityPatterns) {
const match = normalized.match(pattern);
if (match) {
return {
type: 'modal',
operator: 'necessary',
operand: this.parseNatural(match[1].trim())
};
}
}
// Enhanced possibility patterns
const possibilityPatterns = [
/it is possible that (.+)/,
/possibly (.+)/,
/it might be that (.+)/,
/it might be the case that (.+)/,
/might be that (.+)/,
/could be that (.+)/,
/it could be that (.+)/,
/it could be the case that (.+)/,
/can be that (.+)/,
/it can be that (.+)/,
/it may be that (.+)/,
/may be that (.+)/,
/perhaps (.+)/,
/maybe (.+)/
];
for (const pattern of possibilityPatterns) {
const match = normalized.match(pattern);
if (match) {
return {
type: 'modal',
operator: 'possible',
operand: this.parseNatural(match[1].trim())
};
}
}
// Check for modal operators at the start (without "that")
if (normalized.startsWith('necessarily ')) {
return {
type: 'modal',
operator: 'necessary',
operand: this.parseNatural(normalized.substring(12).trim())
};
}
if (normalized.startsWith('possibly ')) {
return {
type: 'modal',
operator: 'possible',
operand: this.parseNatural(normalized.substring(9).trim())
};
}
// Fall back to propositional parser for non-modal content
return this.propParser.parse(normalized) as any;
}
private parseSymbolic(input: string): ModalFormula {
const trimmed = input.trim();
logger.debug(`Parsing symbolic modal formula: ${trimmed}`);
// Handle negation (¬) first
if (trimmed.startsWith('¬') || trimmed.toLowerCase().startsWith('not ')) {
const content = trimmed.startsWith('¬') ? trimmed.slice(1) : trimmed.slice(4);
return {
type: 'unary',
operator: '¬',
operand: this.parseSymbolic(content.trim())
} as any;
}
// Check for modal operators at the start
if (trimmed.startsWith('□') || trimmed.startsWith('[]')) {
const content = trimmed.startsWith('□') ? trimmed.slice(1) : trimmed.slice(2);
return {
type: 'modal',
operator: '□',
operand: this.parseSymbolic(content.trim())
};
}
if (trimmed.startsWith('◇') || trimmed.startsWith('<>')) {
const content = trimmed.startsWith('◇') ? trimmed.slice(1) : trimmed.slice(2);
return {
type: 'modal',
operator: '◇',
operand: this.parseSymbolic(content.trim())
};
}
// Handle parentheses - but only strip outermost if they match
if (trimmed.startsWith('(') && this.hasMatchingClosingParen(trimmed)) {
return this.parseSymbolic(trimmed.slice(1, -1));
}
// Parse binary operators with proper precedence
// Order: implies/iff (lowest) > or > and > modal/not (highest)
// Try to find implication (→, implies) at the top level
const impliesPos = this.findTopLevelOperator(trimmed, ['→', 'implies']);
if (impliesPos !== -1) {
const left = trimmed.substring(0, impliesPos).trim();
const right = trimmed.substring(impliesPos + (trimmed[impliesPos] === '→' ? 1 : 7)).trim();
return {
type: 'binary',
operator: 'implies',
left: this.parseSymbolic(left),
right: this.parseSymbolic(right)
} as any;
}
// Try to find iff (↔, iff)
const iffPos = this.findTopLevelOperator(trimmed, ['↔', 'iff']);
if (iffPos !== -1) {
const left = trimmed.substring(0, iffPos).trim();
const right = trimmed.substring(iffPos + (trimmed[iffPos] === '↔' ? 1 : 3)).trim();
return {
type: 'binary',
operator: 'iff',
left: this.parseSymbolic(left),
right: this.parseSymbolic(right)
} as any;
}
// Try to find or (∨, or)
const orPos = this.findTopLevelOperator(trimmed, ['∨', 'or']);
if (orPos !== -1) {
const left = trimmed.substring(0, orPos).trim();
const right = trimmed.substring(orPos + (trimmed[orPos] === '∨' ? 1 : 2)).trim();
return {
type: 'binary',
operator: 'or',
left: this.parseSymbolic(left),
right: this.parseSymbolic(right)
} as any;
}
// Try to find and (∧, and)
const andPos = this.findTopLevelOperator(trimmed, ['∧', 'and']);
if (andPos !== -1) {
const left = trimmed.substring(0, andPos).trim();
const right = trimmed.substring(andPos + (trimmed[andPos] === '∧' ? 1 : 3)).trim();
return {
type: 'binary',
operator: 'and',
left: this.parseSymbolic(left),
right: this.parseSymbolic(right)
} as any;
}
// Try to find xor (⊕, xor)
const xorPos = this.findTopLevelOperator(trimmed, ['⊕', 'xor']);
if (xorPos !== -1) {
const left = trimmed.substring(0, xorPos).trim();
const right = trimmed.substring(xorPos + (trimmed[xorPos] === '⊕' ? 1 : 3)).trim();
return {
type: 'binary',
operator: 'xor',
left: this.parseSymbolic(left),
right: this.parseSymbolic(right)
} as any;
}
// If no operators found, must be a variable
if (this.isVariable(trimmed)) {
return {
type: 'variable',
name: trimmed
};
}
throw new Error(`Failed to parse modal formula: ${input}`);
}
/**
* Find the position of a top-level operator (not inside parentheses)
*/
private findTopLevelOperator(input: string, operators: string[]): number {
let depth = 0;
for (let i = 0; i < input.length; i++) {
if (input[i] === '(') {
depth++;
} else if (input[i] === ')') {
depth--;
} else if (depth === 0) {
// Check each operator
for (const op of operators) {
if (input.substring(i, i + op.length) === op) {
// For word operators, ensure they're not part of a larger word
if (op.match(/[a-z]/i)) {
const before = i === 0 || !input[i - 1].match(/[a-zA-Z0-9]/);
const after = i + op.length >= input.length || !input[i + op.length].match(/[a-zA-Z0-9]/);
if (before && after) {
return i;
}
} else {
return i;
}
}
}
}
}
return -1;
}
/**
* Check if the first character is '(' and has a matching ')' at the end
*/
private hasMatchingClosingParen(input: string): boolean {
if (!input.startsWith('(')) return false;
let depth = 0;
for (let i = 0; i < input.length; i++) {
if (input[i] === '(') depth++;
else if (input[i] === ')') depth--;
if (depth === 0) {
return i === input.length - 1;
}
}
return false;
}
/**
* Check if a string is a valid variable name
*/
private isVariable(input: string): boolean {
return /^[A-Za-z][A-Za-z0-9_]*$/.test(input);
}
parseArgument(input: string, format: 'natural' | 'symbolic' | 'mixed' = 'symbolic', system: ModalSystem = 'K'): ModalArgument {
logger.debug(`Parsing modal argument with system ${system}`);
// Split by conclusion indicators (including "prove that", "show that")
const conclusionPattern = /\b(therefore|thus|hence|so|prove that|show that|demonstrate that|∴)\b/i;
const match = input.match(conclusionPattern);
if (!match) {
throw new Error('No conclusion indicator found in argument');
}
const premisesText = input.substring(0, match.index).trim();
const conclusionText = input.substring(match.index! + match[0].length).trim();
// Parse premises (split by commas or semicolons)
const premiseStrings = premisesText.split(/[,;]/).map(p => p.trim()).filter(p => p);
const premises = premiseStrings.map(p => this.parse(p, format));
// Parse conclusion
const conclusion = this.parse(conclusionText, format);
return { premises, conclusion, system };
}
formatFormula(formula: ModalFormula): string {
if ('type' in formula && formula.type === 'modal') {
const op = formula.operator === 'necessary' || formula.operator === '□' ? '□' : '◇';
return `${op}${this.formatFormula(formula.operand)}`;
}
// Use custom formatter for non-modal formulas
return this.formatPropositionalFormula(formula as any);
}
private formatPropositionalFormula(formula: any): string {
if (!formula) return '';
switch (formula.type) {
case 'variable':
return formula.name;
case 'unary':
return `¬${this.formatPropositionalFormula(formula.operand)}`;
case 'binary':
const left = this.formatPropositionalFormula(formula.left);
const right = this.formatPropositionalFormula(formula.right);
let op = formula.operator;
// Convert operator names to symbols
if (op === 'and') op = '∧';
else if (op === 'or') op = '∨';
else if (op === 'implies') op = '→';
else if (op === 'iff') op = '↔';
return `(${left} ${op} ${right})`;
default:
return formula.toString();
}
}
}
