----------------------------------------------------------------------------- -- | -- Module : Data.SBV.Examples.CodeGeneration.Fibonacci -- Copyright : (c) Lee Pike, Levent Erkok -- License : BSD3 -- Maintainer : erkokl@gmail.com -- Stability : experimental -- Portability : portable -- -- 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 n = select table 0 n 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