ptr1 and v0tp

[matthia...@bejocama.de]

Hi,

after migrating the string functions in the lib of the linux kernel to ats I'm now starting to

to improve the code in an ats sense. A first step was to change from ptr0_get/set to

ptr1 (sure, still unsafe stuff - but better type checked regarding implicit type conversions).

The code at the end demonstrates a little problem. ptr1_succ<char>(pp) doesn't have the

property l:agz even pp has it. Second, looking on the template parameter of ptr1_succ

I get vt0p which stands for viewt@ype. I cannot actually get this in sync with documentation,

because a viewt@ype should be something like vtypedef VT(T:t@ype,l:addr) = ( T@l | ptr(l) ).

So I think the template parameter should be of t0p = t@ype. Otherwise I have wrong expectations
in how to use these functions - and I don't really understand why my code compiles.

Finally an last minute insight regarding the usage of ptr1_pred: l:addr | l > (null + sizeof(a)) .. works -

without the null not. I know, in this case I should not be surprised. But l,r:agz | r == (l + sizeof(a)) --

doesn't imply r >= l.

Here is the code - c-style strlen - very often called by the kernel and the performance seems

to be good. The ptr0 version works (and also my pointer type modification pgz):

#define ATS_DYNLOADFLAG 0
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
staload "prelude/SATS/unsafe.sats"

fn strlen{l:agz}(p:ptr(l)) : [r:nat] size_t(r) =
let
  fun loop{ll:agz| ll >= l}(pp:ptr(ll)) : [r:agz| r >= ll] ptr(r) =
      case+ ptr1_get<char>(pp) = '\0' of
        | true => pp
        | false => loop(ptr1_succ<char>(pp))
in
  g1ofg0(cast{size_t}(loop(p) - p))
end

implement main0 () =
let
var s = @[char][4]('A','B','C','\0')
val x = strlen(addr@(s))
in
println!(x)
end

[Hongwei Xi]

Your code should work if you add the following lines

at the beginning:

prfun
lemma_char_size()
: [sizeof(char) > 0] void

prval () = lemma_char_size()

These lines tell the type-checker that sizeof(char) is positive.

Right now, the type system only knows that 'sizeof(char)' is an int.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9e71a4f6-6be7-44ed-8e61-c7b44d260b34o%40googlegroups.com.

[Matthias Wolff]

Surprising answer, because I don't understand the details at the moment.
It comes earlier than I expected. But I will take the chance. Thanks.

Am 25.07.20 um 21:32 schrieb Hongwei Xi:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLoo4t-5ZisDftmGV1rUuHLqnuLWiw_he%3DLQYY2PUww9ZA%40mail.gmail.com.

[Hongwei Xi]

#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#staload UN = "prelude/SATS/unsafe.sats"

#define ATS_DYNLOADFLAG 0

(*
Recursion is at the center of programming.
And recursively defined concepts are occurring everywhere.
For instance, the C-string concept is recursively defined.
Let 'string(n)' be a type for C-strings of the size 'n'.

We can readily implement the following three functions
for recursively traversing a C-string:
*)

extern
fun{}
string_nilq
{n:int}(string(n)): bool(n==0)
extern
fun{}
string_head{n:pos}(string(n)): char
extern
fun{}
string_tail{n:pos}(string(n)): string(n-1)

(*
For saving time, these three functions
are given the following UNSAFE implementation
*)
implement
string_nilq<>(cs) =
$UN.cast
(
iseqz
($UN.ptr0_get<char>(string2ptr(cs)))
)
//
implement
string_head<>(cs) =
($UN.ptr0_get<char>(string2ptr(cs)))
//
implement
string_tail<>(cs) =
$UN.cast(ptr_succ<char>(string2ptr(cs)))

(*
Then the length for C-strings can be implemented
as follows:
*)

fun
strlen
{n:nat}
(cs: string(n)): int(n) =
loop(cs, 0) where
{
fun
loop
{i,j:nat|i+j==n}.<i>.
(cs: string(i), j:int(j)): int(n) =
if
string_nilq(cs)
then j else loop(string_tail(cs), j+1)

}

implement main0 () =
let
var s = @[char][4]('A','B','C','\0')

val x = strlen($UN.cast{String0}(addr@(s)))
in
println!(x)
end

######

When compiled to assembly (after inlining), the strlen function implemented

above is essentially the same as the one you did that uses pointers explicitly.

Obviously, you can replace C-strings with other forms of sequences.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/3159e612-bc45-e896-f00a-776c03261c2d%40bejocama.de.

[Matthias Wolff]

Your speed is impressing. I take all I can get. It's really an adventure.
In my early stage of my playground "ats linux kernel" it helps to make
good design decisions.

Am 25.07.20 um 23:34 schrieb Hongwei Xi:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp-8Jy%3DRSriqH5vjGjhvxsDV_uSLEkU3KPKBBH2OReS8Q%40mail.gmail.com.

[Hongwei Xi]

As I suggested in my previous email, please try to build a library of your own for this project.

Try to avoid using ptr and use cptr instead. Note that ptr is like void* and cptr(T) is like T* in C.

Also try to avoid using dependent type at the beginning. Dependent types can be introduced later

for the purpose of static debugging.

Personally, I feel that ATS3 would be a lot better for such a project, but ATS2 is adequate. Once ATS3

becomes ready, the project can be readily translated from ATS2 into ATS3.

Cheers!

--Hongwei

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/c0521819-7262-7387-b588-dc1a3bbb52bd%40bejocama.de.