Reducing duplication when assembling and disassembling views

[Shea Levy]

Hi all,

Some context: my errno project (relevant code at https://github.com/shlevy/elvysh-errno/blob/master/include/elvysh/errno.sats) introduces a view “errno_v” that ensures proper error checking: If a function takes an errno_v (free) and does not consume it or change its type, you know that it checks errno every time it is set. I’ve also added a convenience view “neg1_errno” for functions which return -1 when they set errno: neg1_errno is indexed by an int and is constructed from an errno_v (free) when the int is not -1 and from an errno_v (set) (which must then be checked) if the int is -1. Finally, “get_errno” can be used to check the value of errno and transform an errno_v (set) into an errno_v (free). Putting it all together, if bar is a function that sets errno if it returns -1 and foo is a function which takes and does not consume an errno_v(free), I’d *like* to write:

implement foo ( ev | (* void *) ) = let

  val res = bar ( ev )

in if res = ~1 then let

  prval neg1_errno_set ( ev ) = ev

  val res = get_errno ( ev )

in res end else let

  prval neg1_errno_free ( ev ) = ev

in 0 end end

But instead, I have to write:

implement foo ( ev | (* void *) ) = let

  val res = bar ( ev )

in if res = ~1 then let

  prval neg1_errno_set ( ev2 ) = ev

  val res = get_errno ( ev2 )

  prval _ = ev := ev2

in res end else let

  prval neg1_errno_free ( ev2 ) = ev

  prval _ = ev := ev2

in 0 end end

I think this might be because assigning to ‘ev’ in the pattern matching creates a *new* variable named ev instead of updating the existing one. Is there any way to rewrite this so that I don’t have to introduce the intermediate prval ev2?

Thanks,

Shea

[gmhwxi]

You could implement the following proof function:

prfun
un_neg1_errno_set (ev: !neg1_errno(~1) >> errno_v(set))

Then

>>prval neg1_errno_set ( ev ) = ev

changes into

prval () = un_neg1_errno_set(ev)

[Shea Levy]

Ah ha, thanks!

--
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 http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/30d6330e-b832-4ad4-ac6e-5edaa27fb87f%40googlegroups.com.