fun first1 {ndx:int | ndx >= 1} (ndx: ulint ndx, nzer: ulint): (ulint, ulint
) =
if (ndx land 1ul) = 0ul
then first1 ((ndx >> 1ul), nzer + 1ul)
else (ndx, nzer)
the above code gives the following error:
error(3): the symbol [>>] cannot be resolved as no match is found.
as you can see, I tried to introduce a dependent type, mostly in
speculation of the conditions where the compiler would approve of a bit
shift, or consider it “safe”
Is there a general overview for bitwise operations in ats2? I haven’t been
able to find anything in the html book from the main site.
However, the typechecker does not know that ndx >> 1 yields a nonzero
integer in this case. So you
will encounter a type-error.On Tuesday, June 24, 2014 1:10:18 PM UTC-4, Justin Smith wrote:
fun first1 {ndx:int | ndx >= 1} (ndx: ulint ndx, nzer: ulint): (ulint,
ulint) =
if (ndx land 1ul) = 0ul
then first1 ((ndx >> 1ul), nzer + 1ul)
else (ndx, nzer)
the above code gives the following error:
error(3): the symbol [>>] cannot be resolved as no match is found.
as you can see, I tried to introduce a dependent type, mostly in
speculation of the conditions where the compiler would approve of a bit
shift, or consider it “safe”
Is there a general overview for bitwise operations in ats2? I haven’t been
able to find anything in the html book from the main site.
fun
first1{i:pos}
(
ndx: ulint(i), nzer: uint
) : (ulint, uint) =
(
if
iseqz (ndx land 1ul)
then let
val ndx = ndx >> 1
val [i:int] ndx = g1ofg0 (ndx)
prval () = __assert () where
{
extern praxi __assert (): [i >= 1] void
}
in
first1 (ndx, succ(nzer))
end // end of [then]
else (ndx, nzer) // end of [else]
) (* end of [first1] *)On Tuesday, June 24, 2014 1:10:18 PM UTC-4, Justin Smith wrote:
fun first1 {ndx:int | ndx >= 1} (ndx: ulint ndx, nzer: ulint): (ulint,
ulint) =
if (ndx land 1ul) = 0ul
then first1 ((ndx >> 1ul), nzer + 1ul)
else (ndx, nzer)
the above code gives the following error:
error(3): the symbol [>>] cannot be resolved as no match is found.
as you can see, I tried to introduce a dependent type, mostly in
speculation of the conditions where the compiler would approve of a bit
shift, or consider it “safe”
Is there a general overview for bitwise operations in ats2? I haven’t been
able to find anything in the html book from the main site.
Brandon Barker
brandon…@gmail.comOn Tue, Jun 24, 2014 at 1:10 PM, Justin Smith noise...@gmail.com wrote:
fun first1 {ndx:int | ndx >= 1} (ndx: ulint ndx, nzer: ulint): (ulint,
ulint) =
if (ndx land 1ul) = 0ul
then first1 ((ndx >> 1ul), nzer + 1ul)
else (ndx, nzer)
the above code gives the following error:
error(3): the symbol [>>] cannot be resolved as no match is found.
as you can see, I tried to introduce a dependent type, mostly in
speculation of the conditions where the compiler would approve of a bit
shift, or consider it “safe”
Is there a general overview for bitwise operations in ats2? I haven’t been
able to find anything in the html book from the main site.