Modeled after ‘ptr_get_index’, I tried to write the following:
typedef offset ( count : int ) = [ off : nat | off < count ] size_t off
prfn offset_get_index { count : int } { off : nat | off < count } ( off :
size_t off ) : [ off’ : nat | off < count ] EQINT ( off, off’ ) =
eqint_make { off, off } ()
fn { size : int } foo ( off : offset size ) : void = let
prval [ off : int ] EQINT () = offset_get_index { size } ( off )
in () end
But the line where I call offset_get_index fails with a complaint that off
cannot be determined to be at least 0, despite that being ensured in its
type. Is there any way to do what I am aiming for here?
The actual function this came from takes an argument whose size depends on
the ‘size’ int. Doesn’t that mean it has to be a template argument to
compile?
On Monday, November 30, 2015 at 6:41:04 PM UTC-5, gmhwxi wrote:
This seems like a bug. I will investigate.
Still, it is a mistake to write ‘fn {size: int} foo …’; it should be
‘fn foo {size:int} …’.
Modeled after ‘ptr_get_index’, I tried to write the following:
typedef offset ( count : int ) = [ off : nat | off < count ] size_t off
prfn offset_get_index { count : int } { off : nat | off < count } ( off
: size_t off ) : [ off’ : nat | off < count ] EQINT ( off, off’ ) =
eqint_make { off, off } ()
fn { size : int } foo ( off : offset size ) : void = let
prval [ off : int ] EQINT () = offset_get_index { size } ( off )
in () end
But the line where I call offset_get_index fails with a complaint that
off cannot be determined to be at least 0, despite that being ensured in
its type. Is there any way to do what I am aiming for here?
Still, it is a mistake to write ‘fn {size: int} foo …’; it should be ‘fn
foo {size:int} …’.On Mon, Nov 30, 2015 at 5:48 PM, Shea Levy sh...@shealevy.com wrote:
Hi all,
Modeled after ‘ptr_get_index’, I tried to write the following:
typedef offset ( count : int ) = [ off : nat | off < count ] size_t off
prfn offset_get_index { count : int } { off : nat | off < count } ( off :
size_t off ) : [ off’ : nat | off < count ] EQINT ( off, off’ ) =
eqint_make { off, off } ()
fn { size : int } foo ( off : offset size ) : void = let
prval [ off : int ] EQINT () = offset_get_index { size } ( off )
in () end
But the line where I call offset_get_index fails with a complaint that off
cannot be determined to be at least 0, despite that being ensured in its
type. Is there any way to do what I am aiming for here?
The actual function this came from takes an argument whose size depends on
the ‘size’ int. Doesn’t that mean it has to be a template argument to
compile?On Monday, November 30, 2015 at 6:41:04 PM UTC-5, gmhwxi wrote:
This seems like a bug. I will investigate.
Still, it is a mistake to write ‘fn {size: int} foo …’; it should be ‘fn
foo {size:int} …’.
On Mon, Nov 30, 2015 at 5:48 PM, Shea Levy <sh...@shealevy.com <javascript:>> wrote:
Hi all,
Modeled after ‘ptr_get_index’, I tried to write the following:
typedef offset ( count : int ) = [ off : nat | off < count ] size_t off
prfn offset_get_index { count : int } { off : nat | off < count } ( off :
size_t off ) : [ off’ : nat | off < count ] EQINT ( off, off’ ) =
eqint_make { off, off } ()
fn { size : int } foo ( off : offset size ) : void = let
prval [ off : int ] EQINT () = offset_get_index { size } ( off )
in () end
But the line where I call offset_get_index fails with a complaint that
off cannot be determined to be at least 0, despite that being ensured in
its type. Is there any way to do what I am aiming for here?