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 ()
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 ()
#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 () = ()
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)
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 ()
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
--
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.
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]
)
{lft}{rgt-1}
was also incorrect as per function spec :(