While loop statements & invariant

[palainp]

Dear @davidgiven, thank you for developing that language, that's very enjoyable and interesting!
Reading some code in, e.g. strings.coh, I noticed that you often use "loop+break" idioms, and rarely rely on "while loop invariants", for example:

sub StrLen(s: [uint8]): (size: intptr) is
       var p := s;
       loop
                var c := [p];
                if c == 0 then
                        break;
                end if;
                p := p + 1;
        end loop;
        size := p - s;
        end loop;
end sub;

could also be written as:

sub StrLen(s: [uint8]): (size: intptr) is
	var p := s;
        # invariant: forall x in [s..p[: [x] != 0
	while [p] != 0 loop
                # here we know that [s..p[ != 0 (invariant) and [p] != 0 (loop condition)
                # so it's safe to increase p and consider [s..p[ != 0 (invariant is restored)
		p := @next p;
	end loop;
	size := p - s;
end sub;

Maybe the underlying assembly is easier to generate with breaks?

Another thought is that some loop condition can be really terrible as with StrICmp (not sure about syntax errors, I'm just starting to learn the language):

sub StrICmp(s1: [uint8], s2: [uint8]): (res: int8) is
	while ((ToLower([s1]) - ToLower([s2])) == 0) and ([s1] != 0) loop
		s1 := @next s1;
		s2 := @next s2;
	end loop;
        # if [s1] = 0 we reached the end of the strings (second condition),
        # otherwise the strings are different (first condition)
	res := [s1] as int8;
end sub;

EDIT: the last res value is wrong here as s1 can be shorter than s2. Therefore another computation is needed and this is avoided with the "break template". Maybe that's a fair enough reason to keep breaks :)

[palainp]

When I read deeper into the code with this invariant loop construction in mind, I found some places where a do/while loop would be better than a classical while loop. Would it be a possible way, for me, to propose a PR that add such loop syntax or is there simply no need to go any further?

[davidgiven]

Thank you for the kind words!

Re strlen: probably that code was copied from another loop which actually used c. You're right, that could trivially be replaced with a while loop, and it'd be shorter code too, as c wouldn't get stored and the if..end if would be removed (there's no trivial basic block elision). I generally use mid-loop breaks whenever the logic gets even slightly complicated do improve readability.

There's no real reason why do..while isn't implemented other than laziness. Ada, which the Cowgol syntax is loosely based on, doesn't have this, and I'd have to think of a meaningful syntax; while can't be used to terminate a loop because the compiler couldn't distinguish this from starting a new loop. loop..until, maybe? I am, in fact, working (slowly) on a replacement parser which should be smaller and faster and allow this kind of thing to be easily added.

[palainp]

Thank you for the insight for the future of the language!

I understand that do..while can be an issue for the parser, and loop..until is a good replacement candidate 👍
I'm only worried about the inversion of the nature of the loop condition (while wants a condition for continuing the loop, whereas until wants a condition for stopping the loop). But anyway, it will be easier to translate some loop .. if C then break; ... loops as the nature of C is the same in an loop .. until C; loop :)

[davidgiven]

Oh, yeah, I forgot to mention: I do also want to add break if ... (as the equivalent of Ada's exit when), which should make mid-loop exits both faster and much more convenient.

[palainp]

Speaking of naming, Pascal has repeat .. until :)