import { PredicateFormula, PredicateArgument } from '../../../types.js';
import { PredicateParseTreeVisualizer } from './parseTreeVisualizer.js';
import { ModelVisualizer, PredicateModel } from './modelVisualizer.js';
import { QuantifierScopeVisualizer } from './quantifierScopeVisualizer.js';
/**
* Model definition for predicate logic (simplified)
*/
export interface SimplePredicateModel {
domain: string[];
constants: Map<string, string>;
predicates: Map<string, (args: string[]) => boolean>;
}
/**
* Main visualization class for predicate logic
* Provides a unified interface for different visualization options
*/
export class PredicateVisualizer {
private parseTreeVisualizer: PredicateParseTreeVisualizer;
private quantifierScopeVisualizer: QuantifierScopeVisualizer;
constructor() {
this.parseTreeVisualizer = new PredicateParseTreeVisualizer();
this.quantifierScopeVisualizer = new QuantifierScopeVisualizer();
}
/**
* Generate a visualization for a predicate formula or argument
* @param input The formula or argument to visualize
* @param type Type of visualization to generate
* @param format Output format
* @returns Visualization in the requested format
*/
visualize(
input: PredicateFormula | PredicateArgument,
type: 'parseTree' | 'model' | 'quantifierScope' = 'parseTree',
format: 'html' | 'svg' | 'text' = 'html'
): string {
// Generate the requested visualization type
switch (type) {
case 'parseTree':
if ('premises' in input) {
// For arguments, generate a combined parse tree
return this.generateCombinedParseTree(input, format);
} else {
// For single formulas, generate a standard parse tree
return this.parseTreeVisualizer.generateParseTree(input);
}
case 'model':
if ('premises' in input) {
// For arguments, we don't have a specific model to show
return this.generateArgumentModelPlaceholder(format);
} else {
// For single formulas, create a sample model
const model = this.createSampleModel(input);
const modelVisualizer = new ModelVisualizer(model);
return modelVisualizer.visualize(format);
}
case 'quantifierScope':
if ('premises' in input) {
// For arguments, we don't have a specific model to show
return this.generateQuantifierScopePlaceholder(format);
} else {
// For single formulas, use the quantifier scope visualizer
return this.quantifierScopeVisualizer.visualize(input, format);
}
default:
if ('premises' in input) {
return this.generateCombinedParseTree(input, format);
} else {
return this.parseTreeVisualizer.generateParseTree(input);
}
}
}
/**
* Generate a combined parse tree for a predicate argument
* @param argument The argument to visualize
* @param format Output format
* @returns Visualization in the requested format
*/
private generateCombinedParseTree(
argument: PredicateArgument,
format: 'html' | 'svg' | 'text'
): string {
// Create individual parse trees for each formula
const premiseTrees = argument.premises.map(premise =>
this.parseTreeVisualizer.generateParseTree(premise)
);
const conclusionTree = this.parseTreeVisualizer.generateParseTree(argument.conclusion);
// Combine trees into a single HTML layout
if (format === 'html' || format === 'text') {
let html = '<div class="combined-parse-tree">\n';
// Add premise trees
html += '<div class="premises">\n';
argument.premises.forEach((premise, index) => {
html += `<div class="premise">\n`;
html += `<h3>Premise ${index + 1}: ${this.formatFormula(premise)}</h3>\n`;
html += premiseTrees[index];
html += '</div>\n';
});
html += '</div>\n';
// Add therefore symbol
html += '<div class="therefore">\n';
html += '<h2>∴ (Therefore)</h2>\n';
html += '</div>\n';
// Add conclusion tree
html += '<div class="conclusion">\n';
html += `<h3>Conclusion: ${this.formatFormula(argument.conclusion)}</h3>\n`;
html += conclusionTree;
html += '</div>\n';
// Add CSS styling
html += `
<style>
.combined-parse-tree {
font-family: Arial, sans-serif;
margin: 20px 0;
}
.premises {
display: flex;
flex-wrap: wrap;
justify-content: center;
gap: 20px;
margin-bottom: 20px;
}
.premise, .conclusion {
border: 1px solid #ddd;
border-radius: 10px;
padding: 10px;
background-color: #f9f9f9;
}
.premise h3, .conclusion h3 {
text-align: center;
margin: 0 0 10px 0;
}
.therefore {
text-align: center;
margin: 20px 0;
}
.therefore h2 {
font-size: 24px;
margin: 0;
}
.conclusion {
margin: 0 auto;
max-width: 80%;
}
</style>
`;
html += '</div>';
return html;
} else {
// For SVG format, just return the conclusion tree for now
return conclusionTree;
}
}
/**
* Create a sample model for demonstration purposes
* @param formula Formula to create model for
* @returns Sample model
*/
private createSampleModel(formula: PredicateFormula): PredicateModel {
// Extract predicates, functions, and constants from the formula
const predicates = new Map<string, Set<string>>();
const functions = new Map<string, Map<string, string>>();
const constants = new Map<string, string>();
const extractSymbols = (f: PredicateFormula): void => {
switch (f.type) {
case 'predicate':
if (!predicates.has(f.name)) {
predicates.set(f.name, new Set<string>());
}
// Add a sample tuple
const tuple = f.args.map(arg =>
arg.type === 'constant' ? arg.name : 'a'
).join(',');
predicates.get(f.name)!.add(tuple);
break;
case 'constant':
if (!constants.has(f.name)) {
constants.set(f.name, 'a'); // Simple domain element mapping
}
break;
case 'function':
if (!functions.has(f.name)) {
functions.set(f.name, new Map<string, string>());
}
break;
case 'unary':
extractSymbols(f.operand);
break;
case 'binary':
extractSymbols(f.left);
extractSymbols(f.right);
break;
case 'quantified':
extractSymbols(f.formula);
break;
}
};
extractSymbols(formula);
// Create a simple domain
const domain = ['a', 'b', 'c'];
return {
domain,
constants,
functions,
predicates
};
}
/**
* Visualize quantifier scopes for an argument (placeholder)
* @param argument Argument to visualize
* @param format Output format
* @returns Visualization
*/
private visualizeArgumentScopes(argument: PredicateArgument, format: 'html' | 'svg' | 'text'): string {
return this.generateQuantifierScopePlaceholder(format);
}
/**
* Generate a placeholder for argument model visualization
* @param format Output format
* @returns Placeholder visualization
*/
private generateArgumentModelPlaceholder(format: 'html' | 'svg' | 'text'): string {
if (format === 'html') {
return `
<div style="padding: 20px; border: 1px solid #ddd; border-radius: 5px; background-color: #f9f9f9; text-align: center;">
<h3>Predicate Logic Model Visualization</h3>
<p>This feature is coming soon in a future update. Currently in development.</p>
<p>The model visualization will show the interpretation of predicates, functions, and constants in a finite domain.</p>
</div>
`;
} else if (format === 'svg') {
return `
<svg width="400" height="200" xmlns="http://www.w3.org/2000/svg">
<rect x="0" y="0" width="400" height="200" fill="#f9f9f9" stroke="#ddd" stroke-width="2" rx="5" ry="5" />
<text x="200" y="80" text-anchor="middle" font-family="Arial" font-size="18" font-weight="bold">Model Visualization</text>
<text x="200" y="120" text-anchor="middle" font-family="Arial" font-size="14">Coming soon in a future update.</text>
</svg>
`;
} else {
return "Model Visualization\n\nThis feature is coming soon in a future update. Currently in development.\n";
}
}
/**
* Generate a placeholder for quantifier scope visualization (to be implemented later)
* @param format Output format
* @returns Placeholder visualization
*/
private generateQuantifierScopePlaceholder(format: 'html' | 'svg' | 'text'): string {
if (format === 'html') {
return `
<div style="padding: 20px; border: 1px solid #ddd; border-radius: 5px; background-color: #f9f9f9; text-align: center;">
<h3>Quantifier Scope Visualization</h3>
<p>This feature is coming soon in a future update. Currently in development.</p>
<p>The quantifier scope visualization will show nested scopes of universal and existential quantifiers in predicate formulas.</p>
</div>
`;
} else if (format === 'svg') {
return `
<svg width="400" height="200" xmlns="http://www.w3.org/2000/svg">
<rect x="0" y="0" width="400" height="200" fill="#f9f9f9" stroke="#ddd" stroke-width="2" rx="5" ry="5" />
<text x="200" y="80" text-anchor="middle" font-family="Arial" font-size="18" font-weight="bold">Quantifier Scope Visualization</text>
<text x="200" y="120" text-anchor="middle" font-family="Arial" font-size="14">Coming soon in a future update.</text>
</svg>
`;
} else {
return "Quantifier Scope Visualization\n\nThis feature is coming soon in a future update. Currently in development.\n";
}
}
/**
* Format a predicate formula as a string
* @param formula The formula to format
* @returns Formatted string representation
*/
private formatFormula(formula: PredicateFormula): string {
switch (formula.type) {
case 'variable':
return formula.name;
case 'constant':
return formula.name;
case 'function':
if (formula.args.length === 0) {
return formula.name;
} else {
const args = formula.args.map(arg => this.formatFormula(arg)).join(', ');
return `${formula.name}(${args})`;
}
case 'predicate':
if (formula.args.length === 0) {
return formula.name;
} else {
const args = formula.args.map(arg => this.formatFormula(arg)).join(', ');
return `${formula.name}(${args})`;
}
case 'unary':
const unaryOpSymbol = formula.operator === 'not' ? '¬' : formula.operator;
const operand = this.formatFormula(formula.operand);
// Add parentheses if the operand is not a variable, constant, function, or predicate
if (
formula.operand.type !== 'variable' &&
formula.operand.type !== 'constant' &&
formula.operand.type !== 'function' &&
formula.operand.type !== 'predicate'
) {
return `${unaryOpSymbol}(${operand})`;
} else {
return `${unaryOpSymbol}${operand}`;
}
case 'binary':
const left = this.formatFormula(formula.left);
const right = this.formatFormula(formula.right);
// Convert operator to symbol if needed
let binaryOpSymbol: string;
switch (formula.operator) {
case 'and': binaryOpSymbol = '∧'; break;
case 'or': binaryOpSymbol = '∨'; break;
case 'implies': binaryOpSymbol = '→'; break;
case 'iff': binaryOpSymbol = '↔'; break;
default: binaryOpSymbol = formula.operator;
}
// Add parentheses around operands if needed
const leftStr = (
formula.left.type === 'binary' ||
formula.left.type === 'quantified'
) ? `(${left})` : left;
const rightStr = (
formula.right.type === 'binary' ||
formula.right.type === 'quantified'
) ? `(${right})` : right;
return `${leftStr} ${binaryOpSymbol} ${rightStr}`;
case 'quantified':
const quantSymbol = formula.quantifier === 'forall' ? '∀' :
formula.quantifier === 'exists' ? '∃' :
formula.quantifier;
const subformula = this.formatFormula(formula.formula);
// Add parentheses if the subformula is a binary operation
const formulaStr = formula.formula.type === 'binary' ? `(${subformula})` : subformula;
return `${quantSymbol}${formula.variable}.${formulaStr}`;
default:
return 'Unknown formula type';
}
}
/**
* Check if a predicate formula is valid (true in all models)
* Not fully implemented - placeholder for future development
* @param formula The formula to check
* @returns Whether the formula is valid
*/
isFormulaValid(formula: PredicateFormula): boolean {
// This would require a theorem prover for predicate logic
// For now, return a placeholder result
return false;
}
/**
* Check if a predicate argument is valid (conclusion follows from premises)
* Not fully implemented - placeholder for future development
* @param argument The argument to check
* @returns Whether the argument is valid
*/
isArgumentValid(argument: PredicateArgument): boolean {
// This would require a theorem prover for predicate logic
// For now, return a placeholder result
return false;
}
}
