packages feed

quickspec 2.1.1 → 2.1.2

raw patch · 47 files changed

+3889/−3855 lines, 47 filesdep ~twee-lib

Dependency ranges changed: twee-lib

Files

quickspec.cabal view
@@ -1,5 +1,5 @@ Name:                quickspec-Version:             2.1.1+Version:             2.1.2 Cabal-version:       >= 1.6 Build-type:          Simple @@ -9,7 +9,7 @@  License:             BSD3 License-file:        LICENSE-Copyright:           2009-2018 Nick Smallbone+Copyright:           2009-2019 Nick Smallbone  Category:            Testing @@ -75,28 +75,29 @@   hs-source-dirs: src   Exposed-modules:     QuickSpec-    QuickSpec.Explore-    QuickSpec.Explore.Conditionals-    QuickSpec.Explore.PartialApplication-    QuickSpec.Explore.Polymorphic-    QuickSpec.Explore.Schemas-    QuickSpec.Explore.Terms-    QuickSpec.Haskell-    QuickSpec.Haskell.Resolve-    QuickSpec.Parse-    QuickSpec.Prop-    QuickSpec.Pruning-    QuickSpec.Pruning.Background-    QuickSpec.Pruning.Twee-    QuickSpec.Pruning.Types-    QuickSpec.Pruning.UntypedTwee-    QuickSpec.Term-    QuickSpec.Terminal-    QuickSpec.Testing-    QuickSpec.Testing.DecisionTree-    QuickSpec.Testing.QuickCheck-    QuickSpec.Type-    QuickSpec.Utils+    QuickSpec.Internal+    QuickSpec.Internal.Explore+    QuickSpec.Internal.Explore.Conditionals+    QuickSpec.Internal.Explore.Polymorphic+    QuickSpec.Internal.Explore.Schemas+    QuickSpec.Internal.Explore.Terms+    QuickSpec.Internal.Haskell+    QuickSpec.Internal.Haskell.Resolve+    QuickSpec.Internal.Parse+    QuickSpec.Internal.Prop+    QuickSpec.Internal.Pruning+    QuickSpec.Internal.Pruning.Background+    QuickSpec.Internal.Pruning.Twee+    QuickSpec.Internal.Pruning.Types+    QuickSpec.Internal.Pruning.UntypedTwee+    QuickSpec.Internal.Pruning.PartialApplication+    QuickSpec.Internal.Term+    QuickSpec.Internal.Terminal+    QuickSpec.Internal.Testing+    QuickSpec.Internal.Testing.DecisionTree+    QuickSpec.Internal.Testing.QuickCheck+    QuickSpec.Internal.Type+    QuickSpec.Internal.Utils    Build-depends:     QuickCheck >= 2.10,
src/QuickSpec.hs view
@@ -93,341 +93,11 @@   withInferInstanceTypes,    -- * Re-exported functionality-  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary,--  -- * For QuickSpec hackers-  unSig, Context(..), SingleUse(..), NoWarnings(..),-  quickSpecResult, addBackground, addInstances, instFun, customConstant, withPrintFilter, withMaxCommutativeSize) where+  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where -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-import qualified QuickSpec.Pruning.UntypedTwee as Twee-import QuickSpec.Explore.PartialApplication-import QuickSpec.Prop-import QuickSpec.Term(Term)-import Test.QuickCheck-import Test.QuickCheck.Random+import QuickSpec.Internal+import QuickSpec.Internal.Haskell(Observe(..))+import QuickSpec.Internal.Type(A, B, C, D, E)+import Data.Typeable import Data.Constraint-import Data.Lens.Light-import QuickSpec.Utils-import QuickSpec.Type hiding (defaultTo)-import Data.Proxy-import System.Environment-import Data.Semigroup(Semigroup(..))---- | Run QuickSpec. See the documentation at the top of this file.-quickSpec :: Signature sig => sig -> IO ()-quickSpec sig = do-  quickSpecResult sig-  return ()---- | Run QuickSpec, returning the list of discovered properties.-quickSpecResult :: Signature sig => sig -> IO [Prop (Term (PartiallyApplied Haskell.Constant))]-quickSpecResult sig = do-  -- Undocumented feature for testing :)-  seed <- lookupEnv "QUICKCHECK_SEED"-  let-    sig' = case seed of-      Nothing -> signature sig-      Just xs -> signature [signature sig, withFixedSeed (read xs)]--  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 }---- Settings for building the signature.--- Int: number of nested calls to 'background'.--- [String]: list of names to exclude.-data Context = Context Int [String]--instance Semigroup Sig where-  Sig sig1 <> Sig sig2 = Sig (\ctx -> sig2 ctx . sig1 ctx)-instance Monoid Sig where-  mempty = Sig (\_ -> id)-  mappend = (<>)---- | A class of things that can be used as a QuickSpec signature.-class Signature sig where-  -- | Convert the thing to a signature.-  signature :: sig -> Sig--instance Signature Sig where-  signature = id--instance Signature sig => Signature [sig] where-  signature = mconcat . map signature--runSig :: Signature sig => sig -> Context -> Haskell.Config -> Haskell.Config-runSig = unSig . signature---- | Declare a constant with a given name and value.--- If the constant you want to use is polymorphic, you can use the types--- `A`, `B`, `C`, `D`, `E` to monomorphise it, for example:------ > constant "reverse" (reverse :: [A] -> [A])------ QuickSpec will then understand that the constant is really polymorphic.-con :: Typeable a => String -> a -> Sig-con name x =-  Sig $ \ctx@(Context _ names) ->-    if name `elem` names then id else-      unSig (customConstant (Haskell.con name x)) ctx---- | Add a custom constant.-customConstant :: Haskell.Constant -> Sig-customConstant con =-  Sig $ \(Context n _) ->-    modL Haskell.lens_constants (appendAt n [con])---- | Type class constraints as first class citizens-type c ==> t = Dict c -> t---- | Lift a constrained type to a `==>` type which QuickSpec--- can work with-liftC :: (c => a) -> c ==> a-liftC a Dict = a---- | Add an instance of a type class to the signature-instanceOf :: forall c. (Typeable c, c) => Sig-instanceOf = inst (Sub Dict :: () :- c)---- | 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.------ For example:------ @--- sig = [---   `con` "delete" (`Data.List.delete` :: Int -> [Int] -> [Int]),---   `con` "insert" (`Data.List.insert` :: Int -> [Int] -> [Int]),---   predicate "member" (member :: Int -> [Int] -> Bool) ]--- @-predicate :: ( Predicateable a-             , Typeable a-             , Typeable (PredicateTestCase a))-             => String -> a -> Sig-predicate name x =-  Sig $ \ctx@(Context _ names) ->-    if name `elem` names then id else-    let (insts, con) = Haskell.predicate name x in-      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-monoType _ =-  mconcat [-    inst (Sub Dict :: () :- Ord a),-    inst (Sub Dict :: () :- Arbitrary a)]---- | Declare a new monomorphic type using observational equivalence.--- The type must implement `Observe` and `Arbitrary`.-monoTypeObserve :: forall proxy test outcome a.-  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>-  proxy a -> Sig-monoTypeObserve _ =-  mconcat [-    inst (Sub Dict :: () :- Observe test outcome a),-    inst (Sub Dict :: () :- Arbitrary a)]---- | Declare a new monomorphic type, saying how you want variables of that type to be named.-monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig-monoTypeWithVars xs proxy =-  monoType proxy `mappend` vars xs proxy---- | Customize how variables of a particular type are named.-vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig-vars xs _ = instFun (Names xs :: Names a)---- | 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--- the following two declarations to your signature:------ @--- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B))--- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B))--- @-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)--addInstances :: Haskell.Instances -> Sig-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.--- Declaring background functions may improve the laws you get out.------ Here is an example, which tests @++@ and @length@, giving @0@ and @+@ as--- background functions:------ > main = quickSpec [--- >   con "++" ((++) :: [A] -> [A] -> [A]),--- >   con "length" (length :: [A] -> Int),--- >--- >   background [--- >     con "0" (0 :: Int),--- >     con "+" ((+) :: Int -> Int -> Int) ] ]-background :: Signature sig => sig -> Sig-background sig =-  Sig (\(Context _ xs) -> runSig sig (Context 0 xs))---- | Remove a function or predicate from the signature.--- Useful in combination with 'prelude' and friends.-without :: Signature sig => sig -> [String] -> Sig-without sig xs =-  Sig (\(Context n ys) -> runSig sig (Context n (ys ++ xs)))---- | Run QuickCheck on a series of signatures. Tests the functions in the first--- signature, then adds the functions in the second signature, then adds the--- functions in the third signature, and so on.------ This can be useful when you have a core API you want to test first, and a--- larger API you want to test later. The laws for the core API will be printed--- separately from the laws for the larger API.------ Here is an example which first tests @0@ and @+@ and then adds @++@ and @length@:------ > main = quickSpec [sig1, sig2]--- >   where--- >     sig1 = [--- >       con "0" (0 :: Int),--- >       con "+" ((+) :: Int -> Int -> Int) ]--- >     sig2 = [--- >       con "++" ((++) :: [A] -> [A] -> [A]),--- >       con "length" (length :: [A] -> Int) ]-series :: Signature sig => [sig] -> Sig-series = foldr op mempty . map signature-  where-    op sig sigs = sig `mappend` later (signature sigs)-    later sig =-      Sig (\(Context n xs) cfg -> unSig sig (Context (n+1) xs) cfg)---- | 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-withMaxTests n =-  Sig (\_ -> setL (QuickCheck.lens_num_tests # Haskell.lens_quickCheck) n)---- | Set the maximum value for QuickCheck's size parameter when generating test--- data (default: 20).-withMaxTestSize :: Int -> Sig-withMaxTestSize n =-  Sig (\_ -> setL (QuickCheck.lens_max_test_size # Haskell.lens_quickCheck) n)---- | Set which type polymorphic terms are tested at.-defaultTo :: Typeable a => proxy a -> Sig-defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy))---- | Set how hard QuickSpec tries to filter out redundant equations (default: no limit).------ If you experience long pauses when running QuickSpec, try setting this number--- to 2 or 3.-withPruningDepth :: Int -> Sig-withPruningDepth n =-  Sig (\_ -> setL (Twee.lens_max_cp_depth # Haskell.lens_twee) n)---- | Set the maximum term size QuickSpec will reason about when it filters out--- redundant equations (default: same as maximum term size).------ If you get laws you believe are redundant, try increasing this number to 1 or--- 2 more than the maximum term size.-withPruningTermSize :: Int -> Sig-withPruningTermSize n =-  Sig (\_ -> setL (Twee.lens_max_term_size # Haskell.lens_twee) n)---- | Set the random number seed used for test case generation.--- Useful if you want repeatable results.-withFixedSeed :: Int -> Sig-withFixedSeed s = Sig (\_ -> setL (QuickCheck.lens_fixed_seed # Haskell.lens_quickCheck) (Just . mkQCGen $ s))---- | Automatically infer types to add to the universe from--- available type class instances-withInferInstanceTypes :: Sig-withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)---- | A signature containing boolean functions:--- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.-bools :: Sig-bools = background [-  "||"    `con` (||),-  "&&"    `con` (&&),-  "not"   `con` not,-  "True"  `con` True,-  "False" `con` False]---- | A signature containing arithmetic operations:--- @0@, @1@, @(`+`)@.--- Instantiate it with e.g. @arith (`Proxy` :: `Proxy` `Int`)@.-arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig-arith proxy = background [-  monoType proxy,-  "0" `con` (0   :: a),-  "1" `con` (1   :: a),-  "+" `con` ((+) :: a -> a -> a)]---- | A signature containing list operations:--- @[]@, @(:)@, @(`++`)@.-lists :: Sig-lists = background [-  "[]"      `con` ([]      :: [A]),-  ":"       `con` ((:)     :: A -> [A] -> [A]),-  "++"      `con` ((++)    :: [A] -> [A] -> [A])]---- | A signature containing higher-order functions:--- @(`.`)@ and `id`.--- Useful for testing `map` and similar.-funs :: Sig-funs = background [-  "."  `con` ((.) :: (A -> A) -> (A -> A) -> (A -> A)),-  "id" `con` (id  :: A -> A) ]---- | The QuickSpec prelude.--- Contains boolean, arithmetic and list functions, and function composition.--- For more precise control over what gets included,--- see 'bools', 'arith', 'lists', 'funs' and 'without'.-prelude :: Sig-prelude = signature [bools, arith (Proxy :: Proxy Int), lists]+import Test.QuickCheck
− src/QuickSpec/Explore.hs 
@@ -1,99 +0,0 @@-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts #-}-module QuickSpec.Explore where--import QuickSpec.Explore.Polymorphic-import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Utils-import QuickSpec.Prop-import QuickSpec.Terminal-import Control.Monad-import Control.Monad.Trans.Class-import Control.Monad.Trans.State.Strict-import Text.Printf-import Data.Semigroup(Semigroup(..))--newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }---- N.B. order matters!--- Later enumerators get to see terms which were generated by earlier ones.-instance Semigroup (Enumerator a) where-  e1 <> e2 = Enumerator $ \n tss ->-    let us = enumerate e1 n tss-        vs = enumerate e2 n (appendAt n us tss)-    in us ++ vs-instance Monoid (Enumerator a) where-  mempty = Enumerator (\_ _ -> [])-  mappend = (<>)--mapEnumerator :: ([a] -> [a]) -> Enumerator a -> Enumerator a-mapEnumerator f e =-  Enumerator $ \n tss ->-    f (enumerate e n tss)--filterEnumerator :: (a -> Bool) -> Enumerator a -> Enumerator a-filterEnumerator p e =-  mapEnumerator (filter p) e--enumerateConstants :: Sized a => [a] -> Enumerator a-enumerateConstants ts = Enumerator (\n _ -> [t | t <- ts, size t == n])--enumerateApplications :: Apply a => Enumerator a-enumerateApplications = Enumerator $ \n tss ->-    [ unPoly v-    | i <- [0..n],-      t <- tss !! i,-      u <- tss !! (n-i),-      Just v <- [tryApply (poly t) (poly u)] ]--filterUniverse :: Typed f => Universe -> Enumerator (Term f) -> Enumerator (Term f)-filterUniverse univ e =-  filterEnumerator (`usefulForUniverse` univ) e--sortTerms :: Ord b => (a -> b) -> Enumerator a -> Enumerator a-sortTerms measure e =-  mapEnumerator (sortBy' measure) e--quickSpec ::-  (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, Apply (Term fun), PrettyTerm fun,-  MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>-  (Prop (Term fun) -> m ()) ->-  (Term fun -> testcase -> result) ->-  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()-quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do-  let-    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval--    loop m n _ | m > n = return ()-    loop m n tss = do-      putStatus (printf "enumerating terms of size %d" m)-      let-        ts = enumerate (filterUniverse univ enum) m tss-        total = length ts-        consider (i, t) = do-          putStatus (printf "testing terms of size %d: %d/%d" m i total)-          res <- explore t-          putStatus (printf "testing terms of size %d: %d/%d" m i total)-          lift $ mapM_ present (result_props res)-          case res of-            Accepted _ -> return True-            Rejected _ -> return False-      us <- map snd <$> filterM consider (zip [1 :: Int ..] ts)-      clearStatus-      loop (m+1) n (appendAt m us tss)--  evalStateT (loop 0 maxSize (repeat [])) state0--pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc-pPrintSignature funs =-  text "== Functions ==" $$-  vcat (map pPrintDecl decls)-  where-    decls = [ (prettyShow f, pPrintType (typ f)) | f <- funs ]-    maxWidth = maximum (0:map (length . fst) decls)-    pad xs = nest (maxWidth - length xs) (text xs)-    pPrintDecl (name, ty) =-      pad name <+> text "::" <+> ty
− src/QuickSpec/Explore/Conditionals.hs 
@@ -1,222 +0,0 @@-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE DeriveFunctor #-}-module QuickSpec.Explore.Conditionals where--import QuickSpec.Prop-import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Pruning-import QuickSpec.Pruning.Background(Background(..))-import QuickSpec.Testing-import QuickSpec.Terminal-import QuickSpec.Utils-import QuickSpec.Explore.PartialApplication-import QuickSpec.Explore.Polymorphic-import qualified Twee.Base as Twee-import Data.List-import Control.Monad-import Control.Monad.Trans.Class-import Control.Monad.IO.Class--newtype Conditionals m a = Conditionals (m a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)-instance MonadTrans Conditionals where-  lift = Conditionals-instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  MonadPruner (Term fun) norm (Conditionals m) where-  normaliser = lift $ do-    norm <- normaliser-    return (norm . fmap Normal)-  add prop = do-    redundant <- conditionallyRedundant prop-    if redundant then return False else do-      res <- lift (add (mapFun Normal prop))-      when res (considerConditionalising prop)-      return res--conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe-conditionalsUniverse tys funs =-  universe $-    tys ++-    (map typ $-      map Normal funs ++-      [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])--runConditionals ::-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  [fun] -> Conditionals m a -> m a-runConditionals preds mx =-  run (mapM_ considerPredicate preds >> mx)-  where-    run (Conditionals mx) = mx--class Predicate fun where-  classify :: fun -> Classification fun--data Classification fun =-    Predicate { clas_selectors :: [fun], clas_test_case :: Type, clas_true :: Term fun }-  | Selector { clas_index :: Int, clas_pred :: fun, clas_test_case :: Type }-  | Function-  deriving (Eq, Ord, Functor)--instance (Arity fun, Predicate fun) => Predicate (PartiallyApplied fun) where-  classify f =-    case getTotal f of-      Nothing -> Function-      Just f -> fmap total (classify f)--data WithConstructor fun =-    Constructor fun Type-  | Normal fun-  deriving (Eq, Ord)--instance Sized fun => Sized (WithConstructor fun) where-  size Constructor{} = 0-  size (Normal f) = size f--instance Arity fun => Arity (WithConstructor fun) where-  arity Constructor{} = 1-  arity (Normal f) = arity f--instance Pretty fun => Pretty (WithConstructor fun) where-  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"-  pPrintPrec l p (Normal f) = pPrintPrec l p f--instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where-  termStyle (Constructor _ _) = curried-  termStyle (Normal f) = termStyle f--instance PrettyArity fun => PrettyArity (WithConstructor fun) where-  prettyArity (Constructor _ _) = 1-  prettyArity (Normal f) = prettyArity f--instance (Predicate fun, Background fun) => Background (WithConstructor fun) where-  background (Normal f) = map (mapFun Normal) (background f)-  background _ = []--instance Typed fun => Typed (WithConstructor fun) where-  typ (Constructor pred ty) =-    arrowType (typeArgs (typ pred)) ty-  typ (Normal f) = typ f-  otherTypesDL (Constructor pred _) = typesDL pred-  otherTypesDL (Normal f) = otherTypesDL f-  typeSubst_ sub (Constructor pred ty) = Constructor (typeSubst_ sub pred) (typeSubst_ sub ty)-  typeSubst_ sub (Normal f) = Normal (typeSubst_ sub f)--predType :: TyCon -> [Type] -> Type-predType name tys =-  Twee.build (Twee.app (Twee.fun name) tys)--considerPredicate ::-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  fun -> Conditionals m ()-considerPredicate f =-  case classify f of-    Predicate sels ty true -> do-      let-        x = Var (V ty 0)-        eqns =-          [App (Constructor f ty) [App (Normal sel) [x] | sel <- sels] === x,-           App (Normal f) [App (Normal sel) [x] | sel <- sels] === fmap Normal true]-      mapM_ (lift . add) eqns-    _ -> return ()--considerConditionalising ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  Prop (Term fun) -> Conditionals m ()-considerConditionalising (lhs :=>: t :=: u) = do-  norm <- normaliser-  -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True"-  -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n"-  -- to the set of known equations-  case t of-    App f ts | Predicate{..} <- classify f -> -- It is an interesting predicate, i.e. it was added by the user-      when (norm u == norm clas_true) $-        addPredicate lhs f ts-    _ -> return ()--conditionallyRedundant ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  Prop (Term fun) -> Conditionals m Bool-conditionallyRedundant (lhs :=>: t :=: u) = do-  t' <- normalise t-  u' <- normalise u-  conditionallyRedundant' lhs t u t' u'--conditionallyRedundant' ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool-conditionallyRedundant' lhs t u t' u' = do-  forM_ (usort (funs [t, u])) $ \f ->-    case classify f of-      Selector{..} -> do-        let-          Predicate{..} = classify clas_pred-          tys = typeArgs (typ clas_pred)-          argss = sequence [ [ arg | arg <- terms [t, u] >>= subterms, typ arg == ty ] | ty <- tys ]-        forM_ argss $ \args -> do-          norm <- normaliser-          let p = App clas_pred args-          when (norm p == norm clas_true) $ do-            addPredicate lhs clas_pred args-      _ -> return ()--  t'' <- normalise t-  u'' <- normalise u-  if t'' == u'' then-    return True-   else if t'' == t' && u'' == u' then-     return False-    else-     conditionallyRedundant' lhs t u t'' u''--addPredicate ::-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()-addPredicate lhs f ts = do-  let Predicate{..} = classify f-      ts' = map (fmap Normal) ts-      lhs' = map (fmap (fmap Normal)) lhs-      -- The "to_p x1 x2 ... xm" term-      construction = App (Constructor f clas_test_case) ts'-      -- The "p_n (to_p x1 x2 ... xn ... xm) = xn"-      -- equations-      equations = [ lhs' :=>: App (Normal (clas_selectors !! i)) [construction] :=: x | (x, i) <- zip ts' [0..]]--  -- Declare the relevant equations as axioms-  mapM_ (lift . add) equations--conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun)-conditionalise (lhs :=>: t :=: u) =-  go lhs t u-  where-    -- Replace one predicate with a conditional-    go lhs t u =-      case [ (p, x, clas_selectors, clas_true) | (App f [Var x]) <- subterms t ++ subterms u, Selector _ p _ <- [classify f], Predicate{..} <- [classify p] ] of-        [] -> sort lhs :=>: t :=: u-        ((p, x, sels, true):_) ->-          let-            n = freeVar [t, u]-            tys = typeArgs (typ p)-            xs = map Var (zipWith V tys [n..])-            subs = [(App (sels !! i) [Var x], xs !! i) | i <- [0..length tys-1]]-          in-            go ((App p xs :=: true):lhs) (replaceMany subs t) (replaceMany subs u)--    replace from to t-      | t == from = to-    replace from to (App f ts) =-      App f (map (replace from to) ts)-    replace _ _ (Var x) = Var x--    replaceMany subs t =-      foldr (uncurry replace) t subs
− src/QuickSpec/Explore/PartialApplication.hs 
@@ -1,95 +0,0 @@--- Pruning support for partial application and the like.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}-module QuickSpec.Explore.PartialApplication where--import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Pruning.Background-import QuickSpec.Prop-import qualified Twee.Base as Twee-import Data.Maybe--data PartiallyApplied f =-    -- A partially-applied function symbol.-    -- The Int describes how many arguments the function expects.-    Partial f Int-    -- The ($) operator, for oversaturated applications.-    -- The type argument is the type of the first argument to ($).-  | Apply Type-  deriving (Eq, Ord, Functor)--instance Sized f => Sized (PartiallyApplied f) where-  size (Partial f _) = size f-  size (Apply _) = 1--instance Arity (PartiallyApplied f) where-  arity (Partial _ n) = n-  arity (Apply _) = 2--instance Pretty f => Pretty (PartiallyApplied f) where-  pPrint (Partial f _) = pPrint f-  pPrint (Apply _) = text "$"--instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where-  termStyle (Partial f _) = termStyle f-  termStyle (Apply _) = invisible--instance PrettyArity f => PrettyArity (PartiallyApplied f) where-  prettyArity (Partial f _) = prettyArity f-  prettyArity (Apply _) = 1--instance Typed f => Typed (PartiallyApplied f) where-  typ (Apply ty) = arrowType [ty] ty-  typ (Partial f _) = typ f-  otherTypesDL (Apply _) = mempty-  otherTypesDL (Partial f _) = otherTypesDL f-  typeSubst_ sub (Apply ty) = Apply (typeSubst_ sub ty)-  typeSubst_ sub (Partial f n) = Partial (typeSubst_ sub f) n--instance (Arity f, Typed f) => Apply (Term (PartiallyApplied f)) where-  tryApply t u = do-    tryApply (typ t) (typ u)-    return $-      case t of-        App (Partial f n) ts | n < arity f ->-          App (Partial f (n+1)) (ts ++ [u])-        _ ->-          simpleApply t u--getTotal :: Arity f => PartiallyApplied f -> Maybe f-getTotal (Partial f n) | arity f == n = Just f-getTotal _ = Nothing--partial :: f -> Term (PartiallyApplied f)-partial f = App (Partial f 0) []--total :: Arity f => f -> PartiallyApplied f-total f = Partial f (arity f)--simpleApply ::-  Typed f =>-  Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)-simpleApply t u =-  App (Apply (typ t)) [t, u]--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] ]-    where-      partial i =-        App (Partial f i) (take i vs)-      vs = map Var (zipWith V (typeArgs (typ f)) [0..])-  background _ = []--evalPartiallyApplied ::-  (Applicative f, Monad m) =>-  (fun -> m (Value f)) ->-  (PartiallyApplied fun -> m (Value f))-evalPartiallyApplied eval (Partial f _) = eval f-evalPartiallyApplied _ (Apply ty) =-  return $ fromJust $-    cast (Twee.build (Twee.app (Twee.fun Arrow) [ty, ty]))-      (toValue (pure (($) :: (A -> B) -> (A -> B))))
− src/QuickSpec/Explore/Polymorphic.hs 
@@ -1,251 +0,0 @@--- Theory exploration which handles polymorphism.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE RecordWildCards #-}-module QuickSpec.Explore.Polymorphic(module QuickSpec.Explore.Polymorphic, Result(..), Universe(..)) where--import qualified QuickSpec.Explore.Schemas as Schemas-import QuickSpec.Explore.Schemas(Schemas, Result(..))-import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Utils-import QuickSpec.Prop-import qualified Data.Map.Strict as Map-import Data.Map(Map)-import qualified Data.Set as Set-import Data.Set(Set)-import Data.Lens.Light-import Control.Monad.Trans.State.Strict-import Control.Monad.Trans.Class-import qualified Twee.Base as Twee-import Control.Monad-import qualified Data.DList as DList--data Polymorphic testcase result fun norm =-  Polymorphic {-    pm_schemas :: Schemas testcase result (PolyFun fun) norm,-    pm_universe :: Universe }--data PolyFun fun =-  PolyFun { fun_original :: fun, fun_specialised :: fun }-  deriving (Eq, Ord)--instance Pretty fun => Pretty (PolyFun fun) where-  pPrint = pPrint . fun_specialised--instance PrettyTerm fun => PrettyTerm (PolyFun fun) where-  termStyle = termStyle . fun_specialised---- The set of all types being explored-data Universe = Universe { univ_types :: Set Type }--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 singleUse univ inst eval =-  Polymorphic {-    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),-    pm_universe = univ }--polyFun :: Typed fun => fun -> PolyFun fun-polyFun x = PolyFun x (oneTypeVar x)--polyTerm :: Typed fun => Term fun -> Term (PolyFun fun)-polyTerm = oneTypeVar . fmap polyFun--instance Typed fun => Typed (PolyFun fun) where-  typ = typ . fun_specialised-  otherTypesDL = otherTypesDL . fun_specialised-  typeSubst_ _ x = x -- because it's supposed to be monomorphic--newtype PolyM testcase result fun norm m a = PolyM { unPolyM :: StateT (Polymorphic testcase result fun norm) m a }-  deriving (Functor, Applicative, Monad)--explore ::-  (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>-  Term fun ->-  StateT (Polymorphic testcase result fun norm) m (Result fun)-explore t = do-  univ <- access univ-  unless (t `usefulForUniverse` univ) $-    error ("Type " ++ prettyShow (typ t) ++ " not in universe for " ++ prettyShow t)-  if not (t `inUniverse` univ) then-    return (Accepted [])-   else do-    res <- exploreNoMGU t-    case res of-      Rejected{} -> return res-      Accepted{} -> do-        ress <- forM (typeInstances univ t) $ \u ->-          exploreNoMGU u-        return res { result_props = concatMap result_props (res:ress) }--exploreNoMGU ::-  (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>-  Term fun ->-  StateT (Polymorphic testcase result fun norm) m (Result fun)-exploreNoMGU t = do-  univ <- access univ-  if not (t `inUniverse` univ) then return (Rejected []) else do-    schemas1 <- access schemas-    (res, schemas2) <- unPolyM (runStateT (Schemas.explore (polyTerm t)) schemas1)-    schemas ~= schemas2-    return (mapProps (regeneralise . mapFun fun_original) res)-  where-    mapProps f (Accepted props) = Accepted (map f props)-    mapProps f (Rejected props) = Rejected (map f props)--instance (PrettyTerm fun, Ord fun, Typed fun, Apply (Term fun), MonadPruner (Term fun) norm m) =>-  MonadPruner (Term (PolyFun fun)) norm (PolyM testcase result fun norm m) where-  normaliser = PolyM $ do-    norm <- normaliser-    return (norm . fmap fun_specialised)-  add prop = PolyM $ do-    univ <- access univ-    let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))-    or <$> mapM add insts--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))---- Given a property which only contains one type variable,--- add as much polymorphism to the property as possible.--- e.g.    map (f :: a -> a) (xs++ys) = map f xs++map f ys--- becomes map (f :: a -> b) (xs++ys) = map f xs++map f ys.-regeneralise :: (PrettyTerm fun, Typed fun, Apply (Term fun)) => Prop (Term fun) -> Prop (Term fun)-regeneralise =-  -- First replace each type variable occurrence with a fresh-  -- type variable (generalise), then unify type variables-  -- where necessary to preserve well-typedness (restrict).-  restrict . unPoly . generalise-  where-    generalise (lhs :=>: rhs) =-      polyApply (:=>:) (polyList (map genLit lhs)) (genLit rhs)-    genLit (t :=: u) = polyApply (:=:) (genTerm t) (genTerm u)-    genTerm (Var (V ty x)) =-      -- It's tempting to return Var (V typeVar x) here.-      -- But this is wrong!-      -- In the case of the type (), we get the law x == y :: (),-      -- which we must not generalise to x == y :: a.-      poly (Var (V (genType ty) x))-    genTerm (App f ts) =-      let-        -- Need to polymorphise all of ts together so that type variables which-        -- only occur in subterms of ts don't get unified-        (f', us) = unPoly (polyPair (poly f) (polyList (map genTerm ts)))-        Just ty = fmap unPoly (polyMgu (polyTyp (poly f')) (polyApply arrowType (poly (map typ us)) (poly typeVar)))-        tys = take (length us) (typeArgs ty)-        Just f'' = cast ty f'-        Just us' = sequence (zipWith cast tys us)-      in-        poly (App f'' us')--    genType = Twee.build . aux 0 . Twee.singleton-      where-        aux !_ Twee.Empty = mempty-        aux n (Twee.Cons (Twee.Var _) ts) =-          Twee.var (Twee.V n) `mappend` aux (n+1) ts-        aux n (Twee.Cons (Twee.App f ts) us) =-          Twee.app f (aux n ts) `mappend`-          aux (n+Twee.lenList ts) us--    restrict prop = typeSubst sub prop-      where-        Just sub = Twee.unifyList (Twee.buildList (map fst cs)) (Twee.buildList (map snd cs))-        cs = [(var_ty x, var_ty y) | x:xs <- vs, y <- xs] ++ concatMap litCs (lhs prop) ++ litCs (rhs prop)-        -- Two variables that were equal before generalisation must have the-        -- same type afterwards-        vs = partitionBy skel (concatMap vars (terms prop >>= subterms))-        skel (V ty x) = V (oneTypeVar ty) x-    litCs (t :=: u) = [(typ t, typ u)]--typeInstancesList :: [Type] -> [Type] -> [Twee.Var -> Type]-typeInstancesList types prop =-  map eval-    (foldr intersection [Map.empty]-      (map constrain-        (usort prop)))-  where-    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--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 ]-  where-    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 univ)-  where-    -- 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]--usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool-t `usefulForUniverse` Universe{..} =-  and [oneTypeVar (typ u) `Set.member` univ_types | u <- properSubterms t] &&-  oneTypeVar (typeRes (typ t)) `Set.member` univ_types
− src/QuickSpec/Explore/Schemas.hs 
@@ -1,168 +0,0 @@--- Theory exploration which works on a schema at a time.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, MultiParamTypeClasses, FlexibleInstances #-}-module QuickSpec.Explore.Schemas where--import qualified Data.Map.Strict as Map-import Data.Map(Map)-import QuickSpec.Prop-import QuickSpec.Pruning-import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Testing-import QuickSpec.Utils-import qualified QuickSpec.Explore.Terms as Terms-import QuickSpec.Explore.Terms(Terms)-import Control.Monad.Trans.State.Strict hiding (State)-import Data.List-import Data.Ord-import Data.Lens.Light-import qualified Data.Set as Set-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) }--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 singleUse inst eval =-  Schemas {-    sc_single_use = singleUse,-    sc_instantiate_singleton = inst,-    sc_empty = Terms.initialState eval,-    sc_classes = Terms.initialState eval,-    sc_instantiated = Set.empty,-    sc_instances = Map.empty }--data Result fun =-    Accepted { result_props :: [Prop (Term fun)] }-  | Rejected { result_props :: [Prop (Term fun)] }---- The schema is represented as a term where there is only one distinct variable of each type-explore ::-  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>-  Term fun -> StateT (Schemas testcase result fun norm) m (Result fun)-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-      if inst t then-        instantiateRep t-       else do-        -- Add the most general instance of the schema-        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))-        return (Accepted [])-    Terms.Discovered ([] :=>: _ :=: u) ->-      exploreIn u t-    Terms.Knew ([] :=>: _ :=: u) ->-      exploreIn u t-    _ -> error "term layer returned non-equational property"--{-# INLINEABLE exploreIn #-}-exploreIn ::-  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>-  Term fun -> Term fun ->-  StateT (Schemas testcase result fun norm) m (Result fun)-exploreIn rep t = do-  -- First check if schema is redundant-  singleUse <- access single_use-  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))-  case res of-    Terms.Discovered prop -> do-      add prop-      return (Rejected [prop])-    Terms.Knew _ ->-      return (Rejected [])-    Terms.Singleton -> do-      -- Instantiate rep too if not already done-      inst <- access instantiated-      props <--        if Set.notMember rep inst-        then result_props <$> instantiateRep rep-        else return []-      res <- instantiate rep t-      return res { result_props = props ++ result_props res }--{-# INLINEABLE instantiateRep #-}-instantiateRep ::-  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>-  Term fun ->-  StateT (Schemas testcase result fun norm) m (Result fun)-instantiateRep t = do-  instantiated %= Set.insert t-  instantiate t t--{-# INLINEABLE instantiate #-}-instantiate ::-  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  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 = 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 :: (Type -> Bool) -> Term f -> Term f-mostGeneral singleUse s = evalState (aux s) Map.empty-  where-    aux (Var (V ty _)) = do-      m <- get-      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 :: (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] | not (singleUse ty) = [V ty x, V ty (succ x)]-    select xs = take 4 xs
− src/QuickSpec/Explore/Terms.hs 
@@ -1,105 +0,0 @@--- Theory exploration which accepts one term at a time.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards #-}-module QuickSpec.Explore.Terms where--import qualified Data.Map.Strict as Map-import Data.Map(Map)-import QuickSpec.Term-import QuickSpec.Prop-import QuickSpec.Type-import QuickSpec.Pruning-import QuickSpec.Testing-import QuickSpec.Testing.DecisionTree hiding (Result, Singleton)-import Control.Monad.Trans.State.Strict hiding (State)-import Data.Lens.Light-import QuickSpec.Utils--data Terms testcase result term norm =-  Terms {-    -- Empty decision tree.-    tm_empty :: DecisionTree testcase result term,-    -- Terms already explored. These are stored in the *values* of the map.-    -- The keys are those terms but normalised.-    -- We do it like this so that explore can guarantee to always return-    -- the same representative for each equivalence class (see below).-    tm_terms  :: Map norm term,-    -- Decision tree mapping test case results to terms.-    -- Terms are not stored normalised.-    -- Terms of different types must not be equal, because that results in-    -- ill-typed equations and bad things happening in the pruner.-    tm_tree   :: Map Type (DecisionTree testcase result term) }--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)--initialState ::-  (term -> testcase -> result) ->-  Terms testcase result term norm-initialState eval =-  Terms {-    tm_empty = empty eval,-    tm_terms = Map.empty,-    tm_tree = Map.empty }--data Result term =-    -- Discovered a new law.-    Discovered (Prop term)-    -- Term is equal to an existing term so redundant.-  | Knew (Prop term)-  | Singleton---- The Prop returned is always t :=: u, where t is the term passed to explore--- and u is the representative of t's equivalence class, not normalised.--- The representatives of the equivalence classes are guaranteed not to change.------ Discovered properties are not added to the pruner.-explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>-  term -> StateT (Terms testcase result term norm) m (Result term)-explore t = do-  res <- explore' t-  -- case res of-  --   Discovered prop -> traceM ("discovered " ++ prettyShow prop)-  --   Knew prop -> traceM ("knew " ++ prettyShow prop)-  --   Singleton -> traceM ("singleton " ++ prettyShow t)-  return res-explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>-  term -> StateT (Terms testcase result term norm) m (Result term)-explore' t = do-  norm <- normaliser-  exp norm $ \prop -> do-    res <- test prop-    case res of-      Nothing -> do-        return (Discovered prop)-      Just tc -> do-        treeForType ty %= addTestCase tc-        exp norm $-          error "returned counterexample failed to falsify property"--  where-    ty = typ t-    exp norm found = do-      tm@Terms{..} <- get-      case Map.lookup t' tm_terms of-        Just u -> return (Knew (t === u))-        Nothing ->-          case insert t (tm ^. treeForType ty) of-            Distinct tree -> do-              put (setL (treeForType ty) tree tm { tm_terms = Map.insert t' t tm_terms })-              return Singleton-            EqualTo u-              -- tm_terms is not kept normalised wrt the discovered laws;-              -- instead, we normalise it lazily like so.-              | t' == u' -> do-                put tm { tm_terms = Map.insert u' u tm_terms }-                return (Knew prop)-              -- Ask QuickCheck for a counterexample to the property.-              | otherwise -> found prop-              where-                u' = norm u-                prop = t === u-      where-        t' = norm t
− src/QuickSpec/Haskell.hs 
@@ -1,696 +0,0 @@-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE PatternGuards #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE DefaultSignatures #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE ConstraintKinds #-}-module QuickSpec.Haskell where--import QuickSpec.Haskell.Resolve-import QuickSpec.Type-import QuickSpec.Prop-import QuickSpec.Pruning-import Test.QuickCheck hiding (total, classify, subterms)-import Data.Constraint hiding ((\\))-import Data.List-import Data.Proxy-import qualified Twee.Base as Twee-import QuickSpec.Term-import Data.Functor.Identity-import Data.Maybe-import Data.MemoUgly-import Test.QuickCheck.Gen.Unsafe-import Data.Char-import Data.Ord-import qualified QuickSpec.Testing.QuickCheck as QuickCheck-import qualified QuickSpec.Pruning.Twee as Twee-import QuickSpec.Explore hiding (quickSpec)-import qualified QuickSpec.Explore-import QuickSpec.Explore.PartialApplication-import QuickSpec.Explore.Polymorphic(Universe(..))-import QuickSpec.Pruning.Background(Background)-import Control.Monad-import Control.Monad.Trans.State.Strict-import QuickSpec.Terminal-import Text.Printf-import QuickSpec.Utils-import Data.Lens.Light-import GHC.TypeLits-import QuickSpec.Explore.Conditionals-import Control.Spoon-import qualified Data.Set as Set-import qualified Test.QuickCheck.Poly as Poly-import Numeric.Natural-import Test.QuickCheck.Instances()--baseInstances :: Instances-baseInstances =-  mconcat [-    -- Generate tuple values (pairs and () are built into findInstance)-    inst $ \(x :: A) (y :: B) (z :: C) -> (x, y, z),-    inst $ \(x :: A) (y :: B) (z :: C) (w :: D) -> (x, y, z, w),-    inst $ \(x :: A) (y :: B) (z :: C) (w :: D) (v :: E) -> (x, y, z, w, v),-    -- Split conjunctions of typeclasses into individuals-    inst $ \() -> Dict :: Dict (),-    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) -> Dict :: Dict (ClassA, ClassB),-    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) -> Dict :: Dict (ClassA, ClassB, ClassC),-    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD),-    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE),-    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) (Dict :: Dict ClassF) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE, ClassF),-    -- Derive typeclass instances using (:-)-    -- N.B. flip is there to resolve (:-) first to reduce backtracking-    inst $ flip $ \(Dict :: Dict ClassA) (Sub Dict :: ClassA :- ClassB) -> Dict :: Dict ClassB,-    -- Standard names-    inst $ \(Names names :: Names A) ->-      Names (map (++ "s") names) :: Names [A],-    inst (Names ["p", "q", "r"] :: Names (A -> Bool)),-    inst (Names ["f", "g", "h"] :: Names (A -> B)),-    inst (Names ["dict"] :: Names (Dict ClassA)),-    inst (Names ["x", "y", "z", "w"] :: Names A),-    -- Standard instances-    baseType (Proxy :: Proxy ()),-    baseType (Proxy :: Proxy Int),-    baseType (Proxy :: Proxy Integer),-    baseType (Proxy :: Proxy Natural),-    baseType (Proxy :: Proxy Bool),-    baseType (Proxy :: Proxy Char),-    baseType (Proxy :: Proxy Poly.OrdA),-    baseType (Proxy :: Proxy Poly.OrdB),-    baseType (Proxy :: Proxy Poly.OrdC),-    inst (Sub Dict :: () :- CoArbitrary ()),-    inst (Sub Dict :: () :- CoArbitrary Int),-    inst (Sub Dict :: () :- CoArbitrary Integer),-    inst (Sub Dict :: () :- CoArbitrary Natural),-    inst (Sub Dict :: () :- CoArbitrary Bool),-    inst (Sub Dict :: () :- CoArbitrary Char),-    inst (Sub Dict :: () :- CoArbitrary Poly.OrdA),-    inst (Sub Dict :: () :- CoArbitrary Poly.OrdB),-    inst (Sub Dict :: () :- CoArbitrary Poly.OrdC),-    inst (Sub Dict :: Eq A :- Eq [A]),-    inst (Sub Dict :: Ord A :- Ord [A]),-    inst (Sub Dict :: Arbitrary A :- Arbitrary [A]),-    inst (Sub Dict :: CoArbitrary A :- CoArbitrary [A]),-    inst (Sub Dict :: Eq A :- Eq (Maybe A)),-    inst (Sub Dict :: Ord A :- Ord (Maybe A)),-    inst (Sub Dict :: Arbitrary A :- Arbitrary (Maybe A)),-    inst (Sub Dict :: CoArbitrary A :- CoArbitrary (Maybe A)),-    inst (Sub Dict :: (Eq A, Eq B) :- Eq (Either A B)),-    inst (Sub Dict :: (Ord A, Ord B) :- Ord (Either A B)),-    inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Either A B)),-    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (Either A B)),-    inst (Sub Dict :: (Eq A, Eq B) :- Eq (A, B)),-    inst (Sub Dict :: (Ord A, Ord B) :- Ord (A, B)),-    inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (A, B)),-    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (A, B)),-    inst (Sub Dict :: (Eq A, Eq B, Eq C) :- Eq (A, B, C)),-    inst (Sub Dict :: (Ord A, Ord B, Ord C) :- Ord (A, B, C)),-    inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C) :- Arbitrary (A, B, C)),-    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C) :- CoArbitrary (A, B, C)),-    inst (Sub Dict :: (Eq A, Eq B, Eq C, Eq D) :- Eq (A, B, C, D)),-    inst (Sub Dict :: (Ord A, Ord B, Ord C, Ord D) :- Ord (A, B, C, D)),-    inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C, Arbitrary D) :- Arbitrary (A, B, C, D)),-    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C, CoArbitrary D) :- CoArbitrary (A, B, C, D)),-    inst (Sub Dict :: (CoArbitrary A, Arbitrary B) :- Arbitrary (A -> B)),-    inst (Sub Dict :: (Arbitrary A, CoArbitrary B) :- CoArbitrary (A -> B)),-    inst (Sub Dict :: Ord A :- Eq A),-    -- From Arbitrary to Gen-    inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,-    -- Observation functions-    inst (\(Dict :: Dict (Observe A B C)) -> observeObs :: ObserveData C B),-    inst (\(Dict :: Dict (Ord A)) -> observeOrd :: ObserveData A A),-    inst (\(Dict :: Dict (Arbitrary A)) (obs :: ObserveData B C) -> observeFunction obs :: ObserveData (A -> B) C),-    inst (\(obs :: ObserveData A B) -> WrappedObserveData (toValue obs)),-    -- No warnings for TestCaseWrapped-    inst (NoWarnings :: NoWarnings (TestCaseWrapped SymA A)),-    -- Needed for typeclass-polymorphic predicates to work currently-    inst (\(Dict :: Dict ClassA) -> Dict :: Dict (Arbitrary (Dict ClassA)))]---- 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---- | A typeclass for types which support observational equality, typically used--- for types that have no `Ord` instance.------ An instance @Observe test outcome a@ declares that values of type @a@ can be--- /tested/ for equality by random testing. You supply a function--- @observe :: test -> outcome -> a@. Then, two values @x@ and @y@ are considered--- equal, if for many random values of type @test@, @observe test x == observe test y@.------ The function `QuickSpec.monoTypeObserve` declares a monomorphic--- type with an observation function. For polymorphic types, use--- `QuickSpec.inst` to declare the `Observe` instance.------ For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.-class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where-  -- | Make an observation on a value. Should satisfy the following law: if-  -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@.-  observe :: test -> a -> outcome--  default observe :: (test ~ (), outcome ~ a) => test -> a -> outcome-  observe _ x = x--instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where-  observe (x, obs) f = observe obs (f x)---- An observation function along with instances.--- The parameters are in this order so that we can use findInstance to get at appropriate Wrappers.-data ObserveData a outcome where-  ObserveData :: (Arbitrary test, Ord outcome) => (test -> a -> outcome) -> ObserveData a outcome-newtype WrappedObserveData a = WrappedObserveData (Value (ObserveData a))--observeOrd :: Ord a => ObserveData a a-observeOrd = ObserveData (\() x -> x)--observeFunction :: Arbitrary a => ObserveData b outcome -> ObserveData (a -> b) outcome-observeFunction (ObserveData obs) =-  ObserveData (\(x, test) f -> obs test (f x))--observeObs :: Observe test outcome a => ObserveData a outcome-observeObs = ObserveData observe--baseType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Instances-baseType _ =-  mconcat [-    inst (Dict :: Dict (Ord a)),-    inst (Dict :: Dict (Arbitrary a))]---- Declares what variable names should be used for values of a particular type.-newtype Names a = Names { getNames :: [String] }--names :: Instances -> Type -> [String]-names insts ty =-  case findInstance insts (skolemiseTypeVars ty) of-    Just x  -> ofValue getNames x-    Nothing -> error "don't know how to name variables"---- An Ordy a represents a value of type a together with its Ord instance.--- A Value Ordy is a value of unknown type which implements Ord.-data Ordy a where Ordy :: Ord a => a -> Ordy a-instance Eq (Value Ordy) where x == y = compare x y == EQ--instance Ord (Value Ordy) where-  compare x y =-    case unwrap x of-      Ordy xv `In` w ->-        let Ordy yv = reunwrap w y in-        compare xv yv---- | A test case is everything you need to evaluate a Haskell term.-data TestCase =-  TestCase {-    -- | Evaluate a variable. Returns @Nothing@ if no `Arbitrary` instance was found.-    tc_eval_var :: Var -> Maybe (Value Identity),-    -- | Apply an observation function to get a value implementing `Ord`.-    -- Returns @Nothing@ if no observer was found.-    tc_test_result :: Value Identity -> Maybe (Value Ordy) }---- | Generate a random test case.-arbitraryTestCase :: Type -> Instances -> Gen TestCase-arbitraryTestCase def insts =-  TestCase <$> arbitraryValuation def insts <*> arbitraryObserver def insts---- | Generate a random variable valuation.-arbitraryValuation :: Type -> Instances -> Gen (Var -> Maybe (Value Identity))-arbitraryValuation def insts = do-  memo <$> arbitraryFunction (sequence . findGenerator def insts . var_ty)---- | Generate a random observation.-arbitraryObserver :: Type -> Instances -> Gen (Value Identity -> Maybe (Value Ordy))-arbitraryObserver def insts = do-  find <- arbitraryFunction $ sequence . findObserver insts-  return $ \x -> do-    obs <- find (defaultTo def (typ x))-    return (obs x)--findGenerator :: Type -> Instances -> Type -> Maybe (Gen (Value Identity))-findGenerator def insts ty =-  bringFunctor <$> (findInstance insts (defaultTo def ty) :: Maybe (Value Gen))--findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy))-findObserver insts ty = do-  inst <- findInstance insts ty :: Maybe (Value WrappedObserveData)-  return $-    case unwrap inst of-      WrappedObserveData val `In` valueWrapper ->-        case unwrap val of-          -- This brings Arbitrary and Ord instances into scope-          ObserveData obs `In` outcomeWrapper -> do-            test <- arbitrary-            return $ \x ->-              let value = runIdentity (reunwrap valueWrapper x)-                  outcome = obs test value-              in wrap outcomeWrapper (Ordy outcome)---- | Generate a random function. Should be in QuickCheck.-arbitraryFunction :: CoArbitrary a => (a -> Gen b) -> Gen (a -> b)-arbitraryFunction gen = promote (\x -> coarbitrary x (gen x))---- | Evaluate a Haskell term in an environment.-evalHaskell :: Type -> Instances -> TestCase -> Term (PartiallyApplied Constant) -> Either (Value Ordy) (Term (PartiallyApplied Constant))-evalHaskell def insts (TestCase env obs) t =-  maybe (Right t) Left $ do-    let eval env t = evalTerm env (evalPartiallyApplied (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 {-    con_name  :: String,-    con_style :: TermStyle,-    con_pretty_arity :: Int,-    con_value :: Value Identity,-    con_type :: Type,-    con_constraints :: [Type],-    con_size :: Int,-    con_classify :: Classification Constant }--instance Eq Constant where-  x == y =-    con_name x == con_name y && typ (con_value x) == typ (con_value y)--instance Ord Constant where-  compare =-    comparing $ \con ->-      (con_name con, twiddle (arity con), typ con)-      where-        -- This trick comes from Prover9 and improves the ordering somewhat-        twiddle 1 = 2-        twiddle 2 = 1-        twiddle x = x--instance Background Constant--con :: Typeable a => String -> a -> Constant-con name val =-  constant' name (toValue (Identity val))--constant' :: String -> Value Identity -> Constant-constant' name val =-  Constant {-    con_name = name,-    con_style =-      case () of-        _ | name == "()" -> curried-          | take 1 name == "," -> fixedArity (length name+1) tupleStyle-          | take 2 name == "(," -> fixedArity (length name-1) tupleStyle-          | isOp name && typeArity (typ val) >= 2 -> infixStyle 5-          | isOp name -> prefix-          | otherwise -> curried,-    con_pretty_arity =-      case () of-        _ | isOp name && typeArity (typ val) >= 2 -> 2-          | isOp name -> 1-          | otherwise -> typeArity (typ val),-    con_value = val,-    con_type = ty,-    con_constraints = constraints,-    con_size = 1,-    con_classify = Function }-  where-    (constraints, ty) = splitConstrainedType (typ val)--isOp :: String -> Bool-isOp "[]" = False-isOp ('"':_) = False-isOp xs | all (== '.') xs = True-isOp xs = not (all isIdent xs)-  where-    isIdent x = isAlphaNum x || x == '\'' || x == '_' || x == '.'---- Get selectors of a predicate-selectors :: Constant -> [Constant]-selectors con =-  case con_classify con of-    Predicate{..} -> clas_selectors-    _ -> []---- Move the constraints of a constant back into the main type-unhideConstraint :: Constant -> Constant-unhideConstraint con =-  con {-    con_type = typ (con_value con),-    con_constraints = [] }--instance Typed Constant where-  typ = con_type-  otherTypesDL con =-    return (typ (con_value con)) `mplus`-    case con_classify con of-      Predicate{..} ->-        -- Don't call typesDL on clas_selectors because it in turn-        -- contains a reference to the predicate-        typesDL (map con_value clas_selectors) `mplus` typesDL clas_test_case `mplus` typesDL clas_true-      Selector{..} ->-        typesDL clas_pred `mplus` typesDL clas_test_case-      Function -> mzero-  typeSubst_ sub con =-    con { con_value = typeSubst_ sub (con_value con),-          con_type = typeSubst_ sub (con_type con),-          con_constraints = map (typeSubst_ sub) (con_constraints con),-          con_classify = fmap (typeSubst_ sub) (con_classify con) }--instance Pretty Constant where-  pPrint = text . con_name--instance PrettyTerm Constant where-  termStyle = con_style--instance PrettyArity Constant where-  prettyArity = con_pretty_arity--instance Sized Constant where-  size = con_size--instance Arity Constant where-  arity = typeArity . typ--instance Predicate Constant where-  classify = con_classify--evalConstant :: Instances -> Constant -> Maybe (Value Identity)-evalConstant insts Constant{..} = foldM app con_value con_constraints-  where-    app val constraint = do-      dict <- findValue insts constraint-      return (apply val dict)--class Predicateable a where-  -- A test case for predicates of type a-  -- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))`-  ---  -- Some speedup should be possible by using unboxed tuples instead...-  type PredicateTestCase a-  uncrry :: a -> PredicateTestCase a -> Bool--instance Predicateable Bool where-  type PredicateTestCase Bool = ()-  uncrry = const--instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where-  type PredicateTestCase (a -> b) = (a, PredicateTestCase b)-  uncrry f (a, b) = uncrry (f a) b--data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }--true :: Constant-true = con "True" True--trueTerm :: Term (PartiallyApplied Constant)-trueTerm = App (total true) []---- | 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 =-  let-    -- The following doesn't compile on GHC 7.10:-    -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))-    -- (where sym was created using someSymbolVal)-    -- So do it by hand instead:-    ty = addName (typeRep (Proxy :: Proxy (TestCaseWrapped SymA (PredicateTestCase a))))--    -- Replaces SymA with 'String name'-    -- (XXX: not correct if the type 'a' also contains SymA)-    addName :: forall a. Typed a => a -> a-    addName = typeSubst sub-      where-        sub x-          | Twee.build (Twee.var x) == typeRep (Proxy :: Proxy SymA) =-            Twee.builder (typeFromTyCon (String name))-          | otherwise = Twee.var x--    instances =-      mconcat $ map (valueInst . addName)-        [toValue (Identity inst1), toValue (Identity inst2)]--    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))-    inst1 x = TestCaseWrapped <$> gen x--    inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))-    inst2 = Names [name ++ "_var"]--    conPred = (con name pred) { con_classify = Predicate conSels ty (App true []) }-    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 =-      fromJust (cast (arrowType [ty] (typeArgs (typeOf pred) !! i)) (unPoly (compose (sel i) unwrapV)))-      where-        compose f g = apply (apply cmpV f) g-        sel 0 = fstV-        sel n = compose (sel (n-1)) sndV-        fstV = toPolyValue (fst :: (A, B) -> A)-        sndV = toPolyValue (snd :: (A, B) -> B)-        cmpV = toPolyValue ((.) :: (B -> C) -> (A -> B) -> A -> C)-        unwrapV = toPolyValue (unTestCaseWrapped :: TestCaseWrapped SymA A -> A)-  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_background :: [Prop (Term (PartiallyApplied Constant))],-    cfg_print_filter :: Prop (Term (PartiallyApplied Constant)) -> 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_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 =-  Config {-    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_background = [],-    cfg_print_filter = \_ -> True }---- Extra types for the universe that come from in-scope instances.-instanceTypes :: Instances -> Config -> [Type]-instanceTypes insts Config{..}-  | not cfg_infer_instance_types = []-  | otherwise =-    [ tv-    | cls <- dicts,-      inst <- groundInstances,-      sub <- maybeToList (matchType cls inst),-      (_, tv) <- Twee.substToList sub ]-  where-    dicts =-      concatMap con_constraints (concat cfg_constants) >>=-      maybeToList . getDictionary--    groundInstances :: [Type]-    groundInstances =-      [ dict-      | -- () :- dict-        Twee.App tc (Twee.Cons (Twee.App unit Twee.Empty) (Twee.Cons dict Twee.Empty)) <--        map (typeRes . typ) (is_instances insts),-        Twee.fun_value tc == tyCon (Proxy :: Proxy (:-)),-        Twee.fun_value unit == tyCon (Proxy :: Proxy (() :: Constraint)),-        Twee.isGround dict ]--data Warnings =-  Warnings {-    warn_no_generator :: [Type],-    warn_no_observer :: [Type] }--warnings :: Universe -> Instances -> Config -> Warnings-warnings univ insts Config{..} =-  Warnings {-    warn_no_generator =-      [ ty | ty <- types, isNothing (findGenerator cfg_default_to insts ty) ],-    warn_no_observer =-      [ ty | ty <- types, isNothing (findObserver insts ty) ] }-  where-    -- Check after defaulting types to Int (or whatever it is)-    types =-      [ ty-      | ty <- defaultTo cfg_default_to . Set.toList . univ_types $ univ,-        isNothing (findInstance insts ty :: Maybe (Value NoWarnings)) ]--instance Pretty Warnings where-  pPrint Warnings{..} =-    vcat $-      [section genDoc warn_no_generator] ++-      [section obsDoc warn_no_observer] ++-      [text "" | warnings ]-    where-      warnings = not (null warn_no_generator) || not (null warn_no_observer)-      section _ [] = pPrintEmpty-      section doc xs =-        doc $$-        nest 2 (vcat (map pPrintType xs)) $$-        text ""--      genDoc =-        text "WARNING: The following types have no 'Arbitrary' instance declared." $$-        text "You will not get any variables of the following types:"--      obsDoc =-        text "WARNING: The following types have no 'Ord' or 'Observe' instance declared." $$-        text "You will not get any equations about the following types:"--quickSpec :: Config -> IO [Prop (Term (PartiallyApplied Constant))]-quickSpec cfg@Config{..} = do-  let-    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-    instances = cfg_instances `mappend` baseInstances--    eval = evalHaskell cfg_default_to instances--    present funs prop = do-      norm <- normaliser-      let prop' = makeDefinition funs (ac norm (conditionalise 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:-    --   * it is of the form f lhs = rhs (or vice versa).-    --   * f is not a background function.-    --   * lhs only contains background functions.-    --   * rhs does not contain f.-    --   * all vars in rhs appear in lhs-    makeDefinition cons (lhs :=>: t :=: u)-      | Just (f, ts) <- defines u,-        f `notElem` mapMaybe getTotal (funs t),-        null (usort (vars t) \\ vars ts) =-        lhs :=>: u :=: t-        -- In the case where t defines f, the equation is already oriented correctly-      | otherwise = lhs :=>: t :=: u-      where-        defines (App (Partial f _) ts)-          | f `elem` cons,-            all (`notElem` cons) (mapMaybe getTotal (funs ts)) = Just (f, ts)-        defines _ = Nothing--    -- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative-    ac norm (lhs :=>: App f [Var x, App f1 [Var y, Var z]] :=: App f2 [Var y1, App f3 [Var x1, Var z1]])-      | f == f1, f1 == f2, f2 == f3,-        x == x1, y == y1, z == z1,-        x /= y, y /= z, x /= z,-        norm (App f [Var x, Var y]) == norm (App f [Var y, Var x]) =-          lhs :=>: App f [App f [Var x, Var y], Var z] :=: App f [Var x, App f [Var y, Var z]]-    ac _ prop = prop--    -- Add a type signature when printing the equation x = y.-    maybeType (_ :=>: x@(Var _) :=: Var _) =-      text "::" <+> pPrintType (typ x)-    maybeType _ = pPrintEmpty--    -- XXX do this during testing-    constraintsOk (Partial f _) = constraintsOk1 f-    constraintsOk (Apply _) = True-    constraintsOk1 = memo $ \con ->-      or [ and [ isJust (findValue instances (defaultTo cfg_default_to constraint)) | constraint <- con_constraints (typeSubst sub con) ]-         | ty <- Set.toList (univ_types univ),-           sub <- maybeToList (matchType (typeRes (typ con)) ty) ]--    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-          (map (partial . unhideConstraint) (f cfg_constants))-        putLine ""-      when (n > 0) $ do-        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 cfg_max_commutative_size singleUse univ-        (enumerator [partial fun | fun <- constantsOf g])-      when (n > 0) $ do-        putLine ""--    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--  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 (map total constants) $-    fmap (reverse . snd) $ flip execStateT (1, []) main
− src/QuickSpec/Haskell/Resolve.hs 
@@ -1,117 +0,0 @@--- A data structure for resolving typeclass instances and similar at runtime.------ Takes as input a set of functions ("instances"), and a type, and--- tries to build a value of that type from the instances given.------ For example, given the instances---   ordList :: Dict (Arbitrary a) -> Dict (Arbitrary [a])---   ordChar :: Dict (Arbitrary Char)--- and the target type Dict (Arbitrary [Char]), it will produce the value---   ordList ordChar :: Dict (Arbitrary [Char]).------ The instances can in fact be arbitrary Haskell functions - though--- their types must be such that the instance search will terminate.--{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}-module QuickSpec.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where--import Twee.Base-import QuickSpec.Type-import Data.MemoUgly-import Data.Functor.Identity-import Data.Maybe-import Data.Proxy-import Control.Monad-import Data.Semigroup(Semigroup(..))---- A set of instances.-data Instances =-  Instances {-    -- The available instances.-    -- Each instance is a unary function; 'inst' sees to this.-    is_instances :: [Poly (Value Identity)],-    -- The resulting instance search function (memoised).-    is_find      :: Type -> [Value Identity] }---- A smart constructor for Instances.-makeInstances :: [Poly (Value Identity)] -> Instances-makeInstances is = inst-  where-    inst = Instances is (memo (find_ inst . canonicaliseType))--instance Semigroup Instances where-  x <> y = makeInstances (is_instances x ++ is_instances y)-instance Monoid Instances where-  mempty = makeInstances []-  mappend = (<>)---- Create a single instance.-inst :: Typeable a => a -> Instances-inst x = valueInst (toValue (Identity x))--valueInst :: Value Identity -> Instances-valueInst x = polyInst (poly x)-  where-    polyInst :: Poly (Value Identity) -> Instances-    polyInst x =-      -- Transform x into a single-argument function-      -- (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)) ->-          polyInst (apply uncur x)-        App (F Arrow) _ ->-          makeInstances [x]-        -- A plain old value x (not a function) turns into \() -> x.-        _ ->-          makeInstances [apply delay x]-      where-        uncur = toPolyValue (uncurry :: (A -> B -> C) -> (A, B) -> C)-        delay = toPolyValue ((\x () -> x) :: A -> () -> A)---- Construct a value of a particular type.--- If the type is polymorphic, may return an instance of it.-findValue :: Instances -> Type -> Maybe (Value Identity)-findValue insts = listToMaybe . is_find insts . skolemiseTypeVars---- Given a type a, construct a value of type f a.--- If the type is polymorphic, may return an instance of it.-findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f)-findInstance insts ty =-  unwrapFunctor runIdentity <$> findValue insts ty'-  where-    ty' = typeRep (Proxy :: Proxy f) `applyType` ty---- The unmemoised version of the search algorithm.--- Knows how to apply unary functions, and also knows how to generate:---   * The unit type ()---   * Pairs (a, b) - search for a and then for b--- These two are important because instValue encodes other instances--- using them.------ Invariant: the type of the returned value is an instance of the argument type.-find_ :: Instances -> Type -> [Value Identity]-find_ _ (App (F unit) Empty)-  | unit == tyCon (Proxy :: Proxy ()) =-    return (toValue (Identity ()))-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))-    -- N.B.: subst sub ty2 because searching for x may have constrained y's type-    y <- is_find insts (subst sub ty2)-    sub <- maybeToList (match ty2 (typ y))-    return (pairValues (liftM2 (,)) (typeSubst sub x) y)-find_ insts ty = do-  -- 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)-  sub <- maybeToList (unify ty res)-  fun <- return (typeSubst sub fun)-  arg <- return (typeSubst sub arg)-  -- Find an argument for that function and apply the function.-  val <- is_find insts arg-  sub <- maybeToList (match arg (typ val))-  return (apply (typeSubst sub fun) val)
+ src/QuickSpec/Internal.hs view
@@ -0,0 +1,343 @@+-- | The main QuickSpec module, with internal stuff exported.+-- For QuickSpec hackers only.+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-}+module QuickSpec.Internal where++import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))+import qualified QuickSpec.Internal.Haskell as Haskell+import qualified QuickSpec.Internal.Haskell.Resolve as Haskell+import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck+import qualified QuickSpec.Internal.Pruning.UntypedTwee as Twee+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Term(Term)+import Test.QuickCheck+import Test.QuickCheck.Random+import Data.Constraint+import Data.Lens.Light+import QuickSpec.Internal.Utils+import QuickSpec.Internal.Type hiding (defaultTo)+import Data.Proxy+import System.Environment+import Data.Semigroup(Semigroup(..))++-- | Run QuickSpec. See the documentation at the top of this file.+quickSpec :: Signature sig => sig -> IO ()+quickSpec sig = do+  quickSpecResult sig+  return ()++-- | Run QuickSpec, returning the list of discovered properties.+quickSpecResult :: Signature sig => sig -> IO [Prop (Term Haskell.Constant)]+quickSpecResult sig = do+  -- Undocumented feature for testing :)+  seed <- lookupEnv "QUICKCHECK_SEED"+  let+    sig' = case seed of+      Nothing -> signature sig+      Just xs -> signature [signature sig, withFixedSeed (read xs)]++  Haskell.quickSpec (runSig sig' (Context 1 []) Haskell.defaultConfig)++-- | Add some properties to the background theory.+addBackground :: [Prop (Term 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 }++-- Settings for building the signature.+-- Int: number of nested calls to 'background'.+-- [String]: list of names to exclude.+data Context = Context Int [String]++instance Semigroup Sig where+  Sig sig1 <> Sig sig2 = Sig (\ctx -> sig2 ctx . sig1 ctx)+instance Monoid Sig where+  mempty = Sig (\_ -> id)+  mappend = (<>)++-- | A class of things that can be used as a QuickSpec signature.+class Signature sig where+  -- | Convert the thing to a signature.+  signature :: sig -> Sig++instance Signature Sig where+  signature = id++instance Signature sig => Signature [sig] where+  signature = mconcat . map signature++runSig :: Signature sig => sig -> Context -> Haskell.Config -> Haskell.Config+runSig = unSig . signature++-- | Declare a constant with a given name and value.+-- If the constant you want to use is polymorphic, you can use the types+-- `A`, `B`, `C`, `D`, `E` to monomorphise it, for example:+--+-- > constant "reverse" (reverse :: [A] -> [A])+--+-- QuickSpec will then understand that the constant is really polymorphic.+con :: Typeable a => String -> a -> Sig+con name x =+  Sig $ \ctx@(Context _ names) ->+    if name `elem` names then id else+      unSig (customConstant (Haskell.con name x)) ctx++-- | Add a custom constant.+customConstant :: Haskell.Constant -> Sig+customConstant con =+  Sig $ \(Context n _) ->+    modL Haskell.lens_constants (appendAt n [con])++-- | Type class constraints as first class citizens+type c ==> t = Dict c -> t++-- | Lift a constrained type to a `==>` type which QuickSpec+-- can work with+liftC :: (c => a) -> c ==> a+liftC a Dict = a++-- | Add an instance of a type class to the signature+instanceOf :: forall c. (Typeable c, c) => Sig+instanceOf = inst (Sub Dict :: () :- c)++-- | 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.+--+-- For example:+--+-- @+-- sig = [+--   `con` "delete" (`Data.List.delete` :: Int -> [Int] -> [Int]),+--   `con` "insert" (`Data.List.insert` :: Int -> [Int] -> [Int]),+--   predicate "member" (member :: Int -> [Int] -> Bool) ]+-- @+predicate :: ( Predicateable a+             , Typeable a+             , Typeable (PredicateTestCase a))+             => String -> a -> Sig+predicate name x =+  Sig $ \ctx@(Context _ names) ->+    if name `elem` names then id else+    let (insts, con) = Haskell.predicate name x in+      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+monoType _ =+  mconcat [+    inst (Sub Dict :: () :- Ord a),+    inst (Sub Dict :: () :- Arbitrary a)]++-- | Declare a new monomorphic type using observational equivalence.+-- The type must implement `Observe` and `Arbitrary`.+monoTypeObserve :: forall proxy test outcome a.+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>+  proxy a -> Sig+monoTypeObserve _ =+  mconcat [+    inst (Sub Dict :: () :- Observe test outcome a),+    inst (Sub Dict :: () :- Arbitrary a)]++-- | Declare a new monomorphic type, saying how you want variables of that type to be named.+monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig+monoTypeWithVars xs proxy =+  monoType proxy `mappend` vars xs proxy++-- | Customize how variables of a particular type are named.+vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig+vars xs _ = instFun (Names xs :: Names a)++-- | 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+-- the following two declarations to your signature:+--+-- @+-- `inst` (`Sub` `Dict` :: (Ord A, Ord B) `:-` Ord (Map A B))+-- `inst` (`Sub` `Dict` :: (Arbitrary A, Arbitrary B) `:-` Arbitrary (Map A B))+-- @+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)++addInstances :: Haskell.Instances -> Sig+addInstances insts =+  Sig (\_ -> modL Haskell.lens_instances (`mappend` insts))++withPrintFilter :: (Prop (Term 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.+-- Declaring background functions may improve the laws you get out.+--+-- Here is an example, which tests @++@ and @length@, giving @0@ and @+@ as+-- background functions:+--+-- > main = quickSpec [+-- >   con "++" ((++) :: [A] -> [A] -> [A]),+-- >   con "length" (length :: [A] -> Int),+-- >+-- >   background [+-- >     con "0" (0 :: Int),+-- >     con "+" ((+) :: Int -> Int -> Int) ] ]+background :: Signature sig => sig -> Sig+background sig =+  Sig (\(Context _ xs) -> runSig sig (Context 0 xs))++-- | Remove a function or predicate from the signature.+-- Useful in combination with 'prelude' and friends.+without :: Signature sig => sig -> [String] -> Sig+without sig xs =+  Sig (\(Context n ys) -> runSig sig (Context n (ys ++ xs)))++-- | Run QuickCheck on a series of signatures. Tests the functions in the first+-- signature, then adds the functions in the second signature, then adds the+-- functions in the third signature, and so on.+--+-- This can be useful when you have a core API you want to test first, and a+-- larger API you want to test later. The laws for the core API will be printed+-- separately from the laws for the larger API.+--+-- Here is an example which first tests @0@ and @+@ and then adds @++@ and @length@:+--+-- > main = quickSpec [sig1, sig2]+-- >   where+-- >     sig1 = [+-- >       con "0" (0 :: Int),+-- >       con "+" ((+) :: Int -> Int -> Int) ]+-- >     sig2 = [+-- >       con "++" ((++) :: [A] -> [A] -> [A]),+-- >       con "length" (length :: [A] -> Int) ]+series :: Signature sig => [sig] -> Sig+series = foldr op mempty . map signature+  where+    op sig sigs = sig `mappend` later (signature sigs)+    later sig =+      Sig (\(Context n xs) cfg -> unSig sig (Context (n+1) xs) cfg)++-- | 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+withMaxTests n =+  Sig (\_ -> setL (QuickCheck.lens_num_tests # Haskell.lens_quickCheck) n)++-- | Set the maximum value for QuickCheck's size parameter when generating test+-- data (default: 20).+withMaxTestSize :: Int -> Sig+withMaxTestSize n =+  Sig (\_ -> setL (QuickCheck.lens_max_test_size # Haskell.lens_quickCheck) n)++-- | Set which type polymorphic terms are tested at.+defaultTo :: Typeable a => proxy a -> Sig+defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy))++-- | Set how hard QuickSpec tries to filter out redundant equations (default: no limit).+--+-- If you experience long pauses when running QuickSpec, try setting this number+-- to 2 or 3.+withPruningDepth :: Int -> Sig+withPruningDepth n =+  Sig (\_ -> setL (Twee.lens_max_cp_depth # Haskell.lens_twee) n)++-- | Set the maximum term size QuickSpec will reason about when it filters out+-- redundant equations (default: same as maximum term size).+--+-- If you get laws you believe are redundant, try increasing this number to 1 or+-- 2 more than the maximum term size.+withPruningTermSize :: Int -> Sig+withPruningTermSize n =+  Sig (\_ -> setL (Twee.lens_max_term_size # Haskell.lens_twee) n)++-- | Set the random number seed used for test case generation.+-- Useful if you want repeatable results.+withFixedSeed :: Int -> Sig+withFixedSeed s = Sig (\_ -> setL (QuickCheck.lens_fixed_seed # Haskell.lens_quickCheck) (Just . mkQCGen $ s))++-- | Automatically infer types to add to the universe from+-- available type class instances+withInferInstanceTypes :: Sig+withInferInstanceTypes = Sig (\_ -> setL (Haskell.lens_infer_instance_types) True)++-- | A signature containing boolean functions:+-- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.+bools :: Sig+bools = background [+  "||"    `con` (||),+  "&&"    `con` (&&),+  "not"   `con` not,+  "True"  `con` True,+  "False" `con` False]++-- | A signature containing arithmetic operations:+-- @0@, @1@, @(`+`)@.+-- Instantiate it with e.g. @arith (`Proxy` :: `Proxy` `Int`)@.+arith :: forall proxy a. (Typeable a, Ord a, Num a, Arbitrary a) => proxy a -> Sig+arith proxy = background [+  monoType proxy,+  "0" `con` (0   :: a),+  "1" `con` (1   :: a),+  "+" `con` ((+) :: a -> a -> a)]++-- | A signature containing list operations:+-- @[]@, @(:)@, @(`++`)@.+lists :: Sig+lists = background [+  "[]"      `con` ([]      :: [A]),+  ":"       `con` ((:)     :: A -> [A] -> [A]),+  "++"      `con` ((++)    :: [A] -> [A] -> [A])]++-- | A signature containing higher-order functions:+-- @(`.`)@ and `id`.+-- Useful for testing `map` and similar.+funs :: Sig+funs = background [+  "."  `con` ((.) :: (A -> A) -> (A -> A) -> (A -> A)),+  "id" `con` (id  :: A -> A) ]++-- | The QuickSpec prelude.+-- Contains boolean, arithmetic and list functions, and function composition.+-- For more precise control over what gets included,+-- see 'bools', 'arith', 'lists', 'funs' and 'without'.+prelude :: Sig+prelude = signature [bools, arith (Proxy :: Proxy Int), lists]
+ src/QuickSpec/Internal/Explore.hs view
@@ -0,0 +1,99 @@+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleContexts #-}+module QuickSpec.Internal.Explore where++import QuickSpec.Internal.Explore.Polymorphic+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Utils+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Terminal+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.Trans.State.Strict+import Text.Printf+import Data.Semigroup(Semigroup(..))++newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] }++-- N.B. order matters!+-- Later enumerators get to see terms which were generated by earlier ones.+instance Semigroup (Enumerator a) where+  e1 <> e2 = Enumerator $ \n tss ->+    let us = enumerate e1 n tss+        vs = enumerate e2 n (appendAt n us tss)+    in us ++ vs+instance Monoid (Enumerator a) where+  mempty = Enumerator (\_ _ -> [])+  mappend = (<>)++mapEnumerator :: ([a] -> [a]) -> Enumerator a -> Enumerator a+mapEnumerator f e =+  Enumerator $ \n tss ->+    f (enumerate e n tss)++filterEnumerator :: (a -> Bool) -> Enumerator a -> Enumerator a+filterEnumerator p e =+  mapEnumerator (filter p) e++enumerateConstants :: Sized a => [a] -> Enumerator a+enumerateConstants ts = Enumerator (\n _ -> [t | t <- ts, size t == n])++enumerateApplications :: Apply a => Enumerator a+enumerateApplications = Enumerator $ \n tss ->+    [ unPoly v+    | i <- [0..n],+      t <- tss !! i,+      u <- tss !! (n-i),+      Just v <- [tryApply (poly t) (poly u)] ]++filterUniverse :: Typed f => Universe -> Enumerator (Term f) -> Enumerator (Term f)+filterUniverse univ e =+  filterEnumerator (`usefulForUniverse` univ) e++sortTerms :: Ord b => (a -> b) -> Enumerator a -> Enumerator a+sortTerms measure e =+  mapEnumerator (sortBy' measure) e++quickSpec ::+  (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) ->+  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()+quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do+  let+    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval++    loop m n _ | m > n = return ()+    loop m n tss = do+      putStatus (printf "enumerating terms of size %d" m)+      let+        ts = enumerate (filterUniverse univ enum) m tss+        total = length ts+        consider (i, t) = do+          putStatus (printf "testing terms of size %d: %d/%d" m i total)+          res <- explore t+          putStatus (printf "testing terms of size %d: %d/%d" m i total)+          lift $ mapM_ present (result_props res)+          case res of+            Accepted _ -> return True+            Rejected _ -> return False+      us <- map snd <$> filterM consider (zip [1 :: Int ..] ts)+      clearStatus+      loop (m+1) n (appendAt m us tss)++  evalStateT (loop 0 maxSize (repeat [])) state0++pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc+pPrintSignature funs =+  text "== Functions ==" $$+  vcat (map pPrintDecl decls)+  where+    decls = [ (prettyShow f, pPrintType (typ f)) | f <- funs ]+    maxWidth = maximum (0:map (length . fst) decls)+    pad xs = nest (maxWidth - length xs) (text xs)+    pPrintDecl (name, ty) =+      pad name <+> text "::" <+> ty
+ src/QuickSpec/Internal/Explore/Conditionals.hs view
@@ -0,0 +1,216 @@+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE DeriveFunctor #-}+module QuickSpec.Internal.Explore.Conditionals where++import QuickSpec.Internal.Prop+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Pruning.Background(Background(..))+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Terminal+import QuickSpec.Internal.Utils+import QuickSpec.Internal.Explore.Polymorphic+import qualified Twee.Base as Twee+import Data.List+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.IO.Class++newtype Conditionals m a = Conditionals (m a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)+instance MonadTrans Conditionals where+  lift = Conditionals+instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  MonadPruner (Term fun) norm (Conditionals m) where+  normaliser = lift $ do+    norm <- normaliser+    return (norm . fmap Normal)+  add prop = do+    redundant <- conditionallyRedundant prop+    if redundant then return False else do+      res <- lift (add (mapFun Normal prop))+      when res (considerConditionalising prop)+      return res++conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe+conditionalsUniverse tys funs =+  universe $+    tys +++    (map typ $+      map Normal funs +++      [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])++runConditionals ::+  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  [fun] -> Conditionals m a -> m a+runConditionals preds mx =+  run (mapM_ considerPredicate preds >> mx)+  where+    run (Conditionals mx) = mx++class Predicate fun where+  classify :: fun -> Classification fun++data Classification fun =+    Predicate { clas_selectors :: [fun], clas_test_case :: Type, clas_true :: Term fun }+  | Selector { clas_index :: Int, clas_pred :: fun, clas_test_case :: Type }+  | Function+  deriving (Eq, Ord, Functor)++data WithConstructor fun =+    Constructor fun Type+  | Normal fun+  deriving (Eq, Ord)++instance Sized fun => Sized (WithConstructor fun) where+  size Constructor{} = 0+  size (Normal f) = size f++instance Arity fun => Arity (WithConstructor fun) where+  arity Constructor{} = 1+  arity (Normal f) = arity f++instance Pretty fun => Pretty (WithConstructor fun) where+  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"+  pPrintPrec l p (Normal f) = pPrintPrec l p f++instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where+  termStyle (Constructor _ _) = curried+  termStyle (Normal f) = termStyle f++instance PrettyArity fun => PrettyArity (WithConstructor fun) where+  prettyArity (Constructor _ _) = 1+  prettyArity (Normal f) = prettyArity f++instance (Predicate fun, Background fun) => Background (WithConstructor fun) where+  background (Normal f) = map (mapFun Normal) (background f)+  background _ = []++instance Typed fun => Typed (WithConstructor fun) where+  typ (Constructor pred ty) =+    arrowType (typeArgs (typ pred)) ty+  typ (Normal f) = typ f+  otherTypesDL (Constructor pred _) = typesDL pred+  otherTypesDL (Normal f) = otherTypesDL f+  typeSubst_ sub (Constructor pred ty) = Constructor (typeSubst_ sub pred) (typeSubst_ sub ty)+  typeSubst_ sub (Normal f) = Normal (typeSubst_ sub f)++predType :: TyCon -> [Type] -> Type+predType name tys =+  Twee.build (Twee.app (Twee.fun name) tys)++considerPredicate ::+  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  fun -> Conditionals m ()+considerPredicate f =+  case classify f of+    Predicate sels ty true -> do+      let+        x = Var (V ty 0)+        eqns =+          [Fun (Constructor f ty) :@: [Fun (Normal sel) :$: x | sel <- sels] === x,+           Fun (Normal f) :@: [Fun (Normal sel) :$: x | sel <- sels] === fmap Normal true]+      mapM_ (lift . add) eqns+    _ -> return ()++considerConditionalising ::+  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  Prop (Term fun) -> Conditionals m ()+considerConditionalising (lhs :=>: t :=: u) = do+  norm <- normaliser+  -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True"+  -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n"+  -- to the set of known equations+  case t of+    Fun f :@: ts | Predicate{..} <- classify f -> -- It is an interesting predicate, i.e. it was added by the user+      when (norm u == norm clas_true) $+        addPredicate lhs f ts+    _ -> return ()++conditionallyRedundant ::+  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  Prop (Term fun) -> Conditionals m Bool+conditionallyRedundant (lhs :=>: t :=: u) = do+  t' <- normalise t+  u' <- normalise u+  conditionallyRedundant' lhs t u t' u'++conditionallyRedundant' ::+  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool+conditionallyRedundant' lhs t u t' u' = do+  forM_ (usort (funs [t, u])) $ \f ->+    case classify f of+      Selector{..} -> do+        let+          Predicate{..} = classify clas_pred+          tys = typeArgs (typ clas_pred)+          argss = sequence [ [ arg | arg <- terms [t, u] >>= subterms, typ arg == ty ] | ty <- tys ]+        forM_ argss $ \args -> do+          norm <- normaliser+          let p = Fun clas_pred :@: args+          when (norm p == norm clas_true) $ do+            addPredicate lhs clas_pred args+      _ -> return ()++  t'' <- normalise t+  u'' <- normalise u+  if t'' == u'' then+    return True+   else if t'' == t' && u'' == u' then+     return False+    else+     conditionallyRedundant' lhs t u t'' u''++addPredicate ::+  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()+addPredicate lhs f ts = do+  let Predicate{..} = classify f+      ts' = map (fmap Normal) ts+      lhs' = map (fmap (fmap Normal)) lhs+      -- The "to_p x1 x2 ... xm" term+      construction = Fun (Constructor f clas_test_case) :@: ts'+      -- The "p_n (to_p x1 x2 ... xn ... xm) = xn"+      -- equations+      equations = [ lhs' :=>: Fun (Normal (clas_selectors !! i)) :$: construction :=: x | (x, i) <- zip ts' [0..]]++  -- Declare the relevant equations as axioms+  mapM_ (lift . add) equations++conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun)+conditionalise (lhs :=>: t :=: u) =+  go lhs t u+  where+    -- Replace one predicate with a conditional+    go lhs t u =+      case [ (p, x, clas_selectors, clas_true) | Fun f :$: Var x <- subterms t ++ subterms u, Selector _ p _ <- [classify f], Predicate{..} <- [classify p] ] of+        [] -> sort lhs :=>: t :=: u+        ((p, x, sels, true):_) ->+          let+            n = freeVar [t, u]+            tys = typeArgs (typ p)+            xs = map Var (zipWith V tys [n..])+            subs = [(Fun (sels !! i) :$: Var x, xs !! i) | i <- [0..length tys-1]]+          in+            go ((Fun p :@: xs :=: true):lhs) (replaceMany subs t) (replaceMany subs u)++    replace from to t+      | t == from = to+    replace from to (t :$: u) =+      replace from to t :$: replace from to u+    replace _ _ (Var x) = Var x+    replace _ _ (Fun f) = Fun f++    replaceMany subs t =+      foldr (uncurry replace) t subs
+ src/QuickSpec/Internal/Explore/Polymorphic.hs view
@@ -0,0 +1,251 @@+-- Theory exploration which handles polymorphism.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE RecordWildCards #-}+module QuickSpec.Internal.Explore.Polymorphic(module QuickSpec.Internal.Explore.Polymorphic, Result(..), Universe(..)) where++import qualified QuickSpec.Internal.Explore.Schemas as Schemas+import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..))+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Utils+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Terminal+import qualified Data.Map.Strict as Map+import Data.Map(Map)+import qualified Data.Set as Set+import Data.Set(Set)+import Data.Lens.Light+import Control.Monad.Trans.State.Strict+import Control.Monad.Trans.Class+import qualified Twee.Base as Twee+import Control.Monad+import qualified Data.DList as DList++data Polymorphic testcase result fun norm =+  Polymorphic {+    pm_schemas :: Schemas testcase result (PolyFun fun) norm,+    pm_universe :: Universe }++data PolyFun fun =+  PolyFun { fun_original :: fun, fun_specialised :: fun }+  deriving (Eq, Ord)++instance Pretty fun => Pretty (PolyFun fun) where+  pPrint = pPrint . fun_specialised++instance PrettyTerm fun => PrettyTerm (PolyFun fun) where+  termStyle = termStyle . fun_specialised++-- The set of all types being explored+data Universe = Universe { univ_types :: Set Type }++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 singleUse univ inst eval =+  Polymorphic {+    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),+    pm_universe = univ }++polyFun :: Typed fun => fun -> PolyFun fun+polyFun x = PolyFun x (oneTypeVar x)++polyTerm :: Typed fun => Term fun -> Term (PolyFun fun)+polyTerm = oneTypeVar . fmap polyFun++instance Typed fun => Typed (PolyFun fun) where+  typ = typ . fun_specialised+  otherTypesDL = otherTypesDL . fun_specialised+  typeSubst_ _ x = x -- because it's supposed to be monomorphic++newtype PolyM testcase result fun norm m a = PolyM { unPolyM :: StateT (Polymorphic testcase result fun norm) m a }+  deriving (Functor, Applicative, Monad)++explore ::+  (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>+  Term fun ->+  StateT (Polymorphic testcase result fun norm) m (Result fun)+explore t = do+  univ <- access univ+  unless (t `usefulForUniverse` univ) $+    error ("Type " ++ prettyShow (typ t) ++ " not in universe for " ++ prettyShow t)+  if not (t `inUniverse` univ) then+    return (Accepted [])+   else do+    res <- exploreNoMGU t+    case res of+      Rejected{} -> return res+      Accepted{} -> do+        ress <- forM (typeInstances univ t) $ \u ->+          exploreNoMGU u+        return res { result_props = concatMap result_props (res:ress) }++exploreNoMGU ::+  (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>+  Term fun ->+  StateT (Polymorphic testcase result fun norm) m (Result fun)+exploreNoMGU t = do+  univ <- access univ+  if not (t `inUniverse` univ) then return (Rejected []) else do+    schemas1 <- access schemas+    (res, schemas2) <- unPolyM (runStateT (Schemas.explore (polyTerm t)) schemas1)+    schemas ~= schemas2+    return (mapProps (regeneralise . mapFun fun_original) res)+  where+    mapProps f (Accepted props) = Accepted (map f props)+    mapProps f (Rejected props) = Rejected (map f props)++instance (PrettyTerm fun, Ord fun, Typed fun, Apply (Term fun), MonadPruner (Term fun) norm m, MonadTerminal m) =>+  MonadPruner (Term (PolyFun fun)) norm (PolyM testcase result fun norm m) where+  normaliser = PolyM $ do+    norm <- normaliser+    return (norm . fmap fun_specialised)+  add prop = PolyM $ do+    univ <- access univ+    let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))+    or <$> mapM add insts++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))++-- Given a property which only contains one type variable,+-- add as much polymorphism to the property as possible.+-- e.g.    map (f :: a -> a) (xs++ys) = map f xs++map f ys+-- becomes map (f :: a -> b) (xs++ys) = map f xs++map f ys.+regeneralise :: (PrettyTerm fun, Typed fun, Apply (Term fun)) => Prop (Term fun) -> Prop (Term fun)+regeneralise =+  -- First replace each type variable occurrence with a fresh+  -- type variable (generalise), then unify type variables+  -- where necessary to preserve well-typedness (restrict).+  restrict . unPoly . generalise+  where+    generalise (lhs :=>: rhs) =+      polyApply (:=>:) (polyList (map genLit lhs)) (genLit rhs)+    genLit (t :=: u) = polyApply (:=:) (genTerm t) (genTerm u)+    genTerm (Var (V ty x)) =+      -- It's tempting to return Var (V typeVar x) here.+      -- But this is wrong!+      -- In the case of the type (), we get the law x == y :: (),+      -- which we must not generalise to x == y :: a.+      poly (Var (V (genType ty) x))+    genTerm (Fun f) = poly (Fun f)+    genTerm (t :$: u) =+      let+        (t', u') = unPoly (polyPair (genTerm t) (genTerm u))+        Just ty = fmap unPoly (polyMgu (polyTyp (poly t')) (polyApply (\arg res -> arrowType [arg] res) (polyTyp (poly u')) (poly typeVar)))+        Just (arg, _) = unpackArrow ty+        Just t'' = cast ty t'+        Just u'' = cast arg u'+      in+        poly (t'' :$: u'')++    genType = Twee.build . aux 0 . Twee.singleton+      where+        aux !_ Twee.Empty = mempty+        aux n (Twee.Cons (Twee.Var _) ts) =+          Twee.var (Twee.V n) `mappend` aux (n+1) ts+        aux n (Twee.Cons (Twee.App f ts) us) =+          Twee.app f (aux n ts) `mappend`+          aux (n+Twee.lenList ts) us++    restrict prop = typeSubst sub prop+      where+        Just sub = Twee.unifyList (Twee.buildList (map fst cs)) (Twee.buildList (map snd cs))+        cs = [(var_ty x, var_ty y) | x:xs <- vs, y <- xs] ++ concatMap litCs (lhs prop) ++ litCs (rhs prop)+        -- Two variables that were equal before generalisation must have the+        -- same type afterwards+        vs = partitionBy skel (concatMap vars (terms prop))+        skel (V ty x) = V (oneTypeVar ty) x+    litCs (t :=: u) = [(typ t, typ u)]++typeInstancesList :: [Type] -> [Type] -> [Twee.Var -> Type]+typeInstancesList types prop =+  map eval+    (foldr intersection [Map.empty]+      (map constrain+        (usort prop)))+  where+    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++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) >>= subtermsFO)) ]++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 ]+  where+    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 univ)+  where+    -- 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 =+          case unpackArrow ty of+            Just (arg, res) ->+              [ty] ++ arrows1 arg ++ arrows1 res+            _ -> []+ +inUniverse :: (PrettyTerm fun, Typed fun) => Term fun -> Universe -> Bool+t `inUniverse` Universe{..} =+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- subtermsFO t ++ map Var (vars t)]++usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool+t `usefulForUniverse` Universe{..} =+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- properSubtermsFO t ++ map Var (vars t)] &&+  oneTypeVar (typeRes (typ t)) `Set.member` univ_types
+ src/QuickSpec/Internal/Explore/Schemas.hs view
@@ -0,0 +1,169 @@+-- Theory exploration which works on a schema at a time.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards, TupleSections, MultiParamTypeClasses, FlexibleInstances #-}+module QuickSpec.Internal.Explore.Schemas where++import qualified Data.Map.Strict as Map+import Data.Map(Map)+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Utils+import qualified QuickSpec.Internal.Explore.Terms as Terms+import QuickSpec.Internal.Explore.Terms(Terms)+import Control.Monad.Trans.State.Strict hiding (State)+import Data.List+import Data.Ord+import Data.Lens.Light+import qualified Data.Set as Set+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) }++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 singleUse inst eval =+  Schemas {+    sc_single_use = singleUse,+    sc_instantiate_singleton = inst,+    sc_empty = Terms.initialState eval,+    sc_classes = Terms.initialState eval,+    sc_instantiated = Set.empty,+    sc_instances = Map.empty }++data Result fun =+    Accepted { result_props :: [Prop (Term fun)] }+  | Rejected { result_props :: [Prop (Term fun)] }++-- The schema is represented as a term where there is only one distinct variable of each type+explore ::+  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  Term fun -> StateT (Schemas testcase result fun norm) m (Result fun)+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+      if inst t then+        instantiateRep t+       else do+        -- Add the most general instance of the schema+        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))+        return (Accepted [])+    Terms.Discovered ([] :=>: _ :=: u) ->+      exploreIn u t+    Terms.Knew ([] :=>: _ :=: u) ->+      exploreIn u t+    _ -> error "term layer returned non-equational property"++{-# INLINEABLE exploreIn #-}+exploreIn ::+  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  Term fun -> Term fun ->+  StateT (Schemas testcase result fun norm) m (Result fun)+exploreIn rep t = do+  -- First check if schema is redundant+  singleUse <- access single_use+  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))+  case res of+    Terms.Discovered prop -> do+      add prop+      return (Rejected [prop])+    Terms.Knew _ ->+      return (Rejected [])+    Terms.Singleton -> do+      -- Instantiate rep too if not already done+      inst <- access instantiated+      props <-+        if Set.notMember rep inst+        then result_props <$> instantiateRep rep+        else return []+      res <- instantiate rep t+      return res { result_props = props ++ result_props res }++{-# INLINEABLE instantiateRep #-}+instantiateRep ::+  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  Term fun ->+  StateT (Schemas testcase result fun norm) m (Result fun)+instantiateRep t = do+  instantiated %= Set.insert t+  instantiate t t++{-# INLINEABLE instantiate #-}+instantiate ::+  (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,+  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 = 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 :: (Type -> Bool) -> Term f -> Term f+mostGeneral singleUse s = evalState (aux s) Map.empty+  where+    aux (Var (V ty _)) = do+      m <- get+      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 (Fun f) = return (Fun f)+    aux (t :$: u) = liftM2 (:$:) (aux t) (aux u)++mostSpecific :: Term f -> Term f+mostSpecific = subst (\(V ty _) -> Var (V ty 0))++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] | not (singleUse ty) = [V ty x, V ty (succ x)]+    select xs = take 4 xs
+ src/QuickSpec/Internal/Explore/Terms.hs view
@@ -0,0 +1,105 @@+-- Theory exploration which accepts one term at a time.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, PatternGuards #-}+module QuickSpec.Internal.Explore.Terms where++import qualified Data.Map.Strict as Map+import Data.Map(Map)+import QuickSpec.Internal.Term+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Type+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Testing.DecisionTree hiding (Result, Singleton)+import Control.Monad.Trans.State.Strict hiding (State)+import Data.Lens.Light+import QuickSpec.Internal.Utils++data Terms testcase result term norm =+  Terms {+    -- Empty decision tree.+    tm_empty :: DecisionTree testcase result term,+    -- Terms already explored. These are stored in the *values* of the map.+    -- The keys are those terms but normalised.+    -- We do it like this so that explore can guarantee to always return+    -- the same representative for each equivalence class (see below).+    tm_terms  :: Map norm term,+    -- Decision tree mapping test case results to terms.+    -- Terms are not stored normalised.+    -- Terms of different types must not be equal, because that results in+    -- ill-typed equations and bad things happening in the pruner.+    tm_tree   :: Map Type (DecisionTree testcase result term) }++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)++initialState ::+  (term -> testcase -> result) ->+  Terms testcase result term norm+initialState eval =+  Terms {+    tm_empty = empty eval,+    tm_terms = Map.empty,+    tm_tree = Map.empty }++data Result term =+    -- Discovered a new law.+    Discovered (Prop term)+    -- Term is equal to an existing term so redundant.+  | Knew (Prop term)+  | Singleton++-- The Prop returned is always t :=: u, where t is the term passed to explore+-- and u is the representative of t's equivalence class, not normalised.+-- The representatives of the equivalence classes are guaranteed not to change.+--+-- Discovered properties are not added to the pruner.+explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>+  term -> StateT (Terms testcase result term norm) m (Result term)+explore t = do+  res <- explore' t+  -- case res of+  --   Discovered prop -> traceM ("discovered " ++ prettyShow prop)+  --   Knew prop -> traceM ("knew " ++ prettyShow prop)+  --   Singleton -> traceM ("singleton " ++ prettyShow t)+  return res+explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>+  term -> StateT (Terms testcase result term norm) m (Result term)+explore' t = do+  norm <- normaliser+  exp norm $ \prop -> do+    res <- test prop+    case res of+      Nothing -> do+        return (Discovered prop)+      Just tc -> do+        treeForType ty %= addTestCase tc+        exp norm $+          error "returned counterexample failed to falsify property"++  where+    ty = typ t+    exp norm found = do+      tm@Terms{..} <- get+      case Map.lookup t' tm_terms of+        Just u -> return (Knew (t === u))+        Nothing ->+          case insert t (tm ^. treeForType ty) of+            Distinct tree -> do+              put (setL (treeForType ty) tree tm { tm_terms = Map.insert t' t tm_terms })+              return Singleton+            EqualTo u+              -- tm_terms is not kept normalised wrt the discovered laws;+              -- instead, we normalise it lazily like so.+              | t' == u' -> do+                put tm { tm_terms = Map.insert u' u tm_terms }+                return (Knew prop)+              -- Ask QuickCheck for a counterexample to the property.+              | otherwise -> found prop+              where+                u' = norm u+                prop = t === u+      where+        t' = norm t
+ src/QuickSpec/Internal/Haskell.hs view
@@ -0,0 +1,693 @@+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ConstraintKinds #-}+module QuickSpec.Internal.Haskell where++import QuickSpec.Internal.Haskell.Resolve+import QuickSpec.Internal.Type+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Pruning+import Test.QuickCheck hiding (total, classify, subterms, Fun)+import Data.Constraint hiding ((\\))+import Data.List+import Data.Proxy+import qualified Twee.Base as Twee+import QuickSpec.Internal.Term+import Data.Functor.Identity+import Data.Maybe+import Data.MemoUgly+import Test.QuickCheck.Gen.Unsafe+import Data.Char+import Data.Ord+import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck+import qualified QuickSpec.Internal.Pruning.Twee as Twee+import QuickSpec.Internal.Explore hiding (quickSpec)+import qualified QuickSpec.Internal.Explore+import QuickSpec.Internal.Explore.Polymorphic(Universe(..))+import QuickSpec.Internal.Pruning.Background(Background)+import Control.Monad+import Control.Monad.Trans.State.Strict+import QuickSpec.Internal.Terminal+import Text.Printf+import QuickSpec.Internal.Utils+import Data.Lens.Light+import GHC.TypeLits+import QuickSpec.Internal.Explore.Conditionals+import Control.Spoon+import qualified Data.Set as Set+import qualified Test.QuickCheck.Poly as Poly+import Numeric.Natural+import Test.QuickCheck.Instances()++baseInstances :: Instances+baseInstances =+  mconcat [+    -- Generate tuple values (pairs and () are built into findInstance)+    inst $ \(x :: A) (y :: B) (z :: C) -> (x, y, z),+    inst $ \(x :: A) (y :: B) (z :: C) (w :: D) -> (x, y, z, w),+    inst $ \(x :: A) (y :: B) (z :: C) (w :: D) (v :: E) -> (x, y, z, w, v),+    -- Split conjunctions of typeclasses into individuals+    inst $ \() -> Dict :: Dict (),+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) -> Dict :: Dict (ClassA, ClassB),+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) -> Dict :: Dict (ClassA, ClassB, ClassC),+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD),+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE),+    inst $ \(Dict :: Dict ClassA) (Dict :: Dict ClassB) (Dict :: Dict ClassC) (Dict :: Dict ClassD) (Dict :: Dict ClassE) (Dict :: Dict ClassF) -> Dict :: Dict (ClassA, ClassB, ClassC, ClassD, ClassE, ClassF),+    -- Derive typeclass instances using (:-)+    -- N.B. flip is there to resolve (:-) first to reduce backtracking+    inst $ flip $ \(Dict :: Dict ClassA) (Sub Dict :: ClassA :- ClassB) -> Dict :: Dict ClassB,+    -- Standard names+    inst $ \(Names names :: Names A) ->+      Names (map (++ "s") names) :: Names [A],+    inst (Names ["p", "q", "r"] :: Names (A -> Bool)),+    inst (Names ["f", "g", "h"] :: Names (A -> B)),+    inst (Names ["dict"] :: Names (Dict ClassA)),+    inst (Names ["x", "y", "z", "w"] :: Names A),+    -- Standard instances+    baseType (Proxy :: Proxy ()),+    baseType (Proxy :: Proxy Int),+    baseType (Proxy :: Proxy Integer),+    baseType (Proxy :: Proxy Natural),+    baseType (Proxy :: Proxy Bool),+    baseType (Proxy :: Proxy Char),+    baseType (Proxy :: Proxy Poly.OrdA),+    baseType (Proxy :: Proxy Poly.OrdB),+    baseType (Proxy :: Proxy Poly.OrdC),+    inst (Sub Dict :: () :- CoArbitrary ()),+    inst (Sub Dict :: () :- CoArbitrary Int),+    inst (Sub Dict :: () :- CoArbitrary Integer),+    inst (Sub Dict :: () :- CoArbitrary Natural),+    inst (Sub Dict :: () :- CoArbitrary Bool),+    inst (Sub Dict :: () :- CoArbitrary Char),+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdA),+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdB),+    inst (Sub Dict :: () :- CoArbitrary Poly.OrdC),+    inst (Sub Dict :: Eq A :- Eq [A]),+    inst (Sub Dict :: Ord A :- Ord [A]),+    inst (Sub Dict :: Arbitrary A :- Arbitrary [A]),+    inst (Sub Dict :: CoArbitrary A :- CoArbitrary [A]),+    inst (Sub Dict :: Eq A :- Eq (Maybe A)),+    inst (Sub Dict :: Ord A :- Ord (Maybe A)),+    inst (Sub Dict :: Arbitrary A :- Arbitrary (Maybe A)),+    inst (Sub Dict :: CoArbitrary A :- CoArbitrary (Maybe A)),+    inst (Sub Dict :: (Eq A, Eq B) :- Eq (Either A B)),+    inst (Sub Dict :: (Ord A, Ord B) :- Ord (Either A B)),+    inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Either A B)),+    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (Either A B)),+    inst (Sub Dict :: (Eq A, Eq B) :- Eq (A, B)),+    inst (Sub Dict :: (Ord A, Ord B) :- Ord (A, B)),+    inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (A, B)),+    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B) :- CoArbitrary (A, B)),+    inst (Sub Dict :: (Eq A, Eq B, Eq C) :- Eq (A, B, C)),+    inst (Sub Dict :: (Ord A, Ord B, Ord C) :- Ord (A, B, C)),+    inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C) :- Arbitrary (A, B, C)),+    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C) :- CoArbitrary (A, B, C)),+    inst (Sub Dict :: (Eq A, Eq B, Eq C, Eq D) :- Eq (A, B, C, D)),+    inst (Sub Dict :: (Ord A, Ord B, Ord C, Ord D) :- Ord (A, B, C, D)),+    inst (Sub Dict :: (Arbitrary A, Arbitrary B, Arbitrary C, Arbitrary D) :- Arbitrary (A, B, C, D)),+    inst (Sub Dict :: (CoArbitrary A, CoArbitrary B, CoArbitrary C, CoArbitrary D) :- CoArbitrary (A, B, C, D)),+    inst (Sub Dict :: (CoArbitrary A, Arbitrary B) :- Arbitrary (A -> B)),+    inst (Sub Dict :: (Arbitrary A, CoArbitrary B) :- CoArbitrary (A -> B)),+    inst (Sub Dict :: Ord A :- Eq A),+    -- From Arbitrary to Gen+    inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,+    -- Observation functions+    inst (\(Dict :: Dict (Observe A B C)) -> observeObs :: ObserveData C B),+    inst (\(Dict :: Dict (Ord A)) -> observeOrd :: ObserveData A A),+    inst (\(Dict :: Dict (Arbitrary A)) (obs :: ObserveData B C) -> observeFunction obs :: ObserveData (A -> B) C),+    inst (\(obs :: ObserveData A B) -> WrappedObserveData (toValue obs)),+    -- No warnings for TestCaseWrapped+    inst (NoWarnings :: NoWarnings (TestCaseWrapped SymA A)),+    -- Needed for typeclass-polymorphic predicates to work currently+    inst (\(Dict :: Dict ClassA) -> Dict :: Dict (Arbitrary (Dict ClassA)))]++-- 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++-- | A typeclass for types which support observational equality, typically used+-- for types that have no `Ord` instance.+--+-- An instance @Observe test outcome a@ declares that values of type @a@ can be+-- /tested/ for equality by random testing. You supply a function+-- @observe :: test -> outcome -> a@. Then, two values @x@ and @y@ are considered+-- equal, if for many random values of type @test@, @observe test x == observe test y@.+--+-- The function `QuickSpec.monoTypeObserve` declares a monomorphic+-- type with an observation function. For polymorphic types, use+-- `QuickSpec.inst` to declare the `Observe` instance.+--+-- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.+class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where+  -- | Make an observation on a value. Should satisfy the following law: if+  -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@.+  observe :: test -> a -> outcome++  default observe :: (test ~ (), outcome ~ a) => test -> a -> outcome+  observe _ x = x++instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where+  observe (x, obs) f = observe obs (f x)++-- An observation function along with instances.+-- The parameters are in this order so that we can use findInstance to get at appropriate Wrappers.+data ObserveData a outcome where+  ObserveData :: (Arbitrary test, Ord outcome) => (test -> a -> outcome) -> ObserveData a outcome+newtype WrappedObserveData a = WrappedObserveData (Value (ObserveData a))++observeOrd :: Ord a => ObserveData a a+observeOrd = ObserveData (\() x -> x)++observeFunction :: Arbitrary a => ObserveData b outcome -> ObserveData (a -> b) outcome+observeFunction (ObserveData obs) =+  ObserveData (\(x, test) f -> obs test (f x))++observeObs :: Observe test outcome a => ObserveData a outcome+observeObs = ObserveData observe++baseType :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => proxy a -> Instances+baseType _ =+  mconcat [+    inst (Dict :: Dict (Ord a)),+    inst (Dict :: Dict (Arbitrary a))]++-- Declares what variable names should be used for values of a particular type.+newtype Names a = Names { getNames :: [String] }++names :: Instances -> Type -> [String]+names insts ty =+  case findInstance insts (skolemiseTypeVars ty) of+    Just x  -> ofValue getNames x+    Nothing -> error "don't know how to name variables"++-- An Ordy a represents a value of type a together with its Ord instance.+-- A Value Ordy is a value of unknown type which implements Ord.+data Ordy a where Ordy :: Ord a => a -> Ordy a+instance Eq (Value Ordy) where x == y = compare x y == EQ++instance Ord (Value Ordy) where+  compare x y =+    case unwrap x of+      Ordy xv `In` w ->+        let Ordy yv = reunwrap w y in+        compare xv yv++-- | A test case is everything you need to evaluate a Haskell term.+data TestCase =+  TestCase {+    -- | Evaluate a variable. Returns @Nothing@ if no `Arbitrary` instance was found.+    tc_eval_var :: Var -> Maybe (Value Identity),+    -- | Apply an observation function to get a value implementing `Ord`.+    -- Returns @Nothing@ if no observer was found.+    tc_test_result :: Value Identity -> Maybe (Value Ordy) }++-- | Generate a random test case.+arbitraryTestCase :: Type -> Instances -> Gen TestCase+arbitraryTestCase def insts =+  TestCase <$> arbitraryValuation def insts <*> arbitraryObserver def insts++-- | Generate a random variable valuation.+arbitraryValuation :: Type -> Instances -> Gen (Var -> Maybe (Value Identity))+arbitraryValuation def insts = do+  memo <$> arbitraryFunction (sequence . findGenerator def insts . var_ty)++-- | Generate a random observation.+arbitraryObserver :: Type -> Instances -> Gen (Value Identity -> Maybe (Value Ordy))+arbitraryObserver def insts = do+  find <- arbitraryFunction $ sequence . findObserver insts+  return $ \x -> do+    obs <- find (defaultTo def (typ x))+    return (obs x)++findGenerator :: Type -> Instances -> Type -> Maybe (Gen (Value Identity))+findGenerator def insts ty =+  bringFunctor <$> (findInstance insts (defaultTo def ty) :: Maybe (Value Gen))++findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy))+findObserver insts ty = do+  inst <- findInstance insts ty :: Maybe (Value WrappedObserveData)+  return $+    case unwrap inst of+      WrappedObserveData val `In` valueWrapper ->+        case unwrap val of+          -- This brings Arbitrary and Ord instances into scope+          ObserveData obs `In` outcomeWrapper -> do+            test <- arbitrary+            return $ \x ->+              let value = runIdentity (reunwrap valueWrapper x)+                  outcome = obs test value+              in wrap outcomeWrapper (Ordy outcome)++-- | Generate a random function. Should be in QuickCheck.+arbitraryFunction :: CoArbitrary a => (a -> Gen b) -> Gen (a -> b)+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++data Constant =+  Constant {+    con_name  :: String,+    con_style :: TermStyle,+    con_pretty_arity :: Int,+    con_value :: Value Identity,+    con_type :: Type,+    con_constraints :: [Type],+    con_size :: Int,+    con_classify :: Classification Constant }++instance Eq Constant where+  x == y =+    con_name x == con_name y && typ (con_value x) == typ (con_value y)++instance Ord Constant where+  compare =+    comparing $ \con ->+      (con_name con, twiddle (arity con), typ con)+      where+        -- This trick comes from Prover9 and improves the ordering somewhat+        twiddle 1 = 2+        twiddle 2 = 1+        twiddle x = x++instance Background Constant++con :: Typeable a => String -> a -> Constant+con name val =+  constant' name (toValue (Identity val))++constant' :: String -> Value Identity -> Constant+constant' name val =+  Constant {+    con_name = name,+    con_style =+      case () of+        _ | name == "()" -> curried+          | take 1 name == "," -> fixedArity (length name+1) tupleStyle+          | take 2 name == "(," -> fixedArity (length name-1) tupleStyle+          | isOp name && typeArity (typ val) >= 2 -> infixStyle 5+          | isOp name -> prefix+          | otherwise -> curried,+    con_pretty_arity =+      case () of+        _ | isOp name && typeArity (typ val) >= 2 -> 2+          | isOp name -> 1+          | otherwise -> typeArity (typ val),+    con_value = val,+    con_type = ty,+    con_constraints = constraints,+    con_size = 1,+    con_classify = Function }+  where+    (constraints, ty) = splitConstrainedType (typ val)++isOp :: String -> Bool+isOp "[]" = False+isOp ('"':_) = False+isOp xs | all (== '.') xs = True+isOp xs = not (all isIdent xs)+  where+    isIdent x = isAlphaNum x || x == '\'' || x == '_' || x == '.'++-- Get selectors of a predicate+selectors :: Constant -> [Constant]+selectors con =+  case con_classify con of+    Predicate{..} -> clas_selectors+    _ -> []++-- Move the constraints of a constant back into the main type+unhideConstraint :: Constant -> Constant+unhideConstraint con =+  con {+    con_type = typ (con_value con),+    con_constraints = [] }++instance Typed Constant where+  typ = con_type+  otherTypesDL con =+    return (typ (con_value con)) `mplus`+    case con_classify con of+      Predicate{..} ->+        -- Don't call typesDL on clas_selectors because it in turn+        -- contains a reference to the predicate+        typesDL (map con_value clas_selectors) `mplus` typesDL clas_test_case `mplus` typesDL clas_true+      Selector{..} ->+        typesDL clas_pred `mplus` typesDL clas_test_case+      Function -> mzero+  typeSubst_ sub con =+    con { con_value = typeSubst_ sub (con_value con),+          con_type = typeSubst_ sub (con_type con),+          con_constraints = map (typeSubst_ sub) (con_constraints con),+          con_classify = fmap (typeSubst_ sub) (con_classify con) }++instance Pretty Constant where+  pPrint = text . con_name++instance PrettyTerm Constant where+  termStyle = con_style++instance PrettyArity Constant where+  prettyArity = con_pretty_arity++instance Sized Constant where+  size = con_size++instance Arity Constant where+  arity = typeArity . typ++instance Predicate Constant where+  classify = con_classify++evalConstant :: Instances -> Constant -> Maybe (Value Identity)+evalConstant insts Constant{..} = foldM app con_value con_constraints+  where+    app val constraint = do+      dict <- findValue insts constraint+      return (apply val dict)++class Predicateable a where+  -- A test case for predicates of type a+  -- if `a ~ A -> B -> C -> Bool` we get `TestCase a ~ (A, (B, (C, ())))`+  --+  -- Some speedup should be possible by using unboxed tuples instead...+  type PredicateTestCase a+  uncrry :: a -> PredicateTestCase a -> Bool++instance Predicateable Bool where+  type PredicateTestCase Bool = ()+  uncrry = const++instance forall a b. (Predicateable b, Typeable a) => Predicateable (a -> b) where+  type PredicateTestCase (a -> b) = (a, PredicateTestCase b)+  uncrry f (a, b) = uncrry (f a) b++data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }++true :: Constant+true = con "True" True++trueTerm :: Term Constant+trueTerm = Fun true++-- | 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 =+  let+    -- The following doesn't compile on GHC 7.10:+    -- ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (PredicateTestCase a)))+    -- (where sym was created using someSymbolVal)+    -- So do it by hand instead:+    ty = addName (typeRep (Proxy :: Proxy (TestCaseWrapped SymA (PredicateTestCase a))))++    -- Replaces SymA with 'String name'+    -- (XXX: not correct if the type 'a' also contains SymA)+    addName :: forall a. Typed a => a -> a+    addName = typeSubst sub+      where+        sub x+          | Twee.build (Twee.var x) == typeRep (Proxy :: Proxy SymA) =+            Twee.builder (typeFromTyCon (String name))+          | otherwise = Twee.var x++    instances =+      mconcat $ map (valueInst . addName)+        [toValue (Identity inst1), toValue (Identity inst2)]++    inst1 :: b -> Gen (TestCaseWrapped SymA (PredicateTestCase a))+    inst1 x = TestCaseWrapped <$> gen x++    inst2 :: Names (TestCaseWrapped SymA (PredicateTestCase a))+    inst2 = Names [name ++ "_var"]++    conPred = (con name pred) { con_classify = Predicate conSels ty (Fun true) }+    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 =+      fromJust (cast (arrowType [ty] (typeArgs (typeOf pred) !! i)) (unPoly (compose (sel i) unwrapV)))+      where+        compose f g = apply (apply cmpV f) g+        sel 0 = fstV+        sel n = compose (sel (n-1)) sndV+        fstV = toPolyValue (fst :: (A, B) -> A)+        sndV = toPolyValue (snd :: (A, B) -> B)+        cmpV = toPolyValue ((.) :: (B -> C) -> (A -> B) -> A -> C)+        unwrapV = toPolyValue (unTestCaseWrapped :: TestCaseWrapped SymA A -> A)+  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_background :: [Prop (Term Constant)],+    cfg_print_filter :: Prop (Term Constant) -> 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_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 =+  Config {+    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_background = [],+    cfg_print_filter = \_ -> True }++-- Extra types for the universe that come from in-scope instances.+instanceTypes :: Instances -> Config -> [Type]+instanceTypes insts Config{..}+  | not cfg_infer_instance_types = []+  | otherwise =+    [ tv+    | cls <- dicts,+      inst <- groundInstances,+      sub <- maybeToList (matchType cls inst),+      (_, tv) <- Twee.substToList sub ]+  where+    dicts =+      concatMap con_constraints (concat cfg_constants) >>=+      maybeToList . getDictionary++    groundInstances :: [Type]+    groundInstances =+      [ dict+      | -- () :- dict+        Twee.App tc (Twee.Cons (Twee.App unit Twee.Empty) (Twee.Cons dict Twee.Empty)) <-+        map (typeRes . typ) (is_instances insts),+        Twee.fun_value tc == tyCon (Proxy :: Proxy (:-)),+        Twee.fun_value unit == tyCon (Proxy :: Proxy (() :: Constraint)),+        Twee.isGround dict ]++data Warnings =+  Warnings {+    warn_no_generator :: [Type],+    warn_no_observer :: [Type] }++warnings :: Universe -> Instances -> Config -> Warnings+warnings univ insts Config{..} =+  Warnings {+    warn_no_generator =+      [ ty | ty <- types, isNothing (findGenerator cfg_default_to insts ty) ],+    warn_no_observer =+      [ ty | ty <- types, isNothing (findObserver insts ty) ] }+  where+    -- Check after defaulting types to Int (or whatever it is)+    types =+      [ ty+      | ty <- defaultTo cfg_default_to . Set.toList . univ_types $ univ,+        isNothing (findInstance insts ty :: Maybe (Value NoWarnings)) ]++instance Pretty Warnings where+  pPrint Warnings{..} =+    vcat $+      [section genDoc warn_no_generator] +++      [section obsDoc warn_no_observer] +++      [text "" | warnings ]+    where+      warnings = not (null warn_no_generator) || not (null warn_no_observer)+      section _ [] = pPrintEmpty+      section doc xs =+        doc $$+        nest 2 (vcat (map pPrintType xs)) $$+        text ""++      genDoc =+        text "WARNING: The following types have no 'Arbitrary' instance declared." $$+        text "You will not get any variables of the following types:"++      obsDoc =+        text "WARNING: The following types have no 'Ord' or 'Observe' instance declared." $$+        text "You will not get any equations about the following types:"++quickSpec :: Config -> IO [Prop (Term Constant)]+quickSpec cfg@Config{..} = do+  let+    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+    instances = cfg_instances `mappend` baseInstances++    eval = evalHaskell cfg_default_to instances++    present funs prop = do+      norm <- normaliser+      let prop' = makeDefinition funs (ac norm (conditionalise 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:+    --   * it is of the form f lhs = rhs (or vice versa).+    --   * f is not a background function.+    --   * lhs only contains background functions.+    --   * rhs does not contain f.+    --   * all vars in rhs appear in lhs+    makeDefinition cons (lhs :=>: t :=: u)+      | Just (f, ts) <- defines u,+        f `notElem` funs t,+        null (usort (vars t) \\ vars ts) =+        lhs :=>: u :=: t+        -- In the case where t defines f, the equation is already oriented correctly+      | otherwise = lhs :=>: t :=: u+      where+        defines (Fun f :@: ts)+          | f `elem` cons,+            all (`notElem` cons) (funs ts) = Just (f, ts)+        defines _ = Nothing++    -- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative+    ac norm (lhs :=>: Fun f :@: [Var x, Fun f1 :@: [Var y, Var z]] :=: Fun f2 :@: [Var y1, Fun f3 :@: [Var x1, Var z1]])+      | f == f1, f1 == f2, f2 == f3,+        x == x1, y == y1, z == z1,+        x /= y, y /= z, x /= z,+        norm (Fun f :@: [Var x, Var y]) == norm (Fun f :@: [Var y, Var x]) =+          lhs :=>: Fun f :@: [Fun f :@: [Var x, Var y], Var z] :=: Fun f :@: [Var x, Fun f :@: [Var y, Var z]]+    ac _ prop = prop++    -- Add a type signature when printing the equation x = y.+    maybeType (_ :=>: x@(Var _) :=: Var _) =+      text "::" <+> pPrintType (typ x)+    maybeType _ = pPrintEmpty++    -- XXX do this during testing+    constraintsOk = memo $ \con ->+      or [ and [ isJust (findValue instances (defaultTo cfg_default_to constraint)) | constraint <- con_constraints (typeSubst sub con) ]+         | ty <- Set.toList (univ_types univ),+           sub <- maybeToList (matchType (typeRes (typ con)) ty) ]++    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+          (map (Fun . unhideConstraint) (f cfg_constants))+        putLine ""+      when (n > 0) $ do+        putText (prettyShow (warnings univ instances cfg))+        putLine "== Laws =="+      let pres = if n == 0 then \_ -> return () else present (constantsOf f)+      QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size singleUse univ+        (enumerator (map Fun (constantsOf g)))+      when (n > 0) $ do+        putLine ""++    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++  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
+ src/QuickSpec/Internal/Haskell/Resolve.hs view
@@ -0,0 +1,117 @@+-- A data structure for resolving typeclass instances and similar at runtime.+--+-- Takes as input a set of functions ("instances"), and a type, and+-- tries to build a value of that type from the instances given.+--+-- For example, given the instances+--   ordList :: Dict (Arbitrary a) -> Dict (Arbitrary [a])+--   ordChar :: Dict (Arbitrary Char)+-- and the target type Dict (Arbitrary [Char]), it will produce the value+--   ordList ordChar :: Dict (Arbitrary [Char]).+--+-- The instances can in fact be arbitrary Haskell functions - though+-- their types must be such that the instance search will terminate.++{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}+module QuickSpec.Internal.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where++import Twee.Base+import QuickSpec.Internal.Type+import Data.MemoUgly+import Data.Functor.Identity+import Data.Maybe+import Data.Proxy+import Control.Monad+import Data.Semigroup(Semigroup(..))++-- A set of instances.+data Instances =+  Instances {+    -- The available instances.+    -- Each instance is a unary function; 'inst' sees to this.+    is_instances :: [Poly (Value Identity)],+    -- The resulting instance search function (memoised).+    is_find      :: Type -> [Value Identity] }++-- A smart constructor for Instances.+makeInstances :: [Poly (Value Identity)] -> Instances+makeInstances is = inst+  where+    inst = Instances is (memo (find_ inst . canonicaliseType))++instance Semigroup Instances where+  x <> y = makeInstances (is_instances x ++ is_instances y)+instance Monoid Instances where+  mempty = makeInstances []+  mappend = (<>)++-- Create a single instance.+inst :: Typeable a => a -> Instances+inst x = valueInst (toValue (Identity x))++valueInst :: Value Identity -> Instances+valueInst x = polyInst (poly x)+  where+    polyInst :: Poly (Value Identity) -> Instances+    polyInst x =+      -- Transform x into a single-argument function+      -- (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)) ->+          polyInst (apply uncur x)+        App (F Arrow) _ ->+          makeInstances [x]+        -- A plain old value x (not a function) turns into \() -> x.+        _ ->+          makeInstances [apply delay x]+      where+        uncur = toPolyValue (uncurry :: (A -> B -> C) -> (A, B) -> C)+        delay = toPolyValue ((\x () -> x) :: A -> () -> A)++-- Construct a value of a particular type.+-- If the type is polymorphic, may return an instance of it.+findValue :: Instances -> Type -> Maybe (Value Identity)+findValue insts = listToMaybe . is_find insts . skolemiseTypeVars++-- Given a type a, construct a value of type f a.+-- If the type is polymorphic, may return an instance of it.+findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f)+findInstance insts ty =+  unwrapFunctor runIdentity <$> findValue insts ty'+  where+    ty' = typeRep (Proxy :: Proxy f) `applyType` ty++-- The unmemoised version of the search algorithm.+-- Knows how to apply unary functions, and also knows how to generate:+--   * The unit type ()+--   * Pairs (a, b) - search for a and then for b+-- These two are important because instValue encodes other instances+-- using them.+--+-- Invariant: the type of the returned value is an instance of the argument type.+find_ :: Instances -> Type -> [Value Identity]+find_ _ (App (F unit) Empty)+  | unit == tyCon (Proxy :: Proxy ()) =+    return (toValue (Identity ()))+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))+    -- N.B.: subst sub ty2 because searching for x may have constrained y's type+    y <- is_find insts (subst sub ty2)+    sub <- maybeToList (match ty2 (typ y))+    return (pairValues (liftM2 (,)) (typeSubst sub x) y)+find_ insts ty = do+  -- 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)+  sub <- maybeToList (unify ty res)+  fun <- return (typeSubst sub fun)+  arg <- return (typeSubst sub arg)+  -- Find an argument for that function and apply the function.+  val <- is_find insts arg+  sub <- maybeToList (match arg (typ val))+  return (apply (typeSubst sub fun) val)
+ src/QuickSpec/Internal/Parse.hs view
@@ -0,0 +1,60 @@+-- | Parsing strings into properties.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs #-}+{-# LANGUAGE FlexibleContexts #-}+module QuickSpec.Internal.Parse where++import Control.Monad+import Data.Char+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Term hiding (char)+import QuickSpec.Internal.Type+import qualified Twee.Label as Label+import Text.ParserCombinators.ReadP++class Parse fun a where+  parse :: ReadP fun -> ReadP a++instance Parse fun Var where+  parse _ = do+    x <- satisfy isUpper+    xs <- munch isAlphaNum+    let name = x:xs+    -- Use Twee.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+  parse pfun =+    parseApp <++ parseVar+    where+      parseVar = Var <$> parse pfun+      parseApp = do+        f <- pfun+        args <- parseArgs <++ return []+        return (unPoly (foldl apply (poly (Fun f)) (map poly args)))+      parseArgs = between (char '(') (char ')') (sepBy (parse pfun) (char ','))++instance (Parse fun a, Typed a) => Parse fun (Equation a) where+  parse pfun = do+    t <- parse pfun+    string "="+    u <- parse pfun+    -- Compute type unifier of t and u+    -- "maybe mzero return" injects Maybe into MonadPlus+    pt <- maybe mzero return (polyMgu (poly (typ t)) (poly (typ u)))+    t <- maybe mzero return (cast (unPoly pt) t)+    u <- maybe mzero return (cast (unPoly pt) u)+    return (t :=: u)++instance (Parse fun a, Typed a) => Parse fun (Prop a) where+  parse pfun = do+    lhs <- sepBy (parse pfun) (string "&")+    unless (null lhs) (void (string "=>"))+    rhs <- parse pfun+    return (lhs :=>: rhs)++parseProp :: (Parse fun a, Pretty a) => ReadP fun -> String -> a+parseProp pfun xs =+  case readP_to_S (parse pfun <* eof) (filter (not . isSpace) xs) of+    [(x, [])] -> x+    ps -> error ("parse': got result " ++ prettyShow ps ++ " while parsing " ++ xs)
+ src/QuickSpec/Internal/Prop.hs view
@@ -0,0 +1,117 @@+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-}+module QuickSpec.Internal.Prop where++import Control.Monad+import qualified Data.DList as DList+import Data.Ord+import QuickSpec.Internal.Type+import QuickSpec.Internal.Utils+import QuickSpec.Internal.Term+import GHC.Generics(Generic)+import qualified Data.Map.Strict as Map+import qualified Data.Set as Set+import Control.Monad.Trans.State.Strict+import Data.List++data Prop a =+  (:=>:) {+    lhs :: [Equation a],+    rhs :: Equation a }+  deriving (Show, Generic, Functor)++instance Symbolic f a => Symbolic f (Prop a) where+  termsDL (lhs :=>: rhs) =+    termsDL rhs `mplus` termsDL lhs+  subst sub (lhs :=>: rhs) =+    subst sub lhs :=>: subst sub rhs++instance Ord a => Eq (Prop a) where+  x == y = x `compare` y == EQ+instance Ord a => Ord (Prop a) where+  compare = comparing (\p -> (usort (lhs p), rhs p))++infix 4 :=>:++literals :: Prop a -> [Equation a]+literals p = rhs p:lhs p++unitProp :: Equation a -> Prop a+unitProp p = [] :=>: p++mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)+mapFun f = fmap (fmap f)++instance Typed a => Typed (Prop a) where+  typ _ = typeOf True+  otherTypesDL p = DList.fromList (literals p) >>= typesDL+  typeSubst_ sub (lhs :=>: rhs) =+    map (typeSubst_ sub) lhs :=>: typeSubst_ sub rhs++instance Pretty a => Pretty (Prop a) where+  pPrint ([] :=>: rhs) = pPrint rhs+  pPrint p =+    hsep (punctuate (text " &") (map pPrint (lhs p))) <+> text "=>" <+> pPrint (rhs p)++data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor)++instance Symbolic f a => Symbolic f (Equation a) where+  termsDL (t :=: u) = termsDL t `mplus` termsDL u+  subst sub (t :=: u) = subst sub t :=: subst sub u++infix 5 :=:++instance Typed a => Typed (Equation a) where+  typ (t :=: _) = typ t+  otherTypesDL (t :=: u) = otherTypesDL t `mplus` typesDL u+  typeSubst_ sub (x :=: y) = typeSubst_ sub x :=: typeSubst_ sub y++instance Pretty a => Pretty (Equation a) where+  pPrintPrec _ _ (x :=: y)+    | isTrue x = pPrint y+    | isTrue y = pPrint x+    | otherwise = pPrint x <+> text "=" <+> pPrint y+    where+      -- XXX this is a hack+      isTrue x = show (pPrint x) == "True"++infix 4 ===+(===) :: a -> a -> Prop a+x === y = [] :=>: x :=: y++----------------------------------------------------------------------+-- Making properties look pretty (naming variables, etc.)+----------------------------------------------------------------------++class PrettyArity fun where+  prettyArity :: fun -> Int+  prettyArity _ = 0++instance (PrettyArity fun1, PrettyArity fun2) => PrettyArity (fun1 :+: fun2) where+  prettyArity (Inl x) = prettyArity x+  prettyArity (Inr x) = prettyArity x++prettyProp ::+  (Typed fun, Apply (Term fun), PrettyTerm fun, PrettyArity fun) =>+  (Type -> [String]) -> Prop (Term fun) -> Doc+prettyProp cands = pPrint . nameVars cands++data Named fun = Name String | Ordinary fun+instance Pretty fun => Pretty (Named fun) where+  pPrintPrec _ _ (Name name) = text name+  pPrintPrec l p (Ordinary fun) = pPrintPrec l p fun+instance PrettyTerm fun => PrettyTerm (Named fun) where+  termStyle Name{} = curried+  termStyle (Ordinary fun) = termStyle fun++nameVars :: (Type -> [String]) -> Prop (Term fun) -> Prop (Term (Named fun))+nameVars cands p =+  subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Ordinary) p)+  where+    sub = Map.fromList (evalState (mapM assign (nub (vars p))) Set.empty)+    assign x = do+      s <- get+      let names = supply (cands (typ x))+          name = head (filter (`Set.notMember` s) names)+      modify (Set.insert name)+      return (x, Fun (Name name))
+ src/QuickSpec/Internal/Pruning.hs view
@@ -0,0 +1,56 @@+-- A type of pruners.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs #-}+module QuickSpec.Internal.Pruning where++import QuickSpec.Internal.Prop+import QuickSpec.Internal.Testing+import Control.Monad+import Control.Monad.Trans.Class+import Control.Monad.IO.Class+import Control.Monad.Trans.State.Strict+import Control.Monad.Trans.Reader++class Monad m => MonadPruner term norm m | m -> term norm where+  normaliser :: m (term -> norm)+  add :: Prop term -> m Bool++  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 Bool+  add = lift . add++instance MonadPruner term norm m => MonadPruner term norm (StateT s m)+instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m)++normalise :: MonadPruner term norm m => term -> m norm+normalise t = do+  norm <- normaliser+  return (norm t)++newtype ReadOnlyPruner m a = ReadOnlyPruner { withReadOnlyPruner :: m a }+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term)++instance MonadTrans ReadOnlyPruner where+  lift = ReadOnlyPruner++instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where+  normaliser = ReadOnlyPruner normaliser+  add _ = return True++newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)+  deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)++instance MonadPruner term norm m => MonadPruner term norm (WatchPruner term m) where+  normaliser = lift normaliser+  add prop = do+    res <- lift (add prop)+    when res (WatchPruner (modify (prop:)))+    return res++watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term])+watchPruner (WatchPruner mx) = do+  (x, props) <- runStateT mx []+  return (x, reverse props)+
+ src/QuickSpec/Internal/Pruning/Background.hs view
@@ -0,0 +1,46 @@+-- A pruning layer which automatically adds axioms about functions as they appear.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, TypeOperators #-}+module QuickSpec.Internal.Pruning.Background where++import QuickSpec.Internal.Term+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Terminal+import qualified Data.Set as Set+import Data.Set(Set)+import Control.Monad+import Control.Monad.IO.Class+import Control.Monad.Trans.Class+import Control.Monad.Trans.State.Strict hiding (State)++newtype Pruner fun m a =+  Pruner (StateT (Set fun) m a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTrans, MonadTester testcase term, MonadTerminal)++class Background f where+  background :: f -> [Prop (Term f)]+  background _ = []++run :: Monad m => Pruner fun m a -> m a+run (Pruner x) =+  evalStateT x Set.empty++instance (Ord fun, Background fun, MonadPruner (Term fun) norm m) =>+  MonadPruner (Term fun) norm (Pruner fun m) where+  normaliser = lift normaliser+  add prop = do+    mapM_ addFunction (funs prop)+    lift (add prop)++addFunction :: (Ord fun, Background fun, MonadPruner (Term fun) norm m) => fun -> Pruner fun m ()+addFunction f = do+  funcs <- Pruner get+  unless (f `Set.member` funcs) $ do+    Pruner (put (Set.insert f funcs))+    mapM_ add (background f)++instance (Background fun1, Background fun2) => Background (fun1 :+: fun2) where+  background (Inl x) = map (fmap (fmap Inl)) (background x)+  background (Inr x) = map (fmap (fmap Inr)) (background x)
+ src/QuickSpec/Internal/Pruning/PartialApplication.hs view
@@ -0,0 +1,107 @@+-- Pruning support for partial application and the like.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}+module QuickSpec.Internal.Pruning.PartialApplication where++import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Pruning.Background hiding (Pruner)+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Terminal+import QuickSpec.Internal.Testing+import Control.Monad.IO.Class+import Control.Monad.Trans.Class++data PartiallyApplied f =+    -- A partially-applied function symbol.+    -- The Int describes how many arguments the function expects.+    Partial f Int+    -- The ($) operator, for oversaturated applications.+    -- The type argument is the type of the first argument to ($).+  | Apply Type+  deriving (Eq, Ord, Functor)++instance Sized f => Sized (PartiallyApplied f) where+  size (Partial f _) = size f+  size (Apply _) = 1++instance Arity (PartiallyApplied f) where+  arity (Partial _ n) = n+  arity (Apply _) = 2++instance Pretty f => Pretty (PartiallyApplied f) where+  pPrint (Partial f _) = pPrint f+  pPrint (Apply _) = text "$"++instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where+  termStyle (Partial f _) = termStyle f+  termStyle (Apply _) = invisible++instance PrettyArity f => PrettyArity (PartiallyApplied f) where+  prettyArity (Partial f _) = prettyArity f+  prettyArity (Apply _) = 1++instance Typed f => Typed (PartiallyApplied f) where+  typ (Apply ty) = arrowType [ty] ty+  typ (Partial f _) = typ f+  otherTypesDL (Apply _) = mempty+  otherTypesDL (Partial f _) = otherTypesDL f+  typeSubst_ sub (Apply ty) = Apply (typeSubst_ sub ty)+  typeSubst_ sub (Partial f n) = Partial (typeSubst_ sub f) n++getTotal :: Arity f => PartiallyApplied f -> Maybe f+getTotal (Partial f n) | arity f == n = Just f+getTotal _ = Nothing++partial :: f -> Term (PartiallyApplied f)+partial f = Fun (Partial f 0)++total :: Arity f => f -> PartiallyApplied f+total f = Partial f (arity f)++smartApply ::+  (Arity f, Typed f) => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)+smartApply (Fun (Partial f n) :@: ts) u | n < arity f =+  Fun (Partial f (n+1)) :@: (ts ++ [u])+smartApply t u = simpleApply t u++simpleApply ::+  Typed f =>+  Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)+simpleApply t u =+  Fun (Apply (typ t)) :@: [t, u]++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] ]+    where+      partial i =+        Fun (Partial f i) :@: take i vs+      vs = map Var (zipWith V (typeArgs (typ f)) [0..])+  background _ = []++newtype Pruner fun pruner a =+  Pruner { run :: pruner a }+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)++instance MonadTrans (Pruner fun) where+  lift = Pruner++instance (PrettyTerm fun, Typed fun, Arity fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where+  normaliser =+    Pruner $ do+      norm <- normaliser+      return $ \t ->+        norm . encode $ t++  add prop =+    Pruner $ do+      add (encode <$> canonicalise prop)++encode :: (Typed fun, Arity fun) => Term fun -> Term (PartiallyApplied fun)+encode (Var x) = Var x+encode (Fun f) = partial f+encode (t :$: u) = smartApply (encode t) (encode u)
+ src/QuickSpec/Internal/Pruning/Twee.hs view
@@ -0,0 +1,30 @@+-- A pruner that uses twee. Supports types and background axioms.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}+module QuickSpec.Internal.Pruning.Twee(Config(..), module QuickSpec.Internal.Pruning.Twee) where++import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Term+import QuickSpec.Internal.Terminal+import qualified QuickSpec.Internal.Pruning.Types as Types+import QuickSpec.Internal.Pruning.Types(Tagged)+import qualified QuickSpec.Internal.Pruning.PartialApplication as PartialApplication+import QuickSpec.Internal.Pruning.PartialApplication(PartiallyApplied)+import qualified QuickSpec.Internal.Pruning.Background as Background+import Control.Monad.Trans.Class+import Control.Monad.IO.Class+import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped+import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))++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)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term,+            MonadPruner (Term fun) (Untyped.Norm (Tagged (PartiallyApplied fun))), MonadTerminal)++instance MonadTrans (Pruner fun) where+  lift = Pruner . lift . lift . lift . lift++run :: (Sized 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
@@ -0,0 +1,111 @@+-- Encode monomorphic types during pruning.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}+module QuickSpec.Internal.Pruning.Types where++import QuickSpec.Internal.Pruning+import qualified QuickSpec.Internal.Pruning.Background as Background+import QuickSpec.Internal.Pruning.Background(Background)+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Terminal+import Control.Monad.IO.Class+import Control.Monad.Trans.Class+import qualified Twee.Base as Twee++data Tagged fun =+    Func fun+  | Tag Type+  deriving (Eq, Ord, Show, Typeable)++instance Arity fun => Arity (Tagged fun) where+  arity (Func f) = arity f+  arity (Tag _) = 1++instance Sized fun => Sized (Tagged fun) where+  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 "]"++instance PrettyTerm fun => PrettyTerm (Tagged fun) where+  termStyle (Func f) = termStyle f+  termStyle (Tag _) = uncurried++instance EqualsBonus (Tagged fun) where++type TypedTerm fun = Term fun+type UntypedTerm fun = Term (Tagged fun)++newtype Pruner fun pruner a =+  Pruner { run :: pruner a }+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)++instance MonadTrans (Pruner fun) where+  lift = Pruner++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 -> 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 ->+        norm . encode $ t++  add prop = lift (add (encode <$> canonicalise prop))++instance (Typed fun, Arity fun) => Background (Tagged fun) where+  background = typingAxioms++-- Compute the typing axioms for a function or type tag.+typingAxioms :: (Typed fun, Arity fun) =>+  Tagged fun -> [Prop (UntypedTerm fun)]+typingAxioms (Tag ty) =+  [tag ty (tag ty x) === tag ty x]+  where+    x = Var (V ty 0)+typingAxioms (Func func) =+  [tag res t === t] +++  [tagArg i ty === t | (i, ty) <- zip [0..] args]+  where+    f = Fun (Func func)+    xs = take n (map (Var . V typeVar) [0..])++    ty = typ func+    -- Use arity rather than typeArity, so that we can support+    -- partially-applied functions+    n = arity func+    args = take n (typeArgs ty)+    res = typeDrop n ty++    t = f :@: xs++    tagArg i ty =+      f :@:+        (take i xs +++         [tag ty (xs !! i)] +++         drop (i+1) xs)++tag :: Type -> UntypedTerm fun -> UntypedTerm fun+tag ty t = Fun (Tag ty) :$: t++encode :: Typed fun => TypedTerm fun -> UntypedTerm fun+-- We always add type tags; see comment in normaliseMono.+-- In the common case, twee will immediately remove these surplus type tags+-- by rewriting using the typing axioms.+encode (Var x) = tag (typ x) (Var x)+encode (Fun f :@: ts) =+  tag (typeDrop (length ts) (typ f)) (Fun (Func f) :@: map encode ts)+encode _ = error "partial application"
+ src/QuickSpec/Internal/Pruning/UntypedTwee.hs view
@@ -0,0 +1,128 @@+-- A pruner that uses twee. Does not respect types.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}+module QuickSpec.Internal.Pruning.UntypedTwee where++import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Prop+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import Data.Lens.Light+import qualified Twee+import qualified Twee.Equation as Twee+import qualified Twee.KBO as KBO+import qualified Twee.Base as Twee+import Twee hiding (Config(..))+import Twee.Rule hiding (normalForms)+import Twee.Proof hiding (Config, defaultConfig)+import Twee.Base(Ordered(..), Extended(..), EqualsBonus)+import Control.Monad.Trans.Reader+import Control.Monad.Trans.State.Strict hiding (State)+import Control.Monad.Trans.Class+import Control.Monad.IO.Class+import QuickSpec.Internal.Terminal+import qualified Data.Set as Set+import Data.Set(Set)++data Config =+  Config {+    cfg_max_term_size :: Int,+    cfg_max_cp_depth :: Int }++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+  lessIn = KBO.lessIn++newtype Pruner fun m a =+  Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)++instance MonadTrans (Pruner fun) where+  lift = Pruner . lift . lift++run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a+run Config{..} (Pruner x) =+  evalStateT (runReaderT x config) initialState+  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+  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++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) (Norm fun) (Pruner fun m) where+  normaliser = Pruner $ do+    state <- lift get+    return $ \t ->+      let u = normaliseTwee state t in+      u+      -- traceShow (text "normalise:" <+> pPrint t <+> text "->" <+> pPrint u) u++  add ([] :=>: t :=: u) = Pruner $ do+    state <- lift get+    config <- ask+    let+      t' = normalFormsTwee state t+      u' = normalFormsTwee state u+    -- Add the property anyway in case it could only be joined+    -- by considering all normal forms+    lift (put $! addTwee config t u state)+    return (Set.null (Set.intersection t' u'))++  add _ =+    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 -> Norm fun+normaliseTwee state 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 (Norm fun)+normalFormsTwee state 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)+addTwee config t u state =+  completePure config $+    addAxiom config state axiom+  where+    axiom = Axiom 0 (prettyShow (t :=: u)) (toTwee t Twee.:=: toTwee u)++toTwee :: (Ord f, Typeable f) =>+  Term f -> Twee.Term (Extended f)+toTwee = Twee.build . tt+  where+    tt (Var (V _ x)) =+      Twee.var (Twee.V x)+    tt (Fun f :@: ts) =+      Twee.app (Twee.fun (Function f)) (map tt ts)+    tt _ = error "partially applied term"++skolemise :: (Ord f, Typeable f) =>+  Term f -> Twee.Term (Extended f)+skolemise = Twee.build . sk+  where+    sk (Var (V _ x)) =+      Twee.con (Twee.fun (Skolem (Twee.V x)))+    sk (Fun f :@: ts) =+      Twee.app (Twee.fun (Function f)) (map sk ts)+    sk _ = error "partially applied term"
+ src/QuickSpec/Internal/Term.hs view
@@ -0,0 +1,241 @@+-- | 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 #-}+{-# OPTIONS_GHC -Wno-incomplete-patterns #-}+module QuickSpec.Internal.Term(module QuickSpec.Internal.Term, module Twee.Base, module Twee.Pretty) where++import QuickSpec.Internal.Type+import QuickSpec.Internal.Utils+import Control.Monad+import GHC.Generics(Generic)+import Test.QuickCheck(CoArbitrary)+import Data.DList(DList)+import qualified Data.DList as DList+import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)+import Twee.Pretty+import qualified Data.Map.Strict as Map+import Data.List+import Data.Ord++-- | A typed term.+data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)+  deriving (Eq, Ord, Show, Functor)++-- | A variable, which has a type and a number.+data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }+  deriving (Eq, Ord, Show, Generic, CoArbitrary)++instance Typed Var where+  typ x = var_ty x+  otherTypesDL _ = mzero+  typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x++-- | A class for things that contain terms.+class Symbolic f a | a -> f where+  -- | A different list of all terms contained in the thing.+  termsDL :: a -> DList (Term f)+  -- | Apply a substitution to all terms in the thing.+  subst :: (Var -> Term f) -> a -> a++instance Symbolic f (Term f) where+  termsDL = return+  subst sub (Var x) = sub x+  subst _ (Fun x) = Fun x+  subst sub (t :$: u) = subst sub t :$: subst sub u++instance Symbolic f a => Symbolic f [a] where+  termsDL = msum . map termsDL+  subst sub = map (subst sub)++class Sized a where+  size :: a -> Int++instance Sized f => Sized (Term f) where+  size (Var _) = 1+  size (Fun f) = size f+  size (t :$: u) =+    size t + size u ++    -- Penalise applied function variables, because they can be used+    -- to build many many terms without any constants at all+    case t of+      Var _ -> 1+      _ -> 0++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)++instance PrettyTerm f => Pretty (Term f) where+  pPrintPrec l p (Var x :@: ts) =+    pPrintTerm curried l p (pPrint x) ts+  pPrintPrec l p (Fun f :@: ts) =+    pPrintTerm (termStyle f) l p (pPrint f) ts++-- | All terms contained in a `Symbolic`.+terms :: Symbolic f a => a -> [Term f]+terms = DList.toList . termsDL++-- | All function symbols appearing in a `Symbolic`, in order of appearance,+-- with duplicates included.+funs :: Symbolic f a => a -> [f]+funs x = [ f | t <- terms x, Fun f <- subterms t ]++-- | All variables appearing in a `Symbolic`, in order of appearance,+-- with duplicates included.+vars :: Symbolic f a => a -> [Var]+vars x = [ v | t <- terms x, Var v <- subterms t ]++-- | Decompose a term into a head and a list of arguments.+pattern f :@: ts <- (getApp -> (f, ts)) where+  f :@: ts = foldl (:$:) f ts++getApp :: Term f -> (Term f, [Term f])+getApp (t :$: u) = (f, ts ++ [u])+  where+    (f, ts) = getApp t+getApp t = (t, [])++-- | Compute the number of a variable which does /not/ appear in the `Symbolic`.+freeVar :: Symbolic f a => a -> Int+freeVar x = maximum (0:map (succ . var_id) (vars x))++-- | Count how many times a given function symbol occurs.+occ :: (Eq f, Symbolic f a) => f -> a -> Int+occ x t = length (filter (== x) (funs t))++-- | Count how many times a given variable occurs.+occVar :: Symbolic f a => Var -> a -> Int+occVar x t = length (filter (== x) (vars t))++-- | Map a function over variables.+mapVar :: (Var -> Var) -> Term f -> Term f+mapVar f (Var x) = Var (f x)+mapVar _ (Fun x) = Fun x+mapVar f (t :$: u) = mapVar f t :$: mapVar f u++-- | Find all subterms of a term. Includes the term itself.+subterms :: Term f -> [Term f]+subterms t = t:properSubterms t++-- | Find all subterms of a term. Does not include the term itself.+properSubterms :: Term f -> [Term f]+properSubterms (t :$: u) = subterms t ++ subterms u+properSubterms _ = []++subtermsFO :: Term f -> [Term f]+subtermsFO t = t:properSubtermsFO t++properSubtermsFO :: Term f -> [Term f]+properSubtermsFO (_f :@: ts) = concatMap subtermsFO ts+properSubtermsFO _ = []++-- | Renames variables so that they appear in a canonical order.+-- Also makes sure that variables of different types have different numbers.+canonicalise :: Symbolic fun a => a -> a+canonicalise t = subst (\x -> Map.findWithDefault undefined x sub) t+  where+    sub =+      Map.fromList+        [(x, Var (V ty n))+        | (x@(V ty _), n) <- zip (nub (vars t)) [0..]]++-- | Evaluate a term, given a valuation for variables and function symbols.+evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a+evalTerm var fun = eval+  where+    eval (Var x) = var x+    eval (Fun f) = fun f+    eval (t :$: u) = liftM2 apply (eval t) (eval u)++instance Typed f => Typed (Term f) where+  typ (Var x) = typ x+  typ (Fun f) = typ f+  typ (t :$: _) = typeDrop 1 (typ t)++  otherTypesDL (Var _) = mempty+  otherTypesDL (Fun f) = typesDL f+  otherTypesDL (t :$: u) = typesDL t `mplus` typesDL u++  typeSubst_ sub = tsub+    where+      tsub (Var x) = Var (typeSubst_ sub x)+      tsub (Fun f) = Fun (typeSubst_ sub f)+      tsub (t :$: u) =+        typeSubst_ sub t :$: typeSubst_ sub u++instance (PrettyTerm f, Typed f) => Apply (Term f) where+  tryApply t u = do+    tryApply (typ t) (typ u)+    return (t :$: u)++-- | 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, Int, MeasureFuns f, Int, [Var])+-- | Compute the term ordering for a term.+measure :: (Sized f, Typed f) => Term f -> Measure f+measure t =+  (size t, missing t, -length (vars t), MeasureFuns (skel t),+   -length (usort (vars t)), vars t)+  where+    skel (Var (V ty _)) = Var (V ty 0)+    skel (Fun f) = Fun f+    skel (t :$: u) = skel t :$: skel u+    -- Prefer fully-applied terms to partially-applied ones.+    -- This function counts how many unsaturated function applications+    -- occur in a term.+    missing (Fun f :@: ts) =+      typeArity (typ f) - length ts + sum (map missing ts)+    missing (Var _ :@: ts) =+      sum (map missing ts)++-- | A helper for `Measure`.+newtype MeasureFuns f = MeasureFuns (Term f)+instance Ord f => Eq (MeasureFuns f) where+  t == u = compare t u == EQ+instance Ord f => Ord (MeasureFuns f) where+  compare (MeasureFuns t) (MeasureFuns u) = compareFuns t u++-- | A helper for `Measure`.+compareFuns :: Ord f => Term f -> Term f -> Ordering+compareFuns (f :@: ts) (g :@: us) =+  compareHead f g `mappend` comparing (map MeasureFuns) ts us+  where+    compareHead (Var x) (Var y) = compare x y+    compareHead (Var _) _ = LT+    compareHead _ (Var _) = GT+    compareHead (Fun f) (Fun g) = compare f g+    compareHead _ _ = error "viewApp"++----------------------------------------------------------------------+-- * Data types a la carte-ish.+----------------------------------------------------------------------++-- | A sum type. Intended to be used to build the type of function+-- symbols. Comes with instances that are useful for QuickSpec.+data a :+: b = Inl a | Inr b deriving (Eq, Ord)++instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where+  size (Inl x) = size x+  size (Inr x) = size x++instance (Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) where+  arity (Inl x) = arity x+  arity (Inr x) = arity x++instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where+  typ (Inl x) = typ x+  typ (Inr x) = typ x+  otherTypesDL (Inl x) = otherTypesDL x+  otherTypesDL (Inr x) = otherTypesDL x+  typeSubst_ sub (Inl x) = Inl (typeSubst_ sub x)+  typeSubst_ sub (Inr x) = Inr (typeSubst_ sub x)++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/Internal/Terminal.hs view
@@ -0,0 +1,59 @@+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs #-}+module QuickSpec.Internal.Terminal where++import Control.Monad.Trans.Class+import Control.Monad.IO.Class+import Control.Monad.Trans.State.Strict+import Control.Monad.Trans.Reader+import qualified Test.QuickCheck.Text as Text++class Monad m => MonadTerminal m where+  putText :: String -> m ()+  putLine :: String -> m ()+  putTemp :: String -> m ()++  default putText :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()+  putText = lift . putText++  default putLine :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()+  putLine = lift . putLine++  default putTemp :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()+  putTemp = lift . putTemp++instance MonadTerminal m => MonadTerminal (StateT s m)+instance MonadTerminal m => MonadTerminal (ReaderT r m)++putStatus :: MonadTerminal m => String -> m ()+putStatus str = putTemp ("[" ++ str ++ "...]")++clearStatus :: MonadTerminal m => m ()+clearStatus = putTemp ""++withStatus :: MonadTerminal m => String -> m a -> m a+withStatus str mx = putStatus str *> mx <* clearStatus++newtype Terminal a = Terminal (ReaderT Text.Terminal IO a)+  deriving (Functor, Applicative, Monad, MonadIO)++instance MonadTerminal Terminal where+  putText str = Terminal $ do+    term <- ask+    liftIO $ Text.putPart term str++  putLine str = Terminal $ do+    term <- ask+    liftIO $ Text.putLine term str++  putTemp str = Terminal $ do+    term <- ask+    liftIO $ Text.putTemp term str++withNullTerminal :: Terminal a -> IO a+withNullTerminal (Terminal mx) =+  Text.withNullTerminal (runReaderT mx)++withStdioTerminal :: Terminal a -> IO a+withStdioTerminal (Terminal mx) =+  Text.withStdioTerminal (runReaderT mx)
+ src/QuickSpec/Internal/Testing.hs view
@@ -0,0 +1,18 @@+-- A type of test case generators.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances #-}+module QuickSpec.Internal.Testing where++import QuickSpec.Internal.Prop+import Control.Monad.Trans.Class+import Control.Monad.Trans.State.Strict+import Control.Monad.Trans.Reader++class Monad m => MonadTester testcase term m | m -> testcase term where+  test :: Prop term -> m (Maybe testcase)++  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (Maybe testcase)+  test = lift . test++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
@@ -0,0 +1,95 @@+-- Decision trees for testing terms for equality.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE RecordWildCards #-}+module QuickSpec.Internal.Testing.DecisionTree where++import qualified Data.Map as Map+import Data.Map(Map)++data DecisionTree testcase result term =+  DecisionTree {+    -- A function for evaluating terms on test cases.+    dt_evaluate :: term -> testcase -> result,+    -- The set of test cases gathered so far.+    dt_test_cases :: [testcase],+    -- The tree itself.+    dt_tree :: !(Maybe (InnerTree result term)) }++data InnerTree result term =+    TestCase !(Map result (InnerTree result term))+  | Singleton !term++data Result testcase result term =+    Distinct (DecisionTree testcase result term)+  | EqualTo term++-- Make a new decision tree.+empty :: (term -> testcase -> result) -> DecisionTree testcase result term+empty eval =+  DecisionTree {+    dt_evaluate = eval,+    dt_test_cases = [],+    dt_tree = Nothing }++-- Add a new test case to a decision tree.+addTestCase ::+  testcase -> DecisionTree testcase result term ->+  DecisionTree testcase result term+addTestCase tc dt@DecisionTree{..} =+  dt{dt_test_cases = dt_test_cases ++ [tc]}++-- Insert a value into a decision tree.+insert :: Ord result =>+  term -> DecisionTree testcase result term ->+  Result testcase result term+insert x dt@DecisionTree{dt_tree = Nothing, ..} =+  Distinct dt{dt_tree = Just (Singleton x)}+insert x dt@DecisionTree{dt_tree = Just dt_tree, ..} =+  aux k dt_test_cases dt_tree+  where+    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)) +    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+        Nothing ->+          Distinct (k' (Singleton x))+        Just tree ->+          aux k' ts tree+    aux _ [] (TestCase _) =+      error "unexpected node in decision tree"++data Statistics =+  Statistics {+    -- Total number of terms in the decision tree+    stat_num_terms :: !Int,+    -- Total number of tests executed+    stat_num_tests :: !Int,+    -- Number of distinct test cases used+    stat_num_test_cases :: !Int }+  deriving (Eq, Show)++statistics :: DecisionTree testcase result term -> Statistics+statistics DecisionTree{dt_tree = Nothing} =+  Statistics 0 0 0+statistics DecisionTree{dt_tree = Just dt_tree, ..} =+  Statistics {+    stat_num_terms = x,+    stat_num_tests = y,+    stat_num_test_cases = length dt_test_cases }+  where+    (x, y) = stat dt_tree++    -- Returns (number of terms, number of tests)+    stat Singleton{} = (1, 0)+    -- To calculate the number of test cases, note that each term+    -- under res executed one test case on the way through this node.+    stat (TestCase res) =+      (sum (map fst ss), sum [ x + y | (x, y) <- ss ])+      where+        ss = map stat (Map.elems res)
+ src/QuickSpec/Internal/Testing/QuickCheck.hs view
@@ -0,0 +1,97 @@+-- Testing conjectures using QuickCheck.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-}+module QuickSpec.Internal.Testing.QuickCheck where++import QuickSpec.Internal.Testing+import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Prop+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+import Data.List+import System.Random+import QuickSpec.Internal.Terminal+import Data.Lens.Light++data Config =+  Config {+    cfg_num_tests :: Int,+    cfg_max_test_size :: Int,+    cfg_fixed_seed :: Maybe QCGen}+  deriving Show++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 {+    env_config :: Config,+    env_tests :: [testcase],+    env_eval :: testcase -> term -> result }++newtype Tester testcase term result m a =+  Tester (ReaderT (Environment testcase term result) m a)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal, MonadPruner term' res')++instance MonadTrans (Tester testcase term result) where+  lift = Tester . lift++run ::+  Config -> Gen testcase -> (testcase -> term -> 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+    k = max 1 cfg_max_test_size+    bias = 3+    -- 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)+    tests = zipWith (unGen gen) seeds sizes+  return $ runReaderT x+    Environment {+      env_config = config,+      env_tests = tests,+      env_eval = eval }++-- uniform n k: generate a list of n integers which are distributed evenly between 0 and k-1.+uniform :: Integer -> Integer -> [Integer]+uniform n k =+  -- n `div` k: divide evenly as far as possible.+  concat [replicate (fromIntegral (n `div` k)) i | i <- [0..k-1]] +++  -- The leftovers get distributed at equal intervals.+  [i * k `div` leftovers | i <- [0..leftovers-1]]+  where+    leftovers = n `mod` k++instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where+  test prop =+    Tester $ do+      env <- ask+      return $! quickCheckTest env prop++quickCheckTest :: Eq result =>+  Environment testcase term result ->+  Prop term -> Maybe testcase+quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) =+  msum (map test env_tests)+  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
+ src/QuickSpec/Internal/Type.hs view
@@ -0,0 +1,562 @@+-- | 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 #-}+-- To avoid a warning about TyVarNumber's constructor being unused:+{-# OPTIONS_GHC -fno-warn-unused-binds #-}+module QuickSpec.Internal.Type(+  -- * Types+  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, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,+  isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,+  -- * Things that have types+  Typed(..), typeSubst, typesDL, tyVars, cast, matchType,+  TypeView(..),+  Apply(..), apply, canApply,+  oneTypeVar, defaultTo, skolemiseTypeVars,+  -- * Polymorphic types+  canonicaliseType,+  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu,+  -- * Dynamic values+  Value, toValue, fromValue, valueType,+  unwrap, Unwrapped(..), Wrapper(..),+  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor, bringFunctor) where++import Control.Monad+import Data.DList(DList)+import Data.Maybe+import qualified Data.Typeable as Ty+import Data.Typeable(Typeable)+import GHC.Exts(Any)+import Test.QuickCheck+import Unsafe.Coerce+import Data.Constraint+import Twee.Base+import Data.Proxy+import Data.List+import Data.Char+import Data.Functor.Identity++-- | A (possibly polymorphic) type.+type Type = Term TyCon++-- | A type constructor.+data TyCon =+    -- | The function type constructor @(->)@.+    Arrow+    -- | An ordinary Haskell type constructor.+  | TyCon Ty.TyCon+    -- | A string. Can be used to represent miscellaneous types that do not+    -- really exist in Haskell.+  | String String+  deriving (Eq, Ord, Show)++instance Pretty TyCon where+  pPrint Arrow = text "->"+  pPrint (String x) = text x+  pPrint (TyCon x) = text (show x)+instance PrettyTerm TyCon where+  termStyle Arrow =+    fixedArity 2 $+    TermStyle $ \l p d [x, y] ->+      maybeParens (p > 8) $+        pPrintPrec l 9 x <+> d <+>+        pPrintPrec l 0 y++  termStyle (String _) = curried++  termStyle (TyCon con)+    | con == listTyCon =+      fixedArity 1 $+      TermStyle $ \l _ _ [x] -> brackets (pPrintPrec l 0 x)+    | show con == "()" || show con == "(%%)" =+      fixedArity 0 tupleStyle -- by analogy with case below+    | take 2 (show con) == "(," ||+      take 3 (show con) == "(%," =+      fixedArity (1+length (filter (== ',') (show con))) tupleStyle+    | isAlphaNum (head (show con)) = curried+    | otherwise = infixStyle 5++-- Type and class variables.+newtype A = A Any deriving Typeable+newtype B = B Any deriving Typeable+newtype C = C Any deriving Typeable+newtype D = D Any deriving Typeable+newtype E = E Any deriving Typeable++class ClassA+deriving instance Typeable ClassA+class ClassB+deriving instance Typeable ClassB+class ClassC+deriving instance Typeable ClassC+class ClassD+deriving instance Typeable ClassD+class ClassE+deriving instance Typeable ClassE+class ClassF+deriving instance Typeable ClassF++-- | A polymorphic type of kind Symbol.+type SymA = "__polymorphic_symbol__"++-- | All type variables that are defined in this module.+typeVars :: [Ty.TypeRep]+typeVars =+  [Ty.typeRep (Proxy :: Proxy A),+   Ty.typeRep (Proxy :: Proxy B),+   Ty.typeRep (Proxy :: Proxy C),+   Ty.typeRep (Proxy :: Proxy D),+   Ty.typeRep (Proxy :: Proxy E),+   Ty.typeRep (Proxy :: Proxy ClassA),+   Ty.typeRep (Proxy :: Proxy ClassB),+   Ty.typeRep (Proxy :: Proxy ClassC),+   Ty.typeRep (Proxy :: Proxy ClassD),+   Ty.typeRep (Proxy :: Proxy ClassE),+   Ty.typeRep (Proxy :: Proxy ClassF),+   Ty.typeRep (Proxy :: Proxy SymA)]++-- | A type variable.+typeVar :: Type+typeVar = typeRep (Proxy :: Proxy A)++-- | Check if a type is a type variable.+isTypeVar :: Type -> Bool+isTypeVar = isVar++-- | Construct a type from a `Typeable`.+typeOf :: Typeable a => a -> Type+typeOf x = fromTypeRep (Ty.typeOf x)++-- | Construct a type from a `Typeable`.+typeRep :: Typeable (a :: k) => proxy a -> Type+typeRep x = fromTypeRep (Ty.typeRep x)++-- | Turn a `TyCon` into a type.+typeFromTyCon :: TyCon -> Type+typeFromTyCon tc = build (con (fun tc))++-- | Function application for type constructors.+--+-- For example, @applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])@.+applyType :: Type -> Type -> Type+applyType (App f tys) ty = build (app f (unpack tys ++ [ty]))+applyType _ _ = error "tried to apply type variable"++-- | Construct a function type.+arrowType :: [Type] -> Type -> Type+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).+--+-- For multiple-argument functions, unpacks one argument.+unpackArrow :: Type -> Maybe (Type, Type)+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))) =+  arg:typeArgs res+typeArgs _ = []++-- | The result of a function type.+typeRes :: Type -> Type+typeRes (App (F Arrow) (Cons _ (Cons res Empty))) =+  typeRes res+typeRes ty = ty++-- | Given the type of a function, returns the type of applying that function to+-- @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-1) ty+typeDrop _ _ =+  error "typeDrop on non-function type"++-- | How many arguments does a function take?+typeArity :: Type -> Int+typeArity = length . typeArgs++-- | Unify all type variables in a type.+oneTypeVar :: Typed a => a -> a+oneTypeVar = typeSubst (const (var (V 0)))++-- | Replace all type variables with a particular type.+defaultTo :: Typed a => Type -> a -> a+defaultTo def = typeSubst (const def)++-- | Make a type ground by replacing all type variables+-- with Skolem constants.+skolemiseTypeVars :: Typed a => a -> a+skolemiseTypeVars = typeSubst (const aTy)+  where+    aTy = build (con (fun (tyCon (Proxy :: Proxy A))))++-- | Construct a type from a `Ty.TypeRep`.+fromTypeRep :: Ty.TypeRep -> Type+fromTypeRep ty+  | Just n <- elemIndex ty typeVars =+      build (var (V n))+  | otherwise =+    let (tyCon, tys) = Ty.splitTyConApp ty in+    build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys))++-- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`.+fromTyCon :: Ty.TyCon -> TyCon+fromTyCon ty+  | ty == arrowTyCon = Arrow+  | otherwise = TyCon ty++-- | Some built-in type consructors.+arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon+arrowTyCon = mkCon (Proxy :: Proxy (->))+commaTyCon = mkCon (Proxy :: Proxy (,))+listTyCon  = mkCon (Proxy :: Proxy [])+dictTyCon  = mkCon (Proxy :: Proxy Dict)++mkCon :: Typeable a => proxy a -> Ty.TyCon+mkCon = fst . Ty.splitTyConApp . Ty.typeRep++-- | Get the outermost `TyCon` of a `Typeable`.+tyCon :: Typeable a => proxy a -> TyCon+tyCon = fromTyCon . mkCon++-- | 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))+  | dict == dictTyCon = Just ty+getDictionary _ = Nothing++-- | Check if a type is of the form @`Dict` c@.+isDictionary :: Type -> Bool+isDictionary = isJust . getDictionary++-- | Count how many dictionary arguments a type has.+dictArity :: Type -> Int+dictArity = length . takeWhile isDictionary . typeArgs++-- | Split a type into constraints and normal type.+splitConstrainedType :: Type -> ([Type], Type)+splitConstrainedType ty =+  (dicts, arrowType rest (typeRes ty))+  where+    (dicts, rest) = splitAt (dictArity ty) (typeArgs ty)++-- CoArbitrary instances.+instance CoArbitrary Type where+  coarbitrary = coarbitrary . singleton+instance CoArbitrary (TermList TyCon) where+  coarbitrary Empty = variant 0+  coarbitrary (ConsSym (Var (V x)) ts) =+    variant 1 . coarbitrary x . coarbitrary ts+  coarbitrary (ConsSym (App f _) ts) =+    variant 2 . coarbitrary (fun_id f) . coarbitrary ts++-- | Pretty-print a type. Differs from the `Pretty` instance by printing type+-- variables in lowercase.+pPrintType :: Type -> Doc+pPrintType = ppr . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise+  where+    as = supply [[x] | x <- ['a'..'z']]+    -- Print dictionary arguments specially+    ppr ty+      | Just (dict, res) <- unpackArrow ty,+        Just constraint <- getDictionary dict =+      pPrint constraint <+> text "=>" <+> ppr res+    ppr ty = pPrint ty++-- | A class for things that have a type.+class Typed a where+  -- | The type.+  typ :: a -> Type+  -- | Types that appear elsewhere in the `Typed`, for example, types of subterms.+  -- Should return everything which is affected by `typeSubst`.+  otherTypesDL :: a -> DList Type+  otherTypesDL _ = mzero+  -- | Substitute for all type variables.+  typeSubst_ :: (Var -> Builder TyCon) -> a -> a++-- | Substitute for all type variables in a `Typed`.+{-# INLINE typeSubst #-}+typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a+typeSubst s x = typeSubst_ (evalSubst s) x++-- | A wrapper for using the `Twee.Base.Symbolic` machinery on types.+newtype TypeView a = TypeView { unTypeView :: a }+instance Typed a => Symbolic (TypeView a) where+  type ConstantOf (TypeView a) = TyCon+  termsDL = fmap singleton . typesDL . unTypeView+  subst_ sub = TypeView . typeSubst_ sub . unTypeView+instance Typed a => Has (TypeView a) Type where+  the = typ . unTypeView++-- | All types that occur in a `Typed`.+typesDL :: Typed a => a -> DList Type+typesDL ty = return (typ ty) `mplus` otherTypesDL ty++-- | All type variables that occur in a `Typed`.+tyVars :: Typed a => a -> [Var]+tyVars = vars . TypeView++-- | Cast a `Typed` to a target type.+-- Succeeds if the target type is an instance of the current type.+cast :: Typed a => Type -> a -> Maybe a+cast ty x = do+  s <- match (typ x) ty+  return (typeSubst s x)++-- | Check if the second argument is an instance of the first argument.+matchType :: Type -> Type -> Maybe (Subst TyCon)+matchType = match++-- | Typed things that support function application.+class Typed a => Apply a where+  -- | Apply a function to its argument.+  --+  -- For most instances of `Typed`, the type of the argument must be exactly+  -- equal to the function's argument type. If you want unification to happen,+  -- use the `Typed` instance of `Poly`.+  tryApply :: a -> a -> Maybe a++-- | Apply a function to its argument, crashing on failure.+--+-- For most instances of `Typed`, the type of the argument must be exactly+-- equal to the function's argument type. If you want unification to happen,+-- use the `Typed` instance of `Poly`.+infixl `apply`+apply :: Apply a => a -> a -> a+apply f x =+  case tryApply f x of+    Nothing ->+      error $+        "apply: ill-typed term: can't apply " +++        prettyShow (typ f) ++ " to " ++ prettyShow (typ x)+    Just y -> y++-- | Check if a function can be applied to its argument.+canApply :: Apply a => a -> a -> Bool+canApply f x = isJust (tryApply f x)++-- Instances.+instance Typed Type where+  typ = id+  typeSubst_ = subst++instance Apply Type where+  tryApply (App (F Arrow) (Cons arg (Cons res Empty))) t+    | t == arg = Just res+  tryApply _ _ = Nothing++instance (Typed a, Typed b) => Typed (a, b) where+  typ (x, y) = build (app (fun (TyCon commaTyCon)) [typ x, typ y])+  otherTypesDL (x, y) = otherTypesDL x `mplus` otherTypesDL y+  typeSubst_ f (x, y) = (typeSubst_ f x, typeSubst_ f y)++instance (Typed a, Typed b) => Typed (Either a b) where+  typ (Left x)  = typ x+  typ (Right x) = typ x+  otherTypesDL (Left x)  = otherTypesDL x+  otherTypesDL (Right x) = otherTypesDL x+  typeSubst_ sub (Left x)  = Left  (typeSubst_ sub x)+  typeSubst_ sub (Right x) = Right (typeSubst_ sub x)++instance Typed a => Typed [a] where+  typ [] = typeOf ()+  typ (x:_) = typ x+  otherTypesDL [] = mzero+  otherTypesDL (x:xs) = otherTypesDL x `mplus` msum (map typesDL xs)+  typeSubst_ f xs = map (typeSubst_ f) xs++-- | Represents a forall-quantifier over all the type variables in a type.+-- Wrapping a term in @Poly@ normalises the type by alpha-renaming+-- type variables canonically.+--+-- The `Apply` instance for `Poly` does unification to handle applying a+-- polymorphic function.+newtype Poly a = Poly { unPoly :: a }+  deriving (Eq, Ord, Show, Pretty, Typeable)++-- | Build a `Poly`.+poly :: Typed a => a -> Poly a+poly x = Poly (canonicaliseType x)++-- | Alpha-rename type variables in a canonical way.+canonicaliseType :: Typed a => a -> a+canonicaliseType = unTypeView . canonicalise . TypeView++-- | Get the polymorphic type of a polymorphic value.+polyTyp :: Typed a => Poly a -> Poly Type+polyTyp (Poly x) = Poly (typ x)++-- | Rename the type variables of the second argument so that they don't overlap+-- with those of the first argument.+polyRename :: (Typed a, Typed b) => a -> Poly b -> b+polyRename x (Poly y) =+  unTypeView (renameAvoiding (TypeView x) (TypeView y))++-- | Rename the type variables of both arguments so that they don't overlap.+polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c+polyApply f (Poly x) y = poly (f x (polyRename x y))++-- | Rename the type variables of both arguments so that they don't overlap.+polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)+polyPair = polyApply (,)++-- | Rename the type variables of all arguments so that they don't overlap.+polyList :: Typed a => [Poly a] -> Poly [a]+polyList [] = poly []+polyList (x:xs) = polyApply (:) x (polyList xs)++-- | Find the most general unifier of two types.+polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)+polyMgu ty1 ty2 = do+  let (ty1', ty2') = unPoly (polyPair ty1 ty2)+  sub <- unify ty1' ty2'+  return (poly (typeSubst sub ty1'))++instance Typed a => Typed (Poly a) where+  typ = typ . unPoly+  otherTypesDL = otherTypesDL . unPoly+  typeSubst_ f (Poly x) = poly (typeSubst_ f x)++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'')++-- | Convert an ordinary value to a dynamic value.+toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)+toPolyValue = poly . toValue . pure++-- | Dynamic values inside an applicative functor.+--+-- For example, a value of type @Value Maybe@ represents a @Maybe something@.+data Value f =+  Value {+    valueType :: Type,+    value :: f Any }++instance Show (Value f) where+  show x = "<<" ++ prettyShow (typ x) ++ ">>"++fromAny :: f Any -> f a+fromAny = unsafeCoerce++toAny :: f a -> f Any+toAny = unsafeCoerce++-- | Construct a `Value`.+toValue :: forall f (a :: *). Typeable a => f a -> Value f+toValue x = Value (typeRep (Proxy :: Proxy a)) (toAny x)++-- | Deconstruct a `Value`.+fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)+fromValue x = do+  guard (typ x == typeRep (Proxy :: Proxy a))+  return (fromAny (value x))++instance Typed (Value f) where+  typ = valueType+  typeSubst_ f (Value ty x) = Value (typeSubst_ f ty) x+instance Applicative f => Apply (Value f) where+  tryApply f x = do+    ty <- tryApply (typ f) (typ x)+    return (Value ty (fromAny (value f) <*> value x))++-- | Unwrap a value to get at the thing inside, with an existential type.+unwrap :: Value f -> Unwrapped f+unwrap x =+  value x `In`+    Wrapper+      (\y -> Value (typ x) y)+      (\y ->+        if typ x == typ y+        then fromAny (value y)+        else error "non-matching types")++-- | The unwrapped value. Consists of the value itself (with an existential+-- type) and functions to wrap it up again.+data Unwrapped f where+  In :: f a -> Wrapper a -> Unwrapped f++-- | Functions for re-wrapping an `Unwrapped` value.+data Wrapper a =+  Wrapper {+    -- | Wrap up a value which has the same existential type as this one.+    wrap :: forall g. g a -> Value g,+    -- | Unwrap a value which has the same existential type as this one.+    reunwrap :: forall g. Value g -> g a }++-- | Apply a polymorphic function to a `Value`.+mapValue :: (forall a. f a -> g a) -> Value f -> Value g+mapValue f v =+  case unwrap v of+    x `In` w -> wrap w (f x)++-- | Apply a polymorphic function to a `Value`.+forValue :: Value f -> (forall a. f a -> g a) -> Value g+forValue x f = mapValue f x++-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.+ofValue :: (forall a. f a -> b) -> Value f -> b+ofValue f v =+  case unwrap v of+    x `In` _ -> f x++-- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.+withValue :: Value f -> (forall a. f a -> b) -> b+withValue x f = ofValue f x++-- | Apply a polymorphic function to a pair of `Value`s.+pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f+pairValues f x y =+  ty `seq`+  Value {+    valueType = ty,+    value = toAny (f (value x) (value y)) }+  where+    ty = typeRep (Proxy :: Proxy g) `applyType` typ x `applyType` typ y++wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g+wrapFunctor f x =+  ty `seq`+  Value {+    valueType = ty,+    value = toAny (f (value x)) }+  where+    ty = typeRep (Proxy :: Proxy h) `applyType` valueType x++unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h+unwrapFunctor f x =+  case typ x of+    App _ tys | tys@(_:_) <- unpack tys ->+      case ty `applyType` last tys == typ x of+        True ->+          Value {+            valueType = last tys,+            value = f (fromAny (value x)) }+        False ->+          error "non-matching types"+    _ -> error "value of type f a had wrong type"+  where+    ty = typeRep (Proxy :: Proxy g)++bringFunctor :: Functor f => Value f -> f (Value Identity)+bringFunctor val =+  case unwrap val of+    x `In` w ->+      fmap (wrap w . Identity) x
+ src/QuickSpec/Internal/Utils.hs view
@@ -0,0 +1,138 @@+-- | Miscellaneous utility functions.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE CPP #-}+module QuickSpec.Internal.Utils where++import Control.Arrow((&&&))+import Control.Exception+import Control.Spoon+import Data.List(groupBy, sortBy)+#if !MIN_VERSION_base(4,8,0)+import Data.Monoid+#endif+import Data.Ord(comparing)+import System.IO+import qualified Control.Category as Category+import qualified Data.Map.Strict as Map+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..)++key :: Ord a => a -> Lens (Map a b) (Maybe b)+key x = lens (Map.lookup x) (\my m -> Map.alter (const my) x m)++keyDefault :: Ord a => a -> b -> Lens (Map a b) b+keyDefault x y = lens (Map.findWithDefault y x) (\y m -> Map.insert x y m)++reading :: (a -> Lens a b) -> Lens a b+reading f = lens (\x -> getL (f x) x) (\y x -> setL (f x) y x)++fstLens :: Lens (a, b) a+fstLens = lens fst (\x (_, y) -> (x, y))++sndLens :: Lens (a, b) b+sndLens = lens snd (\y (x, _) -> (x, y))++makeLensAs :: Name -> [(String, String)] -> Q [Dec]+makeLensAs ty names =+  nameMakeLens ty (\x -> lookup x names)++repeatM :: Monad m => m a -> m [a]+repeatM = sequence . repeat++partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]+partitionBy value =+  map (map fst) .+  groupBy (\x y -> snd x == snd y) .+  sortBy (comparing snd) .+  map (id &&& value)++collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)]+collate f = map g . partitionBy fst+  where+    g xs = (fst (head xs), f (map snd xs))++isSorted :: Ord a => [a] -> Bool+isSorted xs = and (zipWith (<=) xs (tail xs))++isSortedBy :: Ord b => (a -> b) -> [a] -> Bool+isSortedBy f xs = isSorted (map f xs)++usort :: Ord a => [a] -> [a]+usort = usortBy compare++usortBy :: (a -> a -> Ordering) -> [a] -> [a]+usortBy f = map head . groupBy (\x y -> f x y == EQ) . sortBy f++sortBy' :: Ord b => (a -> b) -> [a] -> [a]+sortBy' f = map snd . sortBy (comparing fst) . map (\x -> (f x, x))++usortBy' :: Ord b => (a -> b) -> [a] -> [a]+usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x))++orElse :: Ordering -> Ordering -> Ordering+EQ `orElse` x = x+x  `orElse` _ = x++unbuffered :: IO a -> IO a+unbuffered x = do+  buf <- hGetBuffering stdout+  bracket_+    (hSetBuffering stdout NoBuffering)+    (hSetBuffering stdout buf)+    x++spoony :: Eq a => a -> Maybe a+spoony x = teaspoon ((x == x) `seq` x)++labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]+labelM f = mapM (\x -> do { y <- f x; return (x, y) })++#if __GLASGOW_HASKELL__ < 710+isSubsequenceOf :: Ord a => [a] -> [a] -> Bool+[] `isSubsequenceOf` ys = True+(x:xs) `isSubsequenceOf` [] = False+(x:xs) `isSubsequenceOf` (y:ys)+  | x == y = xs `isSubsequenceOf` ys+  | otherwise = (x:xs) `isSubsequenceOf` ys+#endif++appendAt :: Int -> [a] -> [[a]] -> [[a]]+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
− src/QuickSpec/Parse.hs 
@@ -1,60 +0,0 @@--- | Parsing strings into properties.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses, GADTs #-}-{-# LANGUAGE FlexibleContexts #-}-module QuickSpec.Parse where--import Control.Monad-import Data.Char-import QuickSpec.Prop-import QuickSpec.Term hiding (char)-import QuickSpec.Type-import qualified Twee.Label as Label-import Text.ParserCombinators.ReadP--class Parse fun a where-  parse :: ReadP fun -> ReadP a--instance Parse fun Var where-  parse _ = do-    x <- satisfy isUpper-    xs <- munch isAlphaNum-    let name = x:xs-    -- Use Twee.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-  parse pfun =-    parseApp <++ parseVar-    where-      parseVar = Var <$> parse pfun-      parseApp = do-        f <- pfun-        args <- parseArgs <++ return []-        return (unPoly (foldl apply (poly (App f [])) (map poly args)))-      parseArgs = between (char '(') (char ')') (sepBy (parse pfun) (char ','))--instance (Parse fun a, Typed a) => Parse fun (Equation a) where-  parse pfun = do-    t <- parse pfun-    string "="-    u <- parse pfun-    -- Compute type unifier of t and u-    -- "maybe mzero return" injects Maybe into MonadPlus-    pt <- maybe mzero return (polyMgu (poly (typ t)) (poly (typ u)))-    t <- maybe mzero return (cast (unPoly pt) t)-    u <- maybe mzero return (cast (unPoly pt) u)-    return (t :=: u)--instance (Parse fun a, Typed a) => Parse fun (Prop a) where-  parse pfun = do-    lhs <- sepBy (parse pfun) (string "&")-    unless (null lhs) (void (string "=>"))-    rhs <- parse pfun-    return (lhs :=>: rhs)--parseProp :: (Parse fun a, Pretty a) => ReadP fun -> String -> a-parseProp pfun xs =-  case readP_to_S (parse pfun <* eof) (filter (not . isSpace) xs) of-    [(x, [])] -> x-    ps -> error ("parse': got result " ++ prettyShow ps ++ " while parsing " ++ xs)
− src/QuickSpec/Prop.hs 
@@ -1,136 +0,0 @@-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-}-module QuickSpec.Prop where--import Control.Monad-import qualified Data.DList as DList-import Data.Ord-import QuickSpec.Type-import QuickSpec.Utils-import QuickSpec.Term-import GHC.Generics(Generic)-import qualified Data.Map.Strict as Map-import qualified Data.Set as Set-import Control.Monad.Trans.State.Strict-import Data.List--data Prop a =-  (:=>:) {-    lhs :: [Equation a],-    rhs :: Equation a }-  deriving (Show, Generic, Functor)--instance Symbolic f a => Symbolic f (Prop a) where-  termsDL (lhs :=>: rhs) =-    termsDL rhs `mplus` termsDL lhs-  subst sub (lhs :=>: rhs) =-    subst sub lhs :=>: subst sub rhs--instance Ord a => Eq (Prop a) where-  x == y = x `compare` y == EQ-instance Ord a => Ord (Prop a) where-  compare = comparing (\p -> (usort (lhs p), rhs p))--infix 4 :=>:--literals :: Prop a -> [Equation a]-literals p = rhs p:lhs p--unitProp :: Equation a -> Prop a-unitProp p = [] :=>: p--mapFun :: (fun1 -> fun2) -> Prop (Term fun1) -> Prop (Term fun2)-mapFun f = fmap (fmap f)--instance Typed a => Typed (Prop a) where-  typ _ = typeOf True-  otherTypesDL p = DList.fromList (literals p) >>= typesDL-  typeSubst_ sub (lhs :=>: rhs) =-    map (typeSubst_ sub) lhs :=>: typeSubst_ sub rhs--instance Pretty a => Pretty (Prop a) where-  pPrint ([] :=>: rhs) = pPrint rhs-  pPrint p =-    hsep (punctuate (text " &") (map pPrint (lhs p))) <+> text "=>" <+> pPrint (rhs p)--data Equation a = a :=: a deriving (Show, Eq, Ord, Generic, Functor)--instance Symbolic f a => Symbolic f (Equation a) where-  termsDL (t :=: u) = termsDL t `mplus` termsDL u-  subst sub (t :=: u) = subst sub t :=: subst sub u--infix 5 :=:--instance Typed a => Typed (Equation a) where-  typ (t :=: _) = typ t-  otherTypesDL (t :=: u) = otherTypesDL t `mplus` typesDL u-  typeSubst_ sub (x :=: y) = typeSubst_ sub x :=: typeSubst_ sub y--instance Pretty a => Pretty (Equation a) where-  pPrintPrec _ _ (x :=: y)-    | isTrue x = pPrint y-    | isTrue y = pPrint x-    | otherwise = pPrint x <+> text "=" <+> pPrint y-    where-      -- XXX this is a hack-      isTrue x = show (pPrint x) == "True"--infix 4 ===-(===) :: a -> a -> Prop a-x === y = [] :=>: x :=: y--------------------------------------------------------------------------- Making properties look pretty (naming variables, etc.)-------------------------------------------------------------------------class PrettyArity fun where-  prettyArity :: fun -> Int-  prettyArity _ = 0--instance (PrettyArity fun1, PrettyArity fun2) => PrettyArity (fun1 :+: fun2) where-  prettyArity (Inl x) = prettyArity x-  prettyArity (Inr x) = prettyArity x--prettyProp ::-  (Typed fun, Apply (Term fun), PrettyTerm fun, PrettyArity fun) =>-  (Type -> [String]) -> Prop (Term fun) -> Doc-prettyProp cands =-  pPrint . nameVars cands . eta-  where-    eta prop =-      case filter isPretty (etaExpand prop) of-        [] -> last (etaExpand prop)-        (prop:_) -> prop--    isPretty (_ :=>: t :=: u) = isPretty1 t && isPretty1 u-    isPretty1 (App f ts) = prettyArity f <= length ts-    isPretty1 (Var _) = True--    etaExpand prop@(lhs :=>: t :=: u) =-      prop:-      case (tryApply t x, tryApply u x) of-        (Just t', Just u') -> etaExpand (lhs :=>: t' :=: u')-        _ -> []-      where-        x = Var (V (head (typeArgs (typ t))) n)-        n = maximum (0:map (succ . var_id) (vars prop))--data Named fun = Name String | Fun fun-instance Pretty fun => Pretty (Named fun) where-  pPrintPrec _ _ (Name name) = text name-  pPrintPrec l p (Fun fun) = pPrintPrec l p fun-instance PrettyTerm fun => PrettyTerm (Named fun) where-  termStyle Name{} = uncurried-  termStyle (Fun fun) = termStyle fun--nameVars :: (Type -> [String]) -> Prop (Term fun) -> Prop (Term (Named fun))-nameVars cands p =-  subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Fun) p)-  where-    sub = Map.fromList (evalState (mapM assign (nub (vars p))) Set.empty)-    assign x = do-      s <- get-      let names = supply (cands (typ x))-          name = head (filter (`Set.notMember` s) names)-      modify (Set.insert name)-      return (x, App (Name name) [])
− src/QuickSpec/Pruning.hs 
@@ -1,56 +0,0 @@--- A type of pruners.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, GeneralizedNewtypeDeriving, FlexibleInstances, UndecidableInstances, DefaultSignatures, GADTs #-}-module QuickSpec.Pruning where--import QuickSpec.Prop-import QuickSpec.Testing-import Control.Monad-import Control.Monad.Trans.Class-import Control.Monad.IO.Class-import Control.Monad.Trans.State.Strict-import Control.Monad.Trans.Reader--class Monad m => MonadPruner term norm m | m -> term norm where-  normaliser :: m (term -> norm)-  add :: Prop term -> m Bool--  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 Bool-  add = lift . add--instance MonadPruner term norm m => MonadPruner term norm (StateT s m)-instance MonadPruner term norm m => MonadPruner term norm (ReaderT r m)--normalise :: MonadPruner term norm m => term -> m norm-normalise t = do-  norm <- normaliser-  return (norm t)--newtype ReadOnlyPruner m a = ReadOnlyPruner { withReadOnlyPruner :: m a }-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term)--instance MonadTrans ReadOnlyPruner where-  lift = ReadOnlyPruner--instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where-  normaliser = ReadOnlyPruner normaliser-  add _ = return True--newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)-  deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)--instance MonadPruner term norm m => MonadPruner term norm (WatchPruner term m) where-  normaliser = lift normaliser-  add prop = do-    res <- lift (add prop)-    when res (WatchPruner (modify (prop:)))-    return res--watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term])-watchPruner (WatchPruner mx) = do-  (x, props) <- runStateT mx []-  return (x, reverse props)-
− src/QuickSpec/Pruning/Background.hs 
@@ -1,46 +0,0 @@--- A pruning layer which automatically adds axioms about functions as they appear.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, TypeOperators #-}-module QuickSpec.Pruning.Background where--import QuickSpec.Term-import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Prop-import QuickSpec.Terminal-import qualified Data.Set as Set-import Data.Set(Set)-import Control.Monad-import Control.Monad.IO.Class-import Control.Monad.Trans.Class-import Control.Monad.Trans.State.Strict hiding (State)--newtype Pruner fun m a =-  Pruner (StateT (Set fun) m a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTrans, MonadTester testcase term, MonadTerminal)--class Background f where-  background :: f -> [Prop (Term f)]-  background _ = []--run :: Monad m => Pruner fun m a -> m a-run (Pruner x) =-  evalStateT x Set.empty--instance (Ord fun, Background fun, MonadPruner (Term fun) norm m) =>-  MonadPruner (Term fun) norm (Pruner fun m) where-  normaliser = lift normaliser-  add prop = do-    mapM_ addFunction (funs prop)-    lift (add prop)--addFunction :: (Ord fun, Background fun, MonadPruner (Term fun) norm m) => fun -> Pruner fun m ()-addFunction f = do-  funcs <- Pruner get-  unless (f `Set.member` funcs) $ do-    Pruner (put (Set.insert f funcs))-    mapM_ add (background f)--instance (Background fun1, Background fun2) => Background (fun1 :+: fun2) where-  background (Inl x) = map (fmap (fmap Inl)) (background x)-  background (Inr x) = map (fmap (fmap Inr)) (background x)
− src/QuickSpec/Pruning/Twee.hs 
@@ -1,27 +0,0 @@--- A pruner that uses twee. Supports types and background axioms.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}-module QuickSpec.Pruning.Twee(Config(..), module QuickSpec.Pruning.Twee) where--import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Term-import QuickSpec.Terminal-import qualified QuickSpec.Pruning.Types as Types-import qualified QuickSpec.Pruning.Background as Background-import Control.Monad.Trans.Class-import Control.Monad.IO.Class-import qualified QuickSpec.Pruning.UntypedTwee as Untyped-import QuickSpec.Pruning.UntypedTwee(Config(..))--newtype Pruner fun m a =-  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 (Background.run (Types.run x))
− src/QuickSpec/Pruning/Types.hs 
@@ -1,110 +0,0 @@--- Encode monomorphic types during pruning.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}-module QuickSpec.Pruning.Types where--import QuickSpec.Pruning-import qualified QuickSpec.Pruning.Background as Background-import QuickSpec.Pruning.Background(Background)-import QuickSpec.Testing-import QuickSpec.Term-import QuickSpec.Type-import QuickSpec.Prop-import QuickSpec.Terminal-import Control.Monad.IO.Class-import Control.Monad.Trans.Class-import qualified Twee.Base as Twee--data Tagged fun =-    Func fun-  | Tag Type-  deriving (Eq, Ord, Show, Typeable)--instance Arity fun => Arity (Tagged fun) where-  arity (Func f) = arity f-  arity (Tag _) = 1--instance Sized fun => Sized (Tagged fun) where-  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 "]"--instance PrettyTerm fun => PrettyTerm (Tagged fun) where-  termStyle (Func f) = termStyle f-  termStyle (Tag _) = uncurried--instance EqualsBonus (Tagged fun) where--type TypedTerm fun = Term fun-type UntypedTerm fun = Term (Tagged fun)--newtype Pruner fun pruner a =-  Pruner { run :: pruner a }-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)--instance MonadTrans (Pruner fun) where-  lift = Pruner--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 -> 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 ->-        norm . encode $ t--  add prop = lift (add (encode <$> canonicalise prop))--instance (Typed fun, Arity fun) => Background (Tagged fun) where-  background = typingAxioms---- Compute the typing axioms for a function or type tag.-typingAxioms :: (Typed fun, Arity fun) =>-  Tagged fun -> [Prop (UntypedTerm fun)]-typingAxioms (Tag ty) =-  [tag ty (tag ty x) === tag ty x]-  where-    x = Var (V ty 0)-typingAxioms (Func func) =-  [tag res t === t] ++-  [tagArg i ty === t | (i, ty) <- zip [0..] args]-  where-    f = Func func-    xs = take n (map (Var . V typeVar) [0..])--    ty = typ func-    -- Use arity rather than typeArity, so that we can support-    -- partially-applied functions-    n = arity func-    args = take n (typeArgs ty)-    res = typeDrop n ty--    t = App f xs--    tagArg i ty =-      App f $-        take i xs ++-        [tag ty (xs !! i)] ++-        drop (i+1) xs--tag :: Type -> UntypedTerm fun -> UntypedTerm fun-tag ty t = App (Tag ty) [t]--encode :: Typed fun => TypedTerm fun -> UntypedTerm fun--- We always add type tags; see comment in normaliseMono.--- In the common case, twee will immediately remove these surplus type tags--- by rewriting using the typing axioms.-encode (Var x) = tag (typ x) (Var x)-encode (App f ts) =-  tag (typeDrop (length ts) (typ f)) (App (Func f) (map encode ts))
− src/QuickSpec/Pruning/UntypedTwee.hs 
@@ -1,126 +0,0 @@--- A pruner that uses twee. Does not respect types.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}-module QuickSpec.Pruning.UntypedTwee where--import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Prop-import QuickSpec.Term-import QuickSpec.Type-import Data.Lens.Light-import qualified Twee-import qualified Twee.Equation as Twee-import qualified Twee.KBO as KBO-import qualified Twee.Base as Twee-import Twee hiding (Config(..))-import Twee.Rule hiding (normalForms)-import Twee.Proof hiding (Config, defaultConfig)-import Twee.Base(Ordered(..), Extended(..), EqualsBonus)-import Control.Monad.Trans.Reader-import Control.Monad.Trans.State.Strict hiding (State)-import Control.Monad.Trans.Class-import Control.Monad.IO.Class-import QuickSpec.Terminal-import qualified Data.Set as Set-import Data.Set(Set)--data Config =-  Config {-    cfg_max_term_size :: Int,-    cfg_max_cp_depth :: Int }--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-  lessIn = KBO.lessIn--newtype Pruner fun m a =-  Pruner (ReaderT (Twee.Config (Extended fun)) (StateT (State (Extended fun)) m) a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)--instance MonadTrans (Pruner fun) where-  lift = Pruner . lift . lift--run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a-run Config{..} (Pruner x) =-  evalStateT (runReaderT x config) initialState-  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-  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--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) (Norm fun) (Pruner fun m) where-  normaliser = Pruner $ do-    state <- lift get-    return $ \t ->-      let u = normaliseTwee state t in-      u-      -- traceShow (text "normalise:" <+> pPrint t <+> text "->" <+> pPrint u) u--  add ([] :=>: t :=: u) = Pruner $ do-    state <- lift get-    config <- ask-    let-      t' = normalFormsTwee state t-      u' = normalFormsTwee state u-    -- Add the property anyway in case it could only be joined-    -- by considering all normal forms-    lift (put $! addTwee config t u state)-    return (Set.null (Set.intersection t' u'))--  add _ =-    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 -> Norm fun-normaliseTwee state 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 (Norm fun)-normalFormsTwee state 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)-addTwee config t u state =-  completePure config $-    addAxiom config state axiom-  where-    axiom = Axiom 0 (prettyShow (t :=: u)) (toTwee t Twee.:=: toTwee u)--toTwee :: (Ord f, Typeable f) =>-  Term f -> Twee.Term (Extended f)-toTwee = Twee.build . tt-  where-    tt (Var (V _ x)) =-      Twee.var (Twee.V x)-    tt (App f ts) =-      Twee.app (Twee.fun (Function f)) (map tt ts)--skolemise :: (Ord f, Typeable f) =>-  Term f -> Twee.Term (Extended f)-skolemise = Twee.build . sk-  where-    sk (Var (V _ x)) =-      Twee.con (Twee.fun (Skolem (Twee.V x)))-    sk (App f ts) =-      Twee.app (Twee.fun (Function f)) (map sk ts)
− src/QuickSpec/Term.hs 
@@ -1,212 +0,0 @@--- | 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 #-}-module QuickSpec.Term(module QuickSpec.Term, module Twee.Base, module Twee.Pretty) where--import QuickSpec.Type-import QuickSpec.Utils-import Control.Monad-import GHC.Generics(Generic)-import Test.QuickCheck(CoArbitrary)-import Data.DList(DList)-import qualified Data.DList as DList-import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)-import Twee.Pretty-import qualified Data.Map.Strict as Map-import Data.List---- | A typed term.-data Term f = Var {-# UNPACK #-} !Var | App !f ![Term f]-  deriving (Eq, Ord, Show, Functor)---- | A variable, which has a type and a number.-data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }-  deriving (Eq, Ord, Show, Generic, CoArbitrary)--instance Typed Var where-  typ x = var_ty x-  otherTypesDL _ = mzero-  typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x---- | A class for things that contain terms.-class Symbolic f a | a -> f where-  -- | A different list of all terms contained in the thing.-  termsDL :: a -> DList (Term f)-  -- | Apply a substitution to all terms in the thing.-  subst :: (Var -> Term f) -> a -> a--instance Symbolic f (Term f) where-  termsDL = return-  subst sub (Var x) = sub x-  subst sub (App f ts) = App f (map (subst sub) ts)--instance Symbolic f a => Symbolic f [a] where-  termsDL = msum . map termsDL-  subst sub = map (subst sub)--class Sized a where-  size :: a -> Int--instance Sized f => Sized (Term f) where-  size (Var _) = 1-  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)--instance PrettyTerm f => Pretty (Term f) where-  pPrintPrec l p (Var x) = pPrintPrec l p x-  pPrintPrec l p (App f xs) =-    pPrintTerm (termStyle f) l p (pPrint f) xs---- | Is a term an application (i.e. not a variable)?-isApp :: Term f -> Bool-isApp App{} = True-isApp Var{} = False---- | Is a term a variable?-isVar :: Term f -> Bool-isVar = not . isApp---- | All terms contained in a `Symbolic`.-terms :: Symbolic f a => a -> [Term f]-terms = DList.toList . termsDL---- | All function symbols appearing in a `Symbolic`, in order of appearance,--- with duplicates included.-funs :: Symbolic f a => a -> [f]-funs x = [ f | t <- terms x, App f _ <- subterms t ]---- | All variables appearing in a `Symbolic`, in order of appearance,--- with duplicates included.-vars :: Symbolic f a => a -> [Var]-vars x = [ v | t <- terms x, Var v <- subterms t ]---- | Compute the number of a variable which does /not/ appear in the `Symbolic`.-freeVar :: Symbolic f a => a -> Int-freeVar x = maximum (0:map (succ . var_id) (vars x))---- | Count how many times a given function symbol occurs.-occ :: (Eq f, Symbolic f a) => f -> a -> Int-occ x t = length (filter (== x) (funs t))---- | Count how many times a given variable occurs.-occVar :: Symbolic f a => Var -> a -> Int-occVar x t = length (filter (== x) (vars t))---- | Map a function over variables.-mapVar :: (Var -> Var) -> Term f -> Term f-mapVar f (Var x) = Var (f x)-mapVar f (App g xs) = App g (map (mapVar f) xs)---- | Find all subterms of a term. Includes the term itself.-subterms :: Term f -> [Term f]-subterms t = t:properSubterms t---- | Find all subterms of a term. Does not include the term itself.-properSubterms :: Term f -> [Term f]-properSubterms (App _ ts) = concatMap subterms ts-properSubterms _ = []---- | Renames variables so that they appear in a canonical order.--- Also makes sure that variables of different types have different numbers.-canonicalise :: Symbolic fun a => a -> a-canonicalise t = subst (\x -> Map.findWithDefault undefined x sub) t-  where-    sub =-      Map.fromList-        [(x, Var (V ty n))-        | (x@(V ty _), n) <- zip (nub (vars t)) [0..]]---- | Evaluate a term, given a valuation for variables and function symbols.-evalTerm :: (Typed fun, Apply a, Monad m) => (Var -> m a) -> (fun -> m a) -> Term fun -> m a-evalTerm var fun = eval-  where-    eval (Var x) = var x-    eval (App f ts) = do-      f <- fun f-      ts <- mapM eval ts-      return (foldl apply f ts)--instance Typed f => Typed (Term f) where-  typ (Var x) = typ x-  typ (App f ts) =-    typeDrop (length ts) (typ f)--  otherTypesDL (Var _) = mempty-  otherTypesDL (App f ts) =-    typesDL f `mplus` typesDL ts--  typeSubst_ sub = tsub-    where-      tsub (Var x) = Var (typeSubst_ sub x)-      tsub (App f ts) =-        App (typeSubst_ sub f) (map tsub ts)---- | 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, Int, MeasureFuns f, Int, [Var])--- | Compute the term ordering for a term.-measure :: (Sized f, Typed f) => Term f -> Measure f-measure 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)-instance Ord f => Eq (MeasureFuns f) where-  t == u = compare t u == EQ-instance Ord f => Ord (MeasureFuns f) where-  compare (MeasureFuns t) (MeasureFuns u) = compareFuns t u---- | A helper for `Measure`.-compareFuns :: Ord f => Term f -> Term f -> Ordering-compareFuns (Var x) (Var y) = compare x y-compareFuns Var{} App{} = LT-compareFuns App{} Var{} = GT-compareFuns (App f ts) (App g us) =-  compare f g `orElse`-  compare (map MeasureFuns ts) (map MeasureFuns us)--------------------------------------------------------------------------- * Data types a la carte-ish.--------------------------------------------------------------------------- | A sum type. Intended to be used to build the type of function--- symbols. Comes with instances that are useful for QuickSpec.-data a :+: b = Inl a | Inr b deriving (Eq, Ord)--instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where-  size (Inl x) = size x-  size (Inr x) = size x--instance (Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) where-  arity (Inl x) = arity x-  arity (Inr x) = arity x--instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where-  typ (Inl x) = typ x-  typ (Inr x) = typ x-  otherTypesDL (Inl x) = otherTypesDL x-  otherTypesDL (Inr x) = otherTypesDL x-  typeSubst_ sub (Inl x) = Inl (typeSubst_ sub x)-  typeSubst_ sub (Inr x) = Inr (typeSubst_ sub x)--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/Terminal.hs 
@@ -1,59 +0,0 @@-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE GeneralizedNewtypeDeriving, DefaultSignatures, GADTs #-}-module QuickSpec.Terminal where--import Control.Monad.Trans.Class-import Control.Monad.IO.Class-import Control.Monad.Trans.State.Strict-import Control.Monad.Trans.Reader-import qualified Test.QuickCheck.Text as Text--class Monad m => MonadTerminal m where-  putText :: String -> m ()-  putLine :: String -> m ()-  putTemp :: String -> m ()--  default putText :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()-  putText = lift . putText--  default putLine :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()-  putLine = lift . putLine--  default putTemp :: (MonadTrans t, MonadTerminal m', m ~ t m') => String -> m ()-  putTemp = lift . putTemp--instance MonadTerminal m => MonadTerminal (StateT s m)-instance MonadTerminal m => MonadTerminal (ReaderT r m)--putStatus :: MonadTerminal m => String -> m ()-putStatus str = putTemp ("[" ++ str ++ "...]")--clearStatus :: MonadTerminal m => m ()-clearStatus = putTemp ""--withStatus :: MonadTerminal m => String -> m a -> m a-withStatus str mx = putStatus str *> mx <* clearStatus--newtype Terminal a = Terminal (ReaderT Text.Terminal IO a)-  deriving (Functor, Applicative, Monad, MonadIO)--instance MonadTerminal Terminal where-  putText str = Terminal $ do-    term <- ask-    liftIO $ Text.putPart term str--  putLine str = Terminal $ do-    term <- ask-    liftIO $ Text.putLine term str--  putTemp str = Terminal $ do-    term <- ask-    liftIO $ Text.putTemp term str--withNullTerminal :: Terminal a -> IO a-withNullTerminal (Terminal mx) =-  Text.withNullTerminal (runReaderT mx)--withStdioTerminal :: Terminal a -> IO a-withStdioTerminal (Terminal mx) =-  Text.withStdioTerminal (runReaderT mx)
− src/QuickSpec/Testing.hs 
@@ -1,18 +0,0 @@--- A type of test case generators.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DefaultSignatures, GADTs, FlexibleInstances, UndecidableInstances #-}-module QuickSpec.Testing where--import QuickSpec.Prop-import Control.Monad.Trans.Class-import Control.Monad.Trans.State.Strict-import Control.Monad.Trans.Reader--class Monad m => MonadTester testcase term m | m -> testcase term where-  test :: Prop term -> m (Maybe testcase)--  default test :: (MonadTrans t, MonadTester testcase term m', m ~ t m') => Prop term -> m (Maybe testcase)-  test = lift . test--instance MonadTester testcase term m => MonadTester testcase term (StateT s m)-instance MonadTester testcase term m => MonadTester testcase term (ReaderT r m)
− src/QuickSpec/Testing/DecisionTree.hs 
@@ -1,95 +0,0 @@--- Decision trees for testing terms for equality.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards #-}-module QuickSpec.Testing.DecisionTree where--import qualified Data.Map as Map-import Data.Map(Map)--data DecisionTree testcase result term =-  DecisionTree {-    -- A function for evaluating terms on test cases.-    dt_evaluate :: term -> testcase -> result,-    -- The set of test cases gathered so far.-    dt_test_cases :: [testcase],-    -- The tree itself.-    dt_tree :: !(Maybe (InnerTree result term)) }--data InnerTree result term =-    TestCase !(Map result (InnerTree result term))-  | Singleton !term--data Result testcase result term =-    Distinct (DecisionTree testcase result term)-  | EqualTo term---- Make a new decision tree.-empty :: (term -> testcase -> result) -> DecisionTree testcase result term-empty eval =-  DecisionTree {-    dt_evaluate = eval,-    dt_test_cases = [],-    dt_tree = Nothing }---- Add a new test case to a decision tree.-addTestCase ::-  testcase -> DecisionTree testcase result term ->-  DecisionTree testcase result term-addTestCase tc dt@DecisionTree{..} =-  dt{dt_test_cases = dt_test_cases ++ [tc]}---- Insert a value into a decision tree.-insert :: Ord result =>-  term -> DecisionTree testcase result term ->-  Result testcase result term-insert x dt@DecisionTree{dt_tree = Nothing, ..} =-  Distinct dt{dt_tree = Just (Singleton x)}-insert x dt@DecisionTree{dt_tree = Just dt_tree, ..} =-  aux k dt_test_cases dt_tree-  where-    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)) -    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-        Nothing ->-          Distinct (k' (Singleton x))-        Just tree ->-          aux k' ts tree-    aux _ [] (TestCase _) =-      error "unexpected node in decision tree"--data Statistics =-  Statistics {-    -- Total number of terms in the decision tree-    stat_num_terms :: !Int,-    -- Total number of tests executed-    stat_num_tests :: !Int,-    -- Number of distinct test cases used-    stat_num_test_cases :: !Int }-  deriving (Eq, Show)--statistics :: DecisionTree testcase result term -> Statistics-statistics DecisionTree{dt_tree = Nothing} =-  Statistics 0 0 0-statistics DecisionTree{dt_tree = Just dt_tree, ..} =-  Statistics {-    stat_num_terms = x,-    stat_num_tests = y,-    stat_num_test_cases = length dt_test_cases }-  where-    (x, y) = stat dt_tree--    -- Returns (number of terms, number of tests)-    stat Singleton{} = (1, 0)-    -- To calculate the number of test cases, note that each term-    -- under res executed one test case on the way through this node.-    stat (TestCase res) =-      (sum (map fst ss), sum [ x + y | (x, y) <- ss ])-      where-        ss = map stat (Map.elems res)
− src/QuickSpec/Testing/QuickCheck.hs 
@@ -1,97 +0,0 @@--- Testing conjectures using QuickCheck.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts, FlexibleInstances, RecordWildCards, MultiParamTypeClasses, GeneralizedNewtypeDeriving #-}-module QuickSpec.Testing.QuickCheck where--import QuickSpec.Testing-import QuickSpec.Pruning-import QuickSpec.Prop-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-import Data.List-import System.Random-import QuickSpec.Terminal-import Data.Lens.Light--data Config =-  Config {-    cfg_num_tests :: Int,-    cfg_max_test_size :: Int,-    cfg_fixed_seed :: Maybe QCGen}-  deriving Show--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 {-    env_config :: Config,-    env_tests :: [testcase],-    env_eval :: testcase -> term -> result }--newtype Tester testcase term result m a =-  Tester (ReaderT (Environment testcase term result) m a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal, MonadPruner term' res')--instance MonadTrans (Tester testcase term result) where-  lift = Tester . lift--run ::-  Config -> Gen testcase -> (testcase -> term -> 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-    k = max 1 cfg_max_test_size-    bias = 3-    -- 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)-    tests = zipWith (unGen gen) seeds sizes-  return $ runReaderT x-    Environment {-      env_config = config,-      env_tests = tests,-      env_eval = eval }---- uniform n k: generate a list of n integers which are distributed evenly between 0 and k-1.-uniform :: Integer -> Integer -> [Integer]-uniform n k =-  -- n `div` k: divide evenly as far as possible.-  concat [replicate (fromIntegral (n `div` k)) i | i <- [0..k-1]] ++-  -- The leftovers get distributed at equal intervals.-  [i * k `div` leftovers | i <- [0..leftovers-1]]-  where-    leftovers = n `mod` k--instance (Monad m, Eq result) => MonadTester testcase term (Tester testcase term result m) where-  test prop =-    Tester $ do-      env <- ask-      return $! quickCheckTest env prop--quickCheckTest :: Eq result =>-  Environment testcase term result ->-  Prop term -> Maybe testcase-quickCheckTest Environment{env_config = Config{..}, ..} (lhs :=>: rhs) =-  msum (map test env_tests)-  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
− src/QuickSpec/Type.hs 
@@ -1,562 +0,0 @@--- | 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 #-}--- To avoid a warning about TyVarNumber's constructor being unused:-{-# OPTIONS_GHC -fno-warn-unused-binds #-}-module QuickSpec.Type(-  -- * Types-  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, isArrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,-  isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,-  -- * Things that have types-  Typed(..), typeSubst, typesDL, tyVars, cast, matchType,-  TypeView(..),-  Apply(..), apply, canApply,-  oneTypeVar, defaultTo, skolemiseTypeVars,-  -- * Polymorphic types-  canonicaliseType,-  Poly, toPolyValue, poly, unPoly, polyTyp, polyRename, polyApply, polyPair, polyList, polyMgu,-  -- * Dynamic values-  Value, toValue, fromValue, valueType,-  unwrap, Unwrapped(..), Wrapper(..),-  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor, bringFunctor) where--import Control.Monad-import Data.DList(DList)-import Data.Maybe-import qualified Data.Typeable as Ty-import Data.Typeable(Typeable)-import GHC.Exts(Any)-import Test.QuickCheck-import Unsafe.Coerce-import Data.Constraint-import Twee.Base-import Data.Proxy-import Data.List-import Data.Char-import Data.Functor.Identity---- | A (possibly polymorphic) type.-type Type = Term TyCon---- | A type constructor.-data TyCon =-    -- | The function type constructor @(->)@.-    Arrow-    -- | An ordinary Haskell type constructor.-  | TyCon Ty.TyCon-    -- | A string. Can be used to represent miscellaneous types that do not-    -- really exist in Haskell.-  | String String-  deriving (Eq, Ord, Show)--instance Pretty TyCon where-  pPrint Arrow = text "->"-  pPrint (String x) = text x-  pPrint (TyCon x) = text (show x)-instance PrettyTerm TyCon where-  termStyle Arrow =-    fixedArity 2 $-    TermStyle $ \l p d [x, y] ->-      maybeParens (p > 8) $-        pPrintPrec l 9 x <+> d <+>-        pPrintPrec l 0 y--  termStyle (String _) = curried--  termStyle (TyCon con)-    | con == listTyCon =-      fixedArity 1 $-      TermStyle $ \l _ _ [x] -> brackets (pPrintPrec l 0 x)-    | show con == "()" || show con == "(%%)" =-      fixedArity 0 tupleStyle -- by analogy with case below-    | take 2 (show con) == "(," ||-      take 3 (show con) == "(%," =-      fixedArity (1+length (filter (== ',') (show con))) tupleStyle-    | isAlphaNum (head (show con)) = curried-    | otherwise = infixStyle 5---- Type and class variables.-newtype A = A Any deriving Typeable-newtype B = B Any deriving Typeable-newtype C = C Any deriving Typeable-newtype D = D Any deriving Typeable-newtype E = E Any deriving Typeable--class ClassA-deriving instance Typeable ClassA-class ClassB-deriving instance Typeable ClassB-class ClassC-deriving instance Typeable ClassC-class ClassD-deriving instance Typeable ClassD-class ClassE-deriving instance Typeable ClassE-class ClassF-deriving instance Typeable ClassF---- | A polymorphic type of kind Symbol.-type SymA = "__polymorphic_symbol__"---- | All type variables that are defined in this module.-typeVars :: [Ty.TypeRep]-typeVars =-  [Ty.typeRep (Proxy :: Proxy A),-   Ty.typeRep (Proxy :: Proxy B),-   Ty.typeRep (Proxy :: Proxy C),-   Ty.typeRep (Proxy :: Proxy D),-   Ty.typeRep (Proxy :: Proxy E),-   Ty.typeRep (Proxy :: Proxy ClassA),-   Ty.typeRep (Proxy :: Proxy ClassB),-   Ty.typeRep (Proxy :: Proxy ClassC),-   Ty.typeRep (Proxy :: Proxy ClassD),-   Ty.typeRep (Proxy :: Proxy ClassE),-   Ty.typeRep (Proxy :: Proxy ClassF),-   Ty.typeRep (Proxy :: Proxy SymA)]---- | A type variable.-typeVar :: Type-typeVar = typeRep (Proxy :: Proxy A)---- | Check if a type is a type variable.-isTypeVar :: Type -> Bool-isTypeVar = isVar---- | Construct a type from a `Typeable`.-typeOf :: Typeable a => a -> Type-typeOf x = fromTypeRep (Ty.typeOf x)---- | Construct a type from a `Typeable`.-typeRep :: Typeable (a :: k) => proxy a -> Type-typeRep x = fromTypeRep (Ty.typeRep x)---- | Turn a `TyCon` into a type.-typeFromTyCon :: TyCon -> Type-typeFromTyCon tc = build (con (fun tc))---- | Function application for type constructors.------ For example, @applyType (typeRep (Proxy :: Proxy [])) (typeRep (Proxy :: Proxy Int)) == typeRep (Proxy :: Proxy [Int])@.-applyType :: Type -> Type -> Type-applyType (App f tys) ty = build (app f (unpack tys ++ [ty]))-applyType _ _ = error "tried to apply type variable"---- | Construct a function type.-arrowType :: [Type] -> Type -> Type-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).------ For multiple-argument functions, unpacks one argument.-unpackArrow :: Type -> Maybe (Type, Type)-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))) =-  arg:typeArgs res-typeArgs _ = []---- | The result of a function type.-typeRes :: Type -> Type-typeRes (App (F Arrow) (Cons _ (Cons res Empty))) =-  typeRes res-typeRes ty = ty---- | Given the type of a function, returns the type of applying that function to--- @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-1) ty-typeDrop _ _ =-  error "typeDrop on non-function type"---- | How many arguments does a function take?-typeArity :: Type -> Int-typeArity = length . typeArgs---- | Unify all type variables in a type.-oneTypeVar :: Typed a => a -> a-oneTypeVar = typeSubst (const (var (V 0)))---- | Replace all type variables with a particular type.-defaultTo :: Typed a => Type -> a -> a-defaultTo def = typeSubst (const def)---- | Make a type ground by replacing all type variables--- with Skolem constants.-skolemiseTypeVars :: Typed a => a -> a-skolemiseTypeVars = typeSubst (const aTy)-  where-    aTy = build (con (fun (tyCon (Proxy :: Proxy A))))---- | Construct a type from a `Ty.TypeRep`.-fromTypeRep :: Ty.TypeRep -> Type-fromTypeRep ty-  | Just n <- elemIndex ty typeVars =-      build (var (V n))-  | otherwise =-    let (tyCon, tys) = Ty.splitTyConApp ty in-    build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys))---- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`.-fromTyCon :: Ty.TyCon -> TyCon-fromTyCon ty-  | ty == arrowTyCon = Arrow-  | otherwise = TyCon ty---- | Some built-in type consructors.-arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon-arrowTyCon = mkCon (Proxy :: Proxy (->))-commaTyCon = mkCon (Proxy :: Proxy (,))-listTyCon  = mkCon (Proxy :: Proxy [])-dictTyCon  = mkCon (Proxy :: Proxy Dict)--mkCon :: Typeable a => proxy a -> Ty.TyCon-mkCon = fst . Ty.splitTyConApp . Ty.typeRep---- | Get the outermost `TyCon` of a `Typeable`.-tyCon :: Typeable a => proxy a -> TyCon-tyCon = fromTyCon . mkCon---- | 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))-  | dict == dictTyCon = Just ty-getDictionary _ = Nothing---- | Check if a type is of the form @`Dict` c@.-isDictionary :: Type -> Bool-isDictionary = isJust . getDictionary---- | Count how many dictionary arguments a type has.-dictArity :: Type -> Int-dictArity = length . takeWhile isDictionary . typeArgs---- | Split a type into constraints and normal type.-splitConstrainedType :: Type -> ([Type], Type)-splitConstrainedType ty =-  (dicts, arrowType rest (typeRes ty))-  where-    (dicts, rest) = splitAt (dictArity ty) (typeArgs ty)---- CoArbitrary instances.-instance CoArbitrary Type where-  coarbitrary = coarbitrary . singleton-instance CoArbitrary (TermList TyCon) where-  coarbitrary Empty = variant 0-  coarbitrary (ConsSym (Var (V x)) ts) =-    variant 1 . coarbitrary x . coarbitrary ts-  coarbitrary (ConsSym (App f _) ts) =-    variant 2 . coarbitrary (fun_id f) . coarbitrary ts---- | Pretty-print a type. Differs from the `Pretty` instance by printing type--- variables in lowercase.-pPrintType :: Type -> Doc-pPrintType = ppr . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise-  where-    as = supply [[x] | x <- ['a'..'z']]-    -- Print dictionary arguments specially-    ppr ty-      | Just (dict, res) <- unpackArrow ty,-        Just constraint <- getDictionary dict =-      pPrint constraint <+> text "=>" <+> ppr res-    ppr ty = pPrint ty---- | A class for things that have a type.-class Typed a where-  -- | The type.-  typ :: a -> Type-  -- | Types that appear elsewhere in the `Typed`, for example, types of subterms.-  -- Should return everything which is affected by `typeSubst`.-  otherTypesDL :: a -> DList Type-  otherTypesDL _ = mzero-  -- | Substitute for all type variables.-  typeSubst_ :: (Var -> Builder TyCon) -> a -> a---- | Substitute for all type variables in a `Typed`.-{-# INLINE typeSubst #-}-typeSubst :: (Typed a, Substitution s, SubstFun s ~ TyCon) => s -> a -> a-typeSubst s x = typeSubst_ (evalSubst s) x---- | A wrapper for using the `Twee.Base.Symbolic` machinery on types.-newtype TypeView a = TypeView { unTypeView :: a }-instance Typed a => Symbolic (TypeView a) where-  type ConstantOf (TypeView a) = TyCon-  termsDL = fmap singleton . typesDL . unTypeView-  subst_ sub = TypeView . typeSubst_ sub . unTypeView-instance Typed a => Has (TypeView a) Type where-  the = typ . unTypeView---- | All types that occur in a `Typed`.-typesDL :: Typed a => a -> DList Type-typesDL ty = return (typ ty) `mplus` otherTypesDL ty---- | All type variables that occur in a `Typed`.-tyVars :: Typed a => a -> [Var]-tyVars = vars . TypeView---- | Cast a `Typed` to a target type.--- Succeeds if the target type is an instance of the current type.-cast :: Typed a => Type -> a -> Maybe a-cast ty x = do-  s <- match (typ x) ty-  return (typeSubst s x)---- | Check if the second argument is an instance of the first argument.-matchType :: Type -> Type -> Maybe (Subst TyCon)-matchType = match---- | Typed things that support function application.-class Typed a => Apply a where-  -- | Apply a function to its argument.-  ---  -- For most instances of `Typed`, the type of the argument must be exactly-  -- equal to the function's argument type. If you want unification to happen,-  -- use the `Typed` instance of `Poly`.-  tryApply :: a -> a -> Maybe a---- | Apply a function to its argument, crashing on failure.------ For most instances of `Typed`, the type of the argument must be exactly--- equal to the function's argument type. If you want unification to happen,--- use the `Typed` instance of `Poly`.-infixl `apply`-apply :: Apply a => a -> a -> a-apply f x =-  case tryApply f x of-    Nothing ->-      error $-        "apply: ill-typed term: can't apply " ++-        prettyShow (typ f) ++ " to " ++ prettyShow (typ x)-    Just y -> y---- | Check if a function can be applied to its argument.-canApply :: Apply a => a -> a -> Bool-canApply f x = isJust (tryApply f x)---- Instances.-instance Typed Type where-  typ = id-  typeSubst_ = subst--instance Apply Type where-  tryApply (App (F Arrow) (Cons arg (Cons res Empty))) t-    | t == arg = Just res-  tryApply _ _ = Nothing--instance (Typed a, Typed b) => Typed (a, b) where-  typ (x, y) = build (app (fun (TyCon commaTyCon)) [typ x, typ y])-  otherTypesDL (x, y) = otherTypesDL x `mplus` otherTypesDL y-  typeSubst_ f (x, y) = (typeSubst_ f x, typeSubst_ f y)--instance (Typed a, Typed b) => Typed (Either a b) where-  typ (Left x)  = typ x-  typ (Right x) = typ x-  otherTypesDL (Left x)  = otherTypesDL x-  otherTypesDL (Right x) = otherTypesDL x-  typeSubst_ sub (Left x)  = Left  (typeSubst_ sub x)-  typeSubst_ sub (Right x) = Right (typeSubst_ sub x)--instance Typed a => Typed [a] where-  typ [] = typeOf ()-  typ (x:_) = typ x-  otherTypesDL [] = mzero-  otherTypesDL (x:xs) = otherTypesDL x `mplus` msum (map typesDL xs)-  typeSubst_ f xs = map (typeSubst_ f) xs---- | Represents a forall-quantifier over all the type variables in a type.--- Wrapping a term in @Poly@ normalises the type by alpha-renaming--- type variables canonically.------ The `Apply` instance for `Poly` does unification to handle applying a--- polymorphic function.-newtype Poly a = Poly { unPoly :: a }-  deriving (Eq, Ord, Show, Pretty, Typeable)---- | Build a `Poly`.-poly :: Typed a => a -> Poly a-poly x = Poly (canonicaliseType x)---- | Alpha-rename type variables in a canonical way.-canonicaliseType :: Typed a => a -> a-canonicaliseType = unTypeView . canonicalise . TypeView---- | Get the polymorphic type of a polymorphic value.-polyTyp :: Typed a => Poly a -> Poly Type-polyTyp (Poly x) = Poly (typ x)---- | Rename the type variables of the second argument so that they don't overlap--- with those of the first argument.-polyRename :: (Typed a, Typed b) => a -> Poly b -> b-polyRename x (Poly y) =-  unTypeView (renameAvoiding (TypeView x) (TypeView y))---- | Rename the type variables of both arguments so that they don't overlap.-polyApply :: (Typed a, Typed b, Typed c) => (a -> b -> c) -> Poly a -> Poly b -> Poly c-polyApply f (Poly x) y = poly (f x (polyRename x y))---- | Rename the type variables of both arguments so that they don't overlap.-polyPair :: (Typed a, Typed b) => Poly a -> Poly b -> Poly (a, b)-polyPair = polyApply (,)---- | Rename the type variables of all arguments so that they don't overlap.-polyList :: Typed a => [Poly a] -> Poly [a]-polyList [] = poly []-polyList (x:xs) = polyApply (:) x (polyList xs)---- | Find the most general unifier of two types.-polyMgu :: Poly Type -> Poly Type -> Maybe (Poly Type)-polyMgu ty1 ty2 = do-  let (ty1', ty2') = unPoly (polyPair ty1 ty2)-  sub <- unify ty1' ty2'-  return (poly (typeSubst sub ty1'))--instance Typed a => Typed (Poly a) where-  typ = typ . unPoly-  otherTypesDL = otherTypesDL . unPoly-  typeSubst_ f (Poly x) = poly (typeSubst_ f x)--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'')---- | Convert an ordinary value to a dynamic value.-toPolyValue :: (Applicative f, Typeable a) => a -> Poly (Value f)-toPolyValue = poly . toValue . pure---- | Dynamic values inside an applicative functor.------ For example, a value of type @Value Maybe@ represents a @Maybe something@.-data Value f =-  Value {-    valueType :: Type,-    value :: f Any }--instance Show (Value f) where-  show x = "<<" ++ prettyShow (typ x) ++ ">>"--fromAny :: f Any -> f a-fromAny = unsafeCoerce--toAny :: f a -> f Any-toAny = unsafeCoerce---- | Construct a `Value`.-toValue :: forall f (a :: *). Typeable a => f a -> Value f-toValue x = Value (typeRep (Proxy :: Proxy a)) (toAny x)---- | Deconstruct a `Value`.-fromValue :: forall f (a :: *). Typeable a => Value f -> Maybe (f a)-fromValue x = do-  guard (typ x == typeRep (Proxy :: Proxy a))-  return (fromAny (value x))--instance Typed (Value f) where-  typ = valueType-  typeSubst_ f (Value ty x) = Value (typeSubst_ f ty) x-instance Applicative f => Apply (Value f) where-  tryApply f x = do-    ty <- tryApply (typ f) (typ x)-    return (Value ty (fromAny (value f) <*> value x))---- | Unwrap a value to get at the thing inside, with an existential type.-unwrap :: Value f -> Unwrapped f-unwrap x =-  value x `In`-    Wrapper-      (\y -> Value (typ x) y)-      (\y ->-        if typ x == typ y-        then fromAny (value y)-        else error "non-matching types")---- | The unwrapped value. Consists of the value itself (with an existential--- type) and functions to wrap it up again.-data Unwrapped f where-  In :: f a -> Wrapper a -> Unwrapped f---- | Functions for re-wrapping an `Unwrapped` value.-data Wrapper a =-  Wrapper {-    -- | Wrap up a value which has the same existential type as this one.-    wrap :: forall g. g a -> Value g,-    -- | Unwrap a value which has the same existential type as this one.-    reunwrap :: forall g. Value g -> g a }---- | Apply a polymorphic function to a `Value`.-mapValue :: (forall a. f a -> g a) -> Value f -> Value g-mapValue f v =-  case unwrap v of-    x `In` w -> wrap w (f x)---- | Apply a polymorphic function to a `Value`.-forValue :: Value f -> (forall a. f a -> g a) -> Value g-forValue x f = mapValue f x---- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.-ofValue :: (forall a. f a -> b) -> Value f -> b-ofValue f v =-  case unwrap v of-    x `In` _ -> f x---- | Apply a polymorphic function that returns a non-`Value` result to a `Value`.-withValue :: Value f -> (forall a. f a -> b) -> b-withValue x f = ofValue f x---- | Apply a polymorphic function to a pair of `Value`s.-pairValues :: forall f g. Typeable g => (forall a b. f a -> f b -> f (g a b)) -> Value f -> Value f -> Value f-pairValues f x y =-  ty `seq`-  Value {-    valueType = ty,-    value = toAny (f (value x) (value y)) }-  where-    ty = typeRep (Proxy :: Proxy g) `applyType` typ x `applyType` typ y--wrapFunctor :: forall f g h. Typeable h => (forall a. f a -> g (h a)) -> Value f -> Value g-wrapFunctor f x =-  ty `seq`-  Value {-    valueType = ty,-    value = toAny (f (value x)) }-  where-    ty = typeRep (Proxy :: Proxy h) `applyType` valueType x--unwrapFunctor :: forall f g h. Typeable g => (forall a. f (g a) -> h a) -> Value f -> Value h-unwrapFunctor f x =-  case typ x of-    App _ tys | tys@(_:_) <- unpack tys ->-      case ty `applyType` last tys == typ x of-        True ->-          Value {-            valueType = last tys,-            value = f (fromAny (value x)) }-        False ->-          error "non-matching types"-    _ -> error "value of type f a had wrong type"-  where-    ty = typeRep (Proxy :: Proxy g)--bringFunctor :: Functor f => Value f -> f (Value Identity)-bringFunctor val =-  case unwrap val of-    x `In` w ->-      fmap (wrap w . Identity) x
− src/QuickSpec/Utils.hs 
@@ -1,138 +0,0 @@--- | Miscellaneous utility functions.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE CPP #-}-module QuickSpec.Utils where--import Control.Arrow((&&&))-import Control.Exception-import Control.Spoon-import Data.List(groupBy, sortBy)-#if !MIN_VERSION_base(4,8,0)-import Data.Monoid-#endif-import Data.Ord(comparing)-import System.IO-import qualified Control.Category as Category-import qualified Data.Map.Strict as Map-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..)--key :: Ord a => a -> Lens (Map a b) (Maybe b)-key x = lens (Map.lookup x) (\my m -> Map.alter (const my) x m)--keyDefault :: Ord a => a -> b -> Lens (Map a b) b-keyDefault x y = lens (Map.findWithDefault y x) (\y m -> Map.insert x y m)--reading :: (a -> Lens a b) -> Lens a b-reading f = lens (\x -> getL (f x) x) (\y x -> setL (f x) y x)--fstLens :: Lens (a, b) a-fstLens = lens fst (\x (_, y) -> (x, y))--sndLens :: Lens (a, b) b-sndLens = lens snd (\y (x, _) -> (x, y))--makeLensAs :: Name -> [(String, String)] -> Q [Dec]-makeLensAs ty names =-  nameMakeLens ty (\x -> lookup x names)--repeatM :: Monad m => m a -> m [a]-repeatM = sequence . repeat--partitionBy :: Ord b => (a -> b) -> [a] -> [[a]]-partitionBy value =-  map (map fst) .-  groupBy (\x y -> snd x == snd y) .-  sortBy (comparing snd) .-  map (id &&& value)--collate :: Ord a => ([b] -> c) -> [(a, b)] -> [(a, c)]-collate f = map g . partitionBy fst-  where-    g xs = (fst (head xs), f (map snd xs))--isSorted :: Ord a => [a] -> Bool-isSorted xs = and (zipWith (<=) xs (tail xs))--isSortedBy :: Ord b => (a -> b) -> [a] -> Bool-isSortedBy f xs = isSorted (map f xs)--usort :: Ord a => [a] -> [a]-usort = usortBy compare--usortBy :: (a -> a -> Ordering) -> [a] -> [a]-usortBy f = map head . groupBy (\x y -> f x y == EQ) . sortBy f--sortBy' :: Ord b => (a -> b) -> [a] -> [a]-sortBy' f = map snd . sortBy (comparing fst) . map (\x -> (f x, x))--usortBy' :: Ord b => (a -> b) -> [a] -> [a]-usortBy' f = map snd . usortBy (comparing fst) . map (\x -> (f x, x))--orElse :: Ordering -> Ordering -> Ordering-EQ `orElse` x = x-x  `orElse` _ = x--unbuffered :: IO a -> IO a-unbuffered x = do-  buf <- hGetBuffering stdout-  bracket_-    (hSetBuffering stdout NoBuffering)-    (hSetBuffering stdout buf)-    x--spoony :: Eq a => a -> Maybe a-spoony x = teaspoon ((x == x) `seq` x)--labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]-labelM f = mapM (\x -> do { y <- f x; return (x, y) })--#if __GLASGOW_HASKELL__ < 710-isSubsequenceOf :: Ord a => [a] -> [a] -> Bool-[] `isSubsequenceOf` ys = True-(x:xs) `isSubsequenceOf` [] = False-(x:xs) `isSubsequenceOf` (y:ys)-  | x == y = xs `isSubsequenceOf` ys-  | otherwise = (x:xs) `isSubsequenceOf` ys-#endif--appendAt :: Int -> [a] -> [[a]] -> [[a]]-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