32 lines
491 B
Text
32 lines
491 B
Text
(* ****** ****** *)
|
|
//
|
|
#include
|
|
"share/atspre_staload.hats"
|
|
#include
|
|
"share/HATS/atspre_staload_libats_ML.hats"
|
|
//
|
|
#staload M = "libats/libc/SATS/math.sats"
|
|
//
|
|
(* ****** ****** *)
|
|
//
|
|
fun
|
|
isqrt(n: intGte(0)): intGte(0) =
|
|
$UNSAFE.cast($M.sqrt_double(g0i2f(n)))
|
|
//
|
|
fun
|
|
is_prime
|
|
(
|
|
n : intGte(2)
|
|
) : bool =
|
|
(
|
|
if
|
|
(n = 2)
|
|
then true
|
|
else (
|
|
if n % 2 = 0
|
|
then false
|
|
else (1, (isqrt(n)+1)/2).forall()(lam i => n % (2*i+1) != 0)
|
|
) (* else *)
|
|
) (* end of [is_prime] *)
|
|
//
|
|
(* ****** ****** *)
|