Some context: my errno project (relevant code at https://github.com/shlevy/elvysh-errno/blob/master/include/elvysh/errno.satshttps://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?
On Wednesday, March 18, 2015 at 3:33:46 PM UTC-4, Shea Levy wrote:
Hi all,
Some context: my errno project (relevant code at https://github.com/shlevy/elvysh-errno/blob/master/include/elvysh/errno.satshttps://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?
prval () = un_neg1_errno_set(ev)On Wednesday, March 18, 2015 at 3:33:46 PM UTC-4, Shea Levy wrote:
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?