Why am I getting unsolved constraint ?

[chotu s]

Hello,

Maybe I am missing some thing here(I am pretty sure :-) )   , 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

[Brandon Barker]

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

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

[Brandon Barker]

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

[chotu s]

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

[Brandon Barker]

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)

[chotu s]

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 .

[gmhwxi]

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.

[gmhwxi]

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:

[Brandon Barker]

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

Brandon Barker
brandon...@gmail.com

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/47ad10de-0c3b-46b0-954f-19634d5eb2d3%40googlegroups.com.

[Brandon Barker]

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

[chotu s]

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

Thanks

[gmhwxi]

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

[chotu s]

Another stupid mistake I did not realize was that order {lft}{rgt-1}was also incorrect as per function spec :(