cast a dependent type

[Brandon Barker]

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")
}

[gmhwxi]

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

[Brandon Barker]

I see ... sorta. I should read more about the solver.
Brandon Barker
brandon...@gmail.com

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