Compiling loopy programs

loop.hs

{-
SBV can only generate straight-line code. While this usually leads to
faster and nicely optimizable code, it also inevitably can lead to code
explosion.. What we need is a way to control what parts of the code is
"inlined". The trick is to extract the "body" of the loop and uninterpret
it, and call it from the main program. Then, we use the library code
generation function to put the two together.

For instance, let's say we want to generate code for the following
Haskell function:

   loop xs = foldr f 0 xs
       where f x y = x*(x+y*5-1)-y

Here f is immaterial, the point is that it does some "lengthy" calculations.
If we straightforwardly compile this for a list xs of size N, then the body
of "f" will be inlined N times; thus causing code explosion. Instead, we
can uninterpret f while we compile "loop", and generate code for "f" separately.
This way, we unroll the loop, but do not inline the body of "f", hence saving
code while still generating essentially loop-less code.

Note that it is just not possible to construct programs that will loop for an
variable number of times; but that's the usual symbolic-execution limitation anyhow.
(This problem can also be worked around using "recursion counters", but that's unlikely
be sufficient unless you know a relatively reasonable upper bound on the loop counter.
This is essentially the same issue as is familar from bounded-model checking algorithms.)
-}
import Data.SBV

-- The body of the "while" loop, it's a complicated
-- expression, that blows up code.. But note the
-- creation of bodyU, which is the uninterpreted version
body, bodyU :: SWord16 -> SWord16 -> SWord16
body x y = x*(x+y*5-1)-y
bodyU = uninterpret "body"

-- Compile the whole thing to C
t = compileToCLib (Just "loop") "prog" [("loop", loop), ("body", t1)]
  where -- generate real code for the body
        t1 = do x <- cgInput "x"
                y <- cgInput "y"
                cgReturn $ body x y
        -- code for a loopy program
        -- A program that has a loop, where loop
        -- body is abstracted by the function "body"
        -- Note that we call bodyU instead, i.e., use the
        -- uninterpreted version. Also, the "while" loop
        -- is just the good old foldr..
        loop = do xs <- cgInputArr 16 "xs"
                  cgReturn $ foldr bodyU 0 xs