Extracting the existentially-bound variables of an existentially quantified type?

[Shea Levy]

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?

Thanks,

Shea

[Hongwei Xi]

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} ...'.

--
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/146bc984-bd81-4ede-8ee7-829f872de894%40googlegroups.com.

[Shea Levy]

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?

[Hongwei Xi]

Implementing such a function is more involved. See:

https://groups.google.com/forum/#!searchin/ats-lang-users/typeval/ats-lang-users/4p37nbLeNm8/iF9P8f5ONvcJ

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/64b69c6f-0d19-4265-a059-1f54b16b352b%40googlegroups.com.