* update TODO
* add quiet mode to zxc
* Drop and garbage collection
This commit adds Drop instances and related functionality that force
garbage collection at life cycle end of various structs that contain
Terms.
I didn't implement Drop for Computation because its Terms are generally
moved into a converter. This means that back-ends are responsible for
garbage collecting (see new functionality in ILP, R1cs, and ABY).
* collect the cfold table, too
* prevent double-panic as a result of garbage_collect()
* z# parser: zx is a default extension too
* update Cargo.lock
* strictness un-op #()
also added err messages for asserts and ?: ternary support from ZoK upstream
* for assignments, strict rhs => strict lhs
* zsharp: type definitions WIP
Still missing monomorphization.
* type defns: generic inference
* struct monomorphization for type aliased structs
* different approach: no monomorphization, just canonicalize aliases
* canonicalize struct names
* typedef tests
things work except that importing an alias and not its referent breaks typechecking
* add error message about needing to import referent structs
* update hashconsing pointer in Cargo.toml
* maybe_garbage_collect should also return early when panicking
Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu>
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.
