Static integer multiplication

Google Group
1

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

2

//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)On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

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.On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@gmail.com <javascript:>

On Wed, May 14, 2014 at 9:13 PM, gmhwxi <gmh...@gmail.com <javascript:>>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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

4

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.comOn Thu, May 15, 2014 at 2:45 PM, gmhwxi gmh...@gmail.com wrote:

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 :slight_smile:

On Thursday, May 15, 2014 2:34:08 PM UTC-4, Brandon Barker wrote:

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
}

On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

OK, just wanted to verify, thanks.

Brandon Barker
brandon…@gmail.comOn 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-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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

6

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
}On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

7

I think this is what you need:

praxi
m_times_n_Gte0
{m,n:nat}
(m: int (m), n: int (n)): [m*n >= 0] voidOn Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

8

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 :)On Thursday, May 15, 2014 2:34:08 PM UTC-4, Brandon Barker wrote:

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
}

On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

9

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.comOn Thu, May 15, 2014 at 1:18 PM, gmhwxi gmh...@gmail.com wrote:

//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)

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.com?utm_medium=email&utm_source=footer
.

10

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.comOn Thu, May 15, 2014 at 3:01 PM, gmhwxi gmh...@gmail.com wrote:

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 :slight_smile:

On Thursday, May 15, 2014 2:45:49 PM UTC-4, gmhwxi wrote:

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 :slight_smile:

On Thursday, May 15, 2014 2:34:08 PM UTC-4, Brandon Barker wrote:

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
}

On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.com?utm_medium=email&utm_source=footer
.

11

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)

  1. 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.On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

12

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 :)On Thursday, May 15, 2014 2:45:49 PM UTC-4, gmhwxi wrote:

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 :slight_smile:

On Thursday, May 15, 2014 2:34:08 PM UTC-4, Brandon Barker wrote:

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
}

On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

13

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) *)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)))

14

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

15

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.comOn Thu, May 15, 2014 at 2:34 PM, Brandon Barker brandon...@gmail.comwrote:

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
}

On Thursday, May 15, 2014 2:33:15 PM UTC-4, Brandon Barker wrote:

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

On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.com?utm_medium=email&utm_source=footer
.

16

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).On Thursday, May 15, 2014 1:23:55 PM UTC-4, gmhwxi wrote:

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

On Thursday, May 15, 2014 12:35:48 PM UTC-4, Brandon Barker wrote:

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)

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

On Thursday, May 15, 2014 12:00:38 PM UTC-4, gmhwxi wrote:

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.

On Thursday, May 15, 2014 11:38:44 AM UTC-4, Brandon Barker wrote:

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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
brand...@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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.

17

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 herehttps://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d
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-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.comhttps://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer
.