Problème 7

(supprimer le menu, télécharger)

(***************************)
(*                         *)
(*        Problem 7        *)
(*                         *)
(***************************)

staload P = "lib_prime.sats"
staload "lib_prime.dats"

(* Typing of the problem *)

dataprop P7 (m : int, n : int) = // P7 (m, n) is true iff n is the mth prime number
  | P7_Bas (1, 2)
  | {m, n : int} P7_Rec (m + 1, n) of
      [k : int | k < n]
        ($P.Prime n, P7 (m, k), {l : int | k < l && l < n} $P.Prime l -<> [0 == 1] void)

(* Prototype of the main function *)

extern fun p7 {m : pos} (m : int m) :<> [n : int] (P7 (m, n) | int n)


(* Interface *)

implement main () = let
  #define N 10001
  val (_ | k) = p7 N
in
  printf ("The %dth prime number is:\n%d\n\n",
          @(N, k))
end



(* Implementation of the main function *)

implement p7 (m) =
  if m = 1 then (P7_Bas | 2)
  else let
    fun search {m, n : int} (m : int m, n : int n) : [n : int] int n = let
      val (pf_prime | pr) = $P.is_prime n
    in
      if pr then if m = 1 then n else search (m - 1, n + 1) else search (m, n + 1)
    end
    
    val (pf, _ | result) = search (m, 2)
  in
    (pf | result)
  end