import { ModalParser } from './modalParser.js';
import {
createNecessity,
createPossibility,
createVariable,
createImplication,
createConjunction,
testFormulas,
assertModalFormula,
assertVariableFormula,
assertModalOperator
} from '../test-utils/modalTestHelpers.js';
describe('ModalParser', () => {
let parser: ModalParser;
beforeEach(() => {
parser = new ModalParser();
});
describe('Natural Language Parsing', () => {
test('parses "it is necessary that P"', () => {
const result = parser.parse('it is necessary that P', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('necessary');
assertVariableFormula(result.operand, 'p');
}
});
test('parses "necessarily P"', () => {
const result = parser.parse('necessarily P', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('necessary');
}
});
test('parses "it must be that P"', () => {
const result = parser.parse('it must be that P', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('necessary');
}
});
test('parses "it is possible that Q"', () => {
const result = parser.parse('it is possible that Q', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('possible');
assertVariableFormula(result.operand, 'q');
}
});
test('parses "possibly Q"', () => {
const result = parser.parse('possibly Q', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('possible');
}
});
test('parses "it might be that Q"', () => {
const result = parser.parse('it might be that Q', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('possible');
}
});
test('parses "maybe Q"', () => {
const result = parser.parse('maybe Q', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('possible');
}
});
test('parses nested natural language modalities', () => {
const result = parser.parse('it is necessary that it is possible that P', 'natural');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('necessary');
expect(result.operand.type).toBe('modal');
if (result.operand.type === 'modal') {
expect(result.operand.operator).toBe('possible');
}
}
});
});
describe('Symbolic Parsing', () => {
test('parses simple necessity □P', () => {
const result = parser.parse('□P', 'symbolic');
assertModalFormula(result);
assertModalOperator(result, '□');
});
test('parses simple possibility ◇Q', () => {
const result = parser.parse('◇Q', 'symbolic');
assertModalFormula(result);
assertModalOperator(result, '◇');
});
test('parses nested necessity □□P', () => {
const result = parser.parse('□□P', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('□');
expect(result.operand.type).toBe('modal');
if (result.operand.type === 'modal') {
expect(result.operand.operator).toBe('□');
}
}
});
test('parses mixed modalities ◇□P', () => {
const result = parser.parse('◇□P', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operator).toBe('◇');
expect(result.operand.type).toBe('modal');
if (result.operand.type === 'modal') {
expect(result.operand.operator).toBe('□');
}
}
});
test('parses T axiom: (□P) → P', () => {
const result = parser.parse('(□P) → P', 'symbolic');
assertModalFormula(result);
// The parser should recognize this as an implication at the top level
expect(result.type).toBe('binary');
if (result.type === 'binary') {
expect(result.operator).toBe('implies');
expect(result.left.type).toBe('modal');
expect(result.right.type).toBe('variable');
}
});
test('parses S5 axiom: (◇P) → (□◇P)', () => {
const result = parser.parse('(◇P) → (□◇P)', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('binary');
if (result.type === 'binary') {
expect(result.operator).toBe('implies');
expect(result.left.type).toBe('modal');
expect(result.right.type).toBe('modal');
}
});
test('parses complex formula with conjunction: □(P ∧ Q)', () => {
const result = parser.parse('□(P ∧ Q)', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('modal');
if (result.type === 'modal') {
expect(result.operand.type).toBe('binary');
}
});
test('parses negated necessity: ¬□P', () => {
const result = parser.parse('¬□P', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('unary');
if (result.type === 'unary') {
expect(result.operator).toBe('¬');
expect(result.operand.type).toBe('modal');
}
});
test('parses parenthesized modal formula: (□P)', () => {
const result = parser.parse('(□P)', 'symbolic');
assertModalFormula(result);
expect(result.type).toBe('modal');
});
});
describe('Argument Parsing', () => {
test('parses argument with "therefore"', () => {
const arg = parser.parseArgument('□P, □(P → Q) therefore □Q', 'symbolic');
expect(arg.premises).toHaveLength(2);
expect(arg.conclusion).toBeDefined();
expect(arg.system).toBe('K');
});
test('parses argument with "thus"', () => {
const arg = parser.parseArgument('□P thus ◇P', 'symbolic', 'T');
expect(arg.premises).toHaveLength(1);
expect(arg.conclusion).toBeDefined();
expect(arg.system).toBe('T');
});
test('parses argument with multiple premises', () => {
const arg = parser.parseArgument('□P, □Q, □(P ∧ Q → R) therefore □R', 'symbolic');
expect(arg.premises).toHaveLength(3);
});
test('parses argument with natural language', () => {
const arg = parser.parseArgument(
'it is necessary that P, necessarily if P then Q therefore necessarily Q',
'natural'
);
expect(arg.premises).toHaveLength(2);
expect(arg.conclusion).toBeDefined();
});
test('uses specified modal system', () => {
const arg = parser.parseArgument('□P therefore P', 'symbolic', 'S5');
expect(arg.system).toBe('S5');
});
});
describe('Error Handling', () => {
test('throws error for invalid formula', () => {
expect(() => parser.parse('□□□', 'symbolic')).toThrow();
});
test('throws error for argument without conclusion indicator', () => {
expect(() => parser.parseArgument('□P, □Q', 'symbolic')).toThrow('No conclusion indicator found');
});
test('throws error for empty input', () => {
expect(() => parser.parse('', 'symbolic')).toThrow();
});
});
describe('Formula Formatting', () => {
test('formats necessity operator', () => {
const formula = createNecessity(createVariable('P'));
const formatted = parser.formatFormula(formula);
expect(formatted).toContain('□');
});
test('formats possibility operator', () => {
const formula = createPossibility(createVariable('Q'));
const formatted = parser.formatFormula(formula);
expect(formatted).toContain('◇');
});
test('formats complex formula', () => {
const formula = createImplication(
createNecessity(createVariable('P')),
createVariable('P')
);
const formatted = parser.formatFormula(formula);
expect(formatted).toBeTruthy();
expect(formatted.length).toBeGreaterThan(0);
});
});
});
