packages feed

control-invariants (empty) → 0.1.0.0

raw patch · 6 files changed

+506/−0 lines, 6 filesdep +QuickCheckdep +assertdep +basesetup-changed

Dependencies added: QuickCheck, assert, base, containers, data-default, deepseq, either, lens, mtl, semigroups, template-haskell, th-lift, th-printf, transformers

Files

+ Control/Invariant.hs view
@@ -0,0 +1,252 @@+{-# LANGUAGE CPP, FlexibleInstances, StandaloneDeriving, TypeFamilies #-}+module Control.Invariant+    ( HasInvariant(..), Checked, IsChecked(..)+    , mutate, mutate', create'+    , Controls(..)+    , view',(!.), views'+    , use', uses'+    , HasPrefix(..)+    , (===), isSubsetOf', isProperSubsetOf'+    , relation+    , trading, holds+    , invariantMessage+    , provided, providedM+    , assertFalse'+    , Pre+    , IsAssertion(..)+    , checkAssert+    , checkAssertM+    , Invariant, (##)+    , member'+    , isSubmapOf' +    , isProperSubmapOf' )+where++import Control.DeepSeq+import Control.Lens+import Control.Monad.State+import Control.Monad.RWS+import Control.Precondition++import Data.Default+import Data.Functor.Compose+import Data.Functor.Classes+import Data.List+import Data.Map (isSubmapOf,isProperSubmapOf,Map,member)+import Data.Set (isSubsetOf,isProperSubsetOf,Set)+import Data.Typeable++import GHC.Stack.Utils++import Test.QuickCheck hiding ((===))++import Text.Printf.TH++newtype Checked a = Checked { getChecked :: a }+    deriving (Eq,Ord,NFData,Functor,Foldable,Traversable,Typeable)++instance Show a => Show (Checked a) where+    show (Checked x) = show x++#if MIN_VERSION_transformers(0,5,0)+instance Eq1 Checked where+    liftEq f (Checked a) (Checked b) = a `f` b+#else+instance Eq1 Checked where+    eq1 (Checked a) (Checked b) = a == b+#endif++#if MIN_VERSION_transformers(0,5,0)+instance Show1 Checked where+    liftShowsPrec f _ i (Checked a) = f i a+#else+instance Show1 Checked where+    showsPrec1 = showsPrec+#endif++deriving instance Typeable Compose++newtype InvariantM a = Invariant { runInvariant :: RWS [String] [String] () a }+    deriving (Functor,Applicative,Monad)++type Invariant = InvariantM ()++class Show a => HasInvariant a where+    invariant :: a -> Invariant+    updateCache :: a -> a+    updateCache = id++class HasInvariant b => IsChecked a b | a -> b where+    check :: Pre+          => b -> a+    check' :: Pre+           => b -> a+    content :: Pre+            => Iso' a b++class IsAssertion a where+    toInvariant :: a -> Invariant+    fromBool :: Bool -> a++instance (a ~ ()) => Testable (InvariantM a) where+    property p = conjoin (map (`counterexample` property False) xs)+        where+            xs = invariantResults p++instance IsAssertion Bool where+    toInvariant b = Invariant $ do+        p <- ask+        unless b $ tell [intercalate " - " $ reverse p]+    fromBool = id++instance (a ~ ()) => IsAssertion (InvariantM a) where+    toInvariant b = b >> return ()+    fromBool = toInvariant++instance Monoid a => Monoid (InvariantM a) where+    mempty = return mempty+    mappend = liftM2 mappend+    mconcat = fmap mconcat . sequence++class Controls a b | a -> b where+    content' :: Getter a b+    default content' :: a ~ b => Getter a b+    content' = id++infixl 8 !.++(!.) :: Controls a b => a -> Getting c b c -> c+(!.) = flip view'++view' :: (Controls a b,MonadReader a m) => Getting c b c -> m c+view' ln = view $ content'.ln++views' :: (Controls a b,MonadReader a m) +       => Getting d b c+       -> (c -> d)+       -> m d+views' ln f = views (content'.ln) f++use' :: (Controls a b,MonadState a m) => Getting c b c -> m c+use' ln = use $ content'.ln++uses' :: (Controls a b,MonadState a m) +      => Getting d b c +      -> (c -> d) +      -> m d+uses' ln f = uses (content'.ln) f++instance Controls (Checked a) a where+    content' = to getChecked++instance (Functor f, Show a, Show1 f, Show1 g, HasInvariant (f (g a))) +        => HasInvariant (Compose f g a) where+    invariant = invariant . getCompose+    updateCache = _Wrapped' %~ updateCache++instance HasInvariant a => IsChecked (Checked a) a where+    check    = check' . updateCache+    check' x = Checked $ checkAssert (invariant x) (show x) x+        where+            -- msg = [printf|invariant failure: \n%s|] $ intercalate "\n" p+            -- p = map fst $ filter (not.snd) $ snd $ execRWS (runInvariant $ invariant x) [] ()+    content = iso getChecked check++holds :: IsAssertion prop => prop -> Bool+holds prop = null $ snd $ execRWS (runInvariant $ toInvariant prop) [] ()++checkAssertM :: (IsAssertion a,Monad m,Pre) => a -> String -> m ()+checkAssertM p msg = checkAssert p msg (return ())++checkAssert :: (IsAssertion a,Pre) => a -> String -> b -> b+checkAssert prop detail x = providedMessage' ?loc "Invariants" msg (null p) x+        where+            msg = [s|assertion failure: \n%s\n%s|] (intercalate "\n" p) (take 1000 detail)+            p = invariantResults prop++invariantResults :: IsAssertion a => a -> [String]+invariantResults prop = +        map (take 1000) . snd $ execRWS (runInvariant $ toInvariant prop) [] ()++invariantMessage :: IsAssertion a => a -> String+invariantMessage prop +        | null p    = "pass"+        | otherwise = intercalate "\n" $ "failed" : p+    where+        p = invariantResults prop++trading :: (Functor f,Functor f')+        => Iso (Compose f (Compose g h) x) (Compose f' (Compose g' h') x')+               (Compose f g (h x)) (Compose f' g' (h' x'))+trading = iso (_Wrapped %~ fmap getCompose) (_Wrapped %~ fmap Compose)++instance Controls (Compose Checked f a) (f a) where+    content' = to getCompose . content'++instance HasInvariant (f a) => IsChecked (Compose Checked f a) (f a) where+    check   = Compose . check+    check'  = Compose . check'+    content = iso getCompose Compose . content++instance NFData (f (g x)) => NFData (Compose f g x) where+    rnf = rnf . getCompose++infixr 0 ##++(##) :: (IsAssertion b, Pre) => String -> b -> Invariant+(##) tag b = withStack ?loc $ withPrefix tag $ toInvariant b++infix 4 ===++(===) :: (Eq a, Show a) => a -> a -> Invariant+(===) = relation "/=" (==)++isSubsetOf' :: (Ord a,Show a) => Set a -> Set a -> Invariant+isSubsetOf' = relation "/⊆" isSubsetOf++isProperSubsetOf' :: (Ord a,Show a) => Set a -> Set a -> Invariant+isProperSubsetOf' = relation "/⊂" isProperSubsetOf++{-# INLINE isSubmapOf' #-}+isSubmapOf' :: (Ord k,Eq k,Eq a,Show k,Show a) +            => Map k a -> Map k a -> Invariant+isSubmapOf' = relation "/⊆" isSubmapOf++{-# INLINE isProperSubmapOf' #-}+isProperSubmapOf' :: (Eq k, Eq a,Ord k,Show k,Show a) +                  => Map k a -> Map k a -> Invariant+isProperSubmapOf' = relation "/⊂" isProperSubmapOf++{-# INLINE member' #-}+member' :: (Show k,Show a,Ord k) +        => k -> Map k a -> Invariant+member' = relation "/∈" member++relation :: (Show a,Show b) +         => String +         -> (a -> b -> Bool) +         -> a -> b -> Invariant+relation symb rel x y = [s|%s %s %s|] (show x) symb (show y) ## (x `rel` y)++class HasPrefix m where+    withPrefix :: String -> m a -> m a+    +instance HasPrefix InvariantM where+    withPrefix pre (Invariant cmd) = Invariant $ local (pre:) cmd++instance (HasInvariant a,Arbitrary a) => Arbitrary (Checked a) where+    arbitrary = check' <$> arbitrary+    shrink = fmap check' . shrink . getChecked++mutate :: (IsChecked c a,Pre)+       => c -> State a k -> c+mutate x cmd = x & content %~ execState cmd ++mutate' :: (IsChecked c a,Monad m,Pre) => StateT a m k -> StateT c m k+mutate' = zoom content++create' :: (IsChecked c a,Default a,Pre) => State a k -> c+create' = check . flip execState def ++withStack :: CallStack -> InvariantM a -> InvariantM a+withStack cs = maybe id withPrefix $ stackTrace [__FILE__] cs
+ Control/Precondition.hs view
@@ -0,0 +1,115 @@+{-# 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)
+ GHC/Stack/Utils.hs view
@@ -0,0 +1,38 @@+{-# LANGUAGE CPP #-}+module GHC.Stack.Utils+    ( module GHC.Stack.Utils+    , module GHC.Stack )+where++import Data.Maybe++import GHC.Stack++#if !(MIN_VERSION_base(4,9,0))+import GHC.SrcLoc+#endif+++import Text.Printf++stackTrace' :: [FilePath] -> CallStack -> String -> String+stackTrace' fs stack str = fromMaybe str $ stackTrace fs stack++getSrcLocs :: [FilePath] -> CallStack -> [(String,SrcLoc)]+getSrcLocs fs cs = filter notHere $ getCallStack cs+    where+        notHere :: (a,SrcLoc) -> Bool+        notHere (_,x) = srcLocFile x `notElem` __FILE__:fs++stackTrace :: [FilePath] -> CallStack -> Maybe String+stackTrace fs cs | null loc  = Nothing+                 | otherwise = Just $ '\n':concatMap f (reverse loc)+    where+        loc = getSrcLocs fs cs+        f (fn,loc) = printf "%s - %s\n" (locToString loc) fn++locToString :: SrcLoc -> String+locToString loc = printf "%s:%d:%d" +            (srcLocFile loc) +            (srcLocStartLine loc)+            (srcLocStartCol loc)
+ LICENSE view
@@ -0,0 +1,20 @@+Copyright (c) 2016 Simon Hudon++Permission is hereby granted, free of charge, to any person obtaining+a copy of this software and associated documentation files (the+"Software"), to deal in the Software without restriction, including+without limitation the rights to use, copy, modify, merge, publish,+distribute, sublicense, and/or sell copies of the Software, and to+permit persons to whom the Software is furnished to do so, subject to+the following conditions:++The above copyright notice and this permission notice shall be included+in all copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ control-invariants.cabal view
@@ -0,0 +1,79 @@+-- Initial invariants.cabal generated by cabal init.  For further +-- documentation, see http://haskell.org/cabal/users-guide/++-- The name of the package.+name:                control-invariants++-- The package version.  See the Haskell package versioning policy (PVP) +-- for standards guiding when and how versions should be incremented.+-- http://www.haskell.org/haskellwiki/Package_versioning_policy+-- PVP summary:      +-+------- breaking API changes+--                   | | +----- non-breaking API additions+--                   | | | +--- code changes with no API change+version:             0.1.0.0++-- A short (one-line) description of the package.+synopsis:            Invariants and contract monitoring++-- A longer description of the package.+description:         Invariants and contract monitoring++-- The license under which the package is released.+license:             MIT++-- The file containing the license text.+license-file:        LICENSE++-- The package author(s).+author:              Simon Hudon++-- An email address to which users can send suggestions, bug reports, and +-- patches.+maintainer:          simon@cse.yorku.ca++-- A copyright notice.+-- copyright:           ++category:            Control++build-type:          Simple++-- Extra files to be distributed with the package, such as examples or a +-- README.+-- extra-source-files:  ++-- Constraint on the version of Cabal needed to build this package.+cabal-version:       >=1.10++source-repository head+  type: git+  location: https://github.com/literate-unitb/invariants.git++library+  -- Modules exported by the library.+  exposed-modules:     +      Control.Invariant+      Control.Precondition+      GHC.Stack.Utils+  +  -- Modules included in this library but not exported.+  -- other-modules:       +  +  -- LANGUAGE extensions used by modules in this package.+  default-extensions:    StandaloneDeriving, TypeFamilies, RankNTypes, TemplateHaskell, ImplicitParams, ConstraintKinds, QuasiQuotes, DefaultSignatures, MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, DeriveFunctor, DeriveFoldable, DeriveTraversable+  +  -- Other library packages from which modules are imported.+  build-depends:       base >=4.8 && <5, deepseq >=1.4 && <1.5, lens >=4.12 && <4.15, mtl >=2.2 && <2.3, data-default >=0.5 && <0.8, transformers >=0.4 && <0.6, containers >=0.5 && <0.6, assert >=0.0 && <0.1, either >=4.4 && <4.5, semigroups >=0.16 && <0.19, template-haskell >=2.10 && <2.12, th-lift, th-printf, QuickCheck+  +  ghc-options: -W -fwarn-missing-signatures +         -fwarn-incomplete-uni-patterns+         -fwarn-missing-methods+         -fno-ignore-asserts+         -fwarn-tabs+         -j8++  -- Directories containing source files.+  hs-source-dirs:      .+  +  -- Base language which the package is written in.+  default-language:    Haskell2010