diff --git a/quickspec.cabal b/quickspec.cabal --- a/quickspec.cabal +++ b/quickspec.cabal @@ -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, diff --git a/src/QuickSpec.hs b/src/QuickSpec.hs --- a/src/QuickSpec.hs +++ b/src/QuickSpec.hs @@ -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 diff --git a/src/QuickSpec/Explore.hs b/src/QuickSpec/Explore.hs deleted file mode 100644 --- a/src/QuickSpec/Explore.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Explore/Conditionals.hs b/src/QuickSpec/Explore/Conditionals.hs deleted file mode 100644 --- a/src/QuickSpec/Explore/Conditionals.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Explore/PartialApplication.hs b/src/QuickSpec/Explore/PartialApplication.hs deleted file mode 100644 --- a/src/QuickSpec/Explore/PartialApplication.hs +++ /dev/null @@ -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)))) diff --git a/src/QuickSpec/Explore/Polymorphic.hs b/src/QuickSpec/Explore/Polymorphic.hs deleted file mode 100644 --- a/src/QuickSpec/Explore/Polymorphic.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Explore/Schemas.hs b/src/QuickSpec/Explore/Schemas.hs deleted file mode 100644 --- a/src/QuickSpec/Explore/Schemas.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Explore/Terms.hs b/src/QuickSpec/Explore/Terms.hs deleted file mode 100644 --- a/src/QuickSpec/Explore/Terms.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Haskell.hs b/src/QuickSpec/Haskell.hs deleted file mode 100644 --- a/src/QuickSpec/Haskell.hs +++ /dev/null @@ -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 @@. -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 diff --git a/src/QuickSpec/Haskell/Resolve.hs b/src/QuickSpec/Haskell/Resolve.hs deleted file mode 100644 --- a/src/QuickSpec/Haskell/Resolve.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Internal.hs b/src/QuickSpec/Internal.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal.hs @@ -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] diff --git a/src/QuickSpec/Internal/Explore.hs b/src/QuickSpec/Internal/Explore.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Explore.hs @@ -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 diff --git a/src/QuickSpec/Internal/Explore/Conditionals.hs b/src/QuickSpec/Internal/Explore/Conditionals.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Explore/Conditionals.hs @@ -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 diff --git a/src/QuickSpec/Internal/Explore/Polymorphic.hs b/src/QuickSpec/Internal/Explore/Polymorphic.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Explore/Polymorphic.hs @@ -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 diff --git a/src/QuickSpec/Internal/Explore/Schemas.hs b/src/QuickSpec/Internal/Explore/Schemas.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Explore/Schemas.hs @@ -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 diff --git a/src/QuickSpec/Internal/Explore/Terms.hs b/src/QuickSpec/Internal/Explore/Terms.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Explore/Terms.hs @@ -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 diff --git a/src/QuickSpec/Internal/Haskell.hs b/src/QuickSpec/Internal/Haskell.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Haskell.hs @@ -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 @@. +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 diff --git a/src/QuickSpec/Internal/Haskell/Resolve.hs b/src/QuickSpec/Internal/Haskell/Resolve.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Haskell/Resolve.hs @@ -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) diff --git a/src/QuickSpec/Internal/Parse.hs b/src/QuickSpec/Internal/Parse.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Parse.hs @@ -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) diff --git a/src/QuickSpec/Internal/Prop.hs b/src/QuickSpec/Internal/Prop.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Prop.hs @@ -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)) diff --git a/src/QuickSpec/Internal/Pruning.hs b/src/QuickSpec/Internal/Pruning.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning.hs @@ -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) + diff --git a/src/QuickSpec/Internal/Pruning/Background.hs b/src/QuickSpec/Internal/Pruning/Background.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning/Background.hs @@ -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) diff --git a/src/QuickSpec/Internal/Pruning/PartialApplication.hs b/src/QuickSpec/Internal/Pruning/PartialApplication.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning/PartialApplication.hs @@ -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) diff --git a/src/QuickSpec/Internal/Pruning/Twee.hs b/src/QuickSpec/Internal/Pruning/Twee.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning/Twee.hs @@ -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))) diff --git a/src/QuickSpec/Internal/Pruning/Types.hs b/src/QuickSpec/Internal/Pruning/Types.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning/Types.hs @@ -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" diff --git a/src/QuickSpec/Internal/Pruning/UntypedTwee.hs b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Pruning/UntypedTwee.hs @@ -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" diff --git a/src/QuickSpec/Internal/Term.hs b/src/QuickSpec/Internal/Term.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Term.hs @@ -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 diff --git a/src/QuickSpec/Internal/Terminal.hs b/src/QuickSpec/Internal/Terminal.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Terminal.hs @@ -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) diff --git a/src/QuickSpec/Internal/Testing.hs b/src/QuickSpec/Internal/Testing.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Testing.hs @@ -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) diff --git a/src/QuickSpec/Internal/Testing/DecisionTree.hs b/src/QuickSpec/Internal/Testing/DecisionTree.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Testing/DecisionTree.hs @@ -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) diff --git a/src/QuickSpec/Internal/Testing/QuickCheck.hs b/src/QuickSpec/Internal/Testing/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Testing/QuickCheck.hs @@ -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 diff --git a/src/QuickSpec/Internal/Type.hs b/src/QuickSpec/Internal/Type.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Type.hs @@ -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 diff --git a/src/QuickSpec/Internal/Utils.hs b/src/QuickSpec/Internal/Utils.hs new file mode 100644 --- /dev/null +++ b/src/QuickSpec/Internal/Utils.hs @@ -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 diff --git a/src/QuickSpec/Parse.hs b/src/QuickSpec/Parse.hs deleted file mode 100644 --- a/src/QuickSpec/Parse.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Prop.hs b/src/QuickSpec/Prop.hs deleted file mode 100644 --- a/src/QuickSpec/Prop.hs +++ /dev/null @@ -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) []) diff --git a/src/QuickSpec/Pruning.hs b/src/QuickSpec/Pruning.hs deleted file mode 100644 --- a/src/QuickSpec/Pruning.hs +++ /dev/null @@ -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) - diff --git a/src/QuickSpec/Pruning/Background.hs b/src/QuickSpec/Pruning/Background.hs deleted file mode 100644 --- a/src/QuickSpec/Pruning/Background.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Pruning/Twee.hs b/src/QuickSpec/Pruning/Twee.hs deleted file mode 100644 --- a/src/QuickSpec/Pruning/Twee.hs +++ /dev/null @@ -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)) diff --git a/src/QuickSpec/Pruning/Types.hs b/src/QuickSpec/Pruning/Types.hs deleted file mode 100644 --- a/src/QuickSpec/Pruning/Types.hs +++ /dev/null @@ -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)) diff --git a/src/QuickSpec/Pruning/UntypedTwee.hs b/src/QuickSpec/Pruning/UntypedTwee.hs deleted file mode 100644 --- a/src/QuickSpec/Pruning/UntypedTwee.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Term.hs b/src/QuickSpec/Term.hs deleted file mode 100644 --- a/src/QuickSpec/Term.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Terminal.hs b/src/QuickSpec/Terminal.hs deleted file mode 100644 --- a/src/QuickSpec/Terminal.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Testing.hs b/src/QuickSpec/Testing.hs deleted file mode 100644 --- a/src/QuickSpec/Testing.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Testing/DecisionTree.hs b/src/QuickSpec/Testing/DecisionTree.hs deleted file mode 100644 --- a/src/QuickSpec/Testing/DecisionTree.hs +++ /dev/null @@ -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) diff --git a/src/QuickSpec/Testing/QuickCheck.hs b/src/QuickSpec/Testing/QuickCheck.hs deleted file mode 100644 --- a/src/QuickSpec/Testing/QuickCheck.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Type.hs b/src/QuickSpec/Type.hs deleted file mode 100644 --- a/src/QuickSpec/Type.hs +++ /dev/null @@ -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 diff --git a/src/QuickSpec/Utils.hs b/src/QuickSpec/Utils.hs deleted file mode 100644 --- a/src/QuickSpec/Utils.hs +++ /dev/null @@ -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