-----------------------------------------------------------------------------
-- |
-- Module      :  Data.SBV.Examples.CodeGeneration.Fibonacci
-- Copyright   :  (c) Lee Pike, Levent Erkok
-- License     :  BSD3
-- Maintainer  :  erkokl@gmail.com
-- Stability   :  experimental
--
-- Computing Fibonacci numbers and generating C code. Inspired by Lee Pike's
-- original implementation, modified for inclusion in the package. It illustrates
-- symbolic termination issues one can have when working with recursive algorithms
-- and how to deal with such, eventually generating good C code.
-----------------------------------------------------------------------------

module Data.SBV.Examples.CodeGeneration.Fibonacci where

import Data.SBV

-----------------------------------------------------------------------------
-- * A naive implementation
-----------------------------------------------------------------------------

-- | This is a naive implementation of fibonacci, and will work fine (albeit slow)
-- for concrete inputs:
--
-- >>> map fib0 [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
-- However, it is not suitable for doing proofs or generating code, as it is not
-- symbolically terminating when it is called with a symbolic value @n@. When we
-- recursively call @fib0@ on @n-1@ (or @n-2@), the test against @0@ will always
-- explore both branches since the result will be symbolic, hence will not
-- terminate. (An integrated theorem prover can establish termination
-- after a certain number of unrollings, but this would be quite expensive to
-- implement, and would be impractical.)
fib0 :: SWord64 -> SWord64
fib0 n = ite (n .== 0 ||| n .== 1)
             n
             (fib0 (n-1) + fib0 (n-2))

-----------------------------------------------------------------------------
-- * Using a recursion depth, and accumulating parameters
-----------------------------------------------------------------------------

{- $genLookup
One way to deal with symbolic termination is to limit the number of recursive
calls. In this version, we impose a limit on the index to the function, working
correctly upto that limit. If we use a compile-time constant, then SBV's code generator
can produce code as the unrolling will eventually stop.
-}

-- | The recursion-depth limited version of fibonacci. Limiting the maximum number to be 20, we can say:
--
-- >>> map (fib1 20) [0..6]
-- [0 :: SWord64,1 :: SWord64,1 :: SWord64,2 :: SWord64,3 :: SWord64,5 :: SWord64,8 :: SWord64]
--
-- The function will work correctly, so long as the index we query is at most @top@, and otherwise
-- will return the value at @top@. Note that we also use accumulating parameters here for efficiency,
-- although this is orthogonal to the termination concern.
--
-- A note on modular arithmetic: The 64-bit word we use to represent the values will of course
-- eventually overflow, beware! Fibonacci is a fast growing function..
fib1 :: SWord64 -> SWord64 -> SWord64
fib1 top n = fib' 0 1 0
  where fib' :: SWord64 -> SWord64 -> SWord64 -> SWord64
        fib' prev' prev m = ite (m .== top ||| m .== n)          -- did we reach recursion depth, or the index we're looking for
                                prev'                            -- stop and return the result
                                (fib' prev (prev' + prev) (m+1)) -- otherwise recurse

-- | We can generate code for 'fib1' using the 'genFib1' action. Note that the
-- generated code will grow larger as we pick larger values of @top@, but only linearly,
-- thanks to the accumulating parameter trick used by 'fib1'. The following is an excerpt
-- from the code generated for the call @genFib1 10@, where the code will work correctly
-- for indexes up to 10:
--
-- > SWord64 fib1(const SWord64 x)
-- > {
-- >   const SWord64 s0 = x;
-- >   const SBool   s2 = s0 == 0x0000000000000000ULL;
-- >   const SBool   s4 = s0 == 0x0000000000000001ULL;
-- >   const SBool   s6 = s0 == 0x0000000000000002ULL;
-- >   const SBool   s8 = s0 == 0x0000000000000003ULL;
-- >   const SBool   s10 = s0 == 0x0000000000000004ULL;
-- >   const SBool   s12 = s0 == 0x0000000000000005ULL;
-- >   const SBool   s14 = s0 == 0x0000000000000006ULL;
-- >   const SBool   s17 = s0 == 0x0000000000000007ULL;
-- >   const SBool   s19 = s0 == 0x0000000000000008ULL;
-- >   const SBool   s22 = s0 == 0x0000000000000009ULL;
-- >   const SWord64 s25 = s22 ? 0x0000000000000022ULL : 0x0000000000000037ULL;
-- >   const SWord64 s26 = s19 ? 0x0000000000000015ULL : s25;
-- >   const SWord64 s27 = s17 ? 0x000000000000000dULL : s26;
-- >   const SWord64 s28 = s14 ? 0x0000000000000008ULL : s27;
-- >   const SWord64 s29 = s12 ? 0x0000000000000005ULL : s28;
-- >   const SWord64 s30 = s10 ? 0x0000000000000003ULL : s29;
-- >   const SWord64 s31 = s8 ? 0x0000000000000002ULL : s30;
-- >   const SWord64 s32 = s6 ? 0x0000000000000001ULL : s31;
-- >   const SWord64 s33 = s4 ? 0x0000000000000001ULL : s32;
-- >   const SWord64 s34 = s2 ? 0x0000000000000000ULL : s33;
-- >   
-- >   return s34;
-- > }
genFib1 :: SWord64 -> IO ()
genFib1 top = compileToC Nothing "fib1" $ do
        x <- cgInput "x"
        cgReturn $ fib1 top x

-----------------------------------------------------------------------------
-- * Generating a look-up table
-----------------------------------------------------------------------------

{- $genLookup
While 'fib1' generates good C code, we can do much better by taking
advantage of the inherent partial-evaluation capabilities of SBV to generate
a look-up table, as follows.
-}

-- | Compute the fibonacci numbers statically at /code-generation/ time and
-- put them in a table, accessed by the 'select' call. 
fib2 :: SWord64 -> SWord64 -> SWord64
fib2 top = select table 0
  where table = map (fib1 top) [0 .. top]

-- | Once we have 'fib2', we can generate the C code straightforwardly. Below
-- is an excerpt from the code that SBV generates for the call @genFib2 64@. Note
-- that this code is a constant-time look-up table implementation of fibonacci,
-- with no run-time overhead. The index can be made arbitrarily large,
-- naturally. (Note that this function returns @0@ if the index is larger
-- than 64, as specified by the call to 'select' with default @0@.)
--
-- > SWord64 fibLookup(const SWord64 x)
-- > {
-- >   const SWord64 s0 = x;
-- >   static const SWord64 table0[] = {
-- >       0x0000000000000000ULL, 0x0000000000000001ULL,
-- >       0x0000000000000001ULL, 0x0000000000000002ULL,
-- >       0x0000000000000003ULL, 0x0000000000000005ULL,
-- >       0x0000000000000008ULL, 0x000000000000000dULL,
-- >       0x0000000000000015ULL, 0x0000000000000022ULL,
-- >       0x0000000000000037ULL, 0x0000000000000059ULL,
-- >       0x0000000000000090ULL, 0x00000000000000e9ULL,
-- >       0x0000000000000179ULL, 0x0000000000000262ULL,
-- >       0x00000000000003dbULL, 0x000000000000063dULL,
-- >       0x0000000000000a18ULL, 0x0000000000001055ULL,
-- >       0x0000000000001a6dULL, 0x0000000000002ac2ULL,
-- >       0x000000000000452fULL, 0x0000000000006ff1ULL,
-- >       0x000000000000b520ULL, 0x0000000000012511ULL,
-- >       0x000000000001da31ULL, 0x000000000002ff42ULL,
-- >       0x000000000004d973ULL, 0x000000000007d8b5ULL,
-- >       0x00000000000cb228ULL, 0x0000000000148addULL,
-- >       0x0000000000213d05ULL, 0x000000000035c7e2ULL,
-- >       0x00000000005704e7ULL, 0x00000000008cccc9ULL,
-- >       0x0000000000e3d1b0ULL, 0x0000000001709e79ULL,
-- >       0x0000000002547029ULL, 0x0000000003c50ea2ULL,
-- >       0x0000000006197ecbULL, 0x0000000009de8d6dULL,
-- >       0x000000000ff80c38ULL, 0x0000000019d699a5ULL,
-- >       0x0000000029cea5ddULL, 0x0000000043a53f82ULL,
-- >       0x000000006d73e55fULL, 0x00000000b11924e1ULL,
-- >       0x000000011e8d0a40ULL, 0x00000001cfa62f21ULL,
-- >       0x00000002ee333961ULL, 0x00000004bdd96882ULL,
-- >       0x00000007ac0ca1e3ULL, 0x0000000c69e60a65ULL,
-- >       0x0000001415f2ac48ULL, 0x000000207fd8b6adULL,
-- >       0x0000003495cb62f5ULL, 0x0000005515a419a2ULL,
-- >       0x00000089ab6f7c97ULL, 0x000000dec1139639ULL,
-- >       0x000001686c8312d0ULL, 0x000002472d96a909ULL,
-- >       0x000003af9a19bbd9ULL, 0x000005f6c7b064e2ULL, 0x000009a661ca20bbULL
-- >   };
-- >   const SWord64 s65 = s0 >= 65 ? 0x0000000000000000ULL : table0[s0];
-- >   
-- >   return s65;
-- > }
genFib2 :: SWord64 -> IO ()
genFib2 top = compileToC Nothing "fibLookup" $ do
        cgPerformRTCs True       -- protect against potential overflow, our table is not big enough
        x <- cgInput "x"
        cgReturn $ fib2 top x