static integer multiplication

[Brandon Barker]

I seem to recall that integer multiplication can be handled by the solver, but ..

//m, n are of type: [i:nat] int (i)


// This works
val mn_i = m * n
val () = assertloc(mn_i > 0)
val mn = i2sz(mn_i)


// This doesn't work
val () = assertloc(m > 2)
val () = assertloc(n > 2)
val mn = i2sz(m * n)

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(3769->S2Eapp(S2Ecst(mul_int_int); S2EVar(3767->S2Evar(n$6252(11369))), S2EVar(3768->S2Evar(n$6253(11370))))), S2Eintinf(0)))

[Brandon Barker]

Here's a complete minimal working example:

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


extern
fun myCharFun(): char


typedef myInt = [i:nat] int (i)


typedef Point = @{m = myInt, n = myInt}




val mc = myCharFun()
val nc = myCharFun()


val m_in = g1ofg0_int(char2i(mc))
val n_in = g1ofg0_int(char2i(nc))


var data: Point?
val () = data.m := m_in
val () = data.n := n_in


// This works
val mn_i = data.m * data.n
val () = assertloc(mn_i > 0)

val mn = i2sz(mn_i)




// This doesn't work

(* val () = assertloc(data.m > 2) *)
(* val () = assertloc(data.n > 2) *)
(* val mn = i2sz(data.m * data.n) *)

[gmhwxi]

only equalities (no inequalities) involving multiplication can be handled
(in a very limited way).

On Wednesday, May 14, 2014 7:34:57 PM UTC-4, Brandon Barker wrote:

[Brandon Barker]

OK, just wanted to verify, thanks.

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com.

[Brandon Barker]

I introduced a praxi which seemed to work in the above test case (praxi should be relatively easy to use, so I thought I'd try it, even though e.g. assertloc would be fine here):

extern
praxi
m_times_n_Gt0
  {m,n,mn:int | m > 0; n > 0; mn == m*n}
  (m: int (m), n: int (n), mn: int(mn)): [mn > 0] void




val () = assertloc(m_in > 2)
val () = assertloc(n_in > 2)
val mn_j = data.m * data.n
prval mn_iGt0pf = m_times_n_Gt0(m_in, n_in, mn_j)

However, it doesn't seem to work in another example that wraps some of the assignments in a function call (see use of same castfn here
in game.dats & game.sats). 

On Wednesday, May 14, 2014 9:14:47 PM UTC-4, Brandon Barker wrote:

OK, just wanted to verify, thanks.

Brandon Barker
brandon...@gmail.com

On Wed, May 14, 2014 at 9:13 PM, gmhwxi <gmh...@gmail.com> wrote:

only equalities (no inequalities) involving multiplication can be handled
(in a very limited way).

On Wednesday, May 14, 2014 7:34:57 PM UTC-4, Brandon Barker wrote:

I seem to recall that integer multiplication can be handled by the solver, but ..

//m, n are of type: [i:nat] int (i)


// This works
val mn_i = m * n
val () = assertloc(mn_i > 0)
val mn = i2sz(mn_i)


// This doesn't work
val () = assertloc(m > 2)
val () = assertloc(n > 2)
val mn = i2sz(m * n)

error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(>=); S2EVar(3769->S2Eapp(S2Ecst(mul_int_int); S2EVar(3767->S2Evar(n$6252(11369))), S2EVar(3768->S2Evar(n$6253(11370))))), S2Eintinf(0)))

--
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-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

[gmhwxi]

Say you have two occurrences of board.m and board.m.
The typechecker does NOT know these two occurrences have the same type. Try

val board_m = board.m

and replace the other occurrence with board_m.

Brandon Barker
brandon...@gmail.com

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.

[Brandon Barker]

If I understand correctly, this actually requires additional dynamic checking (assertlocs on board_m and board_n after the functional call that initializes board.m and board.n). 

//This does work
val () = boardSetup(board_conf)


val m = board_conf.m
val n = board_conf.n

//But if I comment these out, it doesn't work

val () = assertloc(m > 2)
val () = assertloc(n > 2)

val mn_i = m * n

prval mnGt0pf = m_times_n_Gt0(m, n, mn_i)

val mn = i2sz(mn_i)

I'm a bit confused about why the test case works and the other case doesn't:

1) there are multiple occurrences of data.m in a variant of the test case, and it works:

local

val () = assertloc(data.m > 2)

val () = assertloc(data.n > 2)

in end

val mn_j = data.m * data.

n
prval mn_iGt0pf = m_times_n_Gt0(data.m, data.n, mn_j)

2) Scope does not seem to be the issue, since even if I do this, it doesn't work:

// Didn't work
val () = assertloc(board_conf.m > 2)
val () = assertloc(board_conf.n > 2)
val mn_i = board_conf.m * board_conf.n
prval mnGt0pf = m_times_n_Gt0(board_conf.m, board_conf.n, mn_i)

3) I wasn't sure if you were suggesting it is a problem with record types, given (1), but (2) and the solution suggests it may be a combination of scope and record types.

So the typechecker seems unable to track the type of some values (if I understand correctly) - it would be good to know under what conditions that would be.

[gmhwxi]

>> //But if I comment these out, it doesn't work



It should not work. Both m and n are natural numbers,
which implies that they may be zeros. The compiler cannot
prove that the product of two natural numbers is positive.


//This does work
val () = boardSetup(board_conf)

val m = board_conf.m
val n = board_conf.n

//But if I comment these out, it doesn't work

val () = assertloc(m > 2)
val () = assertloc(n > 2)
val mn_i = m * n

prval mnGt0pf = m_times_n_Gt0(m, n, mn_i)

val mn = i2sz(mn_i)

[gmhwxi]

I think this is what you need:

praxi
m_times_n_Gte0
  {m,n:nat} 
  (m: int (m), n: int (n)): [m*n >= 0] void

[Brandon Barker]

I agree in principle, was just annotating this, since in the function I have another assertloc (well, ckastloc_gintGte) call that does the same thing.

Brandon Barker
brandon...@gmail.com

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.com.

[Brandon Barker]

Thanks, but your comment about the natural numbers made me realize that the assertlocs weren't doing exactly what I thought they were doing. I changed my record type to be:

And I had the following result with my original praxi:

//
// Get user input and configure board
//
val () = boardSetup(board_conf)


// Works:

val m = board_conf.m
val n = board_conf.

n
val mn_i = m * n
prval mnGt0pf = m_times_n_Gt0(m, n, mn_i)


(* // Doesn't work: *)
(* val mn_i = board_conf.m * board_conf.n *)
(* prval mnGt0pf = m_times_n_Gt0(board_conf.m, board_conf.n, mn_i) *)


val mn = i2sz(mn_i)

This makes me thin that there is something funny going on related to record types (funny to me at least).

[Brandon Barker]

Forgot to paste my record type =(:

typedef board_conf_type =

@{

, m = [m:int | m > 2] int (m)

, n = [n:int | n > 2] int (n)

, k = [k: int| k > 2] int (k)

, cursor = board_point

, num_players = int

, player_turn = int

}

[Brandon Barker]

I may now understand your original point:  board.m has a type, but if I assign it to a new variable:

m = board.m

the dependent type of 'm' may be altered somewhat based on the context. I.e., it is no longer the type defined in the record type (just any natural number)

[m:nat] int (m) // my original definition

but it is now more concretely  "int (m)" for some m. 

Brandon Barker
brandon...@gmail.com

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.com.

[gmhwxi]

I think the the main reason for dependent types being difficult is due to
the complexity involved in handling quantifiers. If you use the following
definition, then your problem should be gone:

typedef
board_conf_type = [m,n,k:int | m > 2; n > 2; k > 2]

@{

, m = int (m)

, n = int (n)

, k = int (k)

, cursor = board_point

, num_players = int

, player_turn = int

}

Studying mathematical logic can be very helpful as a very big part of math. logic is about handling quantifiers.
I can say this because I was majored in math. logic :)

[gmhwxi]

BTW, I looked at your code. As of now, it is a bit too "sequential".
Since I have just done APIs for libevent and libev, I am thinking
about using these libraries to re-write your code. Have to say that
I don't really know how to use these libraries yet :)

[Brandon Barker]

I have studied a very little quantification, and it may be naive to say that I think it is enough (I'm sure I could use more), but I think my problem with dependent types up to now largely stems more from trying to understand what quantifiers are currently being applied to the given variables.

I should have used $showtype much earlier ...

Brandon Barker
brandon...@gmail.com

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.com.

[Brandon Barker]

I am happy for you to do so - I have just been doing this for fun and learning, and I'm sure I'll learn at least an equal amount by reading your code. I hope my c-prototype code is at least clear.

Brandon Barker
brandon...@gmail.com

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.com.