Cast a dependent type

Google Group
1

I’d like to do something like the following, but in the version of the cast
assignment that specifies the type of the lvalue or rvalue, for some reason
this doesn’t work. This just worried me a bit, as I’m unsure why there
should be a difference

(* ****** ****** )
//
#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"
//
( ****** ****** *)

staload UN = “prelude/SATS/unsafe.sats”

(* ****** ****** *)

abstype board_point_type = ptr
typedef board_point = board_point_type

(* ****** ****** *)

assume
board_point_type = [m,n: nat| m >= 3; n >= 3]
’(intBtwe(0, m), intBtwe(0, n))

implement main0 () = {

val my_zero = g1ofg0(0)

val test0 = '(my_zero, my_zero)
val _ = $showtype test0
typedef testtype = '(int, int)

// this works
val test = $UN.cast{board_point}{testtype}(’(my_zero, my_zero))
val _ = $showtype test

// this doesn’t
val test = ($UN.cast{board_point}{testtype}(’(my_zero, my_zero)))
:board_point
val _ = $showtype test

// this doesn’t
val test: board_point = $UN.cast{board_point}{testtype}(’(my_zero, my_zero))

val () = println!(“testing”)
}

2

That is right. Support for equality on dependent types is very limited.On Monday, May 19, 2014 5:26:53 PM UTC-4, Brandon Barker wrote:

I’d like to do something like the following, but in the version of the
cast assignment that specifies the type of the lvalue or rvalue, for some
reason this doesn’t work. This just worried me a bit, as I’m unsure why
there should be a difference

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
( ****** ****** *)

staload UN = “prelude/SATS/unsafe.sats”

(* ****** ****** *)

abstype board_point_type = ptr
typedef board_point = board_point_type

(* ****** ****** *)

assume
board_point_type = [m,n: nat| m >= 3; n >= 3]
'(intBtwe(0, m), intBtwe(0, n))

implement main0 () = {

val my_zero = g1ofg0(0)

val test0 = '(my_zero, my_zero)
val _ = $showtype test0
typedef testtype = '(int, int)

// this works
val test = $UN.cast{board_point}{testtype}('(my_zero, my_zero))
val _ = $showtype test

// this doesn’t
val test = ($UN.cast{board_point}{testtype}('(my_zero, my_zero)))
:board_point
val _ = $showtype test

// this doesn’t
val test: board_point = $UN.cast{board_point}{testtype}('(my_zero,
my_zero))

val () = println!(“testing”)
}

3

I see … sorta. I should read more about the solver.
Brandon Barker
brandon…@gmail.comOn Mon, May 19, 2014 at 6:54 PM, gmhwxi gmh...@gmail.com wrote:

That is right. Support for equality on dependent types is very limited.

On Monday, May 19, 2014 5:26:53 PM UTC-4, Brandon Barker wrote:

I’d like to do something like the following, but in the version of the
cast assignment that specifies the type of the lvalue or rvalue, for some
reason this doesn’t work. This just worried me a bit, as I’m unsure why
there should be a difference

(* ****** ****** )
//
#include
“share/atspre_define.hats”
#include
“share/atspre_staload.hats”
//
( ****** ****** *)

staload UN = “prelude/SATS/unsafe.sats”

(* ****** ****** *)

abstype board_point_type = ptr
typedef board_point = board_point_type

(* ****** ****** *)

assume
board_point_type = [m,n: nat| m >= 3; n >= 3]
'(intBtwe(0, m), intBtwe(0, n))

implement main0 () = {

val my_zero = g1ofg0(0)

val test0 = '(my_zero, my_zero)
val _ = $showtype test0
typedef testtype = '(int, int)

// this works
val test = $UN.cast{board_point}{testtype}('(my_zero, my_zero))
val _ = $showtype test

// this doesn’t
val test = ($UN.cast{board_point}{testtype}('(my_zero,
my_zero))):board_point
val _ = $showtype test

// this doesn’t
val test: board_point = $UN.cast{board_point}{testtype}('(my_zero,
my_zero))

val () = println!(“testing”)
}

–
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/9da46f38-0837-4f2d-9ddb-c2d6e2e6fa90%40googlegroups.com.