removing lemma_not_empty and lemma_not_zero

[doublec]

trafficstars

I wondered why lemma_not_empty and lemma_not_zero is needed since you have the if that should narrow down the constraint:

if length(s) > 0 && pad > 0

If you use nested if's, checking each boolean separately then you don't need the lemma. I asked Hongwei about this once and he said:

'&&' is a macro (due to shortcut evaluation); it is not given a dependent type. Replacing '&&' with * (bmul) should work, though.

Replacing the 'if' with:

if (length(s) > 0) * (pad > 0)

does allow type checking if the lemmas are removed. Just noting this as to why the lemmas are needed and why ATS2 isn't computing it itself.

[deech]

Ah nice. Ok, now I know to stay away from macros. :) And interesting that a boolean multiply is a workaround. I tried a case statement with a tuple and that seemed to work as well. I like it a little better but that might just be my ML background:

case @(length(s) > 0, pad > 0) of
   | @(true, true) =>
       (
        let
          val (pf | res) = left_pad(i2ssz(pad),c, string1_copy(s))
        in
          begin
            println! ("padding: ", res);
            strnptr_free(res);
          end
        end
       )
   | _ => print "Usage: left-pad <string-to-pad> <pad-length>\n"

[githwxi]

Please try

case (isneqz(s), pad > 0) of (true, true) => ... | (_, _) => ...

There is no need to form tuples. By the way, 'ats' code highlighting is supported.