feat: Implement Turing Machine Elaborator

[Paul-Lez]

See discussion in #229.

[tcosmo]

Minor comments only :)

If you want to add tests for the simulation of Turing machines here are some ideas:

• Check that 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA halts after 47,176,870 steps
• Check that 1RB2LA1RA1RA_1LB1LA3RB1RZ halts after 3,932,964 steps

In case you want to add tests about nonhalting machines then you probably need to have at least one decider implemented (i.e. algorithm that proves that a machine does not halt) and if you do, the simplest target is to syntactically recognise machines with no halting transition (i.e. no undefined transition and no mention of a state bigger than state count), like for instance 1RB0LA_1LB0RB. The nonhalting proof is trivial: there is no instruction that makes it halt.

Slightly more ambitious but certainly off-topic for your project are loops (machines that eventually repeat the same configuration, potentially translated in space) and here are some references for implementation:

• Cyclers only (repeating exactly the same configuration, no translation, e.g. 1RB0RB_1LC1RD_0LA1RA_---1RE_1LD0LD): Section 2
• Translated Cyclers legacy algorithm (repeating the same configuration, translated in space, e.g. 1RA---_------; 1RB0LE_1LC0RD_---1LD_1RE0LA_1LA0RE): Section 3
• Coq-BB5 algorithms for loops, which detects both of the above with a new, elegant, algorithm: Section 4.3

Note that these deciders have already been implemented in Lean: https://git.sr.ht/~vigoux/busybeaver/tree/master/item/Busybeaver/Deciders

[tcosmo]

Note: I'm going offline tomorrow until about Aug 25th, I apologise in advance for this delay for future reviews

[eric-wieser]

I assume you also want to check here that it is divisible by 3?

[eric-wieser]

I take this back, I think the previous version actually makes more sense, since then you get an error on the last piece that isn't long enough.

[Paul-Lez]

Reverted back to the previous version

[Paul-Lez]

Ah actually I think it might be worth keeping this (otherwise one can run into unspecified behaviour of String.next)