The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to discharge verification conditions generated by the Whiley Compiler. WyTP operates over a variant of first-order logic which includes integer arithmetic, arrays and quantification.
The interface NameResolver should be relocated into WyCC. However, this is not a completely straightforward process. It requires the following changes:
[ ] Refactor NameID into interface. Perhaps locate in Path and Path.Name ?
[ ] Create AbstractCompilationUnit or similar and locate WyalFile.Name (and other things) here. AbstractCompilationUnit.Name then implements NameID.
[ ] Update NameResolver to work with NameID rather than Name. We might use a template argument here T extends NameID.
[ ] Move NameResolver over.
These steps will involve a fair bit of refactoring of WyC and other modules. We could potentially go further by including e.g. import declarations in AbstractCompilationUnit. This would allow a generic AbstractNameResolver implementation in WyCC.
Also, NameResolver could become Path.Name.Resolver for example.
The interface
NameResolvershould be relocated into WyCC. However, this is not a completely straightforward process. It requires the following changes:[ ] Refactor
NameIDinto interface. Perhaps locate inPathandPath.Name?[ ] Create
AbstractCompilationUnitor similar and locateWyalFile.Name(and other things) here.AbstractCompilationUnit.Namethen implementsNameID.[ ] Update NameResolver to work with
NameIDrather thanName. We might use a template argument hereT extends NameID.[ ] Move
NameResolverover.These steps will involve a fair bit of refactoring of WyC and other modules. We could potentially go further by including e.g.
importdeclarations inAbstractCompilationUnit. This would allow a genericAbstractNameResolverimplementation in WyCC.Also,
NameResolvercould becomePath.Name.Resolverfor example.