Expand description
The portable-core checker.
Resolves names, checks types, and fixes the exact operator semantics of a
surface program produced by one of the language frontends. The result is
the portable-core program the emitters consume: every expression carries
its type and every operator carries the source language’s semantics, so a
target can never silently substitute its own (for example, Lean’s Euclidean
Int division for JavaScript’s truncating BigInt division).
Mirrors js/src/translation/check.js, including the order in which fresh
names are drawn, so both runtimes produce the same checked program.
Functions§
- check_
program - Checks a surface program into the portable core.
- coerce
- Inserts the source language’s implicit conversions, which only JavaScript has.
- collect_
calls - The functions an expression calls, in evaluation order.