Fibonorial.dats

(*
**
** Fibonorial(verify)
**
** The given implementation is of a particular
** programming style in ATS, combining programming with
** theorem-proving in a syntactically intertwined manner
**
*)

(* ****** ****** *)

#include
"share/atspre_define.hats"
#include
"share/atspre_staload.hats"

(* ****** ****** *)

#define ATS_MAINATSFLAG 1
#define ATS_DYNLOADNAME "my_dynload"

dataprop
FIB (int, int) =
  | FIB0 (0, 0)
  | FIB1 (1, 1)
  | {n:nat}
    {r0,r1:int}
    FIB2 (n+2, r0+r1) of (FIB (n, r0), FIB (n+1, r1))
// end of [FIB] // end of [dataprop]

(* ****** ****** *)
//
fun
fibats{n:nat}
  (n: int (n))
: [r:int] (FIB (n, r) | int r) = let
  fun loop
    {i:nat | i <= n}{r0,r1:int}
  (
    pf0: FIB (i, r0), pf1: FIB (i+1, r1)
  | ni: int (n-i), r0: int r0, r1: int r1
  ) : [r:int] (FIB (n, r) | int r) =
    if (ni > 0)
      then loop{i+1}(pf1, FIB2 (pf0, pf1) | ni - 1, r1, r0 + r1)
      else (pf0 | r0)
    // end of [if]
  // end of [loop]
in
  loop {0} (FIB0 (), FIB1 () | n, 0, 1)
end // end of [fibats]
//
(* ****** ****** *)
//
val N = 10
val (pf | res) = fibats(N)
val () = println! ("fibats(", N, ") = ", res)
//
(* ****** ****** *)

dataprop
FIBONORIAL (int, int) =
  | FIBONORIAL0 (0, 1)
  | {n: nat} {r1,r2: int}
    FIBONORIALN (n+1, r1*r2) of (FIB(n+1, r1), FIBONORIAL(n, r2))
// end of [FIBONORIAL]

(* ****** ****** *)

fun
fibonorialats
  {n:nat}
(
  n: int (n)
) : [r:int] (FIBONORIAL(n,r) | int r) = let
//
fun loop
  {i:nat | i <= n}
  {r0,r1,r2 : int}
(
  pf0: FIB(i,r0), pf1: FIB(i+1, r1), pf2: FIBONORIAL(i, r2)
| iterationsLeft: int (n-i), r0: int r0, r1: int r1, r2: int r2
) : [r:int] (FIBONORIAL(n,r) | int r) =
  if (iterationsLeft > 0)
    then loop{i+1}(pf1, FIB2(pf0, pf1), FIBONORIALN(pf1, pf2) | iterationsLeft-1, r1, r0+r1, r1 * r2)
    else (pf2 | r2)
  // end of [if]
in
  loop{0}(FIB0(), FIB1(), FIBONORIAL0() | n, 0, 1, 1)
end // end of [fibonorialats]

(* ****** ****** *)
//
val N = 10
val (pf | res) = fibonorialats(N)
val () = println! ("fibonorialats(", N, ") = ", res)
//
(* ****** ****** *)

implement main0 () = ()

(* ****** ****** *)

(* end of [Fibonorial.dats] *)