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.
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 :)
On Sun, Feb 24, 2019 at 2:52 AM M88 <abysgr...@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-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/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/CAPPSPLoRY2BOhYJxY7x_W2h2-FR6M3Q047Zd%2BHRS3tfa64Mfow%40mail.gmail.com.
