Books.hs

{-# LANGUAGE CPP #-}

#define DISCOUNT_PERCENTAGE   2
#define BOOK_THRESHOLD        2

module Books where

calculateDiscount' :: Customer -> Int -> Int

---------------------------------------------------------------------------------------
-- 1. Define: Types of customers
---------------------------------------------------------------------------------------

data Customer = Vip | Reg deriving (Eq)

---------------------------------------------------------------------------------------
-- 2. Define: Discountable Customers and Discounts
---------------------------------------------------------------------------------------

{-@ inline customerGetsDiscount @-}
customerGetsDiscount :: Customer -> Int -> Bool
customerGetsDiscount c i = c == Vip && i >= BOOK_THRESHOLD

{-@ inline discount @-}
discount :: Int -> Int
discount bookCount = (bookCount - BOOK_THRESHOLD) * DISCOUNT_PERCENTAGE

{-@ type Discount i = {v:Int | v == discount i} @-}

---------------------------------------------------------------------------------------
-- 3. Policy: Only compute discounts for discountable customers
---------------------------------------------------------------------------------------

{-@ calculateDiscount' :: c:Customer -> i:{Int | customerGetsDiscount c i} -> Discount i @-}
calculateDiscount' c i = discount i

---------------------------------------------------------------------------------------
-- 4. Implement: Code to compute discounts, if suitable, is accepted
---------------------------------------------------------------------------------------

{-@ calculateDiscount :: Int -> Nat -> Nat @-}
calculateDiscount userId bookCount
  | getsDiscount = calculateDiscount' c bookCount
  | otherwise    = 0
  where
    getsDiscount = customerGetsDiscount c bookCount
    c            = customerType userId

---------------------------------------------------------------------------------------
-- 5. Buggy Implementation, with wrong check, is rejected
---------------------------------------------------------------------------------------

{-@ misCalculateDiscount :: Int -> Nat -> Nat @-}
misCalculateDiscount userId bookCount
  | getsDiscount = calculateDiscount' c bookCount
  | otherwise    = 0
  where
    getsDiscount = c == Vip
    c            = customerType userId

customerType :: Int -> Customer
customerType = undefined