/usr/share/doc/ats-lang-anairiats-examples/examples/KernighanRitchie/Chapter01/longest_line.dats is in ats-lang-anairiats-examples 0.2.5-0ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 | //
// K&R, 2nd edition, page 29
//
//
// Translated into ATS by Hongwei Xi (hwxi AT cs DOT bu DOT edu)
//
(*
** Handling C strings (byte sequences ending with the null byte)
** in ATS is a constant challenge. This example makes use of several
** advanced features in ATS that are probably difficult for a beginner
** to grasp. So skip it if you find it to be the case.
*)
(* ****** ****** *)
staload "libc/SATS/stdio.sats"
(****** ****** *)
#define MAXLINE 1000
typedef b0ytes (n: int) = @[byte?][n]
(* ****** ****** *)
// implemented in C
extern
fun getline {m:pos} {l:addr}
(pf_buf: b0ytes m @ l | p_buf: ptr l, m: int m)
: [n:nat | n < m] (strbuf (m, n) @ l | int n)
= "__getline"
// end of [getline]
(* ****** ****** *)
// implemented in C
extern
fun copy {m,n:nat | n < m} {l_to,l_from:addr} (
pf_to: !b0ytes m @ l_to >> strbuf (m, n) @ l_to
, pf_from: !strbuf (m, n) @ l_from
| p_to: ptr l_to, p_from: ptr l_from
) : void
= "__copy"
// end of [copy]
(* ****** ****** *)
#define s2b bytes_v_of_strbuf_v // from [prelude/SATS/string.sats]
(*
** It is formally verified in the type system of ATS that there is
** *no* possibility of buffer overlow in this implementation under the
** assumption that both [getline] and [copy] are implemented correctly
** in C.
*)
implement main () = let
#define M MAXLINE
var !p_line with pf_line = @[byte][M]()
var !p_longest with pf_longest = @[byte][M]()
val () = bytes_strbuf_trans (pf_longest | p_longest, 0)
val max = loop (pf_line, pf_longest | p_line, p_longest, 0) where {
fun loop {max:nat | max < M} (
pf_line: !b0ytes M @ p_line
, pf_longest: !strbuf (M, max) @ p_longest >> strbuf (M, max) @ p_longest
| p_line: ptr p_line, p_longest: ptr p_longest, max: int (max)
) : #[max: nat | max < M] int max = let
val (pf_line_new | n) = getline (pf_line | p_line, M)
in
if n = 0 then let
prval () = pf_line := s2b (pf_line_new)
in
max // loop exits
end else begin
if max < n then let
prval () = pf_longest := s2b (pf_longest)
val () = copy (pf_longest, pf_line_new | p_longest, p_line)
prval () = pf_line := s2b (pf_line_new)
in
loop (pf_line, pf_longest | p_line, p_longest, n)
end else let
prval () = pf_line := s2b (pf_line_new)
in
loop (pf_line, pf_longest | p_line, p_longest, max)
end (* endif *)
end // end of [if]
end (* end of [loop] *)
}
in
if (max > 0) then let
val () = print_string (str) where {
extern castfn string_of_ptr (p: ptr): string
val str = string_of_ptr (p_longest)
} // end of [val]
prval () = pf_longest := s2b (pf_longest)
in
// empty
end else let
prval () = pf_longest := s2b (pf_longest)
in
// empty
end // end of [if]
end // end of [main]
(* ****** ****** *)
%{$
ats_int_type
__getline (
ats_ptr_type s0, ats_int_type lim
) {
int c, i; char *s = (char*)s0 ;
for (i = 0; i < lim-1 && (c=getchar()) != EOF && c!='\n'; ++i)
s[i] = c;
if (c == '\n') { s[i] = c; ++i; }
s[i] = '\0';
return i;
} // end of [__getline]
ats_void_type
__copy (
ats_ptr_type to, ats_ptr_type from
) {
int i;
i = 0;
while ((((char*)to)[i] = ((char*)from)[i]) != '\0') ++i;
return ;
} // end of [__copy]
%} // end of [%{$]
(* ****** ****** *)
(* end of [longest_line.dats] *)
|