( ce: IComputeEngine, pattern: Expression )
| 64 | ): { predicate: Expression; undeclared: string[] } { |
| 65 | // The ownership snapshot: the names the scope already binds, read BEFORE |
| 66 | // this call parses or boxes anything, so a binding the call itself causes |
| 67 | // can be told from one that predates it (`introducibleNames`). |
| 68 | const boundAtEntry = who === 'assume' ? boundNamesInScope(ce) : undefined; |
| 69 | const boxed = boxPredicate(ce, predicate, who); |
| 70 | return { |
| 71 | predicate: boxed, |
| 72 | // The names the predicate mentions that the assumption is answerable |
| 73 | // for. Read here, on the still-uncanonicalized predicate, because |
| 74 | // canonicalizing it binds every free symbol it mentions. |
| 75 | undeclared: boundAtEntry ? introducibleNames(boxed, boundAtEntry) : [], |
| 76 | }; |
| 77 | } |
| 78 | |
| 79 | /** Box the predicate argument, per the rules described on |
| 80 | * `predicateFromArg`. */ |
| 81 | function boxPredicate( |
| 82 | ce: IComputeEngine, |
| 83 | predicate: Expression | string, |
| 84 | who: 'assume' | 'verify' |
| 85 | ): Expression { |
| 86 | if (typeof predicate !== 'string') return ce.expr(predicate, { form: 'raw' }); |
| 87 | |
| 88 | // `asLatexString` strips `$…$`/`$$…$$`; a plain string is used verbatim. |
| 89 | const latex = asLatexString(predicate) ?? predicate; |
| 90 | const parsed = parseLatex(latex); |
| 91 | const boxed = |
| 92 | parsed === null |
| 93 | ? null |
| 94 | : ce.expr(parsed, { form: who === 'assume' ? 'raw' : 'canonical' }); |
| 95 | if (boxed === null || !boxed.isValid) |
| 96 | throw new Error( |
| 97 | `${who}(): cannot parse the predicate string ${JSON.stringify( |
| 98 | predicate |
| 99 | )} as a mathematical expression` |
| 100 | ); |
| 101 | return boxed; |
| 102 | } |
| 103 | |
| 104 | /** |
| 105 | * Every symbol name the current context's scope chain binds, at the moment |
| 106 | * this is called. |
| 107 | * |
| 108 | * `lookupDefinition()` resolves a name by walking exactly this chain, so a |
| 109 | * name absent from the returned set is a name nothing had bound. |
| 110 | */ |
| 111 | function boundNamesInScope(ce: IComputeEngine): Set<string> { |
| 112 | const names = new Set<string>(); |
| 113 | let scope: IComputeEngine['context']['lexicalScope'] | null | undefined = |
| 114 | ce.context?.lexicalScope; |
| 115 | while (scope) { |
| 116 | for (const name of scope.bindings.keys()) names.add(name); |
| 117 | scope = scope.parent; |
| 118 | } |
| 119 | return names; |
| 120 | } |
| 121 | |
| 122 | /** |
| 123 | * The names `predicate` mentions that the `assume()` call itself brought into |
no test coverage detected