# Static integer multiplication

**URL:** <https://discourse.ats-lang.org/t/static-integer-multiplication/700>\
**Category:** Google Group\
**Created:** [May 14, 2014, 11:34pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700 "2014-05-14T23:34:57Z")\
**Posts on this page:** 17\
**Page:** 1

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 14, 2014, 11:34pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/1 "2014-05-14T23:34:57Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 5:18pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/2 "2014-05-15T17:18:43Z")

</div>

> > //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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > 
> > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 4:00pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/3 "2014-05-15T16:00:38Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com) \<javascript:\>
> > 
> > On Wed, May 14, 2014 at 9:13 PM, gmhwxi \<[gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com) \<javascript:\>.  
> > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 7:01pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/4 "2014-05-15T19:01:16Z")

</div>

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](mailto: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 🙂
> 
> 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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > > > 
> > > > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > > > > > > > > To view this discussion on the web visit  
> > > > > > > > > > [https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-)  
> > > > > > > > > > 17e2-4f32-ace7-683c7d5b0ea6%[40googlegroups.com](http://40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://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](mailto:ats-lang-user...@googlegroups.com).  
> > > > > > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/5975a385-0ea3-446f-a1bf-9e408b32177c%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 1:14am UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/5 "2014-05-15T01:14:47Z")

</div>

OK, just wanted to verify, thanks.

Brandon Barker  
brandon…@gmail.comOn Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang-user...@googlegroups.com).  
> > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 6:34pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/6 "2014-05-15T18:34:08Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > 
> > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 5:23pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/7 "2014-05-15T17:23:55Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > 
> > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 6:45pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/8 "2014-05-15T18:45:49Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > > 
> > > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 6:11pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/9 "2014-05-15T18:11:15Z")

</div>

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](mailto: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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > 
> > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > > > > > To view this discussion on the web visit [https://groups.google.com/d/](https://groups.google.com/d/)  
> > > > > > > msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%  
> > > > > > > [40googlegroups.com](http://40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://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](mailto:ats-lang-user...@googlegroups.com).  
> > > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/b9ea779c-1847-4d48-a55d-03d15a7d55f3%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 7:05pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/10 "2014-05-15T19:05:19Z")

</div>

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](mailto: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 🙂
> 
> 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 🙂
> > 
> > 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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > > > > 
> > > > > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > > > > > > > > > To view this discussion on the web visit  
> > > > > > > > > > > [https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-)  
> > > > > > > > > > > 17e2-4f32-ace7-683c7d5b0ea6%[40googlegroups.com](http://40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://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](mailto:ats-lang-user...@googlegroups.com).  
> > > > > > > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/baa45331-24e5-4091-a4c4-9ad7f7545660%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 4:35pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/11 "2014-05-15T16:35:48Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > 
> > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > .

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 7:01pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/12 "2014-05-15T19:01:18Z")

</div>

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 🙂
> 
> 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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > > > 
> > > > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 14, 2014, 11:59pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/13 "2014-05-14T23:59:09Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [May 15, 2014, 1:13am UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/14 "2014-05-15T01:13:00Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 6:44pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/15 "2014-05-15T18:44:25Z")

</div>

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.com](mailto:brandon...@gmail.com)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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > > > 
> > > > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto:ats-l...@googlegroups.com).  
> > > > > > > > > To view this discussion on the web visit  
> > > > > > > > > [https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-)  
> > > > > > > > > 17e2-4f32-ace7-683c7d5b0ea6%[40googlegroups.com](http://40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://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](mailto:ats-lang-user...@googlegroups.com).  
> > > > > > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/bc26f9cd-6c7b-4a67-b320-3c68d46af2ca%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 6:33pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/16 "2014-05-15T18:33:15Z")

</div>

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 here[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brand...@gmail.com)
> > > > > 
> > > > > On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang...@googlegroups.com).  
> > > > > > > To post to this group, send email to [ats-l...@googlegroups.com](mailto: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.com](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > > > > > .

---

<div class="post-metadata">

**Author:** ![Brandon\_Barker](https://sea1.discourse-cdn.com/flex019/user_avatar/discourse.ats-lang.org/brandon_barker/32/61_2.png) [@Brandon\_Barker](https://discourse.ats-lang.org/u/Brandon_Barker)\
**Post date:** [May 15, 2014, 3:38pm UTC](https://discourse.ats-lang.org/t/static-integer-multiplication/700/17 "2014-05-15T15:38:44Z")

</div>

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[https://github.com/bbarker/M-N-K-Tic-Tac-Toe/tree/9153776731de1c3559af6fc0949b47eef4946f3d](https://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](mailto:brandon...@gmail.com)
> 
> On Wed, May 14, 2014 at 9:13 PM, gmhwxi [gmh...@gmail.com](mailto: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](mailto:ats-lang-user...@googlegroups.com).  
> > > To post to this group, send email to [ats-lan...@googlegroups.com](mailto: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](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com)[https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm\_medium=email&utm\_source=footer](https://groups.google.com/d/msgid/ats-lang-users/9c7bedb5-17e2-4f32-ace7-683c7d5b0ea6%40googlegroups.com?utm_medium=email&utm_source=footer)  
> > > .