In *non-recursive* type-checking, perhaps better called *type computing*
we perform a minimal traversal in order to compute the type of a term,
without recursively type-checking it. Informally, we assume it is well
typed, and do the minimal amount of work needed to compute its type.
Two improvements:
1. No longer implemented with recursion.
2. Caches all intermediate results.
Implementation:
* `check_dependencies(Term) -> Vec<Term>`: maps a terms to the immediate
children of it whose types are needed to compute its type.
* `check_raw_step(Term, TypeTable) -> Sort`: assumes those children have
their types in the table, and computes this term's type.
* `check_raw`: glues the two above functions together into a suitable
traversal. Similar to `rec_check_raw`, but the traversal isn't total.
Significance:
Previously, we had a non-recursive implementation for array stores that
*didn't cache intermediate results* which could cause quadratic
type-checking time (if the type-check callee was doing a top-down
traversal). Edward sent me a benchmark that was experiencing this,
resulting in 74.1% of total compilation time being spent type-checking.
Now it's down to 0.4% of total compilation time.
