I was thinking about how to support multiple files and one approach might be to make it possible to take an lexp and print it to a file, and then read it back.
Then "exporting" the definitions of a particular module could look something like "take those defs, put them into a tuple, and print it to the file", and then importing definitions from a file would be a macro which reads the file and returns the corresponding lexp.
As for how to "print & read", there'd be two ways to go about it:
A- define brand new primitives that go straight from lexp <-> string.
B- rework our lexp <-> sexp code to make it robust enough.
Option B would also be useful in macros, so it's definitely something we should try to do. But it also means that reading would go through "sexp -> lexp" i.e. through elaboration. We could probably arrange for it not to do any macro-expansion and maybe also to avoid any need for unification, but it seems like it'd inherently be clunky/inefficient.
So, I think option A is preferable.
Stefan