Ability to include one file of definitions in another

[xsebek]

Describe the bug
Using the command run X does not run file X before checking next expression.

To Reproduce
Consider files x.sw and y.sw:

def x = 1 end;

run "x";
def y = x + 1 end

Writing run "y" in REPL produces:

run: Error in test2
 2: Unbound variable x

Expected behavior
I would expect it successfully load both variables.

[byorgey]

The problem has nothing to do with when run is evaluated. The problem is that typechecking does not take into account any definitions that will be loaded by the run command. You don't need two files to observe this; just put this in m.sw:

def m = move end

then at the REPL try typing run "m"; m. It will not let you, but will complain that m is unbound, because it tries to typecheck the entire expression before executing it.

This is a tricky problem in general. I can imagine a few different stopgaps to make this better but they end up creating other problems. Perhaps I was trying to be too clever by making run a command in the cmd monad, rather than a special REPL command. Now it invites you to use it as a sort of poor man's module system, but it really doesn't work for that, as this issue demonstrates. If we want to be able to break up code into modules and import them into each other we'll have to actually figure out a sensible, coherent design for that. run isn't it.

[byorgey]

Maybe the right thing to do here is to just bite the bullet and have special typechecking for the run command: typechecking run would actually load the file, typecheck it recursively, and then make available the types of any definitions to things after the run. Some thoughts:

• We have to be careful that import cycles don't get the typechecker stuck in an infinite loop.
• Ideally, we would only load a file from disk once, instead of loading it once at typechecking time and once at runtime.
• We could solve both the above problems by maintaining a map from module names to parsed, typechecked, and elaborated terms.
• All of the above would mean adding several new effects to the Infer monad (namely, IO, and some kind of state effect with the current map from file names to checked terms).

These ideas are now filed at #495.

[byorgey]

I am now more convinced that the above comment is the right way to do things. We might also consider renaming run to something like import.

[byorgey]

Closing this in favor of #495 . Of course it will still be here for anyone who wants to read the discussion.