(proposition: Expression)
| 412 | if (isSymbol(val, 'True')) return 'tautology'; |
| 413 | if (isSymbol(val, 'False')) return 'contradiction'; |
| 414 | return 'not-a-predicate'; |
| 415 | } |
| 416 | |
| 417 | const ce = proposition.engine; |
| 418 | |
| 419 | // Case 2 |
| 420 | // @todo: this is dubious. Should we allow this? |
| 421 | // i.e. `ce.assume(ce.parse("x = 3"))` |
| 422 | // that's not really an assumption, that's an assignment. |
| 423 | // Assumptions are meant to be complementary to declarations, not replacing |
| 424 | // them, i.e. `ce.assume(ce.parse("x > 0"))` |
| 425 | if (!isFunction(proposition)) return 'not-a-predicate'; |
| 426 | const lhsExpr = proposition.op1; |
| 427 | const lhs = isSymbol(lhsExpr) ? lhsExpr.symbol : undefined; |
| 428 | if (lhs && !hasValue(ce, lhs) && !proposition.op2.has(lhs)) { |
| 429 | const val = proposition.op2.evaluate(); |
| 430 | if (!val.isValid) return 'not-a-predicate'; |
| 431 | const def = ce.lookupDefinition(lhs); |
| 432 | if (!def || !isValueDef(def)) { |
| 433 | ce.declare(lhs, { value: val }); |
| 434 | markAssumptionValue(ce, lhs); |
| 435 | return 'ok'; |
| 436 | } |
| 437 | if (def.value.type && !val.type.matches(def.value.type)) |
| 438 | if (!def.value.inferredType) return 'contradiction'; |
| 439 | |
| 440 | // Set the value for the symbol, scoped to the current context so the |
| 441 | // assumed value is automatically reverted when this scope is popped. |
| 442 | // If lhs is declared in a parent scope, shadow it in the current scope |
| 443 | // so we don't permanently mutate the parent definition. |
| 444 | markAssumptionValue(ce, lhs); |
| 445 | if (!ce.context.lexicalScope.bindings.has(lhs)) { |
| 446 | ce.declare(lhs, { value: val }); |
| 447 | } else { |
| 448 | // Set the (inferred) type *before* the value. The `set type` accessor |
| 449 | // resets `_value` when the new type is `unknown` (which `inferTypeFromValue` |
| 450 | // yields for a free-symbol rhs like `a = b`); doing it after |
| 451 | // `_setSymbolValue` would silently wipe the assigned value. Setting the |
| 452 | // value last guarantees it survives. |
| 453 | if (def.value.inferredType) { |
| 454 | const previous = def.value.type; |
| 455 | def.value.type = inferTypeFromValue(ce, val); |
| 456 | recordAssumedType(ce, def.value, proposition, previous); |
| 457 | } |
| 458 | ce._setSymbolValue(lhs, val); |
| 459 | } |
| 460 | return 'ok'; |
| 461 | } |
| 462 | |
| 463 | // Case 3 |
| 464 | if (unknowns.length === 1) { |
| 465 | const lhs = unknowns[0]; |
| 466 | const sols = findUnivariateRoots(proposition, lhs); |
| 467 | const def = ce.lookupDefinition(lhs); |
| 468 | |
| 469 | // Contradiction check (P1-3): an *explicitly* typed symbol whose declared |
| 470 | // type is incompatible with every root is inconsistent with the equation. |
| 471 | // Compare *each root* against the definition's type; the earlier code |
no test coverage detected