hi, you are looking for
https://www.cs.bu.edu/~hwxi/atslangweb/Documents.html
ats-lang.org redirects to this site now
чт, 15 февр. 2024 г., 09:10 Ricardo Bocchi :
> Hello everybody,
>
> It would be great if there was a document describing the language's API,
> something basic with just types,
t;solution" is to use
>> primes()
>> to implement primes_vt() and then uses primes_vt() to generate a linear
>> stream of
>> prime numbers.
>>
>> Again, thanks for the example. I hope that ATS3 will be a lot more
>> convenient to use
>> than ATS2 w
>> real2m35.548s
>> user2m35.532s
>> sys 0m0.000s
>>
>> Haskell (GHC-7.10.3)
>> 14630843
>> real7m41.733s
>> user7m36.208s
>> sys 0m1.688s
>> *)
>>
>> I could not get the haskell implementation to finish
ilar
>>>>>
>>>>> ATS version using non-linear stream is here:
>>>>> https://github.com/dambaev/mobt2/blob/master/ats2/src/TEST/test1.dats
>>>>> , but it takes to much memory as `stream_take_while` duplicates data, as I
>>>>>
s slow as Haskell, so I had started to think of how to
>>> eliminate intermediate data structure.
>>>
>>> So, not a production issue, hehe, just found an interesting topic to dig
>>> in :)
>>>
>>> сб, 9 июл. 2022 г. в 11:11, Hongwei Xi :
>
> wanted to do exactly.
> If you show me how to use a non-linear stream to do it, then I could
> probably say more.
>
> On Sat, Jul 9, 2022 at 5:26 AM Dambaev Alexander
> wrote:
>
>> Hi,
>>
>> I had tried to implement function of type:
>>
>> ```
Hi,
I had tried to implement function of type:
```
fun
{a:t0p}
isPrime
( xs: !stream_vt( int)
, x: int
):
bool
```
Ie, I want to force evaluation of some portion of a stream, but I need to
preserve it for a later use.
I had tried to make a similar version:
```
fun
{a:t0p}
I can confirm, that having ghc (1 GB+) just to build ats package is
overkill.
I am not speaking of cross compiling ghc to another architecture/libc is
pain as well, as it requires big amounts of RAM and 2+ hours of building
for stage1/stage2 compilers Then, you need to build cabal and only
Hi,
In this case, you can try `print_string`, you can see
prelude/SATS/string.sats for reference.
--
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
./prelude/basics_pre.sats:sortdef agz = { l:addr | l > null }
./prelude/basics_pre.sats:sortdef agez = { l:addr | l >= null }
./prelude/basics_pre.sats:sortdef alez = { l:addr | l <= null }
it seems, that addr can be less than null, by the way :)
>
--
You received this message because you are
Hi,
1. agez stands for "address greater or equal zero". so it is like [l: addr
| l >= null]. which is different from [l:addr | l > null], which is 'agz';
2. json_object0 defines a short cat to a json_object that can have null
address. json_object1 in its turn, defines json_object that can only
thanks, that helped!
--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
Can you share the original error message as well?
ATS's prelude heavy relies on templates, so I guess you sign yourself to a
pain by disabling prelude. For example, you can check how arithmetic
operators are being defined by issuing
```
find -name '*.sats' -exec grep -s -H "overload +" {}
\; |
are there any gotchas with partial specification?
I have such template definition:
fn
{env:viewt0ype+}
{a:viewt0ype+}
{element:viewt0ype+}
ifold_left
{fe:eff}
( env: !INV(env)
, i: !INV(a)
, f: (size_t, !INV(env),!INV(element))- bool
):
void
```
and this partial
can I confirm, that ATS2 does not supports partial template specialization?
пн, 6 июл. 2020 г. в 20:14, Hongwei Xi :
> Wow! This is wild C++ code :)
>
> Can't support variadic stuff in ATS3. The type system for type-checking
> in the presence of variadicity would be too complicated.
>
> I did an
Hi,
try to place
```
#include "share/atspre_staload.hats"
```
at the top of of your module
>
>
--
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
The trick is to count the brackets :)
S2Eeqeq is quite easy, as it is a binary operator, so it has 2 operands:
S2Evar(f1(8784)) is the first one, as it followed by '*;', *so the rest is
the second operand :)
>
>
--
You received this message because you are subscribed to the Google Groups
and by the way, the failing constraint was f1 == f1+1
сб, 8 мая 2021 г. в 22:09, d4v3y_5c0n3s :
> Thanks, I appreciate the help. I'm glad that the issue was a simple fix.
> :D
>
> On Saturday, May 8, 2021 at 3:14:33 PM UTC-4 gmhwxi wrote:
>
>> This is due to a missing type annotation for
I would like to thank Aditya Siram as well. His speech "A (not so) gentle
introduction into a systems programming language in ATS" was one of the
reasons why I had actually tried to dig into ATS :)
https://www.youtube.com/watch?v=zt0OQb1DBko
And, as I said there in the comment section: instead
Hi,
HX: can you add anything to it? :)
--
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-users+unsubscr...@googlegroups.com.
To view this discussion
and this is my playground just in case if someone do not like to read code
in the email:
https://github.com/dambaev/ats-complexity/blob/master/src/TEST/
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop
another option is to keep proofs (statics arguments) separately from
dynamics arguments, ie instead of having SATS file for declarations and
DATS for implementations, we can have IATS for implementations, DATS for
dynamic declarations and multiple SATS for statics (like, linear types and
so on),
Hi,
I will start with the question first:
I know, that ptr_get, when used as '!' is able to lookup proof arguments
from the context, but I can't find how '!' had been defined, ie:
```
fn foo{l:agz}( pf: !(int @ l | p: ptr l): void = {
val () = println!( "p = ", !p) (* here ! is able to lookup pf
Hi,
I saw that repo and was wondering why is it using C instead of ATS2 :)
My optimistic plan is to provide ATS bindings to some C libraries to be
able to implement LSP in ATS2 :) such that, some more tooling will be
available for ATS2 as a result.
As far as I understand, ideally, libxatsopt
Hi,
I would like to know what is the current status of the libxatsopt.
In particular: is it ready to be used to implement the language server
protocol support for ATS3?
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this
types around
> various
> STL functions (stack, deque, etc.).
>
> By the way, this is also what is planned for xats2cc, which aims at
> compiling XATSCML to C/C++.
>
>
> On Thu, Jan 21, 2021 at 5:36 PM Dambaev Alexander
> wrote:
>
>> And that is why I dream about
And that is why I dream about an ability to be able to render classes to
Java/C++: as soon as we might have a XATSCML->Java / XATSCML->C++ translator
Ie, to be able to render something like this:
```
UCLASS()class AMyActor : public AActor{
GENERATED_BODY()public:
Hi,
It might be offtopic, but the primary goal of my question in the past about
OOP support in ATS was to understand if it will be possible to:
1. write bindings to use gtk2+ - style of OOP;
2. write bindings/generate source code of classes in a target language.
Although, C ABI is probably still
> I took a quick look:
>
> >>but:
> >>1. fixity operator is not able to use macros
> >>2. when test4 produces cryptic compiler error
> https://github.com/dambaev/ats-branch-test/blob/master/src/TEST/test4.dats#L110
> :
>
> As to (1), I don't quite understand. Fixity is resolved before macro
>
So I was wrong and the issue is not that such code is not correct:
```
fn some_function( i: ! $BS.BytestringNSH1): Option_vt(int) = result where {
val substrings = $BS.split_on( '-', i) // returns a list_vt with
substrings, which are references
val result =
case+ substrings of
|
Hi,
I have a simple function, which type defined at
https://github.com/dambaev/ats-lora_timestamps/blob/master/src/SATS/timestamps.sats#L9-L20
and basically,it's purpose is to split the given string into a substrings
and return either None_vt() in case of failure or a tuple with seconds and
Glad to hear that it is already fixed in ATS3.
Need to get myself in a tonus and actually try out the ATS3 :)
ср, 30 дек. 2020 г. в 23:02, Hongwei Xi :
> Yes, if a linear value matches the wildcard pattern '_', it is leaked.
> It is not a bug, though; it is by design.
>
> This is probably a
. в 16:31, Dambaev Alexander :
> Hi,
>
> milis is a datavtype `Bytestring_vtype`described at
> https://github.com/dambaev/ats-bytestring/blob/master/SATS/bytestring.sats#L8
> and in this particular case, being instantiated by `pack_int64' from
> https://github.com/dambaev/ats-byte
дек. 2020 г. в 16:21, Artyom Shalkhakov :
> Hi Alex,
>
> What's the type of [millis]?
>
> ср, 30 дек. 2020 г. в 10:04, Dambaev Alexander :
>
>> Hi all,
>>
>> today I spotted an error in my code. Here is the snippet:
>> ```
>> va
Hi,
>
> The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
>>> The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>>> S2Eextkind(atstype_int), S2EVar(5314))
>>>
>>
this means that typechecker can't make ```int o``` (indexed int/higher
kinded/g1int) from ```int``` (g0)
Ok, it seems like I need to #include HATS file, in which I should include
'infixl' keyword
--
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
In case if someone will hit the same issue: there was an option to dig into
source code of patscc and to try to speed up constraint solving, but for
now I am not too confident in ATS to perform that, so instead, I had
splitted my function on 2 separate parts, like this:
the original function's
Hi,
I have noticed, that I am not able to introduce new symbol inside sats file
and use it in dats file, like this:
file1.sats
```
fn operator( a: int, b: int): int
symintr +++
infixl (+) +++
overload +++ with operator
```
main.dats:
```
#include "share/atspre_staload.hats"
#define
You may be right. Can you provide some scatch of your view just to check it
out? :)
вт, 24 нояб. 2020 г. в 06:24, gmhwxi :
> Thanks for the message!
>
> What I said is not in conflict with what you described in the message.
>
> An external tool for tracking effects can be quite useful in large
Maintaining some external file seems to me as something, which is easy to
ignore or easy to forget about and without some scatch of of example of
usage, I can't see how it will be helpful at all.
For example:
```
fn foo(): void = println!("hello")
implement main0() = foo()
```
and the external
Glad to hear news about ATS3 implementation!
XATSOPT:
>
> Xatsopt is a functioning compiler implemented in ATS2 for translating
> ATS3 into a typed intermediate language of the name XATSCML, which is
> both C-like and ML-like. It is planned for xatsopt to further
> translate XATSCML into
another option is to use uchar instead of uint8, at least until the missing
stuff for uint8 will be filled
--
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
Thanks for the report. I think all of us can't wait to try ATS3,
especially if it will improve user-experience in comparison to ATS2.
As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in
parallel to xats2js at the point, when ATS3-ML should not have planned
backward
Thanks for the report. I think all of us can't wait to try ATS3,
especially if it will improve user-experience in comparison to ATS2.
As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in
parallel to xats2js at the point, when ATS3-ML should not have planned
backward
Thanks for the report. I think all of us can't wait to try ATS3,
especially if it will improve user-experience in comparison to ATS2.
As I guess, "someone" can try to work on ATS3-ML->C/C++ translator in
parallel to xats2js at the point, when ATS3-ML should not have planned
backward
Glad to hear that: this makes fixing such issues much more faster
сб, 17 окт. 2020 г. в 15:57, Hongwei Xi :
> Have already kept a note of this request.
>
>
> On Fri, Oct 2, 2020 at 9:13 AM Dambaev Alexander
> wrote:
>
>> Hi,
>>
>> I found, that it is diff
By the way,
I decided to spend some more time on your issue and got this:
```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#define ATS_DYNLOADFLAG 0
#define FIELD0_SIZE 100
#define FIELD1_SIZE 200
%{^
#define FIELD0_SIZE 100
#define FIELD1_SIZE 200
struct
Hi,
I have the following example:
```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#define ATS_DYNLOADFLAG 0
implement main0() = {
val a = (Some_vt(0), None_vt())
val b =
case+ a:(Option_vt(int), Option_vt(int)) of (* *9* *)
| @( ~Some_vt(_),
so in this particular case it will work, but proper fix is to dig into
codegen in order to fix the generation of atstyarr_field to have a size
information
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop
in this case the issue is that ```fname[]``` contains no size information.
This one works:
```
#define MAXPATHLEN 1024
%{^
#define MAXPATHLEN 1024
#define atstyarr_field_undef(fname) fname[MAXPATHLEN]
%} // end of [%{]
typedef kld_file_stat = @{ version = int, name = @[char][MAXPATHLEN], refs
=
GCC says, that it wants array field at the end of the struct, so:
```
typedef kld_file_stat = @{ version = int, refs = int, name =
@[char][MAXPATHLEN] }
```
works
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group
Hi,
```
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
#define ATS_DYNLOADFLAG 0
%{^
#define \
atstyarr_field_undef(fname) fname[]
%} // end of [%{]
#define MAXPATHLEN 1024
typedef kld_file_stat = @{ version = int, name = (@[char][MAXPATHLEN])}
fun kern_kldstat
Hi,
In this example, I am trying to define a binding of type Option_vt(int),
```
#include "share/atspre_staload.hats"
#define ATS_DYNLOADFLAG 0
implement main0() = {
val a = 0
val b =
case+ a of
| 0 => Some_vt(0) *(* 9 *)*
| _ => None_vt() *(* 10 *)*
val () =
case+ b of
or, in case if this URL is not reachable (seems like relative to my
mailbox):
https://groups.google.com/g/ats-lang-users/c/V5LihCmnXKc
пн, 12 окт. 2020 г. в 08:01, Dambaev Alexander :
> Hi,
>
> check this topic:
>
> https://mail.google.com/mail/u/0/#
Hi,
check this topic:
https://mail.google.com/mail/u/0/#category/forums/QgrcJHsBrnXTtpBcBJPBCfzSNNVXkQVSFQv
пн, 12 окт. 2020 г. в 02:16, d4v3y_5c0n3s :
> Here's my problem:
> I'm encountering this weird error where the compiler is for some reason
> telling me that I cannot produce an
g to skip
> constraint-solving:
>
> --constraint-ignore
>
> This will tell you if constraint-solving is indeed the culprit here.
>
> Using an external constraint-solver like Z3 may improve. However,
> constraint-solving
> is inherently of exponential-time.
>
>
Hi,
I have noticed, that patsopt takes huge amount of time, to compile
relatively small library https://github.com/dambaev/ats-bytestring
``
[nix-shell:/data/devel/ats2/bytestring]$ $(which time) make test1
patscc -O2 -DATS_MEMALLOC_LIBC -I"../libs/" -c -o SATS/bytestring_sats.o
alue argument can be a left-value. So 'i' is
>> treated as a proof,
>> and its erasure is of the type 'void'.
>>
>>
>> On Sat, Oct 3, 2020 at 11:32 PM Dambaev Alexander
>> wrote:
>>
>>> Hi,
>>>
>>> I have a viewtype, defined like
Hi,
I have a viewtype, defined like this:
```
absvt0ype
Bytestring_vtype
( len:int (* size in bytes, which occupied by data *)
, offset: int (* the offset from base pointer at which data of length len
starts *)
, cap: int (* capacity of the buffer *)
, ucap: int (* how much unused bytes
Hi,
I found, that it is difficult to locate constraint, that had been failed to
be solved.
For example, I got error message like this:
```
/data/devel/ats2/bytestring/DATS/bytestring_flat.dats: 12395(line=442,
offs=49) -- 12409(line=442, offs=63): error(3): unsolved constraint:
Hi,
I am starting to think, that my code's goal is to explore corner cases of
type checker :)
This time, I have this error:
```
/data/devel/ats2/bytestring/DATS/bytestring_flat.dats: 8313(line=299,
offs=8) -- 8316(line=299, offs=11): error(3): this constraint cannot be
s3exp2icnstr-handled: s3e0
ah you are right! Big thanks!
вт, 29 сент. 2020 г. в 03:30, Hongwei Xi :
> I believe that #[...] must be at the leading position. Please try to
> change each [...] to #[...].
>
> On Mon, Sep 28, 2020 at 11:16 PM Dambaev Alexander
> wrote:
>
>> Hi.
>>
>> I
Hi.
I want to write a spec for a function 'append', which purpose is to append
content of the second argument into the end of the content of the first one.
I came to this:
```
(* creates new bytestring with content of r appended to l. does not
consumes l and r
in case if 'l' has enough unused
stack-allocated variable ('buf' in this case), there
>> should be a proof of
>> some at-view associated with the variable at the end of its life. In this
>> case, the proof associated
>> with 'buf' is turned into a proof of the view Bytestring_v, which is not
>> an at
Hi,
I got assert failure:
```
exit(ATS): [assert] failed:
/tmp/ATS-Postiats/src/pats_trans3_env_dvar.dats: 14625(line=619, offs=20)
-- 14641(line=619, offs=36)
```
from this code
SATS file:
```
(* abstract viewtype, that describes Bytestring with capacity and size *)
absvt0ype
Bytestring_vtype
hi
I was trying to create a function ptr1_add_sz, which should return a
non-null pointer like this:
```
fn
{a:viewt0ype}
ptr1_add_sz
{*l:agz*}{n:nat}{*sizeof(a) > 0*}
{ l+n*sizeof(a) > null }
( i: ptr l
, n: size_t n
):<>
ptr (l+n*sizeof(a)) = ptr_add(i, n)
```
the initial
hi,
in the error you mentioned, compiler says, that you had moved ar into
ar_copy. In this case, there is an overloadable operator 'copy' to be used
like this:
```
val ar_copy = copy ar
```
but I see no such operator being defined for arrayptr.
if you want to just traverse the whole array, you
Hi,
I want to confirm what I see in practice:
1. I had defined abstract vtype Bytesting and overloaded '+' operator for
it like this:
```
(* the same as append, but consumes arguments in order to make caller's
code clear from bunch of val's and free()
*)
fn
appendC
{l_n, r_n, l_cap, r_cap:
that i >= 0 *
чт, 3 сент. 2020 г. в 19:24, Dambaev Alexander :
> hi
> as far as I can see, the error message asks to prove, that i > 0. You have
> constraint i+1 >= 0, so i can be ~1, which is not natural number, but quite
> from tutorial:
> ```
> A termination metric
*Kiwamu: *wow, thanks for your trust, but after my quick view of your wiki
page http://jats-ug.metasepi.org/doc/ATS2/ATS_Foundations/showtype.html and
at the moment, I don't think, that I can add much more to it
*Hongwei: thanks, you are right. glib's bindings provide 2
Hi
Usually, I am able to parse and solve compiler errors, but now I need help:
```
macdef GSIGNAL_CANCELLED = $extval( $GLIB.gsignal, "cancelled")
fn foo( p: $GLIB.gpointer): void = ()
val p = $GLIB.gpointer the_null_ptr
prval _ = $showtype p
val _ = $GLIB.g_signal_connect( cancellable,
1. the reason why we need to prove, that x = addr@opts is that
shared_unref's type says, that it's return type defines *some* 'l':
```
extern fun shared_unref{a:vt@ype} (shared(a)): *[l:addr]*[c:int]
(option_v(a@l, c <= 1) | ptr l, int c)
```
this *l* can be the same as addr@opts, but can be some
it works when you alias view of opts and proof, that x is the same as
addr@opts
```
implement main0 () = let
var opts: ip6_pktopts with opts_pf
var inp: inpcb
val () = inp.in6p_outputopts := addr@opts
val () = inp.sh := shared_make(opts_pf | addr@opts)
val (pf_oopts | x, count)
or maybe I misunderstood your question? I had unanswered how to restore
type of opts to solve compiler error.
сб, 29 авг. 2020 г. в 08:40, Dambaev Alexander :
> hi, just a quick answer on the go:
> you need to use shared_unref, which will gave you view of type option_v(
> a@l), and wh
hi, just a quick answer on the go:
you need to use shared_unref, which will gave you view of type option_v( a@l),
and when c <= 1, you will be able to use opt_unsome
сб, 29 авг. 2020 г. в 08:31, Kiwamu Okabe :
> Dear all,
>
> There is a security issue on FreeBSD:
>
> * Security Advisory:
>
Hi,
I see, that ATS2 has support of OOP (in particular, as I see in GTK from
contrib package).
Is OOP planned to be supported by ATS3?
Is there any documentation about how to use OOP in ATS2 other than source
code?
--
You received this message because you are subscribed to the Google Groups
In fact, I had some issues to express the same thing in ATS2. The closest
sample (in case if Rust does stack allocation of the clone of the line in
closure) is:
```
staload UN="prelude/SATS/unsafe.sats"
extern prval hack{l:addr} ( pf: int @ l): void
fn
linum
{l:addr}
(
):
( (int0 @ l)
Hi, Timmy.
That is why I have asked: for me, `line` is stack allocated and have to be
freed at linum()'s exit. That is why I am asking how rust is able to move
it to a closure, which lives longer than `linum()` itself. In my world, I
was sure, that only heap allocated memory is being able to
Hi,
I want to ask someone who knows Rust about this example: if I remember
correctly, mutable variable in Rust is stack allocated, so I want to know
how it is able to move line to a closure, because I thought, that the
lifetime of line is the same as lifetime of linum(). Am I missing something?
Hi,
array and arrayptr have constraint {a:vt0p} for most of functions, except
array_set_at / arrayptr_set_at/array_get_at/arrayptr_get_at, which have
constraint {a:t0ype}
So we can enumerate elements as viewtypes with foreach family of functions,
but the only way to set/get them is to use
Oh, that is actually very helpful! Thanks a lot. Looks like I am using too
little tutorials to search for ATS's syntax :)
--
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
Hi,
We know, that ATS is able to keep information about check in appropriate
branch of 'if' expression, like:
```
fn foo( i: int): int =
if i < 1
then (* here typechecker knows, that i < 1*)
else (* here typechecker knows, that i >= 1*)
```
But sometimes, you need to use more conditions
Thanks for your responses, guys
--
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-users+unsubscr...@googlegroups.com.
To view this discussion on the
ah, looks like it is because of sort of return type:
```
): size_t(oidx) =
```
I had spent a day dancing around this scaffold and got it after sending a
messge
сб, 25 июл. 2020 г. в 05:54, Dambaev Alexander :
> Hi,
> I am struggling to satisfy typechecker with implementing a loop
Hi,
I am struggling to satisfy typechecker with implementing a loop with 2
indexes.
```
fn
encode0
{n: nat}{m:nat | m > n}{l:agz}
( o_pf: !array_v(byte, l, m)
| i: &(@[byte][n])
, i_sz: size_t(n)
, o: ptr l
, o_sz: size_t(m)
): #[m1:nat | m1 <= m] size_t(m1)
implement
Hi,
I have tried to manually create datatype constructors, but such way lacks
type checking completely as it consist from many unsafe casts.
I had tuned my previous example with tuples of different sizes a little bit
to get a more or less type safe version:
```
typedef gw_ns_request_v1_max_t =
type 'foo_pstruct' is
> automatically introduced
> (in the same namespace). You can study the generated C code to figure out
> the related details.
>
>
> On Sun, Jul 19, 2020 at 10:47 AM Dambaev Alexander
> wrote:
>
>> So I have tried to use views to replace datatypes. My i
Well, let's hope, that ATS3 will have such feature
сб, 18 июл. 2020 г. в 06:21, Artyom Shalkhakov :
> Hi Alex,
>
> сб, 18 июл. 2020 г. в 09:17, Dambaev Alexander :
>
>> Hi,
>>
>> datatypes/datavtypes are heap-allocated, which runtime representation, I
>> g
Hi,
datatypes/datavtypes are heap-allocated, which runtime representation, I
guess, is a tag and a pointer to data.
ATS has unboxed tuples and unboxed records, which runtime representation, I
guess, are C's structs
Is there a way to define a stack allocated datatype?
I think, we can have them
>
> Going off of what Dambaev said, *it makes sense to prove to the compiler
> that 'i' is >= 0 && < 4, but what sort of statements might I use for this? *
> I worked through chapter 12 of Intro to Programming in ATS, but I'm still
> quite unsure on how to use proofs effectively. Thanks for this
Hi,
just a quick tip:
```
The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
S2Eextkind(atstype_int), S2EVar(6368))
```
means, that you passing an argument of primitive type, but you need a
higher kinded type (int n, where
вс, 12 июл. 2020 г. в 15:50, gmhwxi :
> Am really pleased that you figured it out :)
>
It was pleasure for me as well :D
The first time, when I started to think about it, was when I saw that
array_v_split has no parameters and I asked myself "how does it know on
which parts it should be
And at the end, it turned out, that I am not required to manually write
those proofs:
```
extern
fn recvfrom
{l: agz} {n: pos}{addr_sz:pos}
( buf_pf: !array_v(char?, l, n) >> recvfrom_v(l,n,m)
| socket_fd: int
, buf: ptr l
, sz: size_t n
, flags: int
, src_addr: _struct(addr_sz)? >>
Hi,
thanks for your advice: I think your way is much better, because it does
not requires heap usage
My working code looks like this (in case if someone will struggle with
similar stuff):
```
dataview recvfrom_v(addr, int, int) =
| {l:agz}{n:pos}{m:int | m <= 0 || m > n}
recvfrom_v_fail(l,
My current, not so successful try is to define result_vt:
datavtype result_vt (av: view, a:t@ype+, bv: view, b:t@ype+) =
| Success_vt(av,a, bv, b) of (av | a)
| Failure_vt(av,a, bv, b) of (bv | b)
and function's ftype:
fn
recvfrom
{l: addr} {n: pos}
( buf_pf: array_v(char?, l, n)
|
raw' after this: compiler says, that it
is unable to search proof for it, but using 'raw1' is ok
пт, 10 июл. 2020 г. в 06:29, Dambaev Alexander :
> Thanks, datavtype way is working, but I will try more to not to use heap,
> including latest suggestions
>
> пт, 10 июл. 2020 г. в 06:26, Hon
the fact you’d be using a tuple.
>
> Much easier to use what you’ve already found or what Hongwei describes.
>
> Sent from my iPhone
>
> On 10 Jul 2020, at 04:12, Dambaev Alexander wrote:
>
>
> For now, I have found the only way to achieve my goal is by using box
is
heap-allocated and I don't know how to cleanup such tuple without GC
чт, 9 июл. 2020 г. в 23:54, Dambaev Alexander :
> And again, I had mistyped one thing in initial email:
>
> (* ... *)
> var tmp = (recv_buf_pf | recv_buf) (* var instead of val in both similar
> lines *)
> (* ...
And again, I had mistyped one thing in initial email:
(* ... *)
var tmp = (recv_buf_pf | recv_buf) (* var instead of val in both similar
lines *)
(* ... *)
чт, 9 июл. 2020 г. в 23:47, ice.r...@gmail.com :
> Hi,
>
> I am trying to understand how to use array_foreach_env function to pass to
>
Thanks, I will check it out
ср, 8 июл. 2020 г. в 14:30, Hongwei Xi :
> You can find these operations in prelude/SATS/integer.sats
> There are called:
> lnot (for ~),
> land (for &), lor (for |), lxor (for ^), lsl (for <<), and lsr (for >>).
>
> These operations are for unsigned ints. For signed
1 - 100 of 110 matches
Mail list logo
