Is `:=` a built in operator? (fwd)

Google Group
1

I have moved the discussion to the google-group for ats-lang-users.

A linear proof variable is a left-value (of size 0). So the following code
means to store parray_v_cons (pf1, pf2) into pf:

pf := parray_v_cons (pf1, pf2)

Of course, this is allowed only if there is no linear proof currently
stored in pf.On Wed, Aug 27, 2014 at 9:28 AM, Hongwei Xi hw...@bu.edu wrote:

---------- Forwarded message ----------
Date: Wed, 27 Aug 2014 19:42:05 +0900
From: Kiwamu Okabe kiw...@debian.or.jp
To: ats-lang-users ats-lan...@lists.sourceforge.net
Subject: Re: [ats-lang-users] Is := a built in operator?

Hi,

On Wed, Aug 27, 2014 at 1:47 AM, Brandon Barker brandon...@gmail.com wrote:

I believe that it should be since var updates require it, e.g.,

var x: int
val () = x := 7

Thank’s! I explained it at
Built in operators · githwxi/ATS-Postiats Wiki · GitHub.
However, := is sometimes used for static value.

implement{a}
parray_size (pf | p) = let
  prval () = lemma_parray_v_params (pf)
  fun loop
    {l:addr}{i,j:nat} .<i>. (
    pf: !parray_v (a, l, i) | p: ptr l, j: size_t j
  ) :<> size_t (i+j) = let
    val isnemp = parray_isnot_empty<a> (pf | p)
  in
    if isnemp then let
      prval parray_v_cons (pf1, pf2) = pf
      val n = loop (pf2 | p+sizeof<a>, j+1)
      prval () = pf := parray_v_cons (pf1, pf2)

I will write more information, if I know static value assignment.

Thank’s,

Kiwamu Okabe at METASEPI DESIGN

Slashdot TV.
Video for Nerds. Stuff that matters.
http://tv.slashdot.org/

ats-lang-users mailing list
ats-lan...@lists.sourceforge.net
ats-lang-users List Signup and Options

2

There are many forms of left-values in ATS:

variables, dereferenced pointers, dreferenced references, field selection,
array subscripting, named linear proof values, etc. For each form, you can
write:

left-value := expOn Thursday, August 28, 2014 3:34:56 AM UTC-4, Kiwamu Okabe wrote:

Hi Hongwei,

On Wed, Aug 27, 2014 at 10:33 PM, Hongwei Xi <gmh...@gmail.com <javascript:>> wrote:

A linear proof variable is a left-value (of size 0). So the following
code
means to store parray_v_cons (pf1, pf2) into pf:

pf := parray_v_cons (pf1, pf2)

Of course, this is allowed only if there is no linear proof currently
stored
in pf.

Umm… := has following three meanings?

  1. Assign new value to a dynamic variable (var) that has the old value.
  2. Assign new value to dereferenced (left-value) pointer with valid
    linear proof.
  3. Assign new static value (linear proof) to an uninitialized or empty
    (consumed?) variable.

Thank’s,

Kiwamu Okabe at METASEPI DESIGN