------------------------------------------------------------------------------
-- Auxiliary operations for contract checking.
-- If the contract tool adds some unverified contracts to a program,
-- the definition of these operations are also added.

--- Auxiliary operation to check the validity of a precondition for
--- some function call.
--- For this purpose, a function call
---
---     (f x1 ... xn)
---
--- is transformed into the new call
---
---     checkPreCond (f x1 ... xn) (f'pre x1 ... xn) "f" (x1,...,xn)
---
checkPreCond :: Show a => b -> Bool -> String -> a -> b
checkPreCond x pc fn args =
  if pc
    then x
    else error $ "Precondition of operation '" ++ fn ++
                 "' not satisfied for arguments:\n" ++ show args


--- Auxiliary operation to check the validity of a given postcondition.
--- For this purpose, each rule
---
---     f x1 ... xn = rhs
---
--- is transformed into the new rule
---
---     f x1 ... xn = checkPostCond rhs (f'post x1 ... xn) "f" (x1,...,xn)
---
checkPostCond :: (Show a, Show b) => b -> (b -> Bool) -> String -> a -> b
checkPostCond rhs fpost fname args =
  if fpost rhs
    then rhs
    else error $ "Postcondition of operation '" ++ fname ++
                 "' failed for arguments/result:\n" ++
                 show args ++ " -> " ++ show rhs

------------------------------------------------------------------------------
-- Since there are in general no `Show` instances for arbitrary operations
-- (e.g., polymorphic, higher-order), we provide type-specialized variants
-- of contract checking operations.

checkPreCond_Int :: b -> Bool -> String -> Int -> b
checkPreCond_Int r pc fn x = checkPreCond r pc fn x

-- If there is no type-specialization possible, we provide a variant
-- where the arguments are not shown.
checkPreCond_Any :: b -> Bool -> String -> a -> b
checkPreCond_Any x pc fn _ =
  if pc
    then x
    else error $ "Precondition of operation '" ++ fn ++
                 "' not satisfied for some arguments!"

checkPostCond_Int_Int :: Int -> (Int -> Bool) -> String -> Int -> Int
checkPostCond_Int_Int r pc fn x = checkPostCond r pc fn x

-- If there is no type-specialization possible, we provide a variant
-- where the arguments/result are not shown.
checkPostCond_Any_Any :: b -> (b -> Bool) -> String -> a -> b
checkPostCond_Any_Any rhs fpost fname _ =
  if fpost rhs
    then rhs
    else error $ "Postcondition of operation '" ++ fname ++
                 "' failed for some arguments/result!"

------------------------------------------------------------------------------