Complaint of free variable using fresh variable short-hand

[ghost]

The following snippet fails saying that "x" is free.

theory \Bugs extends \root

val foo = _ =>
  context
    let x:'‹x›'
    show x

The error only appears to show if the context is inside a function expression.

[phlegmaticprogrammer]

That's actually a bigger change I need to do to fix that because it changes the way I currently calculate the free variables in an expression / statement / pattern. Until now it was good enough for each parse tree to know:

1. What are the free variables of this tree?
2. What are the the variables introduced by this tree, if the tree is a statement or pattern

Because of the feature that let and choose statements can introduce variables depending on wether these variables are already introduced or not, we need a third category of variables to capture this. Not sure what a good name would be, 1. is freeVars, 2. is introVars, and 3. will be bindableVars?

[phlegmaticprogrammer]

I don't see a good way for computing this using my current method, which is bottom-up only. I.e. currently I start with the last statement of a block, and compute the free and introduced variables working upwards to the first statement.

Now I would need to compute the free variables bottom up, and the introduced variables top down. Argh. That's not much of a problem once we move to a compiler anyway, but currently that's a quite expensive change for something that's just a notational convenience.

So I will just remove this feature for now and keep it in mind for the next iteration of ProofScript.

[phlegmaticprogrammer]

Removed the feature for now, maybe we'll reintroduce it later again.

[ghost]

Have you also removed the "fresh" function? The following complains with "statement has not been implemented yet":

theory \Bugs extends \root

theory \Bugs extends \root

val foo = _ =>
  context
    val x = fresh "x"
    show x

The function is still listed on the wiki page.

[ghost]

My mistake. It is somehow working now!