Peter, PolyML.NameSpace.nameSpace is essentially an interface. Think of it as a signature or an interface in Java. It defines what any concrete implementation of a name-space must provide for it to work with the compiler. All the fields in the record are functions that are called either during compilation or when the compiled code has completed.

To implement the "conventional" ML name space where each top level declaration can build on the one before there is a global name space implemented as a hash table. This is available as PolyML.globalNameSpace. It makes sense to have delete functions for such a name space and these are the forgetXXX functions.

Other abstract name spaces are possible. PolyML.make builds a "name space" where a look-up may recursively compile a dependency. Isabelle uses name spaces which depend on the current theorem and allow the compiler to run in parallel on independent theorems.

Hope that explains it. Regards, David

On 14/03/2015 20:39, Peter Gammie wrote:

David,

I?ve been trying to repurpose your Poly/ML test harness, that encapsulates the tests in private namespaces. With some head scratching I got it to somewhat work, so thanks for that.

One remaining nit is that the treatment of forgetVal(ue) does not take into account the current namespace. Did you have a reason for leaving it out of the PolyML.NameSpace.nameSpace record?

cheers, peter _______________________________________________ polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml