feat: implement type inference from assumptions (#21)

When assumptions are made, symbol types are now correctly inferred:

- Inequality assumptions (>, <, >=, <=) set the symbol's type to 'real'
- Equality assumptions infer the type from the value:
  - Equal to integer → type 'integer'
  - Equal to rational → type 'real'
  - Equal to real → type 'real'
  - Equal to complex → type 'number'

Implementation:
- Added inferTypeFromValue() function to promote specific types
  (e.g., finite_integer → integer)
- Updated assumeEquality() to use inferTypeFromValue when updating types
- Updated assumeInequality() to set type 'real' even for auto-declared symbols

Examples:
  ce.assume(ce.box(['Greater', 'x', 4]));
  ce.box('x').type.toString();  // → 'real' (was: 'unknown')

  ce.assume(ce.box(['Equal', 'one', 1]));
  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')

Files modified:
- src/compute-engine/assume.ts - Added inferTypeFromValue(), updated type inference
- test/compute-engine/assumptions.test.ts - Enabled 6 tests
- CHANGELOG.md, requirements/TODO.md, requirements/DONE.md - Documentation

https://claude.ai/code/session_01Xx26gPU9ThyiypRqdLcmZQ

Author: claude

CHANGELOG.md

@@ -33,6 +33,19 @@
   This works by extracting lower/upper bounds from inequality assumptions
   and using them during comparison operations.
 
+- **Type Inference from Assumptions**: When assumptions are made, symbol types
+  are now correctly inferred. Inequality assumptions (`>`, `<`, `>=`, `<=`) set
+  the symbol's type to `real`, and equality assumptions infer the type from the
+  value (e.g., equal to an integer means type `integer`).
+
+  ```javascript
+  ce.assume(ce.box(['Greater', 'x', 4]));
+  ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+  ce.assume(ce.box(['Equal', 'one', 1]));
+  ce.box('one').type.toString();  // → 'integer' (was: 'unknown')
+  ```
+
 ### Bug Fixes
 
 - **forget() Now Clears Assumed Values**: Fixed an issue where `ce.forget()` did not

requirements/DONE.md

@@ -1184,3 +1184,52 @@ ce.box('y').evaluate().json;  // → 'y' (was: 10)
 
 **Tests added:**
 - `test/compute-engine/bug-fixes.test.ts` - Test for scoped assumption cleanup
+
+---
+
+### 21. Type Inference from Assumptions ✅
+
+**IMPLEMENTED:** When assumptions are made, symbol types are now correctly inferred
+based on the assumption.
+
+**Problem:** When `ce.assume(['Greater', 'x', 4])` was called, the symbol's type
+remained 'unknown'. Similarly, when `ce.assume(['Equal', 'one', 1])` was called,
+the symbol's type was 'finite_integer' instead of 'integer'.
+
+**Solution:** Modified the assumption processing to update symbol types:
+
+1. **For equality assumptions**: Added `inferTypeFromValue()` function that promotes
+   specific types to more general ones (e.g., `finite_integer` → `integer`,
+   `finite_real_number` → `real`). This is used when updating the type of a symbol
+   with an inferred type.
+
+2. **For inequality assumptions**: Updated `assumeInequality()` to set the symbol's
+   type to 'real' even when the symbol was already auto-declared with an inferred type.
+
+**Type promotion rules:**
+- `finite_integer`, `integer` → `integer`
+- `rational` → `real`
+- `finite_real_number`, `real` → `real`
+- `complex`, `imaginary` → `number`
+
+**Examples that now work:**
+```typescript
+ce.assume(ce.box(['Greater', 'x', 4]));
+ce.box('x').type.toString();  // → 'real' (was: 'unknown')
+
+ce.assume(ce.box(['Equal', 'one', 1]));
+ce.box('one').type.toString();  // → 'integer' (was: 'finite_integer' or 'unknown')
+
+ce.assume(ce.box(['Greater', 't', 0]));
+ce.box('t').type.toString();  // → 'real'
+
+ce.assume(ce.box(['Equal', 'p', 11]));
+ce.box('p').type.toString();  // → 'integer'
+```
+
+**Files modified:**
+- `src/compute-engine/assume.ts` - Added `inferTypeFromValue()`, updated type inference
+
+**Tests enabled:**
+- `test/compute-engine/assumptions.test.ts` - Enabled "TYPE INFERENCE FROM ASSUMPTIONS"
+  describe block (6 tests)

requirements/TODO.md

@@ -824,46 +824,9 @@ CONTRADICTION DETECTION"
 
 ---
 
-### 21. Type Inference from Assumptions
+### ~~21. Type Inference from Assumptions~~ ✅ COMPLETED
 
-**Problem:** When assumptions are made, symbol types should be inferred. For
-example, `x > 4` implies `x` is real, and `one = 1` implies `one` is an integer.
-
-**Current behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Returns: "unknown"
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Returns: "unknown"
-```
-
-**Expected behavior:**
-
-```typescript
-ce.assume(ce.box(['Greater', 'x', 4]));
-ce.box('x').type.toString()  // Should return: "real" (inequalities imply real numbers)
-
-ce.assume(ce.box(['Equal', 'one', 1]));
-ce.box('one').type.toString()  // Should return: "integer" (equal to integer literal)
-```
-
-**Implementation notes:**
-
-- Inequality assumptions (`>`, `<`, `>=`, `<=`) imply the symbol is `real`
-- Equality to an integer implies the symbol is `integer`
-- Equality to a rational implies the symbol is `rational`
-- This might be handled by updating the symbol's type when an assumption is made
-- Alternatively, the type getter could query assumptions
-
-**Files to investigate:**
-
-- `src/compute-engine/assume.ts` - Assumption processing
-- `src/compute-engine/boxed-expression/boxed-symbol.ts` - Symbol type resolution
-
-**Tests:** `test/compute-engine/assumptions.test.ts` - "TYPE INFERENCE FROM
-ASSUMPTIONS"
+See `requirements/DONE.md` for implementation details.
 
 ---
 

src/compute-engine/assume.ts

@@ -19,6 +19,34 @@ import {
 import { MathJsonSymbol } from '../math-json';
 import { isInequalityOperator } from './latex-syntax/utils';
 
+/**
+ * Infer a promoted type from a value expression.
+ * This promotes specific types to more general ones suitable for symbols:
+ * - finite_integer -> integer
+ * - rational -> real
+ * - finite_real_number -> real
+ * - complex/imaginary -> number
+ */
+function inferTypeFromValue(ce: ComputeEngine, value: BoxedExpression): BoxedType {
+  if (value.type.matches('integer')) {
+    // finite_integer, integer, etc. -> integer
+    return ce.type('integer');
+  }
+  if (value.type.matches('rational')) {
+    // rational -> real
+    return ce.type('real');
+  }
+  if (value.type.matches('real')) {
+    // finite_real_number, real -> real
+    return ce.type('real');
+  }
+  if (value.type.matches('complex')) {
+    // complex, imaginary -> number
+    return ce.type('number');
+  }
+  return value.type;
+}
+
 /**
  * An assumption is a predicate that is added to the current context.
  *
@@ -239,8 +267,9 @@ function assumeEquality(proposition: BoxedExpression): AssumeResult {
     // Use _setCurrentContextValue so the value is scoped to the current context
     // and will be automatically removed when the scope is popped.
     ce._setCurrentContextValue(lhs, val);
-    // If the type was inferred, update it based on the value
-    if (def.value.inferredType) def.value.type = val.type;
+    // If the type was inferred, update it based on the value.
+    // Use inferTypeFromValue to promote specific types (e.g., finite_integer -> integer)
+    if (def.value.inferredType) def.value.type = inferTypeFromValue(ce, val);
     return 'ok';
   }
 
@@ -270,8 +299,9 @@ function assumeEquality(proposition: BoxedExpression): AssumeResult {
     // Use _setCurrentContextValue so the value is scoped to the current context
     // and will be automatically removed when the scope is popped.
     ce._setCurrentContextValue(lhs, val);
-    // If the type was inferred, update it based on the value
-    if (def.value.inferredType) def.value.type = val.type;
+    // If the type was inferred, update it based on the value.
+    // Use inferTypeFromValue to promote specific types (e.g., finite_integer -> integer)
+    if (def.value.inferredType) def.value.type = inferTypeFromValue(ce, val);
     return 'ok';
   }
 
@@ -364,10 +394,18 @@ function assumeInequality(proposition: BoxedExpression): AssumeResult {
   const unknowns = result.unknowns;
   if (unknowns.length === 0) return 'not-a-predicate';
 
-  // Case 3
+  // Case 3: single unknown - ensure the symbol has type 'real'
+  // (inequalities imply the symbol is a real number)
   if (unknowns.length === 1) {
-    if (!ce.lookupDefinition(unknowns[0]))
-      ce.declare(unknowns[0], { type: 'real' });
+    const symbol = unknowns[0];
+    const def = ce.lookupDefinition(symbol);
+    if (!def) {
+      // Symbol not defined yet - declare with type 'real'
+      ce.declare(symbol, { type: 'real' });
+    } else if (isValueDef(def) && def.value.inferredType) {
+      // Symbol was auto-declared with inferred type - update to 'real'
+      def.value.type = ce.type('real');
+    }
   }
 
   // Case 3, 4

test/compute-engine/assumptions.test.ts

@@ -95,9 +95,9 @@ describe.skip('TAUTOLOGY AND CONTRADICTION DETECTION', () => {
   });
 });
 
-// TODO #21: Type Inference from Assumptions
+// #21: Type Inference from Assumptions - IMPLEMENTED
 // When assumptions are made, symbol types should be inferred
-describe.skip('TYPE INFERENCE FROM ASSUMPTIONS', () => {
+describe('TYPE INFERENCE FROM ASSUMPTIONS', () => {
   test(`x should have type real (x > 4 assumed)`, () => {
     expect(ce.box('x').type.toString()).toBe('real');
   });