I forgot to put the following line in stdio.cats:
#define atslib_fopen_ref_exn atslib_fopen_exn
You can put it in wclines.dats directly or git-pull again (and then do
’make -f codegen/Makefile_atslib’).
Unfortunately I’m getting an off by 1 disagreement with wclines and other
programs on a large file. It isn’t the last bit of the file causing the
problem either (at least, not using “tail large_file > test.txt” . I will
check it more tomorrow.
I think that the reason for this off-by-1 disagreement is this: for ‘wc’,
EOF is considered a newline if it does not follow ‘\n’ immediately; for
wclines, ‘EOF’ is never counted as a newline.
Thanks; I see that both of these are dependent types now (any constant
integer type appears to be a dependent type). Why is it that int1_of_int(0)
does not work in this case? I think I’m missing something important here.
I think you forgot to do
make -f codegen/Makefile_atslib
Also, the above lemma is already in ATS2.
I’m trying to extend the code to return a dependently typed value (wclines
should always return a natural number). The last line of the wclfil
function in minDisj.dats is giving a constraint error. Perhaps this is
caused by a missing “upstream” constraint somewhere? I haven’t found it yet
if so.
minDisj_wclines.rar (12.1 KB)
In the above comment, ‘wc’ and ‘wclines’ should be swapped.
Anyway, I made a quick fix. Now ‘wc --lines’ and ‘wclines’ should always
concur. Changes have been uploaded.