Why won't this code compile?

[Mark Thom]

Hi,

I've been reading the "Introduction to Programming in ATS" book over the past few months, and I still have no clue as to why this program won't compile:

fn{a:t@ype} ptr_set0 {l:addr} (pf: !a? @ l | p: ptr l, v: a): void =
  !p := v

implement main0 () = let
  var v: int = 5
in
  ( let prval pf = view@(v) in
      ptr_set0(pf | addr@(v), 3) ;
      // !addr@(v) := 3; // uncommenting this line causes the program to compile. no idea why.   
    end ;
    println!("v = ", v)   
  )
end

I know that pf is a linear resource, and it needs to be consumed somehow.. how do I make it happen?

If I don't touch v after the call to ptr_set0 (ie. if I remove the final println!), the program will compile.. which also makes

no sense given what I think I know about linear resources in ATS.

Thanks.

[Chris Double]

On Wed, Nov 7, 2018 at 9:17 AM Mark Thom <markjor...@gmail.com> wrote:

> I know that pf is a linear resource, and it needs to be consumed somehow.. how do I make it happen?
> If I don't touch v after the call to ptr_set0 (ie. if I remove the final println!), the program will compile.. which also makes
> no sense given what I think I know about linear resources in ATS.

The line that assigns the view@ to 'pf' is borrowing the view and
assigning it to 'pf'. It needs to be "given back", which both consumes
the proof (the 'pf') and restores the 'view@':

var v: int = 5

prval pf = view@(v)
val _ = ptr_set0(pf | addr@(v), 3)
prval () = view@(v) := pf

This idiom was used a lot in ATS1 and I think ATS2 made it so in some
cases it wasn't needed. After changing this I hit an issue with
overloading in println:

the symbol [print] cannot be resolved due to too many matches:
D2ITMcst(print_option) of 0
D2ITMcst(print_list_vt) of 0

This seems to be something to do with the type that ATS has assigned
to 'v' being changed after the proof usage. I cheated by using
'cast2int(v)' from unsafe.sats to get it to compile but hopefully
someone knows a better way.

--
http://bluishcoder.co.nz

[Hongwei Xi]

The type for ptr_set0 should be changed to the following one:

fn
{a:t@ype}
ptr_set0{l:addr}

(pf: !a? @ l >> a @ l | p: ptr l, v: a): void =
  !p := v

Then all you need is to provide a template argument explicitly: ptr_set0<int>

--
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/CALn1vHHh9mLBS22Of-8mqJoP%2Bp4K6ExCNtDvaP3YNiK6Oo8xTg%40mail.gmail.com.