| 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 | |