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 <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/7b9e6024-d973-496e-b5b9-0c76835f3d4d%40googlegroups.com.
