Hi, M88 and Hongwei,
On Sunday, February 24, 2019 at 5:45:34 PM UTC+2, gmhwxi wrote:
>
> The following line is problematic:
>
> prval () = $effmask_all(x := env)
>
> as assignment is definitely not a proof.
>
> I suggest that you just do
>
> val () = x := env
>
> The compiler should allocate the same memory for both x and env.
>
Flat viewtypes are represented by plain C structs in ATS, that is, they are
directly copyable. I think this should give the C compiler a hint.
> Theoretically, you could separate x into two parts: data and (linear)
> proof;
> only move the data into env; there is no need to move the data back from
> env
> into x since the data is non-linear. Really not worth the trouble :)
>
In practice, records are really tough to handle this way (especially the
initialization and free -- casts galore! :)).
>
>
> On Sun, Feb 24, 2019 at 2:52 AM M88 <abys...@gmail.com <javascript:>>
> wrote:
>
>> Hello,
>>
>> I have a viewtype and I am using it in a call-by-value function. I want
>> to temporarily assign it to a variable for use in a template that uses
>> call-by-reference.
>>
>> Is there a way to assert that the variable has not been consumed?
>>
>> Right now I am doing this, which typechecks and compiles in my case:
>>
>> extern fun {env}
>> some_template( env : &env >> _ ) : void
>>
>> fun f ( x: !VT) : void =
>> let
>> var env = x
>> val _ = some_template<VT>(env)
>> prval () = $effmask_all(
>> x := env
>> )
>> in
>> end
>>
>> Is this expected behavior? Is it possible to write a proof function that
>> can restore "x"?
>>
>> ( Ultimately, x does not change, and the semantics of call-by-value seem
>> best for this function ).
>>
>>
>>
>>
>>
>> --
>> 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 <javascript:>.
>> To post to this group, send email to ats-lan...@googlegroups.com
>> <javascript:>.
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/ats-lang-users/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/ce57d10d-cb0a-465f-b9f6-954d7d6678cb%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>
--
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 post to this group, send email to ats-lang-users@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/47a5462b-c081-4b1b-a5d3-c135b96b2eec%40googlegroups.com.
