{-# LANGUAGE RankNTypes , CPP , ImplicitParams , ConstraintKinds #-} module Control.Precondition ( module Control.Precondition , module Data.Maybe , module Data.Either.Combinators , Loc(..) ) where import Control.Exception import Control.Exception.Assert (assertMessage) import Control.Lens import Data.Either.Combinators hiding ( fromRight',fromLeft' , mapLeft,mapRight , mapBoth, isRight, isLeft ) import Data.List.NonEmpty import Data.Maybe hiding (fromJust) import GHC.Stack.Utils import Language.Haskell.TH import Language.Haskell.TH.Syntax import Language.Haskell.TH.Lift import Text.Printf fromJust' :: Pre => Maybe a -> a fromJust' (Just x) = x fromJust' Nothing = assertFalse' "Nothing" fromRight' :: Pre => Either a b -> b fromRight' (Right x) = x fromRight' (Left _) = assertFalse' "Left" fromLeft' :: Pre => Either a b -> a fromLeft' (Left x) = x fromLeft' (Right _) = assertFalse' "Right" nonEmpty' :: Pre => [a] -> NonEmpty a nonEmpty' (x : xs) = x :| xs nonEmpty' [] = assertFalse' "empty list cast as non empty" (!) :: (Pre, Ixed m) => m -> Index m -> IxValue m (!) m x = fromJust' $ m^?ix x byPred :: (Show x,Pre) => String -> (x -> Bool) -> x -> a -> a byPred msg p x = providedMessage' ?loc "byPred" (msg ++ "\n" ++ show x) (p x) byEq :: (Eq x, Show x,Pre) => String -> x -> x -> a -> a byEq msg = byRel' msg (==) "≠" byOrd :: (Ord x, Show x,Pre) => String -> Ordering -> x -> x -> a -> a byOrd msg ord = byRel' msg (\x y -> ord == compare x y) symb where symb = case ord of LT -> "≮" GT -> "≯" EQ -> "≠" byRel :: (Show a,Pre) => String -> (a -> a -> Bool) -> a -> a -> x -> x byRel msg rel = byRel' msg rel "/rel/" byRel' :: (Show a,Pre) => String -> (a -> a -> Bool) -> String -> a -> a -> x -> x byRel' tag rel symb x0 x1 r = providedMessage' ?loc tag (show x0 ++ " " ++ symb ++ " " ++ show x1) (x0 `rel` x1) r type Pre = (?loc :: CallStack) assertFalse' :: Pre => String -> a assertFalse' msg = providedMessage' (?loc) "assertion" msg False (error "false assertion: ") undefined' :: Pre => a undefined' = provided False (error "undefined") assertFalseMessage :: Pre => String -> a assertFalseMessage msg = providedMessage' ?loc "False assert" msg False (error "false assertion (2)") provided :: Pre => Bool -> a -> a provided = provided' ?loc provided' :: CallStack -> Bool -> a -> a provided' cs b = assertMessage "Precondition" (fromMaybe "" $ stackTrace [__FILE__] cs) (assert b) providedMessage' :: CallStack -> String -> String -> Bool -> a -> a providedMessage' cs tag msg b = assertMessage tag (fromMaybe "" (stackTrace [__FILE__] cs) ++ "\n" ++ msg) (assert b) providedM :: Pre => Bool -> m a -> m a providedM b cmd = do provided b () `seq` cmd locMsg :: Loc -> String locMsg loc = printf "%s:%d:%d" (loc_filename loc) (fst $ loc_start loc) (snd $ loc_end loc) withLoc :: Name -> ExpQ withLoc fun = do loc <- location [e| $(varE fun) $(lift loc) |] instance Lift Loc where lift = $(makeLift ''Loc)