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 [email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
