Re: Unsolved constraint in factorial example

[Hongwei Xi]

This is because the compiler does not know the product of two natural numbers

is also a natural number.

On Sun, Mar 30, 2014 at 3:40 AM, Shahab Tasharrofi <shahab.t...@gmail.com> wrote:

I still have a constraint in my program that does not pass constraint solving
phase. The general way of the relevant part in my problem was similar to the
factorial example and, so, I took the following factorial implementation from
the ATS book and checked to see if it can pass the constraint solving. I
observed that factorial example below cannot pass the constraint solving
either.

fun fact {n:nat} (x: int n): [r:nat] int r = if x > 0 then x * fact (x-1) else 1

While I cannot be sure if my problem and the problem with factorial example
above are indeed the same, I first want to see what the problem with the
above implementation is and then check if my problem is also the same.

--
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/cb961436-c31d-4839-bf80-6891154d2bbd%40googlegroups.com.

[gmhwxi]

Here is a version that type-checks:

fun
fact{n:nat}
(
  x: int n
) : [r:nat] int r =
(
if x > 0
  then let
    val [r1:int] r1 = fact (x-1)
    prval () = mul_gte_gte_gte {n,r1} ()
  in
    x * r1
  end // end of [then]
  else 1 // end of [else]
) (* end of [if] *)

On Sunday, March 30, 2014 9:49:05 AM UTC-4, gmhwxi wrote:

This is because the compiler does not know the product of two natural numbers

is also a natural number.

On Sun, Mar 30, 2014 at 3:40 AM, Shahab Tasharrofi <shahab.t...@gmail.com> wrote:

I still have a constraint in my program that does not pass constraint solving
phase. The general way of the relevant part in my problem was similar to the
factorial example and, so, I took the following factorial implementation from
the ATS book and checked to see if it can pass the constraint solving. I
observed that factorial example below cannot pass the constraint solving
either.

fun fact {n:nat} (x: int n): [r:nat] int r = if x > 0 then x * fact (x-1) else 1

While I cannot be sure if my problem and the problem with factorial example
above are indeed the same, I first want to see what the problem with the
above implementation is and then check if my problem is also the same.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.