packages feed

quickspec 2.1.5 → 2.2

raw patch · 24 files changed

+607/−186 lines, 24 filesdep ~QuickCheckdep ~basedep ~twee-lib

Dependency ranges changed: QuickCheck, base, twee-lib

Files

examples/Zip.hs view
@@ -10,6 +10,6 @@ main = quickSpec [   -- Explore bigger terms.   withMaxTermSize 8,-  con "++" ((++) @ Int),-  con "zip" (zip @ Int @ Int),-  predicate "eqLen" (eqLen @ Int @ Int) ]+  con "++" ((++) @Int),+  con "zip" (zip @Int @Int),+  predicate "eqLen" (eqLen @Int @Int) ]
quickspec.cabal view
@@ -1,5 +1,5 @@ Name:                quickspec-Version:             2.1.5+Version:             2.2 Cabal-version:       >= 1.10 Build-type:          Simple @@ -101,9 +101,9 @@     QuickSpec.Internal.Utils    Build-depends:-    QuickCheck >= 2.10,+    QuickCheck >= 2.14.2,     quickcheck-instances >= 0.3.16,-    base >= 4 && < 5,+    base >= 4.7 && < 5,     constraints,     containers,     data-lens-light >= 0.1.1,@@ -112,5 +112,5 @@     spoon,     template-haskell,     transformers,-    twee-lib == 2.2,+    twee-lib,     uglymemo
src/QuickSpec.hs view
@@ -31,7 +31,8 @@ -- -- You can only declare monomorphic types with `monoType`. If you want to test -- your own polymorphic types, you must explicitly declare `Arbitrary` and `Ord`--- instances using the `inst` function.+-- instances using the `inst` function. You can also use the `generator` function+-- to use a custom generator instead of the `Arbitrary` instance for a given type. -- -- You can also use QuickSpec to find conditional equations. To do so, you need -- to include some /predicates/ in the signature. These are functions returning@@ -74,7 +75,7 @@   A, B, C, D, E,    -- * Declaring types-  monoType, monoTypeObserve, Observe(..), inst,+  monoType, monoTypeObserve, Observe(..), inst, generator,   vars, monoTypeWithVars, monoTypeObserveWithVars,   variableUse, VariableUse(..),   @@ -93,9 +94,10 @@   type (==>), liftC, instanceOf,    -- * Customising QuickSpec-  withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,+  withMaxTermSize, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,   withPruningDepth, withPruningTermSize, withFixedSeed,   withInferInstanceTypes, withPrintStyle, PrintStyle(..),+  withConsistencyCheck,    -- * Integrating with QuickCheck   (=~=),
src/QuickSpec/Internal.hs view
@@ -1,17 +1,19 @@ -- | The main QuickSpec module, with internal stuff exported. -- For QuickSpec hackers only.+{-# LANGUAGE Haskell2010 #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-}+{-# LANGUAGE GADTs #-} module QuickSpec.Internal where -import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..))+import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..), HasFriendly, FriendlyPredicateTestCase) import qualified QuickSpec.Internal.Haskell as Haskell import qualified QuickSpec.Internal.Haskell.Resolve as Haskell import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck@@ -27,7 +29,9 @@ import QuickSpec.Internal.Type hiding (defaultTo) import Data.Proxy import System.Environment+#if !MIN_VERSION_base(4,9,0) import Data.Semigroup(Semigroup(..))+#endif  -- | Run QuickSpec. See the documentation at the top of this file. quickSpec :: Signature sig => sig -> IO ()@@ -116,6 +120,10 @@ -- It will appear in equations just like any other constant, -- but will also be allowed to appear as a condition. --+-- Warning: if the predicate is unlikely to be true for a+-- randomly-generated value, you will get bad-quality test data.+-- In that case, use `predicateGen` instead.+-- -- For example: -- -- @@@ -125,6 +133,7 @@ --   predicate "member" (member :: Int -> [Int] -> Bool) ] -- @ predicate :: ( Predicateable a+             , Haskell.PredicateResult a ~ Bool              , Typeable a              , Typeable (PredicateTestCase a))              => String -> a -> Sig@@ -139,11 +148,23 @@ -- It will appear in equations just like any other constant, -- but will also be allowed to appear as a condition. -- The third argument is a generator for values satisfying the predicate.+--+-- For example, this declares a predicate that checks if a list is+-- sorted:+--+-- > predicateGen "sorted" sorted genSortedList+--+-- where+--+-- > sorted :: [a] -> Bool+-- > sorted xs = sort xs == xs+-- > genSortedList :: Gen [a]+-- > genSortedList = sort <$> arbitrary predicateGen :: ( Predicateable a                 , Typeable a-                , Typeable b-                , Typeable (PredicateTestCase a))-                => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig+                , Typeable (PredicateTestCase a)+                , HasFriendly (PredicateTestCase a))+                => String -> a -> Gen (FriendlyPredicateTestCase a) -> Sig predicateGen name x gen =   Sig $ \ctx@(Context _ names) ->     if name `elem` names then id else@@ -152,6 +173,17 @@  -- | Declare a new monomorphic type. -- The type must implement `Ord` and `Arbitrary`.+--+-- If the type does not implement `Ord`, you can use `monoTypeObserve`+-- to declare an observational equivalence function. If the type does+-- not implement `Arbitrary`, you can use `generator` to declare a+-- custom QuickCheck generator.+--+-- You do not necessarily need `Ord` and `Arbitrary` instances for+-- every type. If there is no `Ord` (or `Observe` instance) for a+-- type, you will not get equations between terms of that type. If+-- there is no `Arbitrary` instance (or generator), you will not get+-- variables of that type. monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig monoType _ =   mconcat [@@ -234,7 +266,6 @@ variableUse x _ = instFun (Use x :: Use a)  -- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and--- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and -- `Arbitrary` instance for each type you want it to test. -- -- For example, if you are testing @`Data.Map.Map` k v@, you will need to add@@ -244,9 +275,22 @@ -- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B)) -- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B)) -- @+--+-- For a monomorphic type @T@, you can use `monoType` instead, but if you+-- want to use `inst`, you can do it like this:+--+-- @+-- `inst` (`Sub` `Dict` :: () `:-` Ord T)+-- `inst` (`Sub` `Dict` :: () `:-` Arbitrary T)+-- @ inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig inst = instFun +-- | Declare a generator to be used to produce random values of a+-- given type. This will take precedence over any `Arbitrary` instance.+generator :: Typeable a => Gen a -> Sig+generator = instFun+ -- | Declare an arbitrary value to be used by instance resolution. instFun :: Typeable a => a -> Sig instFun x = addInstances (Haskell.inst x)@@ -316,6 +360,10 @@ withMaxCommutativeSize :: Int -> Sig withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n) +-- | Limit how many different function symbols can occur in a term.+withMaxFunctions :: Int -> Sig+withMaxFunctions n = Sig (\_ -> setL Haskell.lens_max_functions n)+ -- | Set how many times to test each discovered law (default: 1000). withMaxTests :: Int -> Sig withMaxTests n =@@ -364,6 +412,11 @@ -- available type class instances withInferInstanceTypes :: Sig withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)++-- | (Experimental) Check that the discovered laws do not imply any+-- false laws+withConsistencyCheck :: Sig+withConsistencyCheck = Sig (\_ -> setL (Haskell.lens_check_consistency) True)  -- | A signature containing boolean functions: -- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
src/QuickSpec/Internal/Explore.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts, PatternGuards #-}+{-# LANGUAGE FlexibleContexts, PatternGuards, CPP #-} module QuickSpec.Internal.Explore where  import QuickSpec.Internal.Explore.Polymorphic@@ -14,7 +14,9 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Text.Printf+#if! MIN_VERSION_base(4,9,0) import Data.Semigroup(Semigroup(..))+#endif import Data.List  newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }@@ -62,7 +64,7 @@   (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, PrettyTerm fun,   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>   (Prop (Term fun) -> m ()) ->-  (Term fun -> testcase -> result) ->+  (Term fun -> testcase -> Maybe result) ->   Int -> Int -> (Type -> VariableUse) -> Universe -> Enumerator (Term fun) -> m () quickSpec present eval maxSize maxCommutativeSize use univ enum = do   let
src/QuickSpec/Internal/Explore/Conditionals.hs view
@@ -11,8 +11,8 @@ {-# LANGUAGE DeriveFunctor #-} module QuickSpec.Internal.Explore.Conditionals where -import QuickSpec.Internal.Prop-import QuickSpec.Internal.Term+import QuickSpec.Internal.Prop as Prop+import QuickSpec.Internal.Term as Term import QuickSpec.Internal.Type import QuickSpec.Internal.Pruning import QuickSpec.Internal.Pruning.Background(Background(..))@@ -37,10 +37,17 @@     return (norm . fmap Normal)   add prop = do     redundant <- conditionallyRedundant prop-    unless redundant $ do-      lift (add (mapFun Normal prop))+    if redundant then return False else do+      res <- lift (add (Prop.mapFun Normal prop))       considerConditionalising prop+      return res +  decodeNormalForm hole t = lift $ do+    t <- decodeNormalForm (fmap (fmap Normal) . hole) t+    let f (Normal x) = Just x+        f _ = Nothing+    return $ t >>= sequence . Term.mapFun f+ conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe conditionalsUniverse tys funs =   universe $@@ -84,7 +91,7 @@   termStyle (Normal f) = termStyle f  instance (Predicate fun, Background fun) => Background (WithConstructor fun) where-  background (Normal f) = map (mapFun Normal) (background f)+  background (Normal f) = map (Prop.mapFun Normal) (background f)   background _ = []  instance Typed fun => Typed (WithConstructor fun) where
src/QuickSpec/Internal/Explore/Polymorphic.hs view
@@ -17,7 +17,7 @@  import qualified QuickSpec.Internal.Explore.Schemas as Schemas import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..), VariableUse(..))-import QuickSpec.Internal.Term+import QuickSpec.Internal.Term hiding (mapFun) import QuickSpec.Internal.Type import QuickSpec.Internal.Testing import QuickSpec.Internal.Pruning@@ -34,6 +34,7 @@ import qualified Twee.Base as Twee import Control.Monad import qualified Data.DList as DList+import Data.Maybe  data Polymorphic testcase result fun norm =   Polymorphic {@@ -60,7 +61,7 @@   (Type -> VariableUse) ->   Universe ->   (Term fun -> Bool) ->-  (Term fun -> testcase -> result) ->+  (Term fun -> testcase -> Maybe result) ->   Polymorphic testcase result fun norm initialState use univ inst eval =   Polymorphic {@@ -125,11 +126,19 @@   add prop = PolyM $ do     univ <- access univ     let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))-    mapM_ add insts+    or <$> mapM add insts +  normTheorems = PolyM normTheorems++  decodeNormalForm hole t =+    PolyM $ do+      t <- decodeNormalForm (fmap (fmap fun_specialised) . hole) t+      return $ fmap (fmap (\f -> PolyFun f f)) t+ instance MonadTester testcase (Term fun) m =>   MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where   test prop = PolyM $ lift (test (mapFun fun_original prop))+  retest testcase prop = PolyM $ lift (retest testcase (mapFun fun_original prop))  -- Given a property which only contains one type variable, -- add as much polymorphism to the property as possible.@@ -223,17 +232,32 @@             ho <- arrows fun,             sub <- typeInstancesList univBase (components fun) ]   -    -- Now close the type universe under "anti-substitution":-    -- if u = typeSubst sub t, and u is in the universe, then-    -- oneTypeVar t should be in the universe.-    -- In practice this means replacing arbitrary subterms of-    -- each type with a type variable.-    univ = fixpoint (usort . oneTypeVar . concatMap antisubst) univHo+    -- Finally, close the universe under the following operations:+    -- * Unifying two types+    -- * Unifying a function's argument with another type+    --   (the closure includes the function type, the argument type+    --   and the result type)+    -- but only if some type in the universe is an instance of the+    -- resulting type. The idea is that, if some term can be built+    -- whose type is a generalisation of the type in the universe,+    -- that generalised type should also be in the universe.+    univ = oneTypeVar (fixpoint (usort . map canonicaliseType . mgus . prune) univHo)       where-        antisubst ty =-          ty:-          [ Twee.build (Twee.replacePosition n (Twee.var (Twee.V 0)) (Twee.singleton ty))-          | n <- [0..Twee.len ty-1] ]+        prune tys = filter (not . subsumed) tys+          where+            subsumed ty =+              or [oneTypeVar pat == oneTypeVar ty && isJust (matchType pat ty) && isNothing (matchType ty pat) | pat <- tys]+        mgus tys =+          tys +++          [ ty+          | ty1 <- tys, ty2 <- tys, +            ty <- unPoly <$> combine (poly ty1) (poly ty2),+            or [isJust (matchType ty bound) | bound <- tys] ]+        combine ty1 ty2 =+          catMaybes [polyMgu ty1 ty2 | ty1 < ty2] +++          maybeToList (tryApply ty1 ty2) +++          -- Get the function and argument types used by tryApply+          concat [[poly x, poly y] | (x, y) <- maybeToList (unPoly <$> polyFunctionMgu ty1 ty2)]      components ty =       case unpackArrow ty of
src/QuickSpec/Internal/Explore/Schemas.hs view
@@ -22,7 +22,7 @@ import Data.Set(Set) import Data.Maybe import Control.Monad-import Twee.Label+import Data.Label  -- | Constrains how variables of a particular type may occur in a term. data VariableUse =@@ -51,7 +51,7 @@ initialState ::   (Type -> VariableUse) ->   (Term fun -> Bool) ->-  (Term fun -> testcase -> result) ->+  (Term fun -> testcase -> Maybe result) ->   Schemas testcase result fun norm initialState use inst eval =   Schemas {@@ -141,8 +141,8 @@       res <- Terms.explore t       case res of         Terms.Discovered prop -> do-          add prop-          return (Just prop)+          res <- add prop+          if res then return (Just prop) else return Nothing         _ -> return Nothing)  -- sortBy (comparing generality) should give most general instances first.
src/QuickSpec/Internal/Explore/Terms.hs view
@@ -37,7 +37,7 @@ treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree)  initialState ::-  (term -> testcase -> result) ->+  (term -> testcase -> Maybe result) ->   Terms testcase result term norm initialState eval =   Terms {@@ -73,9 +73,11 @@   exp norm $ \prop -> do     res <- test prop     case res of-      Nothing -> do+      Untestable ->+        return Singleton+      TestPassed -> do         return (Discovered prop)-      Just tc -> do+      TestFailed tc -> do         treeForType ty %= addTestCase tc         exp norm $           error "returned counterexample failed to falsify property"
src/QuickSpec/Internal/Haskell.hs view
@@ -1,4 +1,6 @@ {-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE Haskell2010 #-}+{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-}@@ -8,7 +10,6 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DefaultSignatures #-}@@ -31,6 +32,7 @@ import Test.QuickCheck.Gen.Unsafe import Data.Char import Data.Ord+import QuickSpec.Internal.Testing import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck import qualified QuickSpec.Internal.Pruning.Twee as Twee import QuickSpec.Internal.Explore hiding (quickSpec)@@ -48,7 +50,7 @@ import Control.Spoon import qualified Data.Set as Set import qualified Test.QuickCheck.Poly as Poly-import Numeric.Natural+import Numeric.Natural(Natural) import Test.QuickCheck.Instances() import Data.Word import Data.List.NonEmpty (NonEmpty)@@ -60,6 +62,9 @@ import Data.Unique import qualified Data.Monoid as DM import qualified Data.Semigroup as DS+import qualified Data.Map.Strict as Map+import Test.QuickCheck.Gen+import Test.QuickCheck.Random  baseInstances :: Instances baseInstances =@@ -256,8 +261,10 @@   observe t = observe t . DM.getFirst instance Observe t p a => Observe t (Maybe p) (DM.Last a) where   observe t = observe t . DM.getLast+#if !MIN_VERSION_base(4,16,0) instance Observe t p a => Observe t (Maybe p) (DS.Option a) where   observe t = observe t . DS.getOption+#endif instance Observe t p a => Observe t (Maybe p) (Maybe a) where   observe t (Just a) = Just $ observe t a   observe _ Nothing  = Nothing@@ -367,15 +374,14 @@ arbitraryFunction gen = promote (\x -> coarbitrary x (gen x))  -- | Evaluate a Haskell term in an environment.-evalHaskell :: Type -> Instances -> TestCase -> Term Constant -> Either (Value Ordy) (Term Constant)-evalHaskell def insts (TestCase env obs) t =-  maybe (Right t) Left $ do-    let eval env t = evalTerm env (evalConstant insts) t-    Identity val `In` w <- unwrap <$> eval env (defaultTo def t)-    res <- obs (wrap w (Identity val))-    -- Don't allow partial results to enter the decision tree-    guard (withValue res (\(Ordy x) -> isJust (teaspoon (x == x))))-    return res+evalHaskell :: Type -> Instances -> TestCase -> Term Constant -> Maybe (Value Ordy)+evalHaskell def insts (TestCase env obs) t = do+  let eval env t = evalTerm env (evalConstant insts) t+  Identity val `In` w <- unwrap <$> eval env (defaultTo def t)+  res <- obs (wrap w (Identity val))+  -- Don't allow partial results to enter the decision tree+  guard (withValue res (\(Ordy x) -> isJust (teaspoon (x == x))))+  return res  data Constant =   Constant {@@ -385,7 +391,8 @@     con_type :: Type,     con_constraints :: [Type],     con_size :: Int,-    con_classify :: Classification Constant }+    con_classify :: Classification Constant,+    con_is_hole :: Bool }  instance Eq Constant where   x == y =@@ -418,7 +425,8 @@     con_type = ty,     con_constraints = constraints,     con_size = 1,-    con_classify = Function }+    con_classify = Function,+    con_is_hole = False }   where     (constraints, ty) = splitConstrainedType (typ val) @@ -487,33 +495,51 @@   --   -- Some speedup should be possible by using unboxed tuples instead...   type PredicateTestCase a-  uncrry :: a -> PredicateTestCase a -> Bool+  type PredicateResult a+  uncrry :: a -> PredicateTestCase a -> PredicateResult a+  true :: proxy a -> Constant  instance Predicateable Bool where   type PredicateTestCase Bool = ()+  type PredicateResult Bool = Bool   uncrry = const+  true _ = con "True" True  instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where   type PredicateTestCase (a -> b) = (a, PredicateTestCase b)+  type PredicateResult (a -> b) = PredicateResult b   uncrry f (a, b) = uncrry (f a) b--data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }+  true _ = true (Proxy :: Proxy b) -true :: Constant-true = con "True" True+-- A more user-friendly type for PredicateTestCase.+type FriendlyPredicateTestCase a = Friendly (PredicateTestCase a)+class HasFriendly a where+  type Friendly a+  unfriendly :: Friendly a -> a+instance HasFriendly () where+  type Friendly () = ()+  unfriendly () = ()+instance HasFriendly (a, ()) where+  type Friendly (a, ()) = a+  unfriendly a = (a, ())+instance HasFriendly (a, (b, ())) where+  type Friendly (a, (b, ())) = (a, b)+  unfriendly (a, b) = (a, (b, ()))+instance HasFriendly (a, (b, (c, ()))) where+  type Friendly (a, (b, (c, ()))) = (a, b, c)+  unfriendly (a, b, c) = (a, (b, (c, ())))+instance HasFriendly (a, (b, (c, (d, ())))) where+  type Friendly (a, (b, (c, (d, ())))) = (a, b, c, d)+  unfriendly (a, b, c, d) = (a, (b, (c, (d, ())))) -trueTerm :: Term Constant-trueTerm = Fun true+data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a } --- | Declare a predicate with a given name and value.--- The predicate should have type @... -> Bool@.--- Uses an explicit generator.-predicateGen :: forall a b. ( Predicateable a-             , Typeable a-             , Typeable b-             , Typeable (PredicateTestCase a))-             => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)-predicateGen name pred gen =+unfriendlyPredicateGen :: forall a b. ( Predicateable a+                       , Typeable a+                       , Typeable b+                       , Typeable (PredicateTestCase a))+                       => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)+unfriendlyPredicateGen name pred gen =   let     -- The following doesn't compile on GHC 7.10:     -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))@@ -541,7 +567,7 @@     inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))     inst2 = Names [name ++ "_var"] -    conPred = (con name pred) { con_classify = Predicate conSels ty (Fun true) }+    conPred = (con name pred) { con_classify = Predicate conSels ty (Fun (true (Proxy :: Proxy a))) }     conSels = [ (constant' (name ++ "_" ++ show i) (select (i + length (con_constraints conPred)))) { con_classify = Selector i conPred ty, con_size = 0 } | i <- [0..typeArity (typ conPred)-1] ]      select i =@@ -559,11 +585,23 @@  -- | Declare a predicate with a given name and value. -- The predicate should have type @... -> Bool@.+-- Uses an explicit generator.+predicateGen :: forall a. ( Predicateable a+             , Typeable a+             , Typeable (PredicateTestCase a)+             , HasFriendly (PredicateTestCase a))+             => String -> a -> (Gen (FriendlyPredicateTestCase a)) -> (Instances, Constant)+predicateGen name pred gen =+  unfriendlyPredicateGen name pred (\() -> unfriendly <$> gen)++-- | Declare a predicate with a given name and value.+-- The predicate should have type @... -> Bool@. predicate :: forall a. ( Predicateable a+          , PredicateResult a ~ Bool           , Typeable a           , Typeable (PredicateTestCase a))           => String -> a -> (Instances, Constant)-predicate name pred = predicateGen name pred inst+predicate name pred = unfriendlyPredicateGen name pred inst   where     inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)     inst Dict = arbitrary `suchThat` uncrry pred@@ -580,6 +618,7 @@     cfg_twee :: Twee.Config,     cfg_max_size :: Int,     cfg_max_commutative_size :: Int,+    cfg_max_functions :: Int,     cfg_instances :: Instances,     -- This represents the constants for a series of runs of QuickSpec.     -- Each index in cfg_constants represents one run of QuickSpec.@@ -589,13 +628,15 @@     cfg_infer_instance_types :: Bool,     cfg_background :: [Prop (Term Constant)],     cfg_print_filter :: Prop (Term Constant) -> Bool,-    cfg_print_style :: PrintStyle+    cfg_print_style :: PrintStyle,+    cfg_check_consistency :: Bool     }  lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x }) lens_twee = lens cfg_twee (\x y -> y { cfg_twee = x }) lens_max_size = lens cfg_max_size (\x y -> y { cfg_max_size = x }) lens_max_commutative_size = lens cfg_max_commutative_size (\x y -> y { cfg_max_commutative_size = x })+lens_max_functions = lens cfg_max_functions (\x y -> y { cfg_max_functions = x }) lens_instances = lens cfg_instances (\x y -> y { cfg_instances = x }) lens_constants = lens cfg_constants (\x y -> y { cfg_constants = x }) lens_default_to = lens cfg_default_to (\x y -> y { cfg_default_to = x })@@ -603,6 +644,7 @@ lens_background = lens cfg_background (\x y -> y { cfg_background = x }) lens_print_filter = lens cfg_print_filter (\x y -> y { cfg_print_filter = x }) lens_print_style = lens cfg_print_style (\x y -> y { cfg_print_style = x })+lens_check_consistency = lens cfg_check_consistency (\x y -> y { cfg_check_consistency = x })  defaultConfig :: Config defaultConfig =@@ -611,13 +653,15 @@     cfg_twee = Twee.Config { Twee.cfg_max_term_size = minBound, Twee.cfg_max_cp_depth = maxBound },     cfg_max_size = 7,     cfg_max_commutative_size = 5,+    cfg_max_functions = maxBound,     cfg_instances = mempty,     cfg_constants = [],     cfg_default_to = typeRep (Proxy :: Proxy Int),     cfg_infer_instance_types = False,     cfg_background = [],     cfg_print_filter = \_ -> True,-    cfg_print_style = ForHumans }+    cfg_print_style = ForHumans,+    cfg_check_consistency = False }  -- Extra types for the universe that come from in-scope instances. instanceTypes :: Instances -> Config -> [Type]@@ -689,7 +733,9 @@ quickSpec cfg@Config{..} = do   let     constantsOf f =-      [true | any (/= Function) (map classify (f cfg_constants))] +++      usort (concatMap funs $+        [clas_true | Predicate{..} <- map classify (f cfg_constants)] +++        [clas_true (classify clas_pred) | Selector{..} <- map classify (f cfg_constants)]) ++       f cfg_constants ++ concatMap selectors (f cfg_constants)     constants = constantsOf concat @@ -699,17 +745,20 @@     eval = evalHaskell cfg_default_to instances     was_observed = isNothing . findOrdInstance instances  -- it was observed if there is no Ord instance directly in scope +    prettierProp funs norm = prettyDefinition funs . prettyAC norm . conditionalise+    prettiestProp funs norm = prettyProp (names instances) . prettierProp funs norm+     present funs prop = do       norm <- normaliser-      let prop' = prettyDefinition funs (prettyAC norm (conditionalise prop))-      when (cfg_print_filter prop) $ do+      let prop' = prettierProp funs norm prop+      when (not (hasBackgroundPredicates prop') && not (isBackgroundProp prop') && cfg_print_filter prop) $ do         (n :: Int, props) <- get-        put (n+1, prop':props)+        put (n+1, props)         putLine $           case cfg_print_style of             ForHumans ->               printf "%3d. %s" n $ show $-                prettyProp (names instances) prop' <+> disambiguatePropType prop+                prettiestProp funs norm prop <+> disambiguatePropType prop             ForQuickCheck ->               renderStyle (style {lineLength = 78}) $ nest 2 $                 prettyPropQC@@ -720,6 +769,22 @@                   prop'                   <+> disambiguatePropType prop +    hasBackgroundPredicates (_ :=>: t :=: u)+      | not (null [p | p <- funs t, isBackgroundPredicate p]),+        not (null [q | q <- funs u, isBackgroundPredicate q]) =+        True+    hasBackgroundPredicates _ = False+    isBackgroundPredicate p =+      p `elem` concat (take 1 cfg_constants) &&+      case classify p of+        Predicate{} -> True+        _ -> False++    isBackgroundProp p =+      not (null fs) && and [f `elem` concat (take 1 cfg_constants) | f <- fs]+      where+        fs = funs p+     -- XXX do this during testing     constraintsOk = memo $ \con ->       or [ and [ isJust (findValue instances (defaultTo cfg_default_to constraint)) | constraint <- con_constraints (typeSubst sub con) ]@@ -729,6 +794,7 @@     enumerator cons =       sortTerms measure $       filterEnumerator (all constraintsOk . funs) $+      filterEnumerator (\t -> length (usort (funs t)) <= cfg_max_functions) $       filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $       enumerateConstants atomic `mappend` enumerateApplications       where@@ -751,7 +817,10 @@         when (cfg_print_style == ForQuickCheck) $ do           putLine "quickspec_laws :: [(String, Property)]"           putLine "quickspec_laws ="-      let pres = if n == 0 then \_ -> return () else present (constantsOf f)+      let+        pres prop = do+          modify $ \(k, props) -> (k, prop:props)+          if n == 0 then return () else present (constantsOf f) prop       QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ         (enumerator (map Fun (constantsOf g)))       when (n > 0) $ do@@ -766,10 +835,54 @@         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))         rounds = length cfg_constants +    -- Used in checkConsistency. Generate a term to be used when a+    -- Twee proof contains a hole ("?"), i.e. a don't-care variable.+    hole ty = do+      -- It doesn't matter what the value of the variable is, so+      -- generate a single random value and use that.+      vgen <- findInstance instances ty :: Maybe (Value Gen)+      let runGen g = Identity (unGen g (mkQCGen 1234) 5)+      return $ Fun $ (constant' "hole" (mapValue runGen vgen)) { con_is_hole = True }++    -- Remove holes by replacing them with a fresh variable.+    removeHoles prop = mapTerm (flatMapFun f) prop+      where+        f con+          | con_is_hole con = Var (V (typ con) n)+          | otherwise = Fun con+        n = freeVar prop++    checkConsistency = do+      thms <- theorems hole+      let numThms = length thms+      norm <- normaliser++      forM_ (zip [1 :: Int ..] thms) $ \(i, thm) -> do+        putStatus (printf "checking laws for consistency: %d/%d" i numThms)+        res <- test (prop thm)+        case res of+          TestFailed testcase -> do+            forM_ (axiomsUsed thm) $ \(ax, insts) ->+              forM_ insts $ \inst -> do+                res <- retest testcase inst+                when (testResult res == TestFailed ()) $ do+                  modify (Map.insertWith Set.union (removeHoles ax) (Set.singleton (removeHoles inst)))+          _ -> return ()++      falseProps <- get+      forM_ (Map.toList falseProps) $ \(ax, insts) -> do+        putLine (printf "*** Law %s is false!" (prettyShow (prettiestProp constants norm ax)))+        putLine "False instances:"+        forM_ (Set.toList insts) $ \inst -> do+          putLine (printf "  %s is false" (prettyShow (prettiestProp constants norm inst)))+        putLine ""+   join $     fmap withStdioTerminal $     generate $     QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $     Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $-    runConditionals constants $-    fmap (reverse . snd) $ flip execStateT (1, []) main+    runConditionals constants $ do+      result <- fmap (reverse . snd) $ flip execStateT (1, []) main+      when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty+      return result
src/QuickSpec/Internal/Haskell/Resolve.hs view
@@ -13,7 +13,7 @@ -- their types must be such that the instance search will terminate.  {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables, CPP #-} module QuickSpec.Internal.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where  import Twee.Base@@ -23,7 +23,9 @@ import Data.Maybe import Data.Proxy import Control.Monad+#if !MIN_VERSION_base(4,9,0) import Data.Semigroup(Semigroup(..))+#endif  -- A set of instances. data Instances =@@ -59,9 +61,9 @@       -- (see comment about is_instances).       case typ x of         -- A function of type a -> (b -> c) gets uncurried.-        App (F Arrow) (Cons _ (Cons (App (F Arrow) _) Empty)) ->+        App (F _ Arrow) (Cons _ (Cons (App (F _ Arrow) _) Empty)) ->           polyInst (apply uncur x)-        App (F Arrow) _ ->+        App (F _ Arrow) _ ->           makeInstances [x]         -- A plain old value x (not a function) turns into \() -> x.         _ ->@@ -92,10 +94,10 @@ -- -- Invariant: the type of the returned value is an instance of the argument type. find_ :: Instances -> Type -> [Value Identity]-find_ _ (App (F unit) Empty)+find_ _ (App (F _ unit) Empty)   | unit == tyCon (Proxy :: Proxy ()) =     return (toValue (Identity ()))-find_ insts (App (F pair) (Cons ty1 (Cons ty2 Empty)))+find_ insts (App (F _ pair) (Cons ty1 (Cons ty2 Empty)))   | pair == tyCon (Proxy :: Proxy (,)) = do     x <- is_find insts ty1     sub <- maybeToList (match ty1 (typ x))@@ -107,7 +109,7 @@   -- Find a function whose result type unifies with ty.   -- Rename it to avoid clashes with ty.   fun <- fmap (polyRename ty) (is_instances insts)-  App (F Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)+  App (F _ Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)   sub <- maybeToList (unify ty res)   fun <- return (typeSubst sub fun)   arg <- return (typeSubst sub arg)
src/QuickSpec/Internal/Parse.hs view
@@ -1,6 +1,6 @@ -- | Parsing strings into properties. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, GADTs, TypeOperators #-} {-# LANGUAGE FlexibleContexts #-} module QuickSpec.Internal.Parse where @@ -9,7 +9,7 @@ import QuickSpec.Internal.Prop import QuickSpec.Internal.Term hiding (char) import QuickSpec.Internal.Type-import qualified Twee.Label as Label+import qualified Data.Label as Label import Text.ParserCombinators.ReadP  class Parse fun a where@@ -20,7 +20,7 @@     x <- satisfy isUpper     xs <- munch isAlphaNum     let name = x:xs-    -- Use Twee.Label as an easy way to generate a variable number+    -- Use Data.Label as an easy way to generate a variable number     return (V typeVar (fromIntegral (Label.labelNum (Label.label name))))  instance (fun1 ~ fun, Apply (Term fun)) => Parse fun1 (Term fun) where
src/QuickSpec/Internal/Prop.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-}+{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators, DeriveTraversable #-} module QuickSpec.Internal.Prop where  import Data.Bool (bool)@@ -19,7 +19,7 @@   (:=>:) {     lhs :: [Equation a],     rhs :: Equation a }-  deriving (Show, Generic, Functor)+  deriving (Show, Generic, Functor, Traversable, Foldable)  instance Symbolic f a => Symbolic f (Prop a) where   termsDL (lhs :=>: rhs) =@@ -43,6 +43,11 @@ mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2) mapFun f = fmap (fmap f) +mapTerm :: (Term fun1 -> Term fun2) -> Prop (Term fun1) -> Prop (Term fun2)+mapTerm f (lhs :=>: rhs) = map (both f) lhs :=>: both f rhs+  where+    both f (t :=: u) = f t :=: f u+ instance Typed a => Typed (Prop a) where   typ _ = typeOf True   otherTypesDL p = DList.fromList (literals p) >>= typesDL@@ -54,7 +59,7 @@   pPrint p =     hsep (punctuate (text " &") (map pPrint (lhs p))) <+> text "=>" <+> pPrint (rhs p) -data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor)+data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor, Traversable, Foldable)  instance Symbolic f a => Symbolic f (Equation a) where   termsDL (t :=: u) = termsDL t `mplus` termsDL u
src/QuickSpec/Internal/Pruning.hs view
@@ -1,25 +1,65 @@ -- A type of pruners. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs #-}+{-# LANGUAGE FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs, TypeOperators, DeriveFunctor, DeriveTraversable #-} module QuickSpec.Internal.Pruning where  import QuickSpec.Internal.Prop import QuickSpec.Internal.Testing+import QuickSpec.Internal.Type(Type)+import Twee.Pretty import Control.Monad.Trans.Class import Control.Monad.IO.Class import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Reader+import Data.Maybe +data Theorem norm =+  Theorem {+    prop :: Prop norm,+    axiomsUsed :: [(Prop norm, [Prop norm])] }+  deriving (Functor, Foldable, Traversable)++instance Pretty norm => Pretty (Theorem norm) where+  pPrint thm =+    (text "prop =" <+> pPrint (prop thm)) $$+    (text "axioms used =" <+> pPrint (axiomsUsed thm))+ class Monad m => MonadPruner term norm m | m -> term norm where   normaliser :: m (term -> norm)-  add :: Prop term -> m ()+  add :: Prop term -> m Bool+  decodeNormalForm :: (Type -> Maybe term) -> norm -> m (Maybe term)+  normTheorems :: m [Theorem norm]    default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm)   normaliser = lift normaliser -  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m ()+  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool   add = lift . add +  default normTheorems :: (MonadTrans t, MonadPruner term' norm m', m ~ t m') => m [Theorem norm]+  normTheorems = lift normTheorems++  default decodeNormalForm :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => (Type -> Maybe term) -> norm -> m (Maybe term)+  decodeNormalForm hole t = lift (decodeNormalForm hole t)++decodeTheorem :: MonadPruner term norm m => (Type -> Maybe term) -> Theorem norm -> m (Maybe (Theorem term))+decodeTheorem hole thm = elimMaybeThm <$> mapM (decodeNormalForm hole) thm+  where+    elimMaybeThm (Theorem prop axs) =+      case sequence prop of+        Nothing -> Nothing+        Just prop -> Just (Theorem prop (mapMaybe elimMaybeAx axs))+    elimMaybeAx (ax, insts) =+      case sequence ax of+        Nothing -> Nothing+        Just ax -> Just (ax, mapMaybe elimMaybeInst insts)+    elimMaybeInst = sequence++theorems :: MonadPruner term norm m => (Type -> Maybe term) -> m [Theorem term]+theorems hole = do+  thms <- normTheorems+  catMaybes <$> mapM (decodeTheorem hole) thms+ instance MonadPruner term norm m => MonadPruner term norm (StateT s m) instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m) @@ -36,7 +76,7 @@  instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where   normaliser = ReadOnlyPruner normaliser-  add _ = return ()+  add _ = return True  newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)   deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)@@ -52,4 +92,4 @@ watchPruner (WatchPruner mx) = do   (x, props) <- runStateT mx []   return (x, reverse props)-    +
src/QuickSpec/Internal/Pruning/PartialApplication.hs view
@@ -3,16 +3,15 @@ {-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-} module QuickSpec.Internal.Pruning.PartialApplication where -import QuickSpec.Internal.Term+import QuickSpec.Internal.Term as Term import QuickSpec.Internal.Type import QuickSpec.Internal.Pruning.Background hiding (Pruner) import QuickSpec.Internal.Pruning-import QuickSpec.Internal.Prop+import QuickSpec.Internal.Prop as Prop import QuickSpec.Internal.Terminal import QuickSpec.Internal.Testing import Control.Monad.IO.Class import Control.Monad.Trans.Class-import Twee.Base(Arity(..))  data PartiallyApplied f =     -- A partially-applied function symbol.@@ -67,7 +66,7 @@  instance (Typed f, Background f) => Background (PartiallyApplied f) where   background (Partial f _) =-    map (mapFun (\f -> Partial f arity)) (background f) +++    map (Prop.mapFun (\f -> Partial f arity)) (background f) ++     [ simpleApply (partial n) (vs !! n) === partial (n+1)     | n <- [0..arity-1] ]     where@@ -94,6 +93,13 @@   add prop =     Pruner $ do       add (encode <$> canonicalise prop)++  decodeNormalForm hole t =+    Pruner $ do+      t <- decodeNormalForm (fmap (fmap (flip Partial 0)) . hole) t+      let f (Partial x _) = NotId x+          f (Apply _) = Id+      return $ t >>= eliminateId . Term.mapFun f  encode :: Typed fun => Term fun -> Term (PartiallyApplied fun) encode (Var x) = Var x
src/QuickSpec/Internal/Pruning/Twee.hs view
@@ -16,6 +16,7 @@ import Control.Monad.IO.Class import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))+import Data.Typeable  newtype Pruner fun m a =   Pruner (PartialApplication.Pruner fun (Types.Pruner (PartiallyApplied fun) (Background.Pruner (Tagged (PartiallyApplied fun)) (Untyped.Pruner (Tagged (PartiallyApplied fun)) m))) a)@@ -25,6 +26,6 @@ instance MonadTrans (Pruner fun) where   lift = Pruner . lift . lift . lift . lift -run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a+run :: (Sized fun, Typeable fun, Ord fun, Monad m) => Config -> Pruner fun m a -> m a run config (Pruner x) =   Untyped.run config (Background.run (Types.run (PartialApplication.run x)))
src/QuickSpec/Internal/Pruning/Types.hs view
@@ -1,6 +1,6 @@ -- Encode monomorphic types during pruning. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-} module QuickSpec.Internal.Pruning.Types where  import QuickSpec.Internal.Pruning@@ -8,12 +8,10 @@ import QuickSpec.Internal.Testing import QuickSpec.Internal.Term import QuickSpec.Internal.Type-import QuickSpec.Internal.Prop+import QuickSpec.Internal.Prop hiding (mapFun) import QuickSpec.Internal.Terminal import Control.Monad.IO.Class import Control.Monad.Trans.Class-import qualified Twee.Base as Twee-import Twee.Base(Arity(..))  data Tagged fun =     Func fun@@ -28,9 +26,6 @@   size (Func f) = size f   size (Tag _) = 0 -instance Sized fun => Twee.Sized (Tagged fun) where-  size f = size f `max` 1- instance Pretty fun => Pretty (Tagged fun) where   pPrint (Func f) = pPrint f   pPrint (Tag ty) = text "tag[" <#> pPrint ty <#> text "]"@@ -39,6 +34,13 @@   termStyle (Func f) = termStyle f   termStyle (Tag _) = uncurried +instance Typed fun => Typed (Tagged fun) where+  typ (Func f) = typ f+  typ (Tag ty) = arrowType [ty] ty++  typeSubst_ sub (Func f) = Func (typeSubst_ sub f)+  typeSubst_ sub (Tag ty) = Tag (typeSubst_ sub ty)+ instance EqualsBonus (Tagged fun) where  type TypedTerm fun = Term fun@@ -66,11 +68,18 @@    add prop = lift (add (encode <$> canonicalise prop)) -instance (Typed fun, Twee.Arity fun, Background fun) => Background (Tagged fun) where+  decodeNormalForm hole t =+    Pruner $ do+      t <- decodeNormalForm (fmap (fmap Func) . hole) t+      let f (Func x) = NotId x+          f (Tag _) = Id+      return $ t >>= eliminateId . mapFun f++instance (Typed fun, Arity fun, Background fun) => Background (Tagged fun) where   background = typingAxioms  -- Compute the typing axioms for a function or type tag.-typingAxioms :: (Typed fun, Twee.Arity fun, Background fun) =>+typingAxioms :: (Typed fun, Arity fun, Background fun) =>   Tagged fun -> [Prop (UntypedTerm fun)] typingAxioms (Tag ty) =   [tag ty (tag ty x) === tag ty x]
src/QuickSpec/Internal/Pruning/UntypedTwee.hs view
@@ -16,7 +16,7 @@ import Twee hiding (Config(..)) import Twee.Rule hiding (normalForms) import Twee.Proof hiding (Config, defaultConfig)-import Twee.Base(Ordered(..), Extended(..), Arity(..), EqualsBonus)+import Twee.Base(Ordered(..), Labelled) import Control.Monad.Trans.Reader import Control.Monad.Trans.State.Strict hiding (State) import Control.Monad.Trans.Class@@ -24,6 +24,9 @@ import QuickSpec.Internal.Terminal import qualified Data.Set as Set import Data.Set(Set)+import qualified Data.Map.Strict as Map+import qualified Data.IntMap as IntMap+import Control.Monad  data Config =   Config {@@ -33,9 +36,41 @@ lens_max_term_size = lens cfg_max_term_size (\x y -> y { cfg_max_term_size = x }) lens_max_cp_depth = lens cfg_max_cp_depth (\x y -> y { cfg_max_cp_depth = x }) -instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Twee.Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where+data Extended fun = Minimal | Skolem Twee.Var | Function fun+  deriving (Eq, Ord, Typeable)++instance (Ord fun, Typeable fun) => Labelled (Extended fun)++instance Sized fun => Sized (Extended fun) where+  size (Function f) = size f+  size _ = 1++instance KBO.Sized (Extended fun) where+  size _ = 1++instance Arity fun => Arity (Extended fun) where+  arity (Function f) = arity f+  arity (Skolem _) = 0+  arity Minimal = 0++instance (Ord fun, Typeable fun) => Twee.Minimal (Extended fun) where+  minimal = Twee.fun Minimal++instance EqualsBonus (Extended fun)++instance (Ord fun, Typeable fun, Pretty fun) => Pretty (Extended fun) where+  pPrintPrec l p (Function f) = pPrintPrec l p f+  pPrintPrec _ _ Minimal = text "?"+  pPrintPrec _ _ (Skolem (Twee.V x)) = text ("sk" ++ show x)++instance (Ord fun, Typeable fun, PrettyTerm fun) => PrettyTerm (Extended fun) where+  termStyle (Function f) = termStyle f+  termStyle _ = curried++instance (Sized fun, Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where   lessEq = KBO.lessEq   lessIn = KBO.lessIn+  lessEqSkolem = KBO.lessEqSkolem  newtype Pruner fun m a =   Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)@@ -44,28 +79,26 @@ instance MonadTrans (Pruner fun) where   lift = Pruner . lift . lift -run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a+run :: (Typeable fun, Ord fun, Sized fun, Monad m) => Config -> Pruner fun m a -> m a run Config{..} (Pruner x) =-  evalStateT (runReaderT x config) initialState+  evalStateT (runReaderT x config) (initialState config)   where     config =       defaultConfig {         Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),         Twee.cfg_max_cp_depth = cfg_max_cp_depth } -instance Sized fun => Sized (Twee.Term fun) where+instance (Labelled fun, Sized fun) => Sized (Twee.Term fun) where   size (Twee.Var _) = 1   size (Twee.App f ts) =     size (Twee.fun_value f) + sum (map size (Twee.unpack ts)) -instance Sized fun => Sized (Twee.Extended fun) where-  size Twee.Minimal = 1-  size (Twee.Skolem _) = 1-  size (Twee.Function f) = size f+instance KBO.Weighted (Extended fun) where+  argWeight _ = 1  type Norm fun = Twee.Term (Extended fun) -instance (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>+instance (Ord fun, Typed fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>   MonadPruner (Term fun) (Norm fun) (Pruner fun m) where   normaliser = Pruner $ do     state <- lift get@@ -77,25 +110,65 @@   add ([] :=>: t :=: u) = Pruner $ do     state <- lift get     config <- ask-    lift (put $! addTwee config t u state)+    let (t' :=: u') = canonicalise (t :=: u)+    if not (null (Set.intersection (normalFormsTwee state t') (normalFormsTwee state u'))) then+      return False+    else do+      lift (put $! addTwee config t u state)+      return True    add _ =-    return ()+    return True     --error "twee pruner doesn't support non-unit equalities" -normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>+  decodeNormalForm hole t = return (decode t (error "ambiguously-typed term"))+    where+      decode (Twee.Var (Twee.V n)) ty =+        Just (Var (V ty n))+      decode (Twee.App (Twee.F _ Minimal) Twee.Empty) ty =+        hole ty+      decode (Twee.App (Twee.F _ (Skolem (Twee.V n))) Twee.Empty) ty =+        Just (Var (V ty n))+      decode (Twee.App (Twee.F _ (Function f)) ts) _ =+        (Fun f :@:) <$> zipWithM decode (Twee.unpack ts) args+        where+          args = typeArgs (typ f)+      decode _ _ = error "ill-typed term"++  normTheorems = Pruner $ do+    state <- lift get+    let actives = IntMap.elems (Twee.st_active_set state)+    let+      toTheorem active =+        Theorem+          (toProp (equation proof))+          (map toAxiom . Map.toList . groundAxiomsAndSubsts $ deriv)+        where+          proof = Twee.active_proof active+          deriv = derivation proof+          toProp (t Twee.:=: u) = [] :=>: t :=: u+          toAxiom (ax, subs) = (toProp eqn, map toProp [Twee.subst sub eqn | sub <- Set.toList subs])+            where+              eqn = axiom_eqn ax++    return (map toTheorem actives)++normaliseTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   State (Extended fun) -> Term fun -> Norm fun normaliseTwee state t =-  result (normaliseTerm state (simplifyTerm state (skolemise t)))+  result u (normaliseTerm state u)+  where+    u = simplifyTerm state (skolemise t) -normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>+normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   State (Extended fun) -> Term fun -> Set (Norm fun) normalFormsTwee state t =-  Set.map result (normalForms state (skolemise t))+  Set.fromList . Map.elems $ Map.mapWithKey result (normalForms state (skolemise t)) -addTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>+addTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun) addTwee config t u state =+  interreduce config $   completePure config $     addAxiom config state axiom   where
src/QuickSpec/Internal/Term.hs view
@@ -1,7 +1,7 @@ -- | This module is internal to QuickSpec. -- -- Typed terms and operations on them.-{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts #-}+{-# LANGUAGE PatternSynonyms, ViewPatterns, TypeSynonymInstances, FlexibleInstances, TypeFamilies, ConstraintKinds, DeriveGeneric, DeriveAnyClass, MultiParamTypeClasses, FunctionalDependencies, UndecidableInstances, TypeOperators, DeriveFunctor, FlexibleContexts, DeriveTraversable #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} module QuickSpec.Internal.Term(module QuickSpec.Internal.Term, module Twee.Base, module Twee.Pretty) where @@ -18,10 +18,11 @@ import Data.Map(Map) import Data.List import Data.Ord+import Data.Maybe  -- | A typed term. data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)-  deriving (Eq, Ord, Show, Functor)+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)  -- | A variable, which has a type and a number. data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }@@ -148,6 +149,42 @@ mapVar f (Var x) = Var (f x) mapVar _ (Fun x) = Fun x mapVar f (t :$: u) = mapVar f t :$: mapVar f u++-- | Map a function over function symbols.+mapFun :: (f -> g) -> Term f -> Term g+mapFun _ (Var x) = Var x+mapFun f (Fun x) = Fun (f x)+mapFun f (t :$: u) = mapFun f t :$: mapFun f u++-- | Map a function over function symbols.+flatMapFun :: (f -> Term g) -> Term f -> Term g+flatMapFun _ (Var x) = Var x+flatMapFun f (Fun x) = f x+flatMapFun f (t :$: u) =+  flatMapFun f t :$: flatMapFun f u++-- | A type representing functions which may be the identity.+data OrId f = Id | NotId f++-- | Eliminate the identity function from a term.+eliminateId :: Term (OrId f) -> Maybe (Term f)+eliminateId t = do+  t <- elim t+  case t of+    Id -> Nothing+    NotId t -> Just t+  where+    elim :: Term (OrId f) -> Maybe (OrId (Term f))+    elim (Var x) = Just (NotId (Var x))+    elim (Fun (NotId f)) = Just (NotId (Fun f))+    elim (Fun Id) = Just Id+    elim (t :$: u) = do+      t <- elim t+      u <- elim u+      case (t, u) of+        (Id, _) -> Just u+        (NotId _, Id) -> Nothing+        (NotId t, NotId u) -> Just (NotId (t :$: u))  -- | Find all subterms of a term. Includes the term itself. subterms :: Term f -> [Term f]
src/QuickSpec/Internal/Terminal.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs, TypeOperators #-} module QuickSpec.Internal.Terminal where  import Control.Monad.Trans.Class
src/QuickSpec/Internal/Testing.hs view
@@ -1,6 +1,6 @@ -- A type of test case generators. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances #-}+{-# LANGUAGE FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances, TypeOperators, DeriveFunctor #-} module QuickSpec.Internal.Testing where  import QuickSpec.Internal.Prop@@ -8,11 +8,33 @@ import Control.Monad.Trans.State.Strict import Control.Monad.Trans.Reader +data TestResult testcase =+    TestPassed+  | TestFailed testcase+  | Untestable+  deriving (Functor, Eq)++testResult :: TestResult testcase -> TestResult ()+testResult = fmap (const ())++testAnd :: TestResult testcase -> TestResult testcase -> TestResult testcase+TestPassed `testAnd` x = x+x `testAnd` _ = x++testImplies :: TestResult testcase -> TestResult testcase -> TestResult testcase+TestPassed `testImplies` x = x+TestFailed _ `testImplies` _ = TestPassed+Untestable `testImplies` _ = Untestable+ class Monad m => MonadTester testcase term m | m -> testcase term where-  test :: Prop term -> m (Maybe testcase)+  test :: Prop term -> m (TestResult testcase)+  retest :: testcase -> Prop term -> m (TestResult testcase) -  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (Maybe testcase)+  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (TestResult testcase)   test = lift . test++  default retest :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => testcase -> Prop term -> m (TestResult testcase)+  retest tc = lift . retest tc  instance MonadTester testcase term m => MonadTester testcase term (StateT s m) instance MonadTester testcase term m => MonadTester testcase term (ReaderT r m)
src/QuickSpec/Internal/Testing/DecisionTree.hs view
@@ -9,7 +9,7 @@ data DecisionTree testcase result term =   DecisionTree {     -- A function for evaluating terms on test cases.-    dt_evaluate :: term -> testcase -> result,+    dt_evaluate :: term -> testcase -> Maybe result,     -- The set of test cases gathered so far.     dt_test_cases :: [testcase],     -- The tree itself.@@ -24,7 +24,7 @@   | EqualTo term  -- Make a new decision tree.-empty :: (term -> testcase -> result) -> DecisionTree testcase result term+empty :: (term -> testcase -> Maybe result) -> DecisionTree testcase result term empty eval =   DecisionTree {     dt_evaluate = eval,@@ -50,17 +50,25 @@     k tree = dt{dt_tree = Just tree}     aux _ [] (Singleton y) = EqualTo y     aux k (t:ts) (Singleton y) =-      aux k (t:ts) $-        TestCase (Map.singleton (dt_evaluate y t) (Singleton y)) +      case dt_evaluate y t of+        Nothing ->+          -- y is untestable, so we can evict it from the tree+          Distinct (k (Singleton x))+        Just val ->+          aux k (t:ts) $+            TestCase (Map.singleton val (Singleton y))      aux k (t:ts) (TestCase res) =-      let-        val = dt_evaluate x t-        k' tree = k (TestCase (Map.insert val tree res))-      in case Map.lookup val res of+      case dt_evaluate x t of         Nothing ->-          Distinct (k' (Singleton x))-        Just tree ->-          aux k' ts tree+          Distinct (k (TestCase res))+        Just val ->+          let+            k' tree = k (TestCase (Map.insert val tree res))+          in case Map.lookup val res of+            Nothing ->+              Distinct (k' (Singleton x))+            Just tree ->+              aux k' ts tree     aux _ [] (TestCase _) =       error "unexpected node in decision tree"
src/QuickSpec/Internal/Testing/QuickCheck.hs view
@@ -9,7 +9,6 @@ import Test.QuickCheck import Test.QuickCheck.Gen import Test.QuickCheck.Random-import Control.Monad import Control.Monad.IO.Class import Control.Monad.Trans.Class import Control.Monad.Trans.Reader@@ -33,7 +32,7 @@   Environment {     env_config :: Config,     env_tests :: [testcase],-    env_eval :: testcase -> term -> result }+    env_eval :: testcase -> term -> Maybe result }  newtype Tester testcase term result m a =   Tester (ReaderT (Environment testcase term result) m a)@@ -43,21 +42,25 @@   lift = Tester . lift  run ::-  Config -> Gen testcase -> (testcase -> term -> result) ->+  Config -> Gen testcase -> (testcase -> term -> Maybe result) ->   Tester testcase term result m a -> Gen (m a) run config@Config{..} gen eval (Tester x) = do   seed <- maybe arbitrary return cfg_fixed_seed   let     seeds = unfoldr (Just . split) seed-    n = cfg_num_tests+    n = fromIntegral (ceiling (fromIntegral cfg_num_tests * (1 - zeroProportion)))+    zeroes = cfg_num_tests - n     k = max 1 cfg_max_test_size     bias = 3+    -- Run this proportion of tests of size 0.+    zeroProportion = 0.01     -- Bias tests towards smaller sizes.     -- We do this by distributing the cube of the size uniformly.     sizes =-      reverse $ map (k -) $-      map (truncate . (** (1/fromInteger bias)) . fromIntegral) $-      uniform (toInteger n) (toInteger k^bias)+      replicate zeroes 0 +++      (reverse $ map (k -) $+       map (truncate . (** (1/fromInteger bias)) . fromIntegral) $+       uniform (toInteger n) (toInteger k^bias))     tests = zipWith (unGen gen) seeds sizes   return $ runReaderT x     Environment {@@ -78,20 +81,21 @@ instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where   test prop =     Tester $ do-      env <- ask-      return $! quickCheckTest env prop+      env@Environment{..} <- ask+      return $! foldr testAnd TestPassed (map (quickCheckTest env prop) env_tests)+  retest testcase prop =+    Tester $ do+      env@Environment{..} <- ask+      return $! quickCheckTest env prop testcase  quickCheckTest :: Eq result =>-  Environment testcase term result ->-  Prop term -> Maybe testcase-quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) =-  msum (map test env_tests)+  Environment testcase term result -> Prop term -> testcase -> TestResult testcase+quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) testcase =+  foldr testAnd (testEq rhs) (map testEq lhs)   where-    test testcase = do-        guard $-          all (testEq testcase) lhs &&-          not (testEq testcase rhs)-        return testcase--    testEq testcase (t :=: u) =-      env_eval testcase t == env_eval testcase u+    testEq (t :=: u) =+      case (env_eval testcase t, env_eval testcase u) of+        (Just t, Just u)+          | t == u -> TestPassed+          | otherwise -> TestFailed testcase+        _ -> Untestable
src/QuickSpec/Internal/Type.hs view
@@ -1,12 +1,13 @@ -- | This module is internal to QuickSpec. -- -- Polymorphic types and dynamic values.-{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs #-}+{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds, GADTs, TypeOperators #-} -- To avoid a warning about TyVarNumber's constructor being unused: {-# OPTIONS_GHC -fno-warn-unused-binds #-} module QuickSpec.Internal.Type(   -- * Types   Typeable,+  Arity(..),   Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,   typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,   arrowType, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,@@ -18,7 +19,7 @@   oneTypeVar, defaultTo, skolemiseTypeVars,   -- * Polymorphic types   canonicaliseType,-  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu,+  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu, polyFunctionMgu,   -- * Dynamic values   Value, toValue, fromValue, valueType,   unwrap, Unwrapped(..), Wrapper(..),@@ -35,7 +36,7 @@ import Data.Constraint import Twee.Base import Data.Proxy-import Data.List+import Data.List hiding (singleton) import Data.Char import Data.Functor.Identity @@ -51,8 +52,10 @@     -- | A string. Can be used to represent miscellaneous types that do not     -- really exist in Haskell.   | String String-  deriving (Eq, Ord, Show)+  deriving (Eq, Ord, Show, Typeable) +instance Labelled TyCon+ instance Pretty TyCon where   pPrint Arrow = text "->"   pPrint (String x) = text x@@ -159,20 +162,20 @@ -- -- For multiple-argument functions, unpacks one argument. unpackArrow :: Type -> Maybe (Type, Type)-unpackArrow (App (F Arrow) (Cons t (Cons u Empty))) =+unpackArrow (App (F _ Arrow) (Cons t (Cons u Empty))) =   Just (t, u) unpackArrow _ =   Nothing  -- | The arguments of a function type. typeArgs :: Type -> [Type]-typeArgs (App (F Arrow) (Cons arg (Cons res Empty))) =+typeArgs (App (F _ Arrow) (Cons arg (Cons res Empty))) =   arg:typeArgs res typeArgs _ = []  -- | The result of a function type. typeRes :: Type -> Type-typeRes (App (F Arrow) (Cons _ (Cons res Empty))) =+typeRes (App (F _ Arrow) (Cons _ (Cons res Empty))) =   typeRes res typeRes ty = ty @@ -180,7 +183,7 @@ -- @n@ arguments. Crashes if the type does not have enough arguments. typeDrop :: Int -> Type -> Type typeDrop 0 ty = ty-typeDrop n (App (F Arrow) (Cons _ (Cons ty Empty))) =+typeDrop n (App (F _ Arrow) (Cons _ (Cons ty Empty))) =   typeDrop (n-1) ty typeDrop _ _ =   error "typeDrop on non-function type"@@ -235,7 +238,7 @@  -- | Check if a type is of the form @`Dict` c@, and if so, return @c@. getDictionary :: Type -> Maybe Type-getDictionary (App (F (TyCon dict)) (Cons ty Empty))+getDictionary (App (F _ (TyCon dict)) (Cons ty Empty))   | dict == dictTyCon = Just ty getDictionary _ = Nothing @@ -259,9 +262,9 @@   coarbitrary = coarbitrary . singleton instance CoArbitrary (TermList TyCon) where   coarbitrary Empty = variant 0-  coarbitrary (ConsSym (Var (V x)) ts) =+  coarbitrary ConsSym{hd = Var (V x), rest = ts} =     variant 1 . coarbitrary x . coarbitrary ts-  coarbitrary (ConsSym (App f _) ts) =+  coarbitrary ConsSym{hd = App f _, rest = ts} =     variant 2 . coarbitrary (fun_id f) . coarbitrary ts  -- | Pretty-print a type. Differs from the `Pretty` instance by printing type@@ -355,7 +358,7 @@   typeSubst_ = subst  instance Apply Type where-  tryApply (App (F Arrow) (Cons arg (Cons res Empty))) t+  tryApply (App (F _ Arrow) (Cons arg (Cons res Empty))) t     | t == arg = Just res   tryApply _ _ = Nothing @@ -426,6 +429,12 @@   sub <- unify ty1' ty2'   return (poly (typeSubst sub ty1')) +polyFunctionMgu :: Apply a => Poly a -> Poly a -> Maybe (Poly (a, a))+polyFunctionMgu f x = do+  let (f', (x', resType)) = unPoly (polyPair f (polyPair x (poly (build (var (V 0))))))+  s <- unify (typ f') (arrowType [typ x'] resType)+  return (poly (typeSubst s (f', x')))+ instance Typed a => Typed (Poly a) where   typ = typ . unPoly   otherTypesDL = otherTypesDL . unPoly@@ -433,10 +442,8 @@  instance Apply a => Apply (Poly a) where   tryApply f x = do-    let (f', (x', resType)) = unPoly (polyPair f (polyPair x (poly (build (var (V 0))))))-    s <- unify (typ f') (arrowType [typ x'] resType)-    let (f'', x'') = typeSubst s (f', x')-    fmap poly (tryApply f'' x'')+    (f', x') <- unPoly <$> polyFunctionMgu f x+    fmap poly (tryApply f' x')  -- | Convert an ordinary value to a dynamic value. toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)@@ -560,3 +567,7 @@   case unwrap val of     x `In` w ->       fmap (wrap w . Identity) x++class Arity f where+  -- | Measure the arity.+  arity :: f -> Int