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.
- 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,