{-# LANGUAGE ForeignFunctionInterface #-}

module Lib
    ( factorial
    , choose
    , doubleFactorial
    ) where

import Control.Composition
import           Foreign.C

foreign import ccall unsafe factorial_ats :: CInt -> CInt
foreign import ccall unsafe choose_ats :: CInt -> CInt -> CInt
foreign import ccall unsafe double_factorial :: CInt -> CInt

{-@ choose :: { n : Nat | n >= 0 } -> { k : Nat | k >= 0 && k <= n } -> Int @-}
choose :: Int -> Int -> Int
choose = fromIntegral .* on choose_ats fromIntegral

doubleFactorial :: Int -> Int
doubleFactorial = fromIntegral . double_factorial . fromIntegral

{-@ factorial :: { n : Nat | n <= 0 } -> Int @-}
factorial :: Int -> Int
factorial = fromIntegral . factorial_ats . fromIntegral