var … with pf

[Yannick Duchêne]

During testings about ATS2 syntax, I found this in one of the sample files I use for the tests:

        var y: int with pfy // pfy is an alias of view@ (y): int? @ y

        val () = y := 2 // pfy = view@ (y): int(2) @ y

        var z: int with pfz = 3 // pfz is an alias of view@ (z): int(3) @ z

It says `var … with pf`, I’ve never seen this before. Usually, we see something like `val (pf | a) = f()`. Is this because it’s `var` instead of `val` or does it create a association of a special kind?

[Chris Double]

I believe it's syntactic sugar for something like:

var y: int
prval pfy = view@ y

It introduces a proof variable providing access to the memory location
of the var.

--
https://bluishcoder.co.nz

[Yannick Duchêne]

Thanks,

So this would indeed be two separate declarations as I suspected.

[Artyom Shalkhakov]

It may actually stand for three declarations! There is also the implicit declaration of a static variable of the same name.

There is also something like:

var x with pf_x = 0

Which stands for something like this:

var x : int

val () = x := 0

prval pf_x = view@ x

prval [x:addr] EQADDR () = ... // <== this

пн, 23 июл. 2018 г. в 8:23, 'Yannick Duchêne' via ats-lang-users <ats-lan...@googlegroups.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-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/ebb39525-cf09-44d8-a155-a87160b87b04%40googlegroups.com.

--

Cheers,
Artyom Shalkhakov