Why am I getting unsolved constraint?

Google Group
1

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

2

Brandon , what I am trying to do is my inputs have relationship l <= r + 1
where l is a nat and r is a int and I want to ensure that result of my
function have property l==r+1.

Here is another example code of what I am trying to do :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

val () = println! (“rough”)

(* l must always be >= 0 and return value must always have
following relation : l == r+1 )
( this function assumes that inputs are l >= 0 and l <= r+1 *)
fun just_a_test2 (l : int , r : int) : (int,int) = let
val () = assertloc (l >= 0 && l <= r+1)
in
if l <= r
then just_a_test2(l , r-1)
else (l,r)
end

val l = just_a_test2(0,10)
val l2 = just_a_test2(0,~1)

val () = println! (l.0 , “,” , l.1)
val () = println! (l2.0 , “,” , l2.1)

//val l3 = just_a_test2(0,~2) // this is invalid input and should fail

implement main0 () = ()On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test (left, right+1)
else ()

3

Ha ! , now I get it(I hope :slight_smile: ) , indeed I was mixing functional and
imperative .

ThanksOn Friday, January 31, 2014 8:18:33 PM UTC+5:30, gmhwxi wrote:

First, the quantifiers should probably be written as follows:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the
call.

On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

4

First, the quantifiers should probably be written as follows:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the call.On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

5

This implementation is of imperative style:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}
(left : int (lft) , right : &int (rgt) >> int (lft-1)): void =
(
if (left <= right)
then (right := right-1; just_a_test (left, right))
else ()
// end of [if]
)On Friday, January 31, 2014 10:12:51 AM UTC-5, Brandon Barker wrote:

I’m curious what part of this is considered imperative programming?

Brandon Barker
brand...@gmail.com <javascript:>

On Fri, Jan 31, 2014 at 9:48 AM, gmhwxi <gmh...@gmail.com <javascript:>>wrote:

First, the quantifiers should probably be written as follows:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}

(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the
call.

On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com
.

6

The following function typechecks:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [rgt:int | lft == rgt+1] int(rgt
) =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else right

Only ‘right’ needs to be returned as ‘left’ stays the same.On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

7

How about this? You need a new static variable (rgt_out) for the right
variable that is being output, as it changes over the course of execution.

fun just_a_test {rgt : int} {lft : nat | lft <= rgt + 1}
(left : int (lft) , right : int (rgt)
) : [rgt_out : int | lft == rgt_out + 1] (int lft, int rgt_out) =
if (left = (right + 1)) then (left, right)
else just_a_test (left,right-1)On Friday, January 31, 2014 8:55:14 AM UTC-5, chotu s wrote:

Brandon , what I am trying to do is my inputs have relationship l <= r +
1 where l is a nat and r is a int and I want to ensure that result of my
function have property l==r+1.

Here is another example code of what I am trying to do :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

val () = println! (“rough”)

(* l must always be >= 0 and return value must always have
following relation : l == r+1 )
( this function assumes that inputs are l >= 0 and l <= r+1 *)
fun just_a_test2 (l : int , r : int) : (int,int) = let
val () = assertloc (l >= 0 && l <= r+1)
in
if l <= r
then just_a_test2(l , r-1)
else (l,r)
end

val l = just_a_test2(0,10)
val l2 = just_a_test2(0,~1)

val () = println! (l.0 , “,” , l.1)
val () = println! (l2.0 , “,” , l2.1)

//val l3 = just_a_test2(0,~2) // this is invalid input and should fail

implement main0 () = ()

On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test (left, right+1)
else ()

8

I’m curious what part of this is considered imperative programming?

Brandon Barker
brandon…@gmail.comOn Fri, Jan 31, 2014 at 9:48 AM, gmhwxi gmh...@gmail.com wrote:

First, the quantifiers should probably be written as follows:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}

(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the
call.

On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com
.

9

Another stupid mistake I did not realize was that order {lft}{rgt-1}was
also incorrect as per function spec :(On Friday, January 31, 2014 5:15:31 PM UTC+5:30, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

10

Sorry, nevermind: I guess it is because only the void is being returned;
but it seems to have no effects, so I thought it was functional.

Brandon Barker
brandon…@gmail.comOn Fri, Jan 31, 2014 at 10:12 AM, Brandon Barker brandon...@gmail.comwrote:

I’m curious what part of this is considered imperative programming?

Brandon Barker
brandon...@gmail.com

On Fri, Jan 31, 2014 at 9:48 AM, gmhwxi gmh...@gmail.com wrote:

First, the quantifiers should probably be written as follows:

fun just_a_test
{lft:nat}{rgt : int | lft <= rgt+1}

(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

You are mixing functional programming with imperative programming.

Note that lft and rgt are fixed integers that cannot change during the
call.

On Friday, January 31, 2014 6:45:31 AM UTC-5, chotu s wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know
why is compiler asking for following constraint to be unsolved (rgt - 1) >=
0 . (I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com
.

11

1: I don’t think you need just_a_test{lft}{rgt-1} in a call to a
polymorphic function, just “just_a_test”.
2: I htink your return type is wrong: if you change the recursive case
to : (left,right+1), it works.
Brandon Barker
brandon…@gmail.comOn Fri, Jan 31, 2014 at 6:45 AM, chotu s chot...@gmail.com wrote:

Hello,

Maybe I am missing some thing here(I am pretty sure :slight_smile: ) , may I know why
is compiler asking for following constraint to be unsolved (rgt - 1) >= 0 .
(I believe this is what it is asking)

Here is the code :

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test{lft}{rgt-1} (left,right-1)
else ()

Is there any counter example that makes above formulation impossible.

Thanks

–
You received this message because you are subscribed to the Google Groups
“ats-lang-users” group.
To unsubscribe from this group and stop receiving emails from it, send an
email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/4674e7ce-9d11-45ff-8d92-f36fa0c49322%40googlegroups.com.

12

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test (left, right+1)
else ()

13

Thanks, yes this seems to work , let me try to plug it in actual program
and see if it solves the issue . But I wonder why original code fragement
does not work , is it not that linear constraints (which I presume it is )
are solved by the compiler , I wonder if my original formulation wrong .On Friday, January 31, 2014 7:43:42 PM UTC+5:30, Brandon Barker wrote:

How about this? You need a new static variable (rgt_out) for the right
variable that is being output, as it changes over the course of execution.

fun just_a_test {rgt : int} {lft : nat | lft <= rgt + 1}
(left : int (lft) , right : int (rgt)
) : [rgt_out : int | lft == rgt_out + 1] (int lft, int rgt_out) =
if (left = (right + 1)) then (left, right)
else just_a_test (left,right-1)

On Friday, January 31, 2014 8:55:14 AM UTC-5, chotu s wrote:

Brandon , what I am trying to do is my inputs have relationship l <= r +
1 where l is a nat and r is a int and I want to ensure that result of my
function have property l==r+1.

Here is another example code of what I am trying to do :

#include “share/atspre_define.hats”
#include “share/atspre_staload.hats”

val () = println! (“rough”)

(* l must always be >= 0 and return value must always have
following relation : l == r+1 )
( this function assumes that inputs are l >= 0 and l <= r+1 *)
fun just_a_test2 (l : int , r : int) : (int,int) = let
val () = assertloc (l >= 0 && l <= r+1)
in
if l <= r
then just_a_test2(l , r-1)
else (l,r)
end

val l = just_a_test2(0,10)
val l2 = just_a_test2(0,~1)

val () = println! (l.0 , “,” , l.1)
val () = println! (l2.0 , “,” , l2.1)

//val l3 = just_a_test2(0,~2) // this is invalid input and should fail

implement main0 () = ()

On Friday, January 31, 2014 7:00:26 PM UTC+5:30, Brandon Barker wrote:

fun just_a_test {rgt : int} {lft : nat | lft <= rgt+1}
(left : int (lft) , right : int (rgt)) : [lft == rgt+1] void =
if (left <= right)
then just_a_test (left, right+1)
else ()