The group has been dormant for quite some time.
>> I hope all is well with development on ATS3 at least!
Thank you!
It is ongoing, and, hopefully, we will have a release this year.
Cheers!
--Hongwei
On Wed, Feb 14, 2024 at 1:08 AM Gianni wrote:
> Hello,
> I was wondering if this group was
By the way, qlist is not flat; it is based on list. To have a flat one, you
can use dynarray
(which is like vector in C++). I suppose that dynarray can further shorten
the running time.
On Tue, Jul 12, 2022 at 8:44 AM Hongwei Xi wrote:
> Thanks for this very interesting example!
>
>
t;
>>>>>>>> ## ATS ##
>>>>>>>>
>>>>>>>> (* Your code using non-linear stream *)
>>>>>>>> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes -DATS_MEMALLOC_LIBC
>>>>>>>> primes.d
ing linear stream that is based on yours*)
>>>>>
>>>>> hwxi@hongwei-t440p:/tmp$ patscc -O2 -o primes2 -DATS_MEMALLOC_LIBC
>>>>> primes2.dats
>>>>> hwxi@hongwei-t440p:/tmp$ time ./primes2
>>>>> 1077871
>>>>>
>>
By looking at your first version, my simple answer is that a linear stream
cannot be used
in this way. The second version is possible but I am not sure what you
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
Currently, my practice is just declare something like:
abstype myenum = int
or
abstype myenum(i:int) = int
Then implement 'myenum' somewhere in a file. It can clearly be done, but it
is really tedious,
involving a lot of boilerplate type of code. I suppose some kind of
meta-programming can be
Where can I find your source code so that I can produce the error you are
referring to?
--Hongwei
On Thu, Dec 30, 2021 at 12:47 PM d4v3y_5c0n3s wrote:
> Ok, so I've been able to get the "dict" type to be abstract, but I can't
> seem to get "bucket" to be abstract. I tried adding the "= ptr"
I could not produce the error by using the code snippet you provided.
The error message in your code is likely due to the conflict between
nominal type equality
(in C) and structural type equality (in ATS); postiats_tyrec_7 and
postiats_tyrec_15 are nominally
different in C but they should be
I don't quite understand.
Templates in ATS2 are supposed to be working with abstract types.
If I could try precisely what you did on your machine, then I may be able
to suggest something.
On Tue, Nov 30, 2021 at 8:27 PM d4v3y_5c0n3s wrote:
> Update 2:
> After investigating the prelude, I've
I tried your code and it compiled without any issue.
Did you have the following line at the top:
#include "share/atspre_staload.hats"
The error messages you showed indicate that many template implementations
were not
available to the compiler (patsopt).
--Hongwei
On Tue, Nov 30, 2021 at
If you try to compile to JS, then you cannot have 'main0' in your code.
For instance, the following code worked when I tried:
*datavtype maybe(a:vt@ype) =| NAH of ()| YAH of (a)fn{a:vt@ype} maybe_nah
() : maybe(a) = NAH()fn{a:vt@ype} maybe_yah ( x: a ) : maybe(a) = YAH(x)*
*val () =
You need the flag '-DATS_MEMALLOC_LIBC'.
On Mon, Nov 29, 2021 at 12:00 PM d4v3y_5c0n3s wrote:
> I tried to compile the above snippet on my local machine, and got the
> following error:
> /usr/lib/gcc/x86_64-pc-cygwin/11/../../../../x86_64-pc-cygwin/bin/ld:
>
Is there a way for me to generate the error you are referring to?
The above code works fine on my end.
--Hongwei
On Mon, Nov 29, 2021 at 10:16 AM d4v3y_5c0n3s wrote:
> I think I've been able to break down a problem I've been having with ATS'
> templates into a simple example provided below.
First, tri_test(0) is just:
[un:int | 0 <= un; un+1 <= 0; un == 0; 0 == 0] int(un)
Clearly, no value can be given the above type as 0 <= un and un+1 <= 0
yields a contradiction.
On Wed, Jun 30, 2021 at 10:12 PM d4v3y_5c0n3s wrote:
> So, I'm trying to get the following code to work:
>
Yes, you can.
Please take a look at how 'charptr' is handled in the following simple
example:
https://github.com/githwxi/ATS-Postiats/blob/master/doc/EXAMPLE/MISC/mysendmailist.dats
On Sat, Jun 5, 2021 at 3:42 PM David Smith wrote:
>
> Hey,
> I'm trying to use a C library (libwayland) from
This kind of guarantee can always be established with a run-time check.
If you want to solve constraints involving 'lor', then you need to use an
external solver like Z3.
But it would require a lot of effort.
I would suggest using a run-time check for now. And you could always come
back to fix
implement(env_t) ifold_left<$BS.Bytestring1>( env, i, f) = ()
should probably be:
implement(env_t) ifold_left<$BS.Bytestring1>( env, i, f) = ()
On Fri, May 21, 2021 at 6:13 AM Dambaev Alexander
wrote:
> are there any gotchas with partial specification?
>
> I have such template definition:
>
You may want to check out some work by Joshua Dunfield on bidirectional
typechecking.
--Hongwei
On Tue, May 11, 2021 at 10:27 PM Elijah Stone wrote:
> Not entirely topical, but--does anybody have resources on implementing
> refinement types?
>
> I found this dissertation
This is due to a missing type annotation for 'ifcase'
in your code:
val ret_fbc =
(
ifcase
| tr=0 =>
(FBT_CONS(fbc.0) | fbc.1+1, fbc.2)
| tr=1 =>
(FBT_CONS(fbc.0) | fbc.1, fbc.2+1)
| _ => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2+1)
) : [f1,b1:nat] fb_count(a, f1, b1)
In general, if-exp, case-exp
-- Forwarded message -
From: Phil Roc
Date: Sun, Apr 18, 2021 at 10:50 AM
Subject: Re: ATS2 source make issue
To: ats-lang-users
Hello,
I've ended up installing ATS2 using Homebrew (
https://formulae.brew.sh/formula/ats2-postiats), instead of compiling it
myself.
Case closed.
FYI.
-- Forwarded message -
From: Philippe de Rochambeau
Date: Sun, Apr 18, 2021 at 1:18 AM
Subject: ATS on iSh
To:
Hello,
for your information, the ATS source code compiles in iSh (https://ish.app/)
on an IPad Air 2.
I’ve tried compiling several computer languages on iSh,
hands are tied with the very task of implementing ATS3.
On Wed, Apr 7, 2021 at 12:50 AM Kiwamu Okabe wrote:
> On Tue, Apr 6, 2021 at 3:50 PM Hongwei Xi wrote:
> > vtypedef rib_cmd_info = @{
> > rc_rt = [l:addr] (rtentry @ l | ptr l)
> > }
> >
> > It seems
Okay. I put some 'topize' functions in basic_dyn.dats.
Changes have been uploaded.
On Tue, Apr 6, 2021 at 3:44 AM Kiwamu Okabe wrote:
> Dear Hongwei,
>
> On Tue, Apr 6, 2021 at 3:32 PM Hongwei Xi wrote:
> > >>I feel the uninitize function is not safe...
> >
> &g
It is difficult to work as the following type as one cannot easily take out
the rc_rt
component:
vtypedef rib_cmd_info = @{
rc_rt = [l:addr] (rtentry @ l | ptr l)
}
It seems that you are trying to do C-style programming in ATS directly.
This would
be difficult; it may not even be practical for
>>I feel the uninitize function is not safe...
Such a function is always safe as initialized data can always
be treated as uninitialized.
On Tue, Apr 6, 2021 at 2:08 AM Kiwamu Okabe wrote:
> Dear Hongwei,
>
> On Tue, Apr 6, 2021 at 3:00 PM Hongwei Xi wrote:
> > I
It seems that you need to unintialize 'e' explicitly:
extern
praxi
uninitize
{a:t0ype}
(x: (a) >> a?): void
implement main0 () = {
var e: wg_endpoint
var so: sockaddr = Af_inet @{
sin_port = 1,
sin_addr = 2,
sin_zero = 3
}
var so6: sockaddr = Af_inet6 @{
sin6_port = 1,
>>val () = !e.e_remote := so
The original linear content in !e.e_remote is discarded, resulting in a
leak. Also, 'so' is
a pointer (instead of a sockaddr).
On Sun, Apr 4, 2021 at 1:33 AM Kiwamu Okabe wrote:
> I think I miss-undertood datavtype.
> In this case, it doesn't need to depend to
For such a use, you need a type annotation:
fun concat_exec_imgact {i:int} (pagesizes: ulint i): ulint = let
val
psize =
(
if
pagesizes > 0UL
then pagesizes else 1UL
) : [i:pos] ulint(i)
in
concat_rnd_base(psize)
end
On Wed, Mar 31, 2021 at 8:31 AM Kiwamu Okabe wrote:
> Dear all,
>
> I wrote
The implementation of FM in ATS/Postiats is largely standard.
One small improvement lies in its handling of an inequality of the
following kind:
2x + 2y >= 1
This inequality is first changed to 2x + 2y >= 2 and then simplified to x +
y >= 1.
The implementation uses linear types to ensure
(x: >> _) means that the argument is call-by-reference; the integer
in it may be updated.
BTW, (x: ) means that the argument is read-only call-by-reference, but
it is not enforced in ATS2
Note that ( >> _) is just a shorthand for ( >> T).
On Fri, Jan 22, 2021 at 8:24 AM d4v3y_5c0n3s wrote:
There are a couple of issues. Maybe the following code is what
you wanted:
fn chng_int_test ( i: >> _ ) : void = i := i + 1
fn test_chnge () : int = let
var i: int = 0
val () = chng_int_test(i)
in
i
end
On Fri, Jan 22, 2021 at 12:51 AM d4v3y_5c0n3s wrote:
> I'm trying to use call by
I think I misunderstood your earlier message.
If I understand you correctly this time, then what you mentioned in this
message
can already be done in ATS2 (you need ats2cpp for using g++ on the generated
code):
https://github.com/githwxi/ATS-Postiats/tree/master/contrib/ats2cpp
1 at 9:58 AM Hongwei Xi wrote:
>
>> 100%, I suppose :)
>>
>>
>> On Thu, Jan 21, 2021 at 12:57 PM Raoul Duke wrote:
>>
>>> To what degree are programs written in ATS expected to be portable
>>> across host languages?
>>>
>>> O
100%, I suppose :)
On Thu, Jan 21, 2021 at 12:57 PM Raoul Duke wrote:
> To what degree are programs written in ATS expected to be portable across
> host languages?
>
> On Thu, Jan 21, 2021 at 9:54 AM Hongwei Xi wrote:
>
>> Strictly speaking, ATS is an "abstract"
Strictly speaking, ATS is an "abstract" language; the language itself
does not have primitive data types. When compiled to C, it uses the
data types defined by C; when to JS, it uses the data types defined
by JS; etc.
On Thu, Jan 21, 2021 at 11:50 AM Raoul Duke wrote:
> $0.02
>
> In my
> > This time I would like to do something a bit more interesting:
> >
> > class
> > > , b:type>
> > mygpair(a, b)
> > *snip*
>
> Do we need to say both and (a,b)? It seems redundant,
> since we already know the class is parametrized according to a and b, but
> maybe I'm missing something?
>
> class mysamepair(a): mypair(a, a) {
> method swap(): void = ...
> }
>
I feel that this is a serious problem with typed OOP. Let me
give another example which I think no current OOP syntax can
handle.
Say we have an object of the type myrectangle(x, y), where
x and y are of the sort
Thanks, Mark!
I took a quick read.
Your description of various ATS2 features is accurate.
To be honest, I myself often forget how certain things are done in ATS2 and
have to use 'grep' to find code examples helping me figure out. For example,
I find the information in Part 5 particularly
Yes, I would like to see an example of this kind.
On Sat, Jan 2, 2021 at 9:19 PM d4v3y_5c0n3s wrote:
> So, I know that it's possible to pass a function to another function as a
> parameter, but what if I want to pass a function template specifically? If
> anyone would like some
This is an issue of the ATS2/Postiats compiler because it uses the absolute
path of a file
to create a name during compilation for the package stored in the file.
This is not a reliable
approach. Hopefully, something better can be used for ATS3. One possibility
is to just follow
what Java does.
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 poor design of mine. It is already abandoned in ATS3.
--Hongwei
On Wed, Dec 30, 2020 at 7:34 AM Dambaev Alexander
wrote:
> here is the repo of the minimum
>>Okay, so what you are saying is that in order for the code to compile, I
will need to implement the template for the given type.
That's right.
Hopefully, such a template can be automatically generated in ATS3 based on
the given (or inferred) type
information. There should be a substantial
It should not as arrayptr_freelin calls array_uninitize$clear to free all
the stored elements.
It is your obligation to implement the latter.
On Tue, Dec 15, 2020 at 9:54 AM d4v3y_5c0n3s wrote:
> I just have a question about using arrayptr_freelin() (which frees an
> arrayptr that contains
This behavior is intended.
In ATS, a fixity declaration like the following one has no effect
outside the module (that is, file) where it is declared:
infixl (+) +++
By the way, symintr is no longer needed in ATS2; it is not even
supported in ATS3.
On Sat, Nov 28, 2020 at 8:47 AM Dambaev
>>Would it still be better to include the effects in the source file,
If we look at a bigger picture, it may not even be practical to require
that this kind of information be stored
in the source. Today it is effect-tracking, and tomorrow it will surely be
something else. And there is only so
>>Can I guess that XATSCL0 is basically the same as the C-file that we have
now during compilation with patscc? Otherwise, what is the purpose of it?
Patscc generates code that contains goto statements. This time I would
exclude goto's in XATSCL0. In this way, compilers for ATS3 targeting other
>>What is the final vision for XATSCL0? Will it be compiled into c? Or
directly into native code (via custom backend, or llvm/similar)?
XATSCL0 should most likely be a subset of C.
To get into native code, one needs to remove function calls of C-style in
XATSCL0.
>>What is the effect on
I could only manage one write-up so far:
https://github.com/xanadu-lang/xats2js/tree/master/docgen/CodeBook/Hello
I plan to implement some word games to showcase this style of
co-programming.
Cheers!
On Sun, Nov 22, 2020 at 1:30 PM Hongwei Xi wrote:
> I will do a few examples today of
I will do a few examples today of co-programming with ATS3 and JS.
Conceptually, it is straightforward: ATS code is compiled to JS via xats2js
and the generated JS code can be directly combined with other JS code.
There is a very small library of JS code needed for running the generated
JS code.
FYI.
-- Forwarded message -
Hi,
It is my pleasure to announce the release
of ATS2-0.4.2. Note that this is the version
currently needed for compiling the ongoing
implementation of ATS3 (ATS/Xanadu).
ATS-Postiats-0.4.2.tgz:
The
The error message says that gint2uint is not implemented for the type uint8.
Of course, you can just implement it. Or you can just use the following
unsafe
approach to circumvent the issue:
#include "share/atspre_staload.hats"
#include "share/atspre_define.hats"
val
twelve =
$UNSAFE.cast(12):
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 difficult to locate constraint, that had been failed
> to be solved.
> For example, I got error message like this:
> ```
>
Thanks for reporting it.
Finally got some time fixing this issue. Basically, records were not
handled. They are now handled.
The changes should go into the next release.
On Wed, Oct 14, 2020 at 5:48 AM Dambaev Alexander
wrote:
> Hi,
> I have the following example:
> ```
> #include
The support for type inference in ATS2 is weak.
Often you need a type annotation for a case-expression
(or an if-expression):
implement main0() = {
val a = 0
val b =
(
case+ a of
| 0 => Some_vt(0) *(* 9 *)*
| _ => None_vt() *(* 10 *)*
) : Option_vt(int)
val () =
case+ b of
In this case, the long time compilation of your ATS code is most likely
caused
by constraint-solving. You may try to use the following flag to skip
constraint-solving:
--constraint-ignore
This will tell you if constraint-solving is indeed the culprit here.
Using an external constraint-solver
By the way, if 'i' is call-by-value, then it cannot be updated. If it needs
to be updated,
then it cannot be call-by-value.
On Sun, Oct 4, 2020 at 1:01 AM Hongwei Xi wrote:
> The following line caused the issue:
>
> val () = i := build( () | (len, offset, cap, i2sz 0, refcnt
The following line caused the issue:
val () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
dynamic, p)) // restore i
It should be changed to
prval () = i := build( () | (len, offset, cap, i2sz 0, refcnt + i2sz 1,
dynamic, p)) // restore i
Only a linear proof call-by-value
In the past, I did use ATS2 to experiment with a kernel implementation:
https://github.com/githwxi/ATS-Postiats-contrib/tree/master/projects/MEDIUM/KernelBuilding
Basically, you can just use some compile-time flags to get rid of various
includes in the generated
C code. The following Makefile
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 want to write a spec for a function 'append', which purpose is to append
> content of the second argument into the end of the
I just modified the code base to issue an error message in this case
(instead of just reporting a line number of with a compiler crash).
On Mon, Sep 28, 2020 at 7:36 AM Hongwei Xi wrote:
> >>I expected, that there will be typechecking error, saying, that buf_pf
> is being preserve
Yes, that is correct. Overloading resolution
only uses type erasures (that is, types without indices) and arity
information.
BTW.
In ATS2, template resolution uses dependent types (that is, types with
indices)
to select template implementation. This caused a nightmare in terms of
usability :(
In
Yes, you are correct.
An overload declaration in a package is available only when the package is
opened.
>>is it ok to have such 2 staloads or are there any other good practice to
staload only overloaded symbols? Maybe, there is a way to staload only some
of symbols (like in haskell's 'import'
It works because the type for sbuf_bcat allows it:
val () = sbuf_bcat{elf_thrmisc_t}(pf_thrmisc | addr_thrmisc) // fails
val () = sbuf_bcat{elf_thrmisc_t?}(pf_thrmisc | addr_thrmisc) // succeeds
On Wed, Sep 16, 2020 at 3:10 AM Kiwamu Okabe wrote:
> Dear all,
>
> I try to avoid following issue
>> fn add2 (x, y: int): int = x * x + y * y
ATS2 does very little of type-inference. Every argument of
a function needs to be given a type in principle.
On Mon, Sep 14, 2020 at 11:54 AM Timmy Jose wrote:
>
> Suppose I have this simple function:
>
> fn add1 (x: int, y: int): int = x * x +
The type-checker has quite a few limitations in handling existential
quantifiers.
Here is a way to circumvent the problem:
implement
mesh_delete( mpf, mpff | m ) =
let
val m1 = !m
in
arrayptr_free(m1.vap);
arrayptr_free(m1.tap);
ptr_free(mpff, mpf | m)
end
implement
*'#include' means copy/paste. It is not meant to be used*
*in the following manner:*
*```glib-ext.sats*
*#include "contrib/glib/SATS/glib.sats"#include
"contrib/glib/SATS/glib-object.sats" (* staloads glib.sats *)*
*```*
*You can create glib-ext.hats containing the following lines:*
This means that gpointer is declared more than once in your code.
You need to check various 'staload' declarations in your code.
On Sun, Aug 30, 2020 at 9:47 PM Dambaev Alexander
wrote:
> Hi
> Usually, I am able to parse and solve compiler errors, but now I need help:
>
> ```
> macdef
Well, you did not prove that the one returned is the same as the one
borrowed :)
On Sat, Aug 29, 2020 at 9:05 PM Kiwamu Okabe wrote:
> Dear Hongwei,
> thank you for your reply.
>
> On Sat, Aug 29, 2020 at 11:05 PM Hongwei Xi wrote:
> > In the following code, the proof of t
In the following code, the proof of the view associated with opts is
stored in inp.sh. This proof needs to be taken out and put back into
view@opts
before the function main0 can exit.
implement main0 () = let
var opts: ip6_pktopts
var inp: inpcb
val () = inp.in6p_outputopts :=
When I encounter a segfault, it is usually caused by recursion depth being
over some kind of limit.
In your code, the 'aux' function is defined but never called. Here is a
fixed version:
fun
{a: t@ype}
brauntest1 (t0: tree a): bool =
let exception Negative of ()
fun aux (t0: tree a):
The following header:
fn
linum (): void - void =
should be changed to
fn
linum (): () - void =
But this does not give what you expected.
You could use a reference:
fn
linum (): () - void=
let
val
line = ref(0)
in
lam () =>
let
val () = !line := !line + 1
in
println! ("Current line number =
Yes. But datatypes are nominal.
Often one uses abstract types to hide information. For example,
abst@ype Point2D
#extern
fun Point2D_get_x(Point2D): double
local
absimpl
Point2D = @{x=double,y=double}
in
implement Point2D_get_x(p) = p.x
end
On Sat, Aug 8, 2020 at 11:33 AM Timmy Jose
>>1. Will ATS3 syntax and semantics diverge significantly from ATS2? (It
looks like it's mostly going to be similar, but please correct me if I'm
wrong), and
The syntax of ATS3 is very similar to that of ATS2.
Here is some code in ATS3:
(a),
k0: a
) : bool =
case+ t0 of
| E () => false
| B (t1, k, t2) =>
let
val sgn =
gcompare_val_val(k0, k)
in
ifcase
| sgn < 0 => bstree_search (t1, k0)
| sgn > 0 => bstree_search (t2, k0)
| _ (* else *) => true
end
On Mon, Aug 3, 2020 at 10:43
There is a COMMA following 'false' that should be removed.
BTW, the syntax of ATS is heavily influenced by Standard ML.
On Mon, Aug 3, 2020 at 10:21 AM Timmy Jose wrote:
>
> Hello,
>
> I've been trying to learn ATS from the official tutorials, and while I
> like the language so far, and think
-- Forwarded message -
Hi,
It is my pleasure to announce the release
of ATS2-0.4.1. Note that this is the version needed
(or may be needed in the future) for compiling the
ongoing implementation of ATS3 (ATS/Xanadu).
I read some of your code in lib/string.dats. I suppose that you would soon
find that
handling structs can be a big challenge.
Even without using linear types, you could potentially find bugs involving
dereferencing
NULL pointers. For example, in the following code, pde_subdir_find
obviously
our 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:
>
>
> #include "share/atspre_define.hats
Forgot to mention that you need parentheses:
(a <= 5) * (b <= 5)
On Sat, Jul 25, 2020 at 10:55 PM Hongwei Xi wrote:
>
> Please use ifcase-expressions:
>
> fun
> foo
> {n:int}
> (n:int(n)): void =
> ifcase
> | n = 0 => () where {prval () = prop_verify{n =
Please use ifcase-expressions:
fun
foo
{n:int}
(n:int(n)): void =
ifcase
| n = 0 => () where {prval () = prop_verify{n == 0}()}
| n = 1 => () where {prval () = prop_verify{n == 1}()}
| _ (*else*) => () where {prval () = prop_verify{n != 0 && n != 1}()}
##
Also, you can use '+' and '*' for
at uses pointers
explicitly.
Obviously, you can replace C-strings with other forms of sequences.
On Sat, Jul 25, 2020 at 5:01 PM Matthias Wolff
wrote:
> Surprising answer, because I don't understand the details at the moment.
> It comes earlier than I expected. But I will take the cha
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.
On Sat,
>> #[m1:nat | m1 <= m] size_t(m1)
Note that the leading '#' is not needed in this case.
You could just use the shorthand 'sizeLte(m)' here.
On Sat, Jul 25, 2020 at 1:58 AM Dambaev Alexander
wrote:
> ah, looks like it is because of sort of return type:
> ```
> ): size_t(oidx) =
> ```
> I had
Here is a little doc on manually constructing values of a datatype:
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x2223.html
If you have a constructor of the name foo, then a type 'foo_pstruct' is
automatically introduced
(in the same namespace). You can study the generated
I made the function mat4_to_quat type-check. See the attached file.
One noticeable change is the type for the 'loop' function in your code:
fun loop {n,m:nat | 0 <= m+1; m+1 <= n} .. (m: int m, qs:
&(@[quat][n]), ws: &(@[float][n]), acc1: vec3) : vec3 = ...
Also, I modified
(mat4_at(m, j, j),
> Sent from my iPhone
>
> On 16 Jul 2020, at 19:01, Hongwei Xi wrote:
>
>
> * >> i := ((if mat4_at(m, 1, 1) > mat4_at(m, 0, 0) then 1 else i):int);*
> *>> i := ((if mat4_at(m, 2, 2) > mat4_at(m, $showtype(i), i) then 2 else
> i):int); // <-- this
* >> i := ((if mat4_at(m, 1, 1) > mat4_at(m, 0, 0) then 1 else i):int);*
*>> i := ((if mat4_at(m, 2, 2) > mat4_at(m, $showtype(i), i) then 2 else
i):int); // <-- this line has the error*
'i' is later used to index an array.
It seems that you just need:
i := ((if mat4_at(m, 1, 1) > mat4_at(m, 0,
Here is another possibility:
var raw = (recv_buf, recv_sz)
var tmp = (recv_buf_pf, view@raw | addr@ raw)
val _ = array_foreach_funenv( ..., tmp)
val (recv_buf_pf, raw_pf | _) = tmp
prval () = view@raw := raw_pf
On Fri, Jul 10, 2020 at 2:23 AM Hongwei Xi wrote:
> There are indeed two raw
There are indeed two raw_pf in this case.
Try this:
val (recv_buf_pf, raw_pf1 | _) = tmp
prval () = raw_pf := raw_pf1
On Fri, Jul 10, 2020 at 2:16 AM Dambaev Alexander
wrote:
> Hi,
>
> Thanks for your answers.
>
> For now, I had tried this:
>
> vtypedef VT = [l1:agz]
>
lement
main0() =
{
val
pow_2_10 =
$extfcall(uint, "lsl", 1, 10)
val () = println!("pow_2_10 = ", pow_2_10)
}
On Wed, Jul 8, 2020 at 10:56 AM Dambaev Alexander
wrote:
> Thanks, I will check it out
>
> ср, 8 июл. 2020 г. в 14:30, Hongwei Xi :
>
>> You can
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 ints, there
are asl (for <<) and asr (for >>).
In ATS2, there is no implicit
fun {n: nat | n > 0}{l: addr}
poll
should be changed to
fun poll{n: nat | n > 0}{l: addr}
Or you can write
fun poll{n:pos}{l: addr}
On Tue, Jul 7, 2020 at 3:31 AM Dambaev Alexander
wrote:
> Missed the return type of poll()
> ```
> fun {n: nat | n > 0}{l: addr}
> poll
> (
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 imitation of your code in ATS3:
#extern
fun
// N = n-i
dotprodN2
( i0: int(i)
, xs: array(a, n)
, ys: array(a, n)): a
(*
Thanks for the writing!
I feel that I have now acquired a pretty clear picture as to how C++
templates
are implemented. Not the details. Just the big picture. I will put into a
post what
I have learned and then outline what kind problem I am trying to address
with a
trait-like feature in ATS3. In
This is just my personal experience. It is difficult for me to
quantify it. My perspective is from my work on implementing
typed and untyped languages. I will say more elsewhere about
some lessons I learned.
My very point here is that we don't get to see a lot of bugs simply
because our bug
Thanks for these clarifying examples.
Now I think my guess is correct that C++ does *not *support embedded
template
implementations. Let me introduce an example to make my point.
Say we want pairs in our code. Traditionally, we declare a class(or struct)
in C++.
Then there will be a constructor
Thanks for your explanation.
I will start another thread to talk about variadic stuff.
On Fri, Jul 3, 2020 at 9:03 AM Matthias Wolff
wrote:
> C++ templates restricted to functions show only one half oft the truth.
>
> template
> struct function;
>
> struct XXX;
>
> template<>
> struct function
Thanks for clarifying.
In your example, there are three templates named g_print.
In particular, the types/interfaces of these three templates do
not have to be the instantiation of one general type/interface.
In ATS, we have one g_print:
fun g_print(x: a): void
And then three implementations:
emplate. In
ATS3, it can finally be properly done:
fun
tabulate(): list(a, n)
fun
tabulate$for{i:nat | i < n}(int(i)): a
Here is some running code that could clarify further:
https://github.com/xanadu-lang/xinterp/blob/master/TEST/prelude/array.dats
Cheers!
On Tue, Jun 30, 2020 at
Hi Artyom,
I will try to answer other questions later.
>>Why are ATS3 templates more powerful than C++ templates? Could you
contrast the two in some way?
I have to say that I do not use C++ on a regular basis.
C++ used to be C + classes + templates. By the way, I often jokingly tell
others this
1 - 100 of 310 matches
Mail list logo
