>> val () = (x := env)
My mistake. This would not work as 'x' is not a left-value.
Both (a) and (b) look like a reasonable way to get around this issue.
I would probably use (a).
On Mon, Feb 25, 2019 at 10:29 PM M88 <abysgr...@gmail.com> wrote:
>
>
> The following line is problematic:
>>
>> prval () = $effmask_all(x := env)
>>
>> as assignment is definitely not a proof.
>>
>
> This looked a bit off. I suppose in theory, one could wrap any function
> in $effmask_all and use it in proofs.
>
>
>
>> I suggest that you just do
>>
>> val () = x := env
>>
>> The compiler should allocate the same memory for both x and env.
>>
>
> in my case, this caused a C compilation error, "Invalid use of void
> expression." Perhaps it's because VT happened to be a file descriptor.
>
> I had supposed assignment was invalid for a call-by-value argument, but it
> would make more sense if "x" was a pointer. Would this end up being the
> equivalent of "(*x) = env" in C?
>
>
>> 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 :)
>>
>>
> I'd tend to agree :)
>
> Another dimension is that I would need to implement templates in terms of
> the data. My interface is currently in terms of VT, so it would likely
> require casting from within the template implementation (or, duplicating an
> interface in terms of some data type T). Since some functions might
> reference T in an unsafe way, it's probably the equivalent of casting.
>
> I gave it some thought, and the two best options appeared to be:
>
> a) Since my interface is in terms of VT, the simplest thing seemed to be
> this:
> var env = $UNSAFE.castvwtp1{VT}(x)
> val _ = some_template<VT>(env)
> prval () = $UNSAFE.cast2void(env)
>
> b) Supposing I want to keep things nice[ish], I could create an interface
> like this:
>
> absvt@ype VT0(x:id)
>
> castfn vt_take( !VT(x) >> VT0(x) ) -> VT(x)
>
> prfn vt_put( !VT0(x) >> VT(x), VT(x) ): void
>
> .....
> var env = vt_take(x)
> val _ = some_template<VT(x)>(env)
> prval () = vt_put( x, env )
>
> Version b seems pretty good for this case.
>
>
>
>> On Sun, Feb 24, 2019 at 2:52 AM M88 <abys...@gmail.com> 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.
>>> To post to this group, send email to ats-lan...@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/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/7b9e6024-d973-496e-b5b9-0c76835f3d4d%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/7b9e6024-d973-496e-b5b9-0c76835f3d4d%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/CAPPSPLq5WCWHvxYjTSXCMM0aRn_KjLdh6fY7xK%2B587pnUXYAmQ%40mail.gmail.com.
