packages feed

quickspec 2.1 → 2.1.1

raw patch · 16 files changed

+281/−159 lines, 16 filesdep ~quickcheck-instances

Dependency ranges changed: quickcheck-instances

Files

examples/ListMonad.hs view
@@ -3,6 +3,7 @@ import QuickSpec  main = quickSpec [+  withMaxTestSize 20,   con "return" (return :: A -> [A]),   con ">>=" ((>>=) :: [A] -> (A -> [B]) -> [B]),   con "++" ((++) :: [A] -> [A] -> [A]),
quickspec.cabal view
@@ -1,5 +1,5 @@ Name:                quickspec-Version:             2.1+Version:             2.1.1 Cabal-version:       >= 1.6 Build-type:          Simple @@ -100,7 +100,7 @@    Build-depends:     QuickCheck >= 2.10,-    quickcheck-instances >= 0.3.15,+    quickcheck-instances >= 0.3.16,     base >= 4 && < 5,     constraints,     containers,
src/QuickSpec.hs view
@@ -69,7 +69,7 @@   quickSpec, Sig, Signature(..),    -- * Declaring functions and predicates-  con, predicate,+  con, predicate, predicateGen,   -- ** Type variables for polymorphic functions   A, B, C, D, E, @@ -95,10 +95,11 @@   -- * Re-exported functionality   Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary, -  -- * Advanced use-  quickSpecResult) where+  -- * For QuickSpec hackers+  unSig, Context(..), SingleUse(..), NoWarnings(..),+  quickSpecResult, addBackground, addInstances, instFun, customConstant, withPrintFilter, withMaxCommutativeSize) where -import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))+import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), SingleUse(..), NoWarnings(..)) import qualified QuickSpec.Haskell as Haskell import qualified QuickSpec.Haskell.Resolve as Haskell import qualified QuickSpec.Testing.QuickCheck as QuickCheck@@ -134,6 +135,11 @@    Haskell.quickSpec (runSig sig' (Context 1 []) Haskell.defaultConfig) +-- | Add some properties to the background theory.+addBackground :: [Prop (Term (PartiallyApplied Haskell.Constant))] -> Sig+addBackground props =+  Sig $ \_ cfg -> cfg { Haskell.cfg_background = Haskell.cfg_background cfg ++ props }+ -- | A signature. newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config } @@ -173,10 +179,11 @@ con name x =   Sig $ \ctx@(Context _ names) ->     if name `elem` names then id else-      unSig (constant (Haskell.con name x)) ctx+      unSig (customConstant (Haskell.con name x)) ctx -constant :: Haskell.Constant -> Sig-constant con =+-- | Add a custom constant.+customConstant :: Haskell.Constant -> Sig+customConstant con =   Sig $ \(Context n _) ->     modL Haskell.lens_constants (appendAt n [con]) @@ -213,8 +220,24 @@   Sig $ \ctx@(Context _ names) ->     if name `elem` names then id else     let (insts, con) = Haskell.predicate name x in-      runSig [addInstances insts `mappend` constant con] ctx+      runSig [addInstances insts `mappend` customConstant con] ctx +-- | Declare a predicate with a given name and value.+-- The predicate should be a function which returns `Bool`.+-- 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.+predicateGen :: ( Predicateable a+                , Typeable a+                , Typeable b+                , Typeable (PredicateTestCase a))+                => String -> a -> (b -> Gen (PredicateTestCase a)) -> Sig+predicateGen name x gen =+  Sig $ \ctx@(Context _ names) ->+    if name `elem` names then id else+    let (insts, con) = Haskell.predicateGen name x gen in+      runSig [addInstances insts `mappend` customConstant con] ctx+ -- | Declare a new monomorphic type. -- The type must implement `Ord` and `Arbitrary`. monoType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Sig@@ -255,6 +278,7 @@ inst :: (Typeable c1, Typeable c2) => c1 :- c2 -> Sig inst = instFun +-- | Declare an arbitrary value to be used by instance resolution. instFun :: Typeable a => a -> Sig instFun x = addInstances (Haskell.inst x) @@ -262,6 +286,10 @@ addInstances insts =   Sig (\_ -> modL Haskell.lens_instances (`mappend` insts)) +withPrintFilter :: (Prop (Term (PartiallyApplied Haskell.Constant)) -> Bool) -> Sig+withPrintFilter p =+  Sig (\_ -> setL Haskell.lens_print_filter p)+ -- | Declare some functions as being background functions. -- These are functions which are not interesting on their own, -- but which may appear in interesting laws with non-background functions.@@ -315,6 +343,9 @@ -- | Set the maximum size of terms to explore (default: 7). withMaxTermSize :: Int -> Sig withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n)++withMaxCommutativeSize :: Int -> Sig+withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n)  -- | Set how many times to test each discovered law (default: 1000). withMaxTests :: Int -> Sig
src/QuickSpec/Explore.hs view
@@ -62,10 +62,10 @@   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>   (Prop (Term fun) -> m ()) ->   (Term fun -> testcase -> result) ->-  Int -> Universe -> Enumerator (Term fun) -> m ()-quickSpec present eval maxSize univ enum = do+  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()+quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do   let-    state0 = initialState univ (\t -> size t <= 5) eval+    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval      loop m n _ | m > n = return ()     loop m n tss = do
src/QuickSpec/Explore/PartialApplication.hs view
@@ -21,7 +21,7 @@  instance Sized f => Sized (PartiallyApplied f) where   size (Partial f _) = size f-  size (Apply _) = 0+  size (Apply _) = 1  instance Arity (PartiallyApplied f) where   arity (Partial _ n) = n@@ -75,9 +75,9 @@  instance (Arity f, Typed f, Background f) => Background (PartiallyApplied f) where   background (Partial f _) =+    map (mapFun (\f -> Partial f (arity f))) (background f) ++     [ simpleApply (partial n) (vs !! n) === partial (n+1)-    | n <- [0..arity f-1] ] ++-    map (mapFun (\f -> Partial f (arity f))) (background f)+    | n <- [0..arity f-1] ]     where       partial i =         App (Partial f i) (take i vs)
src/QuickSpec/Explore/Polymorphic.hs view
@@ -1,6 +1,5 @@ -- Theory exploration which handles polymorphism. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE FlexibleInstances #-}@@ -49,18 +48,18 @@ -- The set of all types being explored data Universe = Universe { univ_types :: Set Type } -makeLensAs ''Polymorphic-  [("pm_schemas", "schemas"),-   ("pm_universe", "univ")]+schemas = lens pm_schemas (\x y -> y { pm_schemas = x })+univ = lens pm_universe (\x y -> y { pm_universe = x })  initialState ::+  (Type -> Bool) ->   Universe ->   (Term fun -> Bool) ->   (Term fun -> testcase -> result) ->   Polymorphic testcase result fun norm-initialState univ inst eval =+initialState singleUse univ inst eval =   Polymorphic {-    pm_schemas = Schemas.initialState (inst . fmap fun_specialised) (eval . fmap fun_specialised),+    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),     pm_universe = univ }  polyFun :: Typed fun => fun -> PolyFun fun@@ -120,7 +119,7 @@     return (norm . fmap fun_specialised)   add prop = PolyM $ do     univ <- access univ-    let insts = typeInstances univ (regeneralise (mapFun fun_original prop))+    let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))     or <$> mapM add insts  instance MonadTester testcase (Term fun) m =>@@ -178,18 +177,22 @@         skel (V ty x) = V (oneTypeVar ty) x     litCs (t :=: u) = [(typ t, typ u)] -typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a]-typeInstances Universe{..} prop =-  [ typeSubst (\x -> Map.findWithDefault (error ("not found: " ++ prettyShow x)) x sub) prop-  | sub <- cs ]+typeInstancesList :: [Type] -> [Type] -> [Twee.Var -> Type]+typeInstancesList types prop =+  map eval+    (foldr intersection [Map.empty]+      (map constrain+        (usort prop)))   where-    cs =-      foldr intersection [Map.empty]-        (map (constrain (Set.toList univ_types))-          (usort (DList.toList (termsDL prop) >>= subterms)))+    constrain t =+      usort [ Map.fromList (Twee.substToList sub) | u <- types, Just sub <- [Twee.match t u] ]+    eval sub x =+      Map.findWithDefault (error ("not found: " ++ prettyShow x)) x sub -    constrain tys t =-      usort [ Map.fromList (Twee.substToList sub) | u <- tys, Just sub <- [Twee.match (typ t) u] ]+typeInstances :: (Pretty a, PrettyTerm fun, Symbolic fun a, Ord fun, Typed fun, Typed a) => Universe -> a -> [a]+typeInstances Universe{..} prop =+  [ typeSubst sub prop+  | sub <- typeInstancesList (Set.toList univ_types) (map typ (DList.toList (termsDL prop) >>= subterms)) ]  intersection :: [Map Twee.Var Type] -> [Map Twee.Var Type] -> [Map Twee.Var Type] ms1 `intersection` ms2 = usort [ Map.union m1 m2 | m1 <- ms1, m2 <- ms2, ok m1 m2 ]@@ -197,14 +200,47 @@     ok m1 m2 = and [ Map.lookup x m1 == Map.lookup x m2 | x <- Map.keys (Map.intersection m1 m2) ]  universe :: Typed a => [a] -> Universe-universe xs = Universe (Set.fromList base)+universe xs = Universe (Set.fromList univ)   where-    -- The universe contains the type variable "a", the argument and-    -- result type of every function (with all type variables unified), and all-    -- subterms of these types-    base = usort $ typeVar:concatMap (oneTypeVar . typs . typ) xs-    typs ty = typeRes ty:typeArgs ty+    -- Types of all functions+    types = usort $ typeVar:map typ xs +    -- Take the argument and result type of every function.+    univBase = usort $ concatMap components types++    -- Add partially-applied functions, if they can be used to+    -- fill in a higher-order argument.+    univHo = usort $ concatMap addHo univBase+      where+        addHo ty =+          ty:+          [ typeSubst sub ho+          | fun <- types,+            ho <- arrows fun,+            sub <- typeInstancesList univBase (components fun) ]+  +    -- Add antiunifiers of all pairs of types, so that each equation+    -- has a most general type+    univ = usort $ oneTypeVar $ fixpoint antiunifiers univHo+      where+        antiunifiers tys =+          usort $ map (unPoly . poly) $+            tys ++ [antiunify ty1 ty2 | ty1 <- tys, ty2 <- tys]++    components ty =+      case unpackArrow ty of+        Nothing -> [ty]+        Just (ty1, ty2) -> components ty1 ++ components ty2++    arrows ty =+      concatMap arrows1 (typeArgs ty)+      where+        arrows1 ty+          | isArrowType ty =+            ty:concatMap arrows1 (typeArgs ty)+          | otherwise =+            []+  inUniverse :: Typed fun => Term fun -> Universe -> Bool t `inUniverse` Universe{..} =   and [oneTypeVar (typ u) `Set.member` univ_types | u <- subterms t]
src/QuickSpec/Explore/Schemas.hs view
@@ -1,6 +1,6 @@ -- Theory exploration which works on a schema at a time. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, TemplateHaskell, MultiParamTypeClasses, FlexibleInstances #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, MultiParamTypeClasses, FlexibleInstances #-} module QuickSpec.Explore.Schemas where  import qualified Data.Map.Strict as Map@@ -21,29 +21,33 @@ import Data.Set(Set) import Data.Maybe import Control.Monad+import Twee.Label  data Schemas testcase result fun norm =   Schemas {+    sc_single_use :: Type -> Bool,     sc_instantiate_singleton :: Term fun -> Bool,     sc_empty :: Terms testcase result (Term fun) norm,     sc_classes :: Terms testcase result (Term fun) norm,     sc_instantiated :: Set (Term fun),     sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) } -makeLensAs ''Schemas-  [("sc_classes", "classes"),-   ("sc_instances", "instances"),-   ("sc_instantiated", "instantiated")]+classes = lens sc_classes (\x y -> y { sc_classes = x })+single_use = lens sc_single_use (\x y -> y { sc_single_use = x })+instances = lens sc_instances (\x y -> y { sc_instances = x })+instantiated = lens sc_instantiated (\x y -> y { sc_instantiated = x })  instance_ :: Ord fun => Term fun -> Lens (Schemas testcase result fun norm) (Terms testcase result (Term fun) norm) instance_ t = reading (\Schemas{..} -> keyDefault t sc_empty # instances)  initialState ::+  (Type -> Bool) ->   (Term fun -> Bool) ->   (Term fun -> testcase -> result) ->   Schemas testcase result fun norm-initialState inst eval =+initialState singleUse inst eval =   Schemas {+    sc_single_use = singleUse,     sc_instantiate_singleton = inst,     sc_empty = Terms.initialState eval,     sc_classes = Terms.initialState eval,@@ -62,6 +66,7 @@ explore t0 = do   let t = mostSpecific t0   res <- zoom classes (Terms.explore t)+  singleUse <- access single_use   case res of     Terms.Singleton -> do       inst <- gets sc_instantiate_singleton@@ -69,7 +74,7 @@         instantiateRep t        else do         -- Add the most general instance of the schema-        zoom (instance_ t) (Terms.explore (mostGeneral t0))+        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))         return (Accepted [])     Terms.Discovered ([] :=>: _ :=: u) ->       exploreIn u t@@ -85,7 +90,8 @@   StateT (Schemas testcase result fun norm) m (Result fun) exploreIn rep t = do   -- First check if schema is redundant-  res <- zoom (instance_ rep) (Terms.explore (mostGeneral t))+  singleUse <- access single_use+  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))   case res of     Terms.Discovered prop -> do       add prop@@ -118,40 +124,45 @@   MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>   Term fun -> Term fun ->   StateT (Schemas testcase result fun norm) m (Result fun)-instantiate rep t = zoom (instance_ rep) $ do-  let instances = sortBy (comparing generality) (allUnifications (mostGeneral t))-  Accepted <$> catMaybes <$> forM instances (\t -> do-    res <- Terms.explore t-    case res of-      Terms.Discovered prop -> do-        add prop-        return (Just prop)-      _ -> return Nothing)+instantiate rep t = do+  singleUse <- access single_use+  zoom (instance_ rep) $ do+    let instances = sortBy (comparing generality) (allUnifications singleUse (mostGeneral singleUse t))+    Accepted <$> catMaybes <$> forM instances (\t -> do+      res <- Terms.explore t+      case res of+        Terms.Discovered prop -> do+          add prop+          return (Just prop)+        _ -> return Nothing)  -- sortBy (comparing generality) should give most general instances first. generality :: Term f -> (Int, [Var]) generality t = (-length (usort (vars t)), vars t)  -- | Instantiate a schema by making all the variables different.-mostGeneral :: Term f -> Term f-mostGeneral s = evalState (aux s) Map.empty+mostGeneral :: (Type -> Bool) -> Term f -> Term f+mostGeneral singleUse s = evalState (aux s) Map.empty   where     aux (Var (V ty _)) = do       m <- get-      let n = Map.findWithDefault 0 ty m-      put $! Map.insert ty (n+1) m-      return (Var (V ty n))+      let n :: Int+          n = Map.findWithDefault 0 ty m+      unless (singleUse ty) $+        put $! Map.insert ty (n+1) m+      let m = fromIntegral (labelNum (label (ty, n)))+      return (Var (V ty m))     aux (App f xs) = fmap (App f) (mapM aux xs)  mostSpecific :: Term f -> Term f mostSpecific = subst (\(V ty _) -> Var (V ty 0)) -allUnifications :: Term fun -> [Term fun]-allUnifications t = map f ss+allUnifications :: (Type -> Bool) -> Term fun -> [Term fun]+allUnifications singleUse t = map f ss   where     vs = [ map (x,) (select xs) | xs <- partitionBy typ (usort (vars t)), x <- xs ]     ss = map Map.fromList (sequence vs)     go s x = Map.findWithDefault undefined x s     f s = subst (Var . go s) t-    select [V ty x] = [V ty x, V ty (succ x)]+    select [V ty x] | not (singleUse ty) = [V ty x, V ty (succ x)]     select xs = take 4 xs
src/QuickSpec/Explore/Terms.hs view
@@ -1,6 +1,6 @@ -- Theory exploration which accepts one term at a time. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TemplateHaskell #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards #-} module QuickSpec.Explore.Terms where  import qualified Data.Map.Strict as Map@@ -30,7 +30,7 @@     -- ill-typed equations and bad things happening in the pruner.     tm_tree   :: Map Type (DecisionTree testcase result term) } -makeLensAs ''Terms [("tm_tree", "tree")]+tree = lens tm_tree (\x y -> y { tm_tree = x })  treeForType :: Type -> Lens (Terms testcase result term norm) (DecisionTree testcase result term) treeForType ty = reading (\Terms{..} -> keyDefault ty tm_empty # tree)
src/QuickSpec/Haskell.hs view
@@ -10,7 +10,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE FunctionalDependencies #-}@@ -21,7 +20,7 @@ import QuickSpec.Type import QuickSpec.Prop import QuickSpec.Pruning-import Test.QuickCheck hiding (total)+import Test.QuickCheck hiding (total, classify, subterms) import Data.Constraint hiding ((\\)) import Data.List import Data.Proxy@@ -45,6 +44,7 @@ import QuickSpec.Terminal import Text.Printf import QuickSpec.Utils+import Data.Lens.Light import GHC.TypeLits import QuickSpec.Explore.Conditionals import Control.Spoon@@ -138,6 +138,8 @@ -- A token used in the instance list for types that shouldn't generate warnings data NoWarnings a = NoWarnings +data SingleUse a = SingleUse+ instance c => Arbitrary (Dict c) where   arbitrary = return Dict @@ -408,10 +410,6 @@  data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a } --- A `suchThat` generator for a predicate-genSuchThat :: (Predicateable a, Arbitrary (PredicateTestCase a)) => a -> Gen (TestCaseWrapped x (PredicateTestCase a))-genSuchThat p = TestCaseWrapped <$> arbitrary `suchThat` uncrry p- true :: Constant true = con "True" True @@ -420,11 +418,13 @@  -- | Declare a predicate with a given name and value. -- The predicate should have type @... -> Bool@.-predicate :: forall a. ( Predicateable a+-- Uses an explicit generator.+predicateGen :: forall a b. ( Predicateable a              , Typeable a+             , Typeable b              , Typeable (PredicateTestCase a))-             => String -> a -> (Instances, Constant)-predicate name pred =+             => String -> a -> (b -> Gen (PredicateTestCase a)) -> (Instances, Constant)+predicateGen name pred gen =   let     -- The following doesn't compile on GHC 7.10:     -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))@@ -446,8 +446,8 @@       mconcat $ map (valueInst . addName)         [toValue (Identity inst1), toValue (Identity inst2)] -    inst1 :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (TestCaseWrapped SymA (PredicateTestCase a))-    inst1 Dict = genSuchThat pred+    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))+    inst1 x = TestCaseWrapped <$> gen x      inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))     inst2 = Names [name ++ "_var"]@@ -468,28 +468,44 @@   in     (instances, conPred) +-- | Declare a predicate with a given name and value.+-- The predicate should have type @... -> Bool@.+predicate :: forall a. ( Predicateable a+          , Typeable a+          , Typeable (PredicateTestCase a))+          => String -> a -> (Instances, Constant)+predicate name pred = predicateGen name pred inst+  where+    inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)+    inst Dict = arbitrary `suchThat` uncrry pred+ data Config =   Config {     cfg_quickCheck :: QuickCheck.Config,     cfg_twee :: Twee.Config,     cfg_max_size :: Int,+    cfg_max_commutative_size :: 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.     -- head cfg_constants contains all the background functions.     cfg_constants :: [[Constant]],     cfg_default_to :: Type,-    cfg_infer_instance_types :: Bool+    cfg_infer_instance_types :: Bool,+    cfg_background :: [Prop (Term (PartiallyApplied Constant))],+    cfg_print_filter :: Prop (Term (PartiallyApplied Constant)) -> Bool     } -makeLensAs ''Config-  [("cfg_quickCheck", "lens_quickCheck"),-   ("cfg_twee", "lens_twee"),-   ("cfg_max_size", "lens_max_size"),-   ("cfg_instances", "lens_instances"),-   ("cfg_constants", "lens_constants"),-   ("cfg_default_to", "lens_default_to"),-   ("cfg_infer_instance_types", "lens_infer_instance_types")]+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_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 })+lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x })+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 })  defaultConfig :: Config defaultConfig =@@ -497,10 +513,13 @@     cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 100, QuickCheck.cfg_fixed_seed = Nothing },     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_instances = mempty,     cfg_constants = [],     cfg_default_to = typeRep (Proxy :: Proxy Int),-    cfg_infer_instance_types = False }+    cfg_infer_instance_types = False,+    cfg_background = [],+    cfg_print_filter = \_ -> True }  -- Extra types for the universe that come from in-scope instances. instanceTypes :: Instances -> Config -> [Type]@@ -571,7 +590,9 @@ quickSpec :: Config -> IO [Prop (Term (PartiallyApplied Constant))] quickSpec cfg@Config{..} = do   let-    constantsOf f = true:f cfg_constants ++ concatMap selectors (f cfg_constants)+    constantsOf f =+      [true | any (/= Function) (map classify (f cfg_constants))] +++      f cfg_constants ++ concatMap selectors (f cfg_constants)     constants = constantsOf concat          univ = conditionalsUniverse (instanceTypes instances cfg) constants@@ -582,11 +603,12 @@     present funs prop = do       norm <- normaliser       let prop' = makeDefinition funs (ac norm (conditionalise prop))-      (n :: Int, props) <- get-      put (n+1, prop':props)-      putLine $-        printf "%3d. %s" n $ show $-          prettyProp (names instances) prop' <+> maybeType prop+      when (cfg_print_filter prop) $ do+        (n :: Int, props) <- get+        put (n+1, prop':props)+        putLine $+          printf "%3d. %s" n $ show $+            prettyProp (names instances) prop' <+> maybeType prop      -- Put an equation that defines the function f into the form f lhs = rhs.     -- An equation defines f if:@@ -633,10 +655,16 @@     enumerator cons =       sortTerms measure $       filterEnumerator (all constraintsOk . funs) $+      filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $       enumerateConstants atomic `mappend` enumerateApplications       where         atomic = cons ++ [Var (V typeVar 0)] +    conditions t = usort [p | f <- funs t, Selector _ p _ <- [classify f]]++    singleUse ty =+      isJust (findInstance instances ty :: Maybe (Value SingleUse))+     mainOf n f g = do       unless (null (f cfg_constants)) $ do         putLine $ show $ pPrintSignature@@ -646,12 +674,15 @@         putText (prettyShow (warnings univ instances cfg))         putLine "== Laws =="       let pres = if n == 0 then \_ -> return () else present (constantsOf f)-      QuickSpec.Explore.quickSpec pres (flip eval) cfg_max_size univ+      QuickSpec.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size singleUse univ         (enumerator [partial fun | fun <- constantsOf g])       when (n > 0) $ do         putLine "" -    main = mapM_ round [0..rounds-1]+    main = do+      forM_ cfg_background $ \prop -> do+        add prop+      mapM_ round [0..rounds-1]       where         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))         rounds = length cfg_constants
src/QuickSpec/Pruning/Twee.hs view
@@ -15,12 +15,13 @@ import QuickSpec.Pruning.UntypedTwee(Config(..))  newtype Pruner fun m a =-  Pruner (Background.Pruner fun (Types.Pruner fun (Untyped.Pruner (Types.Tagged fun) m)) a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadPruner (Term fun) (Term fun), MonadTerminal)+  Pruner (Types.Pruner fun (Background.Pruner (Types.Tagged fun) (Untyped.Pruner (Types.Tagged fun) m)) a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term,+            MonadPruner (Term fun) (Untyped.Norm (Types.Tagged fun)), MonadTerminal)  instance MonadTrans (Pruner fun) where   lift = Pruner . lift . lift . lift  run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a run config (Pruner x) =-  Untyped.run config (Types.run (Background.run x))+  Untyped.run config (Background.run (Types.run x))
src/QuickSpec/Pruning/Types.hs view
@@ -51,18 +51,18 @@ instance MonadTrans (Pruner fun) where   lift = Pruner -instance (PrettyTerm fun, Typed fun, MonadPruner (UntypedTerm fun) (UntypedTerm fun) pruner) => MonadPruner (TypedTerm fun) (TypedTerm fun) (Pruner fun pruner) where+instance (PrettyTerm fun, Typed fun, MonadPruner (UntypedTerm fun) norm pruner) => MonadPruner (TypedTerm fun) norm (Pruner fun pruner) where   normaliser =     Pruner $ do-      norm <- normaliser :: pruner (UntypedTerm fun -> UntypedTerm fun)-      +      norm <- normaliser :: pruner (UntypedTerm fun -> norm)+       -- Note that we don't call addFunction on the functions in the term.       -- This is because doing so might be expensive, as adding typing       -- axioms starts the completion algorithm.       -- This is OK because in encode, we tag all functions and variables       -- with their types (i.e. we can fall back to the naive type encoding).       return $ \t ->-        decode . norm . encode $ t+        norm . encode $ t    add prop = lift (add (encode <$> canonicalise prop)) @@ -108,20 +108,3 @@ encode (Var x) = tag (typ x) (Var x) encode (App f ts) =   tag (typeDrop (length ts) (typ f)) (App (Func f) (map encode ts))--decode :: Typed fun => UntypedTerm fun -> TypedTerm fun-decode = dec Nothing-  where-    dec _ (App (Tag ty) [t]) =-      dec (Just ty) t-    dec _ (App Tag{} _) =-      error "Tag function applied with wrong arity"-    dec (Just ty) (Var (V _ x)) =-      Var (V ty x)-    dec Nothing (Var _) =-      error "Naked variable in type-encoded term"-    dec _ (App (Func f) ts) =-      App f $-        zipWith dec-          (map Just (typeArgs (typ f)))-          ts
src/QuickSpec/Pruning/UntypedTwee.hs view
@@ -1,6 +1,6 @@ -- A pruner that uses twee. Does not respect types. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances, TemplateHaskell #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-} module QuickSpec.Pruning.UntypedTwee where  import QuickSpec.Testing@@ -8,7 +8,7 @@ import QuickSpec.Prop import QuickSpec.Term import QuickSpec.Type-import QuickSpec.Utils+import Data.Lens.Light import qualified Twee import qualified Twee.Equation as Twee import qualified Twee.KBO as KBO@@ -16,7 +16,7 @@ import Twee hiding (Config(..)) import Twee.Rule hiding (normalForms) import Twee.Proof hiding (Config, defaultConfig)-import Twee.Base(Ordered(..), Extended(..), EqualsBonus, pattern F, pattern Empty, unpack)+import Twee.Base(Ordered(..), Extended(..), EqualsBonus) import Control.Monad.Trans.Reader import Control.Monad.Trans.State.Strict hiding (State) import Control.Monad.Trans.Class@@ -30,9 +30,8 @@     cfg_max_term_size :: Int,     cfg_max_cp_depth :: Int } -makeLensAs ''Config-  [("cfg_max_term_size", "lens_max_term_size"),-   ("cfg_max_cp_depth", "lens_max_cp_depth")]+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   lessEq = KBO.lessEq@@ -64,8 +63,10 @@   size (Twee.Skolem _) = 1   size (Twee.Function f) = size f +type Norm fun = Twee.Term (Extended fun)+ instance (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>-  MonadPruner (Term fun) (Term fun) (Pruner fun m) where+  MonadPruner (Term fun) (Norm fun) (Pruner fun m) where   normaliser = Pruner $ do     state <- lift get     return $ \t ->@@ -85,19 +86,18 @@     return (Set.null (Set.intersection t' u'))    add _ =-    error "twee pruner doesn't support non-unit equalities"+    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) =>-  State (Extended fun) -> Term fun -> Term fun+  State (Extended fun) -> Term fun -> Norm fun normaliseTwee state t =-  fromTwee $-    result (normaliseTerm state (simplifyTerm state (skolemise t)))+  result (normaliseTerm state (simplifyTerm state (skolemise t)))  normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>-  State (Extended fun) -> Term fun -> Set (Term fun)+  State (Extended fun) -> Term fun -> Set (Norm fun) normalFormsTwee state t =-  Set.map fromTwee $-    Set.map result (normalForms state (skolemise t))+  Set.map result (normalForms state (skolemise t))  addTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)@@ -124,14 +124,3 @@       Twee.con (Twee.fun (Skolem (Twee.V x)))     sk (App f ts) =       Twee.app (Twee.fun (Function f)) (map sk ts)--fromTwee :: Twee.Term (Extended f) -> Term f-fromTwee = unsk-  where-    unsk (Twee.App (F Minimal) Empty) =-      Var (V typeVar 0)-    unsk (Twee.App (F (Skolem (Twee.V x))) Empty) =-      Var (V typeVar x)-    unsk (Twee.App (F (Function f)) ts) =-      App f (map unsk (unpack ts))-    unsk _ = error "variable introduced by rewriting"
src/QuickSpec/Term.hs view
@@ -53,8 +53,8 @@   size (App f ts) = size f + sum (map size ts)  instance Pretty Var where-  --pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)-  pPrint x = text "X" <#> pPrint (var_id x+1)+  pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)+  --pPrint x = text "X" <#> pPrint (var_id x+1)  instance PrettyTerm f => Pretty (Term f) where   pPrintPrec l p (Var x) = pPrintPrec l p x@@ -148,15 +148,20 @@ -- | A standard term ordering - size, skeleton, generality. -- Satisfies the property: -- if measure (schema t) < measure (schema u) then t < u.-type Measure f = (Int, Int, MeasureFuns f, Int, [Var])+type Measure f = (Int, Int, Int, MeasureFuns f, Int, [Var]) -- | Compute the term ordering for a term.-measure :: Sized f => Term f -> Measure f+measure :: (Sized f, Typed f) => Term f -> Measure f measure t =-  (size t, -length (vars t), MeasureFuns (skel t),+  (size t, sizeHO t, -length (vars t), MeasureFuns (skel t),    -length (usort (vars t)), vars t)   where     skel (Var (V ty _)) = Var (V ty 0)     skel (App f ts) = App f (map skel ts)+    -- Prefer fully-applied terms to partially-applied ones.+    -- This function computes the size, but adds 1 for every+    -- unapplied function.+    sizeHO (App f ts) = size f + typeArity (typ f) - length ts + sum (map sizeHO ts)+    sizeHO Var{} = 1  -- | A helper for `Measure`. newtype MeasureFuns f = MeasureFuns (Term f)@@ -201,7 +206,7 @@ instance (Pretty fun1, Pretty fun2) => Pretty (fun1 :+: fun2) where   pPrintPrec l p (Inl x) = pPrintPrec l p x   pPrintPrec l p (Inr x) = pPrintPrec l p x-  + instance (PrettyTerm fun1, PrettyTerm fun2) => PrettyTerm (fun1 :+: fun2) where   termStyle (Inl x) = termStyle x   termStyle (Inr x) = termStyle x
src/QuickSpec/Testing/QuickCheck.hs view
@@ -1,6 +1,6 @@ -- Testing conjectures using QuickCheck. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving, TemplateHaskell #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-} module QuickSpec.Testing.QuickCheck where  import QuickSpec.Testing@@ -16,7 +16,7 @@ import Data.List import System.Random import QuickSpec.Terminal-import QuickSpec.Utils+import Data.Lens.Light  data Config =   Config {@@ -25,10 +25,9 @@     cfg_fixed_seed :: Maybe QCGen}   deriving Show -makeLensAs ''Config-  [("cfg_num_tests", "lens_num_tests"),-   ("cfg_max_test_size", "lens_max_test_size"),-   ("cfg_fixed_seed", "lens_fixed_seed")]+lens_num_tests = lens cfg_num_tests (\x y -> y { cfg_num_tests = x })+lens_max_test_size = lens cfg_max_test_size (\x y -> y { cfg_max_test_size = x })+lens_fixed_seed = lens cfg_fixed_seed (\x y -> y { cfg_fixed_seed = x })  data Environment testcase term result =   Environment {@@ -53,7 +52,6 @@     n = cfg_num_tests     k = max 1 cfg_max_test_size     bias = 3-    cfg_max_test_size = 100     -- Bias tests towards smaller sizes.     -- We do this by distributing the cube of the size uniformly.     sizes =@@ -77,7 +75,7 @@   where     leftovers = n `mod` k -instance (MonadTerminal m, Eq result) => MonadTester testcase term (Tester testcase term result m) where+instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where   test prop =     Tester $ do       env <- ask
src/QuickSpec/Type.hs view
@@ -9,7 +9,7 @@   Typeable,   Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,   typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,-  arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,+  arrowType, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,   isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,   -- * Things that have types   Typed(..), typeSubst, typesDL, tyVars, cast, matchType,@@ -150,6 +150,10 @@ arrowType [] res = res arrowType (arg:args) res =   build (app (fun Arrow) [arg, arrowType args res])++-- | Is a given type a function type?+isArrowType :: Type -> Bool+isArrowType = isJust . unpackArrow  -- | Decompose a function type into (argument, result). --
src/QuickSpec/Utils.hs view
@@ -17,6 +17,9 @@ import Data.Map(Map) import Language.Haskell.TH.Syntax import Data.Lens.Light+import Twee.Base hiding (lookup)+import Control.Monad.Trans.State.Strict+import Control.Monad  (#) :: Category.Category cat => cat b c -> cat a b -> cat a c (#) = (Category..)@@ -104,3 +107,32 @@ appendAt n xs [] = appendAt n xs [[]] appendAt 0 xs (ys:yss) = (ys ++ xs):yss appendAt n xs (ys:yss) = ys:appendAt (n-1) xs yss++-- Should be in Twee.Base.+antiunify :: Ord f => Term f -> Term f -> Term f+antiunify t u =+  build $ evalState (loop t u) (succ (snd (bound t) `max` snd (bound u)), Map.empty)+  where+    loop (App f ts) (App g us)+      | f == g =+        app f <$> zipWithM loop (unpack ts) (unpack us)+    loop (Var x) (Var y)+      | x == y =+        return (var x)+    loop t u = do+      (next, m) <- get+      case Map.lookup (t, u) m of+        Just v -> return (var v)+        Nothing -> do+          put (succ next, Map.insert (t, u) next m)+          return (var next)++{-# INLINE fixpoint #-}+fixpoint :: Eq a => (a -> a) -> a -> a+fixpoint f x = fxp x+  where+    fxp x+      | x == y = x+      | otherwise = fxp y+      where+        y = f x