/ concept-collection / proofery
Sign in
concept-collection / proofery
proofery / src / simplifier.ts
64 lines · 1.9 KBBlameHistoryRaw
1/**
2 * Expression simplification based on context.
3 */
5import { Expression } from './expression.js';
6import { Context } from './context.js';
8/**
9 * Simplify an expression based on the context.
10 */
11export function simplify(expr: Expression, context: Context): Expression {
12 let current = expr;
13 let previous: Expression | null = null;
15 // Keep applying simplification rules until no more changes
16 while (previous === null || !current.equals(previous)) {
17 previous = current;
18 current = applySimplificationRules(current, context);
19 }
21 return current;
24/**
25 * Apply simplification rules once.
26 */
27function applySimplificationRules(expr: Expression, context: Context): Expression {
28 // Rule: left(h) → a if h has type and(a, b)
29 if (expr.name === 'left' && expr.children.length === 1) {
30 const arg = expr.children[0];
31 const argType = getTypeOfExpr(arg, context);
32 if (argType && argType.name === 'and' && argType.children.length === 2) {
33 return argType.children[0];
34 }
35 }
37 // Rule: right(h) → b if h has type and(a, b)
38 if (expr.name === 'right' && expr.children.length === 1) {
39 const arg = expr.children[0];
40 const argType = getTypeOfExpr(arg, context);
41 if (argType && argType.name === 'and' && argType.children.length === 2) {
42 return argType.children[1];
43 }
44 }
46 // Recursively simplify children
47 const simplifiedChildren = expr.children.map(child =>
48 applySimplificationRules(child, context)
49 );
51 return new Expression(expr.name, simplifiedChildren);
54/**
55 * Get the type of an expression from the context.
56 */
57function getTypeOfExpr(expr: Expression, context: Context): Expression | null {
58 // Simple case: variable name lookup
59 if (expr.children.length === 0) {
60 return context.getVariableType(expr.name) || null;
61 }
63 return null;
moveopenescclose