content: -- | Implement USB5 CRC over a stream of 16-bit words.  The USB5 algorithm
  -- itself is implemented in SBV; see
  -- https://github.com/LeventErkok/sbv/blob/master/Data/SBV/Examples/CodeGeneration/CRC_USB5.hs
  -- .
  
  {-
  
  > runhaskell CRC.hs
  > cd copilot-sbv-codegen
  
  Add a main function to driver.c; something like
  
    int main(void) {
      int i;
      for(i = 0; i < 10; i++) {
        step();
      }
      return 1;
    }
  
  Define a trigger function (look in copilot.h for the prototype), e.g., 
  
    void chksum(uint16_t words, uint16_t current, uint16_t output) {
      printf("words: %u, current: %u, output: %u\n", words, current, output); 
    }
  
  > make driver
  > ./driver
  
  -}
  
  module CRC where
  
  import Prelude ()
  import Language.Copilot hiding (words)
  import qualified Copilot.Compile.SBV as S
  
  import qualified Data.SBV as V
  import Data.SBV.Examples.CodeGeneration.CRC_USB5 (crcUSB)
  
  -- | Incoming stream of words: 1,2,3, ..., 2047,0,1,2, ...
  words :: Stream Word16
  words = [1] ++ words `mod` 2047 -- USB5 is for 11-bit words.
  
  -- | Call the CRC function generated by the SBV package.  (The Nothing argument
  -- says "no interpreter values given.)
  current :: Stream Word16
  current = externFun "crc_sbv" [arg words] Nothing
  
  -- | xor the CRC of the current word and the CRC of the stream so far.
  output :: Stream Word16
  output = [0] ++ current .^. output
  
  -- | The trigger specifies a C function with the prototype 
  -- void chksum(Word16, Word16, Word16);
  spec :: Spec
  spec = 
    trigger "chksum" true [ arg words
                          , arg current
                          , arg output
                          ]
  
  main :: IO ()
  main = 
    reify spec >>=
      S.compileWithSBV 
        S.defaultParams
        [("crc_sbv", sbv)]
      
    where
    sbv = do word <- V.cgInput "word"
             V.cgReturn (crcUSB word)
  
  
  