Arrayptr problem

hello,
I still have a problem with arrayptr.

#include “share/atspre_staload_tmpdef.hats”

staload "prelude/SATS/arrayptr.sats"
staload _ = “prelude/DATS/arrayptr.dats”

extern fun destroy_buf{n: nat}(buffer: arrayptr(float, n)): void

implement destroy_buf(buffer) = () where {
val () = arrayptr_free{float} buffer
}

implement main0() = ()

This simple example does not compile :

test_buf_bug_dats.c: In function
’_057$usr_057$users_057$cydu_057$programming_057$ATS_057$DEV_057$ats3d_057$test_057$test_buf_bug_056$dats_destroy_buf’
:
test_buf_bug_dats.c:243: warning: implicit declaration of function ‘_045$’
/tmp//ccoAoS9d.o: In function
_057$usr_057$users_057$cydu_057$programming_057$ATS_057$DEV_057$ats3d_057$test_057$test_buf_bug_056$dats_destroy_buf': test_buf_bug_dats.c:(.text+0x16): undefined reference to_045$’

whereas this one does compile :

#include “share/atspre_staload_tmpdef.hats”

staload "prelude/SATS/arrayptr.sats"
staload _ = “prelude/DATS/arrayptr.dats”

extern fun{a: t@ype} destroy_buf{n: nat}(buffer: arrayptr(a, n)): void

implement{a} destroy_buf(buffer) = () where {
val () = arrayptr_free{a} buffer
}

implement main0() = ()

thanks :wink:

thanks :wink:

Please delete the following lines:

staload "prelude/SATS/arrayptr.sats"
staload _ = “prelude/DATS/arrayptr.dats”

They have already been loaded.

The second one compiles because you have not used the template
destroy_buffer.