import { ProofLibrary, ProofStep, SavedProof } from '../src/proofLibrary.js';
import * as fs from 'fs';
import * as path from 'path';
describe('ProofLibrary', () => {
let proofLibrary: ProofLibrary;
const testDbPath = './data/test-proofs.db';
beforeEach(() => {
// Remove test database if it exists
if (fs.existsSync(testDbPath)) {
fs.unlinkSync(testDbPath);
}
proofLibrary = new ProofLibrary(testDbPath);
});
afterEach(() => {
// Clean up
proofLibrary.close();
if (fs.existsSync(testDbPath)) {
fs.unlinkSync(testDbPath);
}
});
describe('saveProof', () => {
it('should save a proof successfully', () => {
const proofSteps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' },
{ stepNumber: 2, statement: 'P → Q', justification: 'Premise' },
{ stepNumber: 3, statement: 'Q', justification: 'Modus Ponens', rule: 'MP', references: [1, 2] }
];
const proof = proofLibrary.saveProof(
'Modus Ponens Example',
'A simple modus ponens proof',
'propositional',
['P', 'P → Q'],
'Q',
proofSteps,
['example', 'basic'],
'user'
);
expect(proof).toBeDefined();
expect(proof.id).toBeDefined();
expect(proof.name).toBe('Modus Ponens Example');
expect(proof.system).toBe('propositional');
expect(proof.premises).toEqual(['P', 'P → Q']);
expect(proof.conclusion).toBe('Q');
expect(proof.proofSteps).toEqual(proofSteps);
expect(proof.tags).toEqual(['example', 'basic']);
expect(proof.usageCount).toBe(0);
expect(proof.successRate).toBe(1.0);
});
it('should save a proof without optional parameters', () => {
const proofSteps: ProofStep[] = [
{ stepNumber: 1, statement: 'All men are mortal', justification: 'Premise' },
{ stepNumber: 2, statement: 'Socrates is a man', justification: 'Premise' },
{ stepNumber: 3, statement: 'Socrates is mortal', justification: 'Conclusion' }
];
const proof = proofLibrary.saveProof(
'Socrates Syllogism',
undefined,
'syllogistic',
['All men are mortal', 'Socrates is a man'],
'Socrates is mortal',
proofSteps
);
expect(proof).toBeDefined();
expect(proof.description).toBeUndefined();
expect(proof.tags).toEqual([]);
expect(proof.author).toBe('user');
});
});
describe('getProof', () => {
it('should retrieve a saved proof', () => {
const proofSteps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
const savedProof = proofLibrary.saveProof(
'Test Proof',
'Test description',
'propositional',
['P'],
'P',
proofSteps
);
const retrieved = proofLibrary.getProof(savedProof.id);
expect(retrieved).toBeDefined();
expect(retrieved?.id).toBe(savedProof.id);
expect(retrieved?.name).toBe('Test Proof');
expect(retrieved?.description).toBe('Test description');
});
it('should return null for non-existent proof', () => {
const proof = proofLibrary.getProof('non-existent-id');
expect(proof).toBeNull();
});
});
describe('searchProofs', () => {
beforeEach(() => {
// Add multiple proofs for testing
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
proofLibrary.saveProof('Proof 1', 'About logic', 'propositional', ['P'], 'P', steps, ['logic', 'test']);
proofLibrary.saveProof('Proof 2', 'About reasoning', 'predicate', ['∀x P(x)'], 'P(a)', steps, ['reasoning']);
proofLibrary.saveProof('Proof 3', 'Modal proof', 'modal', ['□P'], 'P', steps, ['modal', 'test']);
});
it('should find proofs by full-text search', () => {
const results = proofLibrary.searchProofs({ query: 'logic' });
expect(results.length).toBeGreaterThan(0);
expect(results[0].name).toBe('Proof 1');
});
it('should filter proofs by system', () => {
const results = proofLibrary.searchProofs({ system: 'modal' });
expect(results.length).toBe(1);
expect(results[0].name).toBe('Proof 3');
});
it('should filter proofs by tags', () => {
const results = proofLibrary.searchProofs({ tags: ['test'] });
expect(results.length).toBe(2);
});
it('should support pagination', () => {
const results = proofLibrary.searchProofs({ limit: 2, offset: 0 });
expect(results.length).toBe(2);
const results2 = proofLibrary.searchProofs({ limit: 2, offset: 2 });
expect(results2.length).toBe(1);
});
});
describe('listProofs', () => {
beforeEach(() => {
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
proofLibrary.saveProof('Proof A', 'Description A', 'propositional', ['P'], 'P', steps);
proofLibrary.saveProof('Proof B', 'Description B', 'modal', ['□P'], 'P', steps);
proofLibrary.saveProof('Proof C', 'Description C', 'propositional', ['Q'], 'Q', steps);
});
it('should list all proofs', () => {
const proofs = proofLibrary.listProofs();
expect(proofs.length).toBe(3);
});
it('should filter by system', () => {
const proofs = proofLibrary.listProofs('propositional');
expect(proofs.length).toBe(2);
});
it('should support pagination', () => {
const proofs = proofLibrary.listProofs(undefined, 2, 0);
expect(proofs.length).toBe(2);
});
});
describe('recordUsage', () => {
it('should update usage count and success rate', () => {
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
const proof = proofLibrary.saveProof(
'Usage Test',
undefined,
'propositional',
['P'],
'P',
steps
);
// Record successful usage
proofLibrary.recordUsage(proof.id, true);
let updated = proofLibrary.getProof(proof.id);
expect(updated?.usageCount).toBe(1);
expect(updated?.successRate).toBeGreaterThan(0.9); // Should still be high
// Record failed usage
proofLibrary.recordUsage(proof.id, false);
updated = proofLibrary.getProof(proof.id);
expect(updated?.usageCount).toBe(2);
expect(updated?.successRate).toBeLessThan(1.0); // Should decrease
});
it('should throw error for non-existent proof', () => {
expect(() => {
proofLibrary.recordUsage('non-existent-id', true);
}).toThrow();
});
});
describe('deleteProof', () => {
it('should delete a proof', () => {
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
const proof = proofLibrary.saveProof(
'To Delete',
undefined,
'propositional',
['P'],
'P',
steps
);
const deleted = proofLibrary.deleteProof(proof.id);
expect(deleted).toBe(true);
const retrieved = proofLibrary.getProof(proof.id);
expect(retrieved).toBeNull();
});
it('should return false for non-existent proof', () => {
const deleted = proofLibrary.deleteProof('non-existent-id');
expect(deleted).toBe(false);
});
});
describe('saveLemma and getLemma', () => {
it('should save and retrieve a lemma', () => {
const lemma = proofLibrary.saveLemma(
'Test Lemma',
'A test lemma',
'propositional',
['P', 'P → Q'],
'Q',
['logic']
);
expect(lemma).toBeDefined();
expect(lemma.id).toBeDefined();
expect(lemma.name).toBe('Test Lemma');
const retrieved = proofLibrary.getLemma(lemma.id);
expect(retrieved).toBeDefined();
expect(retrieved?.name).toBe('Test Lemma');
});
});
describe('searchLemmas', () => {
beforeEach(() => {
proofLibrary.saveLemma('Lemma 1', 'Description 1', 'propositional', ['P'], 'P', ['tag1']);
proofLibrary.saveLemma('Lemma 2', 'Description 2', 'modal', ['□P'], 'P', ['tag2']);
});
it('should filter lemmas by system', () => {
const lemmas = proofLibrary.searchLemmas('propositional');
expect(lemmas.length).toBe(1);
expect(lemmas[0].name).toBe('Lemma 1');
});
it('should filter lemmas by tags', () => {
const lemmas = proofLibrary.searchLemmas(undefined, ['tag2']);
expect(lemmas.length).toBe(1);
expect(lemmas[0].name).toBe('Lemma 2');
});
});
describe('composeLemmas', () => {
it('should compose lemmas into a proof', () => {
const lemma1 = proofLibrary.saveLemma(
'Lemma 1',
'First lemma',
'propositional',
['P'],
'Q',
[]
);
const lemma2 = proofLibrary.saveLemma(
'Lemma 2',
'Second lemma',
'propositional',
['Q'],
'R',
[]
);
const result = proofLibrary.composeLemmas(
'Composed Proof',
[lemma1.id, lemma2.id],
[],
'Composition of two lemmas',
['composed']
);
expect(result.success).toBe(true);
expect(result.composedProof).toBeDefined();
expect(result.composedProof?.name).toBe('Composed Proof');
expect(result.steps.length).toBeGreaterThan(0);
});
it('should fail when composing lemmas from different systems', () => {
const lemma1 = proofLibrary.saveLemma('L1', '', 'propositional', ['P'], 'Q', []);
const lemma2 = proofLibrary.saveLemma('L2', '', 'modal', ['□P'], 'P', []);
const result = proofLibrary.composeLemmas('Mixed', [lemma1.id, lemma2.id]);
expect(result.success).toBe(false);
expect(result.message).toContain('different logical systems');
});
it('should fail when lemma not found', () => {
const result = proofLibrary.composeLemmas('Test', ['non-existent-id']);
expect(result.success).toBe(false);
expect(result.message).toContain('not found');
});
});
describe('getStats', () => {
beforeEach(() => {
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
proofLibrary.saveProof('Proof 1', '', 'propositional', ['P'], 'P', steps, [], 'user');
proofLibrary.saveProof('Proof 2', '', 'modal', ['□P'], 'P', steps, [], 'claude');
proofLibrary.saveLemma('Lemma 1', '', 'propositional', ['P'], 'Q', []);
});
it('should return comprehensive statistics', () => {
const stats = proofLibrary.getStats();
expect(stats.totalProofs).toBe(2);
expect(stats.totalLemmas).toBe(1);
expect(stats.proofsBySystem['propositional']).toBe(1);
expect(stats.proofsBySystem['modal']).toBe(1);
expect(stats.proofsByAuthor.user).toBe(1);
expect(stats.proofsByAuthor.claude).toBe(1);
expect(stats.averageSuccessRate).toBe(1.0);
});
it('should include most used proofs', () => {
const steps: ProofStep[] = [
{ stepNumber: 1, statement: 'P', justification: 'Premise' }
];
const proof = proofLibrary.saveProof('Popular', '', 'propositional', ['P'], 'P', steps);
proofLibrary.recordUsage(proof.id, true);
proofLibrary.recordUsage(proof.id, true);
const stats = proofLibrary.getStats();
expect(stats.mostUsedProofs.length).toBeGreaterThan(0);
expect(stats.mostUsedProofs[0].name).toBe('Popular');
expect(stats.mostUsedProofs[0].usageCount).toBe(2);
});
});
});
