convert license headers to SPDX

Handle missing symbols as problem aborts.

Previously missing symbols resulted in a global failure, now only
the relevant problems will fail. This better suits a regression-test
approach which hopes to converge on correctness gradually.

Tweak reporting of missing symbols.

Make sure the names of the missing symbols turn up on the error
channel, for reasons to do with test infrastructure.

Factor out a common substitution pattern.

Better error for missing symbols.

It's better to get a summary of all missing symbols than an array
index exception.

Faster implementation of pseudo compiling.

Add PArrayValid support.

Not fully tested yet, but this is the rough shape of support for array
size assertions, including dynamic array size assertions.

Import of graph-refine tool.