In the last months Tim has been adding a new function
sameLabel to Ωmega and this finally allowed me to encode the concept of free variables. In just a couple of days I managed to implement environment construction with statically checked proof that no identifier is shadowed.
Here is a little example.
Building on this advance I fulfilled a long lasting desire and managed to prototype LLVM basic blocks in Ωmega with thrists. The approach is implemented in 2 steps:
- build up a labelled sequence of preinstructions, and then
- construct sufficient evidence about well-formedness, that the strict type constraints in the thrist can be proven.
Curiously, the defs propagate to the right and the uses to the right in this thrist. The good thing is, that after all this struggle I am pretty confident that many more properties and constraints can be encoded, such as
- the LLVM type system (on defs, uses and constants),
- that Phi nodes must not go into entry blocks,
- that Phi nodes must preceed other instructions in the basic block,
- every use must happen in the scope of a corresponding def,
- etc.
The next days will surely see more progress, I have crawled out of the swamp and have firm ground under my feet...
