FYI.
I implemented wclines (i.e., wc --lines) in a way that makes use of
rawmemchr
(available with the flag -D_GNU_SOURCE). It should be faster than the
version
using memchr. Here is the source code of wclines:
This implementation also shows a style of mixing C code with ATS code,
which I
have been learning, exploring and practicing for quite some time.
Cheers,
–Hongwei
Also I forgot to add in to wclfil:
val res = wclbuf (pf | p, pz, c, res)
should be:
val res = wclbuf (pf | p, pz, c, res+nEOF)
Very interesting code, in more ways than one (I didn’t know
about -D_GNU_SOURCE or rawmemchr).
I’m ashamed to say I got nearly all the way through backporting to ATS1 but
one line in particular is keeping it from typechecking (if commented out it
typechecks). Having a bit of trouble exactly interpreting the error.
/media/RAID5/share/ATS_learning/wclines.dats: 2707(line=133, offs=30) –
2709(line=133, offs=32): error(3): unsolved constraint: C3STRprop(main;
S2Eeqeq(S2Eapp(S2Ecst(add_addr_int_addr); S2EVar(2437), S2Eint(1)),
S2Eapp(S2Ecst(add_addr_int_addr); S2EVar(2436), S2Eapp(S2Ecst(sizeof);
S2EVar(2434)))))
type-checking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2fhome_2ffac2_2fhwxi_2fresearch_2fATS_2fIMPLEMENT_2fGeizella_2fAnairiats_2fsvn_2fats_2dlang_2fsrc_2fats_error_2esats__FatalErrorException(1233)
staload _(anon) = “libc/SATS/stdio.sats”
//
staload _(anon) = "prelude/DATS/array.dats"
staload _(anon) = “prelude/DATS/array0.dats”
//
staload _(anon) = "prelude/DATS/list.dats"
staload _(anon) = "prelude/DATS/list0.dats"
staload _(anon) = “prelude/DATS/list_vt.dats”
//
staload _(anon) = "prelude/DATS/matrix.dats"
staload _(anon) = “prelude/DATS/matrix0.dats”
//
staload _(anon) = "prelude/DATS/option.dats"
staload _(anon) = “prelude/DATS/option0.dats”
//
staload _(anon) = “prelude/DATS/pointer.dats”
//
staload _(anon) = “prelude/DATS/reference.dats”
//
(* ****** ****** *)
staload
UN = “prelude/SATS/unsafe.sats”
(* ****** ****** *)
staload “libc/SATS/stdio.sats”
(* ****** ****** *)
viewdef bytes_v (l:addr, n:int) = bytes (n) @ l
extern
fun ptr0_add_bytesize (p: ptr, ofs: size_t):<> ptr
implement
ptr0_add_bytesize(p,ofs) = p+ofs
symintr ptr_succ
extern
fun
ptr0_succ (p: ptr):<> ptr
overload ptr_succ with ptr0_succ
extern
fun
ptr1_succ {l:addr} (p: ptr l):<> ptr (l+1)
overload ptr_succ with ptr1_succ
implement
ptr1_succ {l} § =
$UN.cast{ptr(l+1)}(ptr0_succ §)
implement
ptr0_succ § = ptr0_add_bytesize (p, 1)
extern
praxi
bytes_v_unsplit
{l:addr}{n1,n2:int}
(pf1: (bytes_v (l, n1), bytes_v (l+n1, n2))): bytes_v (l, n1+n2)
// end of [bytes_v_unsplit]
(* ****** ****** *)
%{^
extern
void
*rawmemchr(const void *s, int c);
#define atslib_rawmemchr rawmemchr
%}
extern
fun rawmemchr
{l:addr}{m:int}
(
pf: bytes_v (l, m) | p: ptr l, c: int
) : [l2:addr | l+m > l2]
(
bytes_v (l, l2-l), bytes_v (l2, l+m-l2) | ptr l2
) = “mac#atslib_rawmemchr” // end of [rawmemchr]
(* ****** ****** *)
#define BUFSZ 16384
(* ****** ****** *)
extern fun fread1 {l:addr} {n:nat} {f:fm} (pf_mod: file_mode r
| dest: ptr l, sz: size_t 1, count: size_t n, fil: FILEref)
: [m:nat] size_t m = “mac#fread”
extern
fun freadc // read bytes and then add [c] at the end
{b:nat}
{l:addr}
(
pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: char, b: size_t b
) : size_t // end of [freadc]
implement
freadc (pf | inp, p, c, b) = let
val [m:int] m = fread1(file_mode_r | p, 1, b, inp)
val () = assertloc (p > null)
// val _ = if p <> null then
val () = $UN.ptrset (p+m, c)
// else ()
in
m
end (* end of [freadc] *)
(* ****** ****** *)
extern
fun wclbuf
{l:addr}{n:int}
(
pf: !bytes_v (l, n) | p: ptr l, pz: ptr, c: int, res: int
) : int // end of [wclbuf]
implement
wclbuf (pf | p, pz, c, res) =
(
if p < pz then let
val (pf1, pf2 | p2) = rawmemchr (pf | p, c)
prval (pf21, pf22) = array_v_uncons (pf2)
val _ = $showtype p
val p2 = ptr_succ(p2)
val _ = $showtype p
val res = wclbuf (pf22 | p2, pz, c, res + 1)
prval () = pf2 := array_v_cons (pf21, pf22)
prval () = pf := bytes_v_unsplit (pf1, pf2)
in
res
end else
res
// end of [if]
) // end of [wcbuf]
(* ****** ****** *)
extern
fun wclfil{l:addr}
(
pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int
) : int // end of [wclfil]
implement
wclfil{l}
(pf | inp, p, c) = let
//
fun loop
(
pf: !bytes_v (l, BUFSZ)
| inp: FILEref, p: ptr l, c: int, res: int
) : int = let
//
val n = freadc (pf | inp, p, $UN.cast{char}©, size1_of_int1(BUFSZ-1))
//
in
//
if n > 0 then let
//val pz = ptr_add (p, n)
val pz = p+n
val res = wclbuf (pf | p, pz, c, res)
in
loop (pf | inp, p, c, res)
end else res (* end of [if] )
//
end // end of [loop]
//
in
loop (pf | inp, p, c, 0(res))
end ( end of [wclfil] *)
(* ****** ****** *)
implement
main {n} (argc, argv) = () where
{
var inp: FILEref = stdin_ref
val () =
(
if argc >= 2 then
inp := fopen_ref_exn (argv[1], file_mode_r)
// end of [if]
)
//
val (
pfopt | p
) = malloc_ngc (BUFSZ)
val () = assert_errmsg (p > null, #LOCATION)
prval malloc_v_succ (pf_ngc, pf_buf) = pfopt
prval () = pf_buf := bytes_v_of_b0ytes_v (pf_buf)
val res = wclfil (pf_buf | inp, p, $UN.cast2int(’\n’))
val () = free_ngc (pf_ngc, pf_buf | p)
//
val () = println! ("wclines: number of lines = ", res)
//
val () = if argc >= 2 then fclose_exn (inp)
} (* end of [main0] *)
(* ****** ****** *)
(* end of [wclines.dats] *)
Say, the file contains exactly BUFSZ many chars and none of them are ‘\n’.
You version of wclines returns 0 but I think that you want it to return 1.
BTW, I have never compared rawmemchr with memchr in terms of performance.
Is wclines faster than your version that uses memchr?
Also a minor note, it seems I needed to add this in:
extern
praxi b0ytes2bytes_v {bsz:int}
{l:addr} (pf: b0ytes (bsz) @ l): bytes (bsz) @ l
Porting some changes I made in the ATS version to the ATS2 version (to
recognize a missing \n before the EOF as a line) is giving me an error I’m
not so sure of:
wclines_a2_dats.c:792:1: warning: implicit declaration of function
âHITundefâ [-Wimplicit-function-declaration]
wclines_a2_dats.c:792:1: warning: implicit declaration of function
âHSEs2expâ [-Wimplicit-function-declaration]
wclines_a2_dats.c:792:1: warning: implicit declaration of function âS2EVarâ
[-Wimplicit-function-declaration]
wclines_a2_dats.c:792:1: error: expected â;â before âtmp44â
wclines_a2_dats.c:835:1: error: âtmp44â undeclared (first use in this
function)
wclines_a2_dats.c:835:1: note: each undeclared identifier is reported only
once for each function it appears in
(*
** A fast approach to counting newlines
** Author: Hongwei Xi (hwxi AT cs DOT bu DOT edu)
** Time: April 17, 2013
)
( ****** ****** )
//
#include
"share/atspre_staload_tmpdef.hats"
//
( ****** ****** *)
staload
UN = “prelude/SATS/unsafe.sats”
(* ****** ****** *)
staload “libc/SATS/stdio.sats”
(* ****** ****** *)
//extern
//praxi b0ytes2bytes_v {bsz:int}
// {l:addr} (pf: b0ytes (bsz) @ l): bytes (bsz) @ l
extern
praxi
bytes_v_unsplit
{l:addr}{n1,n2:int}
(pf: bytes_v (l, n1), bytes_v (l+n1, n2)): bytes_v (l, n1+n2)
// end of [bytes_v_unsplit]
(* ****** ****** *)
%{^
extern
void
*rawmemchr(const void *s, int c);
#define atslib_rawmemchr rawmemchr
%}
extern
fun rawmemchr
{l:addr}{m:int}
(
pf: bytes_v (l, m) | p: ptr l, c: int
) : [l2:addr | l+m > l2]
(
bytes_v (l, l2-l), bytes_v (l2, l+m-l2) | ptr l2
) = “mac#atslib_rawmemchr” // end of [rawmemchr]
(* ****** ****** *)
#define BUFSZ (16*1024)
(* ****** ****** *)
extern
fun freadc // read bytes and then add [c] at the end
{l:addr}
(
pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: char
) : [n:nat] size_t n // end of [freadc]
implement
freadc (pf | inp, p, c) = let
val n = $extfcall
([n:nat] size_t n, “fread”, p, sizeof, BUFSZ-1, inp)
val () = $UN.ptr0_set (ptr_add (p, n), c)
in
n
end (* end of [freadc] *)
(* ****** ****** *)
extern
fun wclbuf
{l:addr}{n:int}
(
pf: !bytes_v (l, n) | p: ptr l, pz: ptr, c: int, res: int
) : int // end of [wclbuf]
implement
wclbuf (pf | p, pz, c, res) = let
val (pf1, pf2 | p2) = rawmemchr (pf | p, c)
in
//
if p2 < pz then let
prval (pf21, pf22) = array_v_uncons (pf2)
val res = wclbuf (pf22 | ptr_succ(p2), pz, c, res + 1)
prval () = pf2 := array_v_cons (pf21, pf22)
prval () = pf := bytes_v_unsplit (pf1, pf2)
in
res
end else let
prval () = pf := bytes_v_unsplit (pf1, pf2)
in
res
end // end of [if]
//
end (* end of [wcbuf] *)
(* ****** ****** *)
extern
fun wclfil{l:addr}
(
pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int
) : int // end of [wclfil]
implement
wclfil{l}
(pf | inp, p, c) = let
//
fun loop
(
pf: !bytes_v (l, BUFSZ)
| inp: FILEref, p: ptr l, c: int, res: int
) : int = let
//
val n = freadc (pf | inp, p, $UN.cast{char}©)
//
in
//
if n > 0 then let
val pz = ptr_add (p, n)
//val () = assertloc (p > null)
val nEOF = if n < (BUFSZ-1) then
(if ($UN.ptr0_get (ptr_add (p,sz2i(n)-1))) = ‘\n’ then 0
else 1)
else 0 // end of [nEOF]
val res = wclbuf (pf | p, pz, c, res)
in
loop (pf | inp, p, c, res)
end else res (* end of [if] )
//
end // end of [loop]
//
in
loop (pf | inp, p, c, 0(res))
end ( end of [wclfil] *)
(* ****** ****** *)
implement
main0 (argc, argv) =
{
var inp: FILEref = stdin_ref
val () =
(
if argc >= 2 then
inp := fopen_ref_exn (argv[1], file_mode_r)
// end of [if]
)
//
val (
pfat, pfgc | p
) = malloc_gc (g1i2u(BUFSZ))
prval () = pfat := b0ytes2bytes_v (pfat)
val res = wclfil (pfat | inp, p, $UN.cast2int(’\n’))
val () = mfree_gc (pfat, pfgc | p)
//
val () = println! ("wclines: number of lines = ", res)
//
val () = if argc >= 2 then fclose_exn (inp)
} (* end of [main0] *)
(* ****** ****** *)
(* end of [wclines.dats] *)
First, svn-update your ATS (no need to re-compile).
Then change ptrget to ptr0_get. The latter is less picky.
It should fix this issue.
I just wanted to post the corrected version of the loop:
fun loop
(
pf: !bytes_v (l, BUFSZ)
| inp: FILEref, p: ptr l, c: int, res: int, last_c: int
) : int = let
//
val n = freadc (pf | inp, p, $UN.cast{char}©)
//
in
//
if n > 0 then let
val pz = ptr_add (p, n)
val last_c = $UN.cast2int($UN.ptr0_get (ptr_add
(p,sz2i(n)-1)))
val res = wclbuf (pf | p, pz, c, res (+nEOF))
in
loop (pf | inp, p, c, res, last_c)
end else if last_c = c then res else res+1 (* end of [if n > 0] *)
//
end // end of [loop]
You need a type annotation for now:
val nEOF =
(
if n < (BUFSZ-1) then
(if ($UN.ptr0_get (ptr_add (p,sz2i(n)-1))) = ‘\n’ then 0
else 1)
else 0
) : int // end of [nEOF]
This will probably be fixed later so that such an annotation is not needed.
int1_of_int : int -> Int; so the type of int1_of_int(0) is Int, which is
for an integer of unknown value. That is why the typechecker complained.
sz2i(n)-1 ==> pred(n)
It seems easier and faster if you keep the value of the [n] obtained in the
previous round.
Then you only need to compute last_c once.
The typechecker does not know sizeof(byte) = 1. You can introduce
the following lemma and use it somewhere inside the body of wclbuf:
extern
praxi lemma_sizeof_byte (): [sizeof(byte)==1] void
You’re right, I did forget make -f codegen/Makefile_atslib; I found the new
build directions on the wiki now.
All of those fixes cleared everything up. It is the same speed as "wc -l"
on my system. I think I’ll save playing with speeding it up further for
another time; it is good enough I think.
As for the bug, I think the original wclbuf conditional may have allowed
the ‘\n’ from freadc at the end of the buffer to be counted as well.
Yes, I discovered that anonymous staload problem.
All i can say is that it is as fast as wc -l on my ubuntu 64 box :), and
slightly faster than my memchr version (the only difference between my c
memchr version and wc is that wc uses a function called “safe_read”, so
that may be balancing it out somehow. I can look in to safe_read as well as
trying out memchr vs rawmemchr.
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.
That sounds good; I didn’t see it at first. When I try this, I get
confronted with a dependent type error (just when I thought I was getting
the hang of them). I also tried annotating with an “if last_n > 0”, which
seems necessary anyway given the starting condition for last_n.
extern
fun wclfil{l:addr}
(
pf: !bytes_v (l, BUFSZ) | inp: FILEref, p: ptr l, c: int
) : int // end of [wclfil]
implement
wclfil{l}
(pf | inp, p, c) = let
//
fun loop {n:nat}
(
pf: !bytes_v (l, BUFSZ)
| inp: FILEref, p: ptr l, c: int, res: int, last_n: size_t n
) : int = let
//
//val n = freadc (pf | inp, p, $UN.cast{char}©, size1_of_int1(BUFSZ-1))
val n = freadc (pf | inp, p, $UN.cast{char}©, size1_of_int1(BUFSZ))
//
in
//
if n > 0 then let
//val pz = ptr_add (p, n)
val () = assertloc (p > null)
val pz = p+n
val res = wclbuf (pf | p, pz, c, res)
in
loop (pf | inp, p, c, res, n)
end else (* else of [if n > 0] ) (if last_n > 0 then
(if $UN.cast2int($UN.ptrget (p+last_n-1)) = c then res
else res + 1):int
else 0):int
//
end // end of [loop]
//
in
loop (pf | inp, p, c, 0(res), size1_of_int1(0) (last_n))
end ( end of [wclfil] *)
I just tried your code. You also need the following line:
staload _(anon) = “prelude/DATS/unsafe.dats”
That is it!
Cheers,
–Hongwei
oh right, that is certainly a problem.
I tried to correct it by doing:
val nEOF = (if n < (BUFSZ-1) orelse fileref_is_eof(inp) …
but I suppose EOF is not set yet either.
I will write a different version to retain the last read char.
int1_of_int(0) should be changed to 0; then the code typechecks.
Now that I look more closely; my backported version is not just off by 1;
it is reading in more lines.
I’m trying to build your latest version in ATS2 to check to see if it is
something I did, but I’m encountering some build errors (I fetched the most
recent ATS2 version from github, copied over the old directory, then
rebuilt per instructions). Here’s the makefile for wclines:
brandon@gulab:/media/RAID5/share/ATS_learning$ make -f Makefile_wclines_a2
gcc -std=c99 -D_GNU_SOURCE -O2
-I"/media/RAID5/share/ATS_learning/ATS-Postiats"
-I"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/runtime
-DATS_MEMALLOC_LIBC -o wclines_a2.exe wclines_a2_dats.c
-L"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/atslib/lib -latslib
wclines_a2_dats.c:139:1: warning: data definition has no type or storage
class [enabled by default]
wclines_a2_dats.c:139:1: warning: type defaults to ‘int’ in declaration of
‘ATSdyncst_unknown’ [enabled by default]
wclines_a2_dats.c:139:1: warning: parameter names (without types) in
function declaration [enabled by default]
wclines_a2_dats.c: In function ‘ATSLIB_056$prelude_ptr0_succ$12$1’:
wclines_a2_dats.c:487:1: error: ‘atstype_byte’ undeclared (first use in
this function)
wclines_a2_dats.c:487:1: note: each undeclared identifier is reported only
once for each function it appears in
wclines_a2_dats.c: In function ‘mainats_argc_argv_0’:
wclines_a2_dats.c:790:1: error: ‘ATSLIB_056$prelude_file_mode_r’ undeclared
(first use in this function)
make: *** [wclines_a2.exe] Error 1
This results in:
brandon@gulab:/media/RAID5/share/ATS_learning$ make -f Makefile_wclines_a2
gcc -std=c99 -D_GNU_SOURCE -O2
-I"/media/RAID5/share/ATS_learning/ATS-Postiats"
-I"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/runtime
-DATS_MEMALLOC_LIBC -o wclines_a2.exe wclines_a2_dats.c
-L"/media/RAID5/share/ATS_learning/ATS-Postiats"/ccomp/atslib/lib -latslib
wclines_a2_dats.c:139:1: warning: data definition has no type or storage
class [enabled by default]
wclines_a2_dats.c:139:1: warning: type defaults to ‘int’ in declaration of
‘ATSdyncst_unknown’ [enabled by default]
wclines_a2_dats.c:139:1: warning: parameter names (without types) in
function declaration [enabled by default]
wclines_a2_dats.c: In function ‘ATSLIB_056$prelude_ptr0_succ$12$1’:
wclines_a2_dats.c:487:1: error: ‘atstype_byte’ undeclared (first use in
this function)
wclines_a2_dats.c:487:1: note: each undeclared identifier is reported only
once for each function it appears in
wclines_a2_dats.c: In function ‘mainats_argc_argv_0’:
wclines_a2_dats.c:790:1: error: ‘ATSLIB_056$prelude_file_mode_r’ undeclared
(first use in this function)
make: *** [wclines_a2.exe] Error 1