Re: symintr and staload

[Dambaev Alexander]

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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzFqjjOd4g921wEbwoa-6gAt4wByfJPOF7z9OwF5B6%3Drw%40mail.gmail.com.

Re: performance considerations of patsopt

[Dambaev Alexander]

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 type (after the first simplification of
constraints) was:
```
fn
appendC
{l_len, l_offset, l_cap, l_ucap: nat}{l_dynamic:bool}{l_p:addr}
{r_len, r_offset, r_cap, r_ucap: nat}{r_dynamic:bool}{r_p:addr}
( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, 0, l_dynamic, l_p)
, r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
):
[offset, cap, ucap: nat | (l_len > 0 || r_len > 0) && (cap > 0)]
[l:addr | l > null]
[dynamic:bool]
[l:addr | (l_len > 0 || r_len > 0) && l > null]
Bytestring_vtype( l_len+r_len, offset, cap, ucap, 0, dynamic, l)

overload + with appendC
```
which means, that in different cases the result will be different, so I had
decided to have 2 separate functions:
1. for creating new buffer
```
fn
  appendC
  {l_len, l_offset, l_cap, l_ucap: nat | *l_len > 0*}{l_dynamic:bool}
*{l_p:agz*}
  {r_len, r_offset, r_cap, r_ucap: nat | *r_len > 0*}{r_dynamic:bool}{
*r_p:agz*}
  ( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, 0, l_dynamic, l_p)
  , r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
  ):
  *[l:addr | l > null]*
  Bytestring_vtype( l_len+r_len, 0, l_len+r_len, 0, 0, true, *l*)

overload + with appendC

```
2. for filling unused parts of buffer
```
(* O(r_len)
 this function appends 'r' at the end of 'l''s unused buffer.
 See test17 for example of usage.\
 this usage does not perform allocation, but does consumes 'r', so it will
call 'free' in case if 'r' had been dynamically allocated.
 *)
fn
  growC
  {r_len, r_offset, r_cap, r_ucap, l_refcnt: nat | *r_len > 0*
}{r_dynamic:bool}{*r_p:agz*}
  {l_len, l_offset, l_cap, l_ucap: nat | *l_ucap >= r_len*
}{l_dynamic:bool}{*l_p:agz*}
  ( l: Bytestring_vtype(l_len, l_offset, l_cap, l_ucap, l_refcnt,
l_dynamic, l_p)
  , r: Bytestring_vtype(r_len, r_offset, r_cap, r_ucap, 0, r_dynamic, r_p)
  ):
  Bytestring_vtype( l_len+r_len, l_offset, l_cap, l_ucap - r_len, l_refcnt,
l_dynamic, l_p)

symintr ++
infixl (+) ++
overload ++ with growC
```
so by limiting the usage cases and splitting 1 function on 2, I was able to
get rid of excessive constraints on output and now I get reasonable
compilation time of user's code. Plus the caller now is able to explicitly
choose the behavior of appending: either to create new buffer or use unused
part of some existing buffer.

-- 
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 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2Kwv3HCUr8hPvM92OnMvBXib1YXsrURtqB7nPkOp4FCDHQ%40mail.gmail.com.

Re: symintr and staload

[Hongwei Xi]

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 Alexander 
wrote:

> 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 ATS_DYNLOADFLAG 0
>
> (* if I uncomment those lines before staload, then main.dats will be
> compiled as expected. Otherwise, patscc will say, that it is unable to
> resolve +++
> symintr +++
> infixl (+) +++
> *)
> staload "file1.sats"
>
> implement main0() = println!( "1 +++ 2 = ", 1 +++ 2)
> ```
>
> I found a walkaround by introducing symbol and it's precedence before
> staload, but it seems like a bug for me
>
> --
> 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
> https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzsVTfFbMm_VX9vzvE-aPGem1eqVyDR2DCkXh-AAypF%2Bw%40mail.gmail.com
> 
> .
>

-- 
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 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLp2NFK5DyJ5DALefCec5Z6gpdoB3TM_T5Ep4mJLgoZgkw%40mail.gmail.com.

symintr and staload

[Dambaev Alexander]

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 ATS_DYNLOADFLAG 0

(* if I uncomment those lines before staload, then main.dats will be
compiled as expected. Otherwise, patscc will say, that it is unable to
resolve +++
symintr +++
infixl (+) +++
*)
staload "file1.sats"

implement main0() = println!( "1 +++ 2 = ", 1 +++ 2)
```

I found a walkaround by introducing symbol and it's precedence before
staload, but it seems like a bug for me

-- 
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 
https://groups.google.com/d/msgid/ats-lang-users/CAHjn2KzsVTfFbMm_VX9vzvE-aPGem1eqVyDR2DCkXh-AAypF%2Bw%40mail.gmail.com.