The runtime helpers the generated code calls, held as a tree #

The runtime helpers the generated code calls, held as a tree rather than as a block of text.

This is a different language from Js.Expr. Js.Expr is the subset the compiler writes, and its narrowness is what lets the reader in Parse.lean take the whole file back; the helpers need loops, mutable bindings and throw, none of which the compiler ever emits. Giving them their own tree keeps the compiler's tree exactly as narrow as the roundtrip claim needs it.

The builtins the helpers reach for are named in prim and method rather than spelled into a call, so what the model has to assume about JavaScript is a table one can read off the tree.

The printer #

The helpers #

The operations where JavaScript and Lean split on the answer are confined to these definitions.

__has dispatches on the head of the descriptor, and every branch below is named so that a proof walking one of them does not pay for expanding the ten it did not take.

The key a declared type tells its constructors apart by is read off the descriptor rather than spelled in: an author chooses it per type, and the helpers are one copy for the whole package. The tags below are __find's own answer, which is an Option and not the value being checked.

A declared type that names itself is expanded once and bound: mu carries the same key and alternatives a ctors does, and binds them; a ref names the binder that many levels out. Both hand the walk the ctors node the binder holds, under the environment that node was bound in, so everything below them is the walk that was already there.

__norm rebuilds a value the entry check accepted in the shape encodeValue writes: the key the constructor's name is carried under first, then the constructor's fields in the order the descriptor names them. Keys the descriptor does not name are dropped. Branches are named for the reason __has's are.

__out is __norm walked the other way: what the entry reads its result through on the way back out. Every branch is __norm's, save the one this helper exists for — a dictionary declared to cross as a plain object leaves as one, where __norm on the way in made the Map the body ran on. Branches are named for the reason __has's are.

__fold walks a value of a type that names itself, from the leaves up. What it hands the callback is the node itself with each field that came round replaced by what the callback answered for it, so the callback reads a node of the shape the type declares and dispatches on the key the constructor's name is carried under — which is what a match does, and what the compiler compiles the alternatives to.

One callback rather than one per constructor is what keeps .apply at the arity it has: a constructor's field count varies, and a helper cannot apply a callback to an argument list it only has at run time.

The spec is an object keyed by the constructor's name, holding that constructor's fields in declared order as [name, kind]. The kind is read off the spec rather than off the value: which field comes round is the declared type's to say, and a value that happens to hold an object is not a node.