S40.1: a reformatted sequent calculus compiler

[dr.mt...@gmail.com]

I was looking at the chapter on compiling sequent calculus in TBoS and decided it could be rewritten to follow a paper I'm writing.  The technology is good, its just that the explanation is difficult.  This happens when you are explaining something you have just conceived - as it was back in 2020.    The new explanation is much clearer and as a bonus, it will cut about 50 loc off the kernel.  

Wrt to speed the compiler will be much the same.  It will be a little faster but in human terms not detectably so.   We are near the end of optimisation, but 40.1 should take us all the way there.

M. 

[dr.mt...@gmail.com]

40.1 will IMO be absolutely optimal wrt the emitted

object code.   The S40 version is already pretty good so whether the

time differences are humanly detectable is another matter .

But the compiler itself is 13% smaller wrt loc and emits code 

which is much easier to read and debug.

The latter is due actually to the use of macros  which 

act as markup indicating which parts of the output are

to be converted to cons form.  Conversion to cons form

always results in something that causes eye-strain and

makes debugging a nightmare.  S40 suffers from that.

This version will trigger a reformulation of the chapter in

TBoS for sure.  The result should be much easier to follow.

M.