Add Typing Environments

[jakzale]

Adding typing environemnts

• [X] Add type environments to type checker,
• [X] Update existing tests,
• [X] Update progToString to generate ext keywords,
• [X] Add scoping rules for for loops.
• [x] add a Program section specifying all ext variables.
• [x] Update API freeVars to extVars, these are not the free variables that you are looking for.
• [x] Test for loops scopes At the moment there is no test case for for loop shadowing an ext variable.

[jakzale]

This should fix some problems with #76, but it doesnt have assignments yet.

[jakzale]

I thought that problem is already fixed? The problem was that we were renaming programs with loops and we were implicitly assuming that a loop always evaluates at least once, so every variable bound in the loop body gets introduced into the scope. But that was a false assumption, so we removed loops from the typed language. No loops in the typed language = no scoping problems.

Now we have proper scoping rules for for loops, meaning that the discussion for the value of the for loop variable is moot, as the following program is ill typed

for i = 1 to 10 do end;
assert i == 10;

There's still ambiguity in the untyped language, but that doesn't matter, at the moment at least.

What sort of ambiguity you refer to?

What do you mean by assignments?

Since we add a scope for the for loop, the following programs are ill typed

for i = 1 to 10 do
  assert j > 0;
  let j = i * 2;
end;

and

for i = 1 to 10 do
  let j = i * 2;
end;
assert j == 20;

Furthermore, the last assertion in the following program will be true

let j = 0;
for i = 1 to 1 do
  let j = i;
end;
assert j == 0;

I want to add an assignment operator to modify a variable without adding a new binding, which would make the following program's assertion true

let j = 0;
for i = 1 to 1 do
  j <- i;
end;
assert j == 1;

[effectfully]

What sort of ambiguity you refer to?

I misunderstood what you're after.

I've responded in the Loops issue.

[jakzale]

Is this something that we're going to have in the long run? If the plan is to inline the value of a loop variable, then we can unscope the loop variable after the loop (and only inline in the body of the loop then).

Hmm, I need to think about it. Yes, we could technically inline the loop variable and erase it completely. I am still not sure how to do it properly, as there are programs in the spec that depend on variables bound in the body of a for loop. Lemme think about it for a bit.

[effectfully]

I am still not sure how to do it properly, as there are programs in the spec that depend on variables bound in the body of a for loop.

Why is that a problem?

for i = 0 to 1 do
  let x = i;
assert x == 1;

will elaborate to

let x = 0;
let x = 1;
assert x == 1;

[jakzale]

Hmm, maybe I am overdoing it.

[jakzale]

Ah yes, we can do that, then we do not need to do renaming in type checking.