quickspec 2 → 2.1

raw patch · 24 files changed

+1012/−461 lines, 24 filesdep +quickcheck-instancesdep +spoondep −reflectiondep ~twee-lib

Dependencies added: quickcheck-instances, spoon

Dependencies removed: reflection

Dependency ranges changed: twee-lib

Files

• examples/Curry.hs +9/−0
• examples/Lists.hs +1/−4
• examples/PrettyPrinting.hs +2/−2
• examples/PrettyPrintingModel.hs +9/−4
• examples/Sorted.hs +1/−4
• examples/Zip.hs +0/−1
• quickspec.cabal +6/−3
• src/QuickSpec.hs +165/−35
• src/QuickSpec/Explore.hs +57/−22
• src/QuickSpec/Explore/Conditionals.hs +7/−5
• src/QuickSpec/Explore/PartialApplication.hs +15/−9
• src/QuickSpec/Explore/Polymorphic.hs +27/−75
• src/QuickSpec/Haskell.hs +368/−173
• src/QuickSpec/Haskell/Resolve.hs +20/−14
• src/QuickSpec/Parse.hs +60/−0
• src/QuickSpec/Prop.hs +2/−1
• src/QuickSpec/Pruning/Twee.hs +1/−1
• src/QuickSpec/Pruning/Types.hs +5/−1
• src/QuickSpec/Pruning/UntypedTwee.hs +19/−9
• src/QuickSpec/Term.hs +46/−25
• src/QuickSpec/Terminal.hs +8/−0
• src/QuickSpec/Testing/QuickCheck.hs +20/−9
• src/QuickSpec/Type.hs +156/−40
• src/QuickSpec/Utils.hs +8/−24

@@ -0,0 +1,9 @@+import QuickSpec++main = quickSpec [+  con "curry" (curry :: ((A, B) -> C) -> A -> B -> C),+  con "fst" (fst :: (A, B) -> A),+  con "snd" (snd :: (A, B) -> B),+  con "id" (id :: A -> A),+  con "." ((.) :: (B -> C) -> (A -> B) -> A -> C),+  con "|" ((\f g x -> (f x, g x)) :: (A -> B) -> (A -> C) -> A -> (B, C))]

@@ -1,7 +1,6 @@ -- Some usual list functions. {-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-} import QuickSpec-import Data.List  main = quickSpec [   con "reverse" (reverse :: [A] -> [A]),@@ -12,6 +11,4 @@   con "concat" (concat :: [[A]] -> [A]),    -- Add some numeric functions to get more laws about length.-  background [-    con "0" (0 :: Int),-    con "+" ((+) :: Int -> Int -> Int) ] ]+  arith (Proxy :: Proxy Int) ]

@@ -2,6 +2,7 @@ -- Illustrates observational equality and using custom generators. -- See the QuickSpec paper for more details. {-# LANGUAGE DeriveDataTypeable, TypeOperators, StandaloneDeriving, TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}+import Prelude hiding ((<>)) import Control.Monad import Test.QuickCheck import QuickSpec@@ -65,6 +66,5 @@   con "<>" (<>),   con "$$" ($$), -  inst (Sub Dict :: () :- Observe Context Str Doc),-  inst (Sub Dict :: () :- Arbitrary Doc),+  monoTypeObserve (Proxy :: Proxy Doc),   defaultTo (Proxy :: Proxy Bool)]

@@ -2,6 +2,7 @@ -- Illustrates running QuickSpec on a progressively larger set of signatures. -- See the QuickSpec paper for more details. {-# LANGUAGE DeriveDataTypeable, TypeOperators #-}+import Prelude hiding ((<>)) import Control.Monad import Test.QuickCheck import QuickSpec@@ -43,7 +44,11 @@     con "0" (0 :: Int),     con "+" ((+) :: Int -> Int -> Int),     con "length" (length :: String -> Int) ],-  con "text" text,-  con "nest" nest,-  con "$$" ($$),-  con "<>" (<>) ]+  series [sig1, sig2]]+  where+    sig1 = [+      con "text" text,+      con "nest" nest,+      con "$$" ($$),+      con "<>" (<>) ]+    sig2 = [con "nesting" nesting]

@@ -9,10 +9,7 @@ sorted (x:y:xs) = x <= y && sorted (y:xs)  main = quickSpec [-  background [-    con ":" ((:) :: A -> [A] -> [A]),-    con "[]" ([] :: [A]) ],-+  lists `without` ["++"],   con "sort" (sort :: [Int] -> [Int]),   con "insert" (insert :: Int -> [Int] -> [Int]),   predicate "sorted" (sorted :: [Int] -> Bool) ]

@@ -10,7 +10,6 @@ main = quickSpec [   -- Explore bigger terms.   withMaxTermSize 8,-  withPruningDepth 10,   con "++" ((++) @ Int),   con "zip" (zip @ Int @ Int),   predicate "eqLen" (eqLen @ Int @ Int) ]

@@ -1,5 +1,5 @@ Name:                quickspec-Version:             2+Version:             2.1 Cabal-version:       >= 1.6 Build-type:          Simple @@ -51,6 +51,7 @@   examples/Arith.hs   examples/Bools.hs   examples/Composition.hs+  examples/Curry.hs   examples/Geometry.hs   examples/HugeLists.hs   examples/IntSet.hs@@ -82,6 +83,7 @@     QuickSpec.Explore.Terms     QuickSpec.Haskell     QuickSpec.Haskell.Resolve+    QuickSpec.Parse     QuickSpec.Prop     QuickSpec.Pruning     QuickSpec.Pruning.Background@@ -98,14 +100,15 @@    Build-depends:     QuickCheck >= 2.10,+    quickcheck-instances >= 0.3.15,     base >= 4 && < 5,     constraints,     containers,     data-lens-light >= 0.1.1,     dlist,     random,-    reflection,+    spoon,     template-haskell,     transformers,-    twee-lib >= 2.1.2,+    twee-lib == 2.1.5,     uglymemo

@@ -22,10 +22,12 @@ -- You must also declare those instances to QuickSpec, by including them in the -- signature. For monomorphic types you can do this using `monoType`: ----- > data T = ...--- > main = quickSpec [--- >   ...,--- >   `monoType` (Proxy :: Proxy T)]+-- @+-- data T = ...+-- main = quickSpec [+--   ...,+--   `monoType` (Proxy :: Proxy T)]+-- @ -- -- You can only declare monomorphic types with `monoType`. If you want to test -- your own polymorphic types, you must explicitly declare `Arbitrary` and `Ord`@@ -52,10 +54,16 @@ -- * @<https://github.com/nick8325/quickspec/tree/master/examples/Parsing.hs Parsing.hs>@: parser combinators. Demonstrates testing polymorphic datatypes and using observational equality. -- -- You can also find some larger case studies in our paper,--- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick--- specifications for the busy programmer>.+-- <http://www.cse.chalmers.se/~nicsma/papers/quickspec2.pdf Quick specifications for the busy programmer>. -{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, TypeOperators, MultiParamTypeClasses, FunctionalDependencies #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE RankNTypes #-} module QuickSpec(   -- * Running QuickSpec   quickSpec, Sig, Signature(..),@@ -66,23 +74,38 @@   A, B, C, D, E,    -- * Declaring types-  monoType, vars, monoTypeWithVars, inst, Observe(..),+  monoType, monoTypeObserve, vars, monoTypeWithVars, inst, Observe(..), +  -- * Standard signatures+  -- | The \"prelude\": a standard signature containing useful functions+  --   like '++', which can be used as background theory.+  lists, arith, funs, bools, prelude, without,+   -- * Exploring functions in series   background, series, +  -- * Including type class constraints (experimental, subject to change)+  type (==>), liftC, instanceOf,+   -- * Customising QuickSpec   withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,   withPruningDepth, withPruningTermSize, withFixedSeed,+  withInferInstanceTypes,    -- * Re-exported functionality-  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where+  Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary, -import QuickSpec.Haskell(Predicateable, TestCase, Names(..), Observe(..))+  -- * Advanced use+  quickSpecResult) where++import QuickSpec.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..)) 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 Data.Constraint@@ -90,32 +113,55 @@ 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 signature =-  Haskell.quickSpec (sig 0 Haskell.defaultConfig)-  where-    Sig sig = toSig signature+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)+ -- | A signature.-newtype Sig = Sig (Int -> Haskell.Config -> Haskell.Config)+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)-  Sig sig1 `mappend` Sig sig2 = Sig (\n -> sig2 n . sig1 n)+  mappend = (<>)  -- | A class of things that can be used as a QuickSpec signature. class Signature sig where   -- | Convert the thing to a signature.-  toSig :: sig -> Sig+  signature :: sig -> Sig  instance Signature Sig where-  toSig = id+  signature = id  instance Signature sig => Signature [sig] where-  toSig = mconcat . map toSig+  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:@@ -125,8 +171,27 @@ -- QuickSpec will then understand that the constant is really polymorphic. con :: Typeable a => String -> a -> Sig con name x =-  Sig (\n -> modL Haskell.lens_constants (appendAt n (Haskell.con name x)))+  Sig $ \ctx@(Context _ names) ->+    if name `elem` names then id else+      unSig (constant (Haskell.con name x)) ctx +constant :: Haskell.Constant -> Sig+constant 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,@@ -142,15 +207,13 @@ -- @ predicate :: ( Predicateable a              , Typeable a-             , Typeable (TestCase a))+             , Typeable (PredicateTestCase a))              => String -> a -> Sig predicate name x =-  Sig (\n -> modL Haskell.lens_predicates (appendAt n (Haskell.predicate name x)))--appendAt :: Int -> a -> [[a]] -> [[a]]-appendAt n x [] = appendAt n x [[]]-appendAt 0 x (xs:xss) = (xs ++ [x]):xss-appendAt n x (xs:xss) = xs:appendAt (n-1) x xss+  Sig $ \ctx@(Context _ names) ->+    if name `elem` names then id else+    let (insts, con) = Haskell.predicate name x in+      runSig [addInstances insts `mappend` constant con] ctx  -- | Declare a new monomorphic type. -- The type must implement `Ord` and `Arbitrary`.@@ -160,6 +223,16 @@     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 =@@ -183,9 +256,12 @@ inst = instFun  instFun :: Typeable a => a -> Sig-instFun x =-  Sig (\_ -> modL Haskell.lens_instances (`mappend` Haskell.inst x))+instFun x = addInstances (Haskell.inst x) +addInstances :: Haskell.Instances -> Sig+addInstances insts =+  Sig (\_ -> modL Haskell.lens_instances (`mappend` insts))+ -- | 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.@@ -202,11 +278,15 @@ -- >     con "0" (0 :: Int), -- >     con "+" ((+) :: Int -> Int -> Int) ] ] background :: Signature sig => sig -> Sig-background signature =-  Sig (\n -> sig (n+1))-  where-    Sig sig = toSig signature+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.@@ -226,9 +306,11 @@ -- >       con "++" ((++) :: [A] -> [A] -> [A]), -- >       con "length" (length :: [A] -> Int) ] series :: Signature sig => [sig] -> Sig-series = foldl op mempty . map toSig+series = foldr op mempty . map signature   where-    op sigs sig = toSig [background sigs, sig]+    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@@ -270,3 +352,51 @@ -- 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]

@@ -14,32 +14,56 @@ import Control.Monad.Trans.Class import Control.Monad.Trans.State.Strict import Text.Printf+import Data.Semigroup(Semigroup(..)) -moreTerms :: (Ord a, Apply (Term f), Sized f, Typed f) => Universe -> [f] -> (Term f -> a) -> [[Term f]] -> [Term f]-moreTerms univ funs measure tss =-  sortBy' measure $-    atomic +++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 <- uss !! i,-      u <- uss !! (n-i),-      Just v <- [tryApply (poly t) (poly u)],-      unPoly v `usefulForUniverse` univ ]-  where-    n = length tss-    atomic =-      [App f [] | f <- funs, size f == n] ++-      [Var (V typeVar 0) | n == 1]-    uss = tss ++ [atomic]+      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 measure, 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) =>+  (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 -> measure) ->   (Term fun -> testcase -> result) ->-  Int -> Universe -> [fun] -> m ()-quickSpec present measure eval maxSize univ funs = do+  Int -> Universe -> Enumerator (Term fun) -> m ()+quickSpec present eval maxSize univ enum = do   let     state0 = initialState univ (\t -> size t <= 5) eval @@ -47,7 +71,7 @@     loop m n tss = do       putStatus (printf "enumerating terms of size %d" m)       let-        ts = moreTerms univ funs measure tss+        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)@@ -59,6 +83,17 @@             Rejected _ -> return False       us <- map snd <$> filterM consider (zip [1 :: Int ..] ts)       clearStatus-      loop (m+1) n (tss ++ [us])+      loop (m+1) n (appendAt m us tss) -  evalStateT (loop 0 maxSize []) state0+  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

@@ -43,11 +43,13 @@       when res (considerConditionalising prop)       return res -conditionalsUniverse :: (Typed fun, Predicate fun) => [fun] -> Universe-conditionalsUniverse funs =+conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe+conditionalsUniverse tys funs =   universe $-    map Normal funs ++-    [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ]+    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) =>@@ -86,7 +88,7 @@   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 (Constructor f _) = pPrintPrec l p f <#> text "_con"   pPrintPrec l p (Normal f) = pPrintPrec l p f  instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where

@@ -1,6 +1,6 @@ -- Pruning support for partial application and the like. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-} module QuickSpec.Explore.PartialApplication where  import QuickSpec.Term@@ -17,7 +17,7 @@     -- The ($) operator, for oversaturated applications.     -- The type argument is the type of the first argument to ($).   | Apply Type-  deriving (Eq, Ord)+  deriving (Eq, Ord, Functor)  instance Sized f => Sized (PartiallyApplied f) where   size (Partial f _) = size f@@ -40,7 +40,7 @@   prettyArity (Apply _) = 1  instance Typed f => Typed (PartiallyApplied f) where-  typ (Apply ty) = Twee.build (Twee.app (Twee.fun Arrow) [ty, ty])+  typ (Apply ty) = arrowType [ty] ty   typ (Partial f _) = typ f   otherTypesDL (Apply _) = mempty   otherTypesDL (Partial f _) = otherTypesDL f@@ -61,6 +61,9 @@ 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) @@ -81,9 +84,12 @@       vs = map Var (zipWith V (typeArgs (typ f)) [0..])   background _ = [] -instance (Applicative f, Eval fun (Value f)) => Eval (PartiallyApplied fun) (Value f) where-  eval var (Partial f _) = eval var f-  eval _ (Apply ty) =-    fromJust $-      cast (Twee.build (Twee.app (Twee.fun Arrow) [ty, ty]))-        (toValue (pure (($) :: (A -> B) -> (A -> B))))+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))))

@@ -1,7 +1,16 @@ -- Theory exploration which handles polymorphism. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE TemplateHaskell, FlexibleContexts, GeneralizedNewtypeDeriving, FlexibleInstances, MultiParamTypeClasses, BangPatterns, UndecidableInstances, RankNTypes, GADTs, RecordWildCards #-}-module QuickSpec.Explore.Polymorphic(module QuickSpec.Explore.Polymorphic, Result(..)) where+{-# LANGUAGE TemplateHaskell #-}+{-# 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(..))@@ -20,14 +29,11 @@ import Control.Monad.Trans.Class import qualified Twee.Base as Twee import Control.Monad-import Data.Maybe import qualified Data.DList as DList  data Polymorphic testcase result fun norm =   Polymorphic {     pm_schemas :: Schemas testcase result (PolyFun fun) norm,-    pm_unifiable :: Map (Poly Type) ([Poly Type], [(Poly Type, Poly Type)]),-    pm_accepted :: Map (Poly Type) (Set (Term fun)),     pm_universe :: Universe }  data PolyFun fun =@@ -40,15 +46,11 @@ instance PrettyTerm fun => PrettyTerm (PolyFun fun) where   termStyle = termStyle . fun_specialised --- univ_inner: the type universe, with all type variables unified--- univ_root: the set of types allowed for partially applied functions, only at--- the root of a term-data Universe = Universe { univ_inner :: Set Type, univ_root :: Set Type }+-- The set of all types being explored+data Universe = Universe { univ_types :: Set Type }  makeLensAs ''Polymorphic   [("pm_schemas", "schemas"),-   ("pm_unifiable", "unifiable"),-   ("pm_accepted", "accepted"),    ("pm_universe", "univ")]  initialState ::@@ -59,8 +61,6 @@ initialState univ inst eval =   Polymorphic {     pm_schemas = Schemas.initialState (inst . fmap fun_specialised) (eval . fmap fun_specialised),-    pm_unifiable = Map.empty,-    pm_accepted = Map.empty,     pm_universe = univ }  polyFun :: Typed fun => fun -> PolyFun fun@@ -89,25 +89,13 @@   if not (t `inUniverse` univ) then     return (Accepted [])    else do-    let ty = polyTyp (poly t)-    addPolyType ty--    unif <- access unifiable-    let (here, there) = Map.findWithDefault undefined ty unif-    acc <- access accepted-    ress1 <--      concat <$>-      forM there (\(ty', mgu) ->-        forM (Set.toList (Map.findWithDefault undefined ty' acc)) (\u ->-          exploreNoMGU (u `at` mgu)))     res <- exploreNoMGU t-    ress2 <--      forM here (\mgu ->-        exploreNoMGU (t `at` mgu))-    return res { result_props = concatMap result_props (ress1 ++ [res] ++ ress2) }-    where-      t `at` ty =-        fromMaybe undefined (cast (unPoly ty) 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),@@ -116,11 +104,7 @@   StateT (Polymorphic testcase result fun norm) m (Result fun) exploreNoMGU t = do   univ <- access univ-  let ty = polyTyp (poly t)-  acc <- access accepted-  if (t `Set.member` Map.findWithDefault Set.empty ty acc ||-      not (t `inUniverse` univ)) then return (Rejected []) else do-    accepted %= Map.insertWith Set.union ty (Set.singleton t)+  if not (t `inUniverse` univ) then return (Rejected []) else do     schemas1 <- access schemas     (res, schemas2) <- unPolyM (runStateT (Schemas.explore (polyTerm t)) schemas1)     schemas ~= schemas2@@ -129,20 +113,6 @@     mapProps f (Accepted props) = Accepted (map f props)     mapProps f (Rejected props) = Rejected (map f props) -addPolyType :: Monad m => Poly Type -> StateT (Polymorphic testcase result fun norm) m ()-addPolyType ty = do-  unif <- access unifiable-  univ <- access univ-  unless (ty `Map.member` unif) $ do-    let-      tys = [(ty', mgu) | ty' <- Map.keys unif, Just mgu <- [polyMgu ty ty']]-      ok ty mgu = oneTypeVar ty /= mgu && oneTypeVar (unPoly mgu) `Set.member` univ_root univ-      here = [mgu | (_, mgu) <- tys, ok mgu ty]-      there = [(ty', mgu) | (ty', mgu) <- tys, ok mgu ty']-    key ty # unifiable ~= Just (here, there)-    forM_ there $ \(ty', _) ->-      sndLens # keyDefault ty' undefined # unifiable %= (there ++)- 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@@ -215,10 +185,8 @@   where     cs =       foldr intersection [Map.empty]-        (map (constrain (Set.toList univ_inner))-          (usort (DList.toList (termsDL prop) >>= properSubterms)) ++-         map (constrain (Set.toList univ_root))-          (usort (DList.toList (termsDL prop))))+        (map (constrain (Set.toList univ_types))+          (usort (DList.toList (termsDL prop) >>= subterms)))      constrain tys t =       usort [ Map.fromList (Twee.substToList sub) | u <- tys, Just sub <- [Twee.match (typ t) u] ]@@ -229,35 +197,19 @@     ok m1 m2 = and [ Map.lookup x m1 == Map.lookup x m2 | x <- Map.keys (Map.intersection m1 m2) ]  universe :: Typed a => [a] -> Universe-universe xs = Universe (Set.fromList base) (Set.fromList (withFunctions base))+universe xs = Universe (Set.fromList base)   where     -- The universe contains the type variable "a", the argument and     -- result type of every function (with all type variables unified), and all     -- subterms of these types     base = usort $ typeVar:concatMap (oneTypeVar . typs . typ) xs-    typs ty = (typeRes ty:typeArgs ty) >>= Twee.subterms--    -- We then add partial applications, according to the rule:-    -- if f : A1 -> ... -> An -> B is a function in the signature,-    -- and s(A1)...s(An), s(B) are in the universe where s is a substitution,-    -- then s(A1 -> ... -> An -> B) is in the universe, together with all subterms-    withFunctions tys =-      tys ++-      concat [func Twee.emptySubst (typ f) tys >>= Twee.subterms | f <- xs]--    func sub ty tys =-      filter (`elem` tys) [oneTypeVar (typeSubst sub ty)] ++-      [ arrowType [t'] u'-      | Just (t, u) <- [unpackArrow ty],-        t' <- tys,-        Just sub <- [Twee.matchIn sub t t'],-        u' <- func sub u tys ]+    typs ty = typeRes ty:typeArgs ty  inUniverse :: Typed fun => Term fun -> Universe -> Bool t `inUniverse` Universe{..} =-  and [oneTypeVar (typ u) `Set.member` univ_inner | u <- subterms t]+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- subterms t]  usefulForUniverse :: Typed fun => Term fun -> Universe -> Bool t `usefulForUniverse` Universe{..} =-  oneTypeVar (typ t) `Set.member` univ_root &&-  and [oneTypeVar (typ u) `Set.member` univ_inner | u <- properSubterms t]+  and [oneTypeVar (typ u) `Set.member` univ_types | u <- properSubterms t] &&+  oneTypeVar (typeRes (typ t)) `Set.member` univ_types

@@ -2,38 +2,56 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE ScopedTypeVariables, TypeOperators, GADTs, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, RecordWildCards, TemplateHaskell, UndecidableInstances, DefaultSignatures, FunctionalDependencies #-}+{-# LANGUAGE PatternGuards #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE TemplateHaskell #-}+{-# 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)-import Data.Constraint+import Data.Constraint hiding ((\\))+import Data.List import Data.Proxy-import qualified Twee.Base as B+import qualified Twee.Base as Twee import QuickSpec.Term import Data.Functor.Identity import Data.Maybe import Data.MemoUgly-import Test.QuickCheck.Gen-import Test.QuickCheck.Random-import System.Random+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 Data.Reflection hiding (D) import QuickSpec.Utils 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 =@@ -48,6 +66,7 @@     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,@@ -56,18 +75,27 @@       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]),@@ -97,15 +125,22 @@     inst (Sub Dict :: Ord A :- Eq A),     -- From Arbitrary to Gen     inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,-    inst $ \(dict :: Dict ClassA) -> return dict :: Gen (Dict ClassA),-    -- Observe-    inst (\(Dict :: Dict (Observe A B C)) -> Observe2 (do { env <- arbitrary; return (\x -> observe env (x :: C)) })),-    inst (Sub Dict :: (Arbitrary A, Observe B C D) :- Observe (A, B) C (A -> D)),-    inst (\(Dict :: Dict (Ord A)) -> Observe2 (return id) :: Observe2 A A),-    inst (\(Observe2 obsm :: Observe2 B C) (xm :: Gen A) ->-      Observe2 (do {x <- xm; obs <- obsm; return (\f -> obs (f x))}) :: Observe2 (A -> B) C),-    inst (\(obs :: Observe2 A B) -> Observe1 (toValue obs))]+    -- 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++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. --@@ -114,11 +149,11 @@ -- @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@. ----- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@.+-- The function `QuickSpec.monoTypeObserve` declares a monomorphic+-- type with an observation function. For polymorphic types, use+-- `QuickSpec.inst` to declare the `Observe` instance. ----- You must use `QuickSpec.inst` to add the @Observe@ instance to your signature.--- Note that `QuickSpec.monoType` requires an `Ord` instance, so this even applies for--- monomorphic types. Don't forget to add the `Arbitrary` instance too in that case.+-- For an example of using observational equality, see @<https://github.com/nick8325/quickspec/tree/master/examples/PrettyPrinting.hs PrettyPrinting.hs>@. class (Arbitrary test, Ord outcome) => Observe test outcome a | a -> test outcome where   -- | Make an observation on a value. Should satisfy the following law: if   -- @x /= y@, then there exists a value of @test@ such that @observe test x /= observe test y@.@@ -130,106 +165,118 @@ instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where   observe (x, obs) f = observe obs (f x) -data Observe2 a b where-  Observe2 :: Ord b => Gen (a -> b) -> Observe2 a b-  deriving Typeable-data Observe1 a = Observe1 (Value (Observe2 a)) deriving Typeable+-- 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)) --- | Declare that values of a particular type should be compared by observational equality.------ See @examples/PrettyPrinting.hs@ for an example.------ XXX mention what instances must be in scope--- XXX remove constraints etc--- observe :: Ord res => Gen env -> (env -> val -> res) -> Observe val res--- observe gen f =---   Observe (do { env <- gen; return (\x -> f env x) })-  +observeOrd :: Ord a => ObserveData a a+observeOrd = ObserveData (\() x -> x) --- data SomeObserve a = forall args res. (Ord res, Arbitrary args) => SomeObserve (a -> args -> res) deriving Typeable+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))] --- | Declare what variable names you would like to use for values of a particular type. See also `baseTypeNames`.+-- 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-    (x:_) -> ofValue getNames x-    [] -> error "don't know how to name variables"--arbitraryVal :: Type -> Instances -> Gen (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy))-arbitraryVal def insts =-  MkGen $ \g n ->-    let (g1, g2) = split g in-    (memo $ \(V ty x) ->-       case genType ty of-         Nothing ->-           fromJust $ cast (defaultTo def ty) (toValue (Nothing :: Maybe A))-         Just gen ->-           forValue gen $ \gen ->-             Just (unGen (coarbitrary x gen) g1 n),-     ordyVal g2 n)-  where-    genType :: Type -> Maybe (Value Gen)-    genType = memo $ \ty ->-      case findInstance insts (defaultTo def ty) of-        [] -> Nothing-        (gen:_) ->-          Just (mapValue (coarbitrary ty) gen)--    ordyVal :: QCGen -> Int -> Value Identity -> Maybe (Value Ordy)-    ordyVal g n x =-      let ty = defaultTo def (typ x) in-      case ordyTy ty of-        Nothing -> Nothing-        Just f -> Just (unGen f g n x)--    ordyTy :: Type -> Maybe (Gen (Value Identity -> Value Ordy))-    ordyTy = memo $ \ty ->-      case findInstance insts ty :: [Value Observe1] of-        [] -> Nothing-        (val:_) ->-          case unwrap val of-            Observe1 val `In` w1 ->-              case unwrap val of-                Observe2 obs `In` w2 ->-                  Just $-                    MkGen $ \g n ->-                      let observe = unGen obs g n in-                      \x -> wrap w2 (Ordy (observe (runIdentity (reunwrap w1 x))))+    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 =-    compare (typ x) (typ y) `mappend`     case unwrap x of       Ordy xv `In` w ->         let Ordy yv = reunwrap w y in         compare xv yv -evalHaskell :: (Given Type, Typed f, PrettyTerm f, Eval f (Value Maybe)) => (Var -> Value Maybe, Value Identity -> Maybe (Value Ordy)) -> Term f -> Either (Value Ordy) (Term f)-evalHaskell (env, obs) t =-  case unwrap (eval env t) of-    Nothing `In` _ -> Right t-    Just val `In` w ->-      case obs (wrap w (Identity val)) of-        Nothing -> Right t-        Just ordy -> Left ordy+-- | 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 } @@ -271,8 +318,12 @@           | 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@@ -282,9 +333,24 @@   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 = typ . con_value+  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@@ -295,6 +361,8 @@       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@@ -315,39 +383,35 @@ instance Predicate Constant where   classify = con_classify -instance (Given Type, Applicative f) => Eval Constant (Value f) where-  eval _ = mapValue (pure . runIdentity) . con_value+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-  uncrry :: a -> TestCase a -> Bool+  -- 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, TestCase (a -> b) ~ (a, TestCase b)) => Predicateable (a -> b) where+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 --- Foldr over functions-type family (Foldr f b fun) :: * where-  Foldr f def (a -> b) = f a (Foldr f def b)-  Foldr f def b        = def---- 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 TestCase a = Foldr (,) () a- data TestCaseWrapped (t :: Symbol) a = TestCaseWrapped { unTestCaseWrapped :: a }  -- A `suchThat` generator for a predicate-genSuchThat :: (Predicateable a, Arbitrary (TestCase a)) => a -> Gen (TestCaseWrapped x (TestCase a))+genSuchThat :: (Predicateable a, Arbitrary (PredicateTestCase a)) => a -> Gen (TestCaseWrapped x (PredicateTestCase a)) genSuchThat p = TestCaseWrapped <$> arbitrary `suchThat` uncrry p -data PredRep = PredRep { predInstances :: Instances-                       , predCon :: Constant-                       , predCons :: [Constant] }- true :: Constant true = con "True" True @@ -358,44 +422,65 @@ -- The predicate should have type @... -> Bool@. predicate :: forall a. ( Predicateable a              , Typeable a-             , Typeable (TestCase a))-             => String -> a -> PredRep+             , Typeable (PredicateTestCase a))+             => String -> a -> (Instances, Constant) predicate name pred =-  case someSymbolVal name of-    SomeSymbol (_ :: Proxy sym) ->-      let-        instances =-          inst (\(dict :: Dict (Arbitrary (TestCase a))) -> (withDict dict genSuchThat) pred :: Gen (TestCaseWrapped sym (TestCase a)))-          `mappend`-          inst (Names [name ++ "_var"] :: Names (TestCaseWrapped sym (TestCase a)))+  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)))) -        conPred = (con name pred) { con_classify = Predicate conSels ty (App true []) }-        conSels = [ (constant' (name ++ "_" ++ show i) (select i)) { con_classify = Selector i conPred ty, con_size = 0 } | i <- [0..typeArity (typeOf pred)-1] ]+    -- 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 -        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)+    instances =+      mconcat $ map (valueInst . addName)+        [toValue (Identity inst1), toValue (Identity inst2)] -        ty = typeRep (Proxy :: Proxy (TestCaseWrapped sym (TestCase a)))-      in-        PredRep instances conPred (conPred:conSels)+    inst1 :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (TestCaseWrapped SymA (PredicateTestCase a))+    inst1 Dict = genSuchThat pred +    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)+ data Config =   Config {     cfg_quickCheck :: QuickCheck.Config,     cfg_twee :: Twee.Config,     cfg_max_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_predicates :: [[PredRep]],-    cfg_default_to :: Type }+    cfg_default_to :: Type,+    cfg_infer_instance_types :: Bool+    }  makeLensAs ''Config   [("cfg_quickCheck", "lens_quickCheck"),@@ -403,68 +488,178 @@    ("cfg_max_size", "lens_max_size"),    ("cfg_instances", "lens_instances"),    ("cfg_constants", "lens_constants"),-   ("cfg_predicates", "lens_predicates"),-   ("cfg_default_to", "lens_default_to")]+   ("cfg_default_to", "lens_default_to"),+   ("cfg_infer_instance_types", "lens_infer_instance_types")]  defaultConfig :: Config defaultConfig =   Config {-    cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 20, QuickCheck.cfg_fixed_seed = Nothing },+    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_instances = mempty,     cfg_constants = [],-    cfg_predicates = [],-    cfg_default_to = typeRep (Proxy :: Proxy Int) }+    cfg_default_to = typeRep (Proxy :: Proxy Int),+    cfg_infer_instance_types = False } -quickSpec :: Config -> IO ()-quickSpec Config{..} = give cfg_default_to $ do+-- 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:f cfg_constants ++ f (map (concatMap predCons) cfg_predicates)+    constantsOf f = true:f cfg_constants ++ concatMap selectors (f cfg_constants)     constants = constantsOf concat-    univ = conditionalsUniverse constants-    instances = mconcat (cfg_instances:map predInstances (concat cfg_predicates) ++ [baseInstances])+    +    univ = conditionalsUniverse (instanceTypes instances cfg) constants+    instances = cfg_instances `mappend` baseInstances -    present prop = do-      n :: Int <- get-      put (n+1)-      putLine (printf "%3d. %s" n (show (prettyProp (names instances) (conditionalise prop) <+> maybeType prop)))+    eval = evalHaskell cfg_default_to instances +    present funs prop = do+      norm <- normaliser+      let prop' = makeDefinition funs (ac norm (conditionalise prop))+      (n :: Int, props) <- get+      put (n+1, prop':props)+      putLine $+        printf "%3d. %s" n $ show $+          prettyProp (names instances) prop' <+> maybeType prop++    -- 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 -    mainOf f g = do-      printConstants (f cfg_constants ++ f (map (map predCon) cfg_predicates))-      putLine ""-      putLine "== Laws =="-      QuickSpec.Explore.quickSpec present measure (flip evalHaskell) cfg_max_size univ-        [ Partial fun 0 | fun <- constantsOf g ]-      putLine ""+    -- 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) ] -    main = mapM_ round [1..rounds]+    enumerator cons =+      sortTerms measure $+      filterEnumerator (all constraintsOk . funs) $+      enumerateConstants atomic `mappend` enumerateApplications       where-        round n = mainOf (concat . take 1 . drop (rounds-n)) (concat . drop (rounds-n))-        rounds = max (length cfg_constants) (length cfg_predicates)+        atomic = cons ++ [Var (V typeVar 0)] +    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 univ+        (enumerator [partial fun | fun <- constantsOf g])+      when (n > 0) $ do+        putLine ""++    main = 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 (arbitraryVal cfg_default_to instances) evalHaskell $+    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) $-    flip evalStateT 1 $-      main--printConstants :: MonadTerminal m => [Constant] -> m ()-printConstants cs = do-  putLine "== Functions =="-  let-    decls = [ (show (pPrint (App (Partial c 0) [])), pPrintType (typ c)) | c <- cs ]-    maxWidth = maximum (0:map (length . fst) decls)-    pad xs = replicate (maxWidth - length xs) ' ' ++ xs-    pPrintDecl (name, ty) =-      hang (text (pad name) <+> text "::") 2 ty--  mapM_ (putLine . show . pPrintDecl) decls+    fmap (reverse . snd) $ flip execStateT (1, []) main

@@ -14,7 +14,7 @@  {-# OPTIONS_HADDOCK hide #-} {-# LANGUAGE RankNTypes, ScopedTypeVariables #-}-module QuickSpec.Haskell.Resolve(Instances, inst, findInstance, findValue) where+module QuickSpec.Haskell.Resolve(Instances(..), inst, valueInst, findInstance, findValue) where  import Twee.Base import QuickSpec.Type@@ -23,6 +23,7 @@ import Data.Maybe import Data.Proxy import Control.Monad+import Data.Semigroup(Semigroup(..))  -- A set of instances. data Instances =@@ -39,22 +40,27 @@   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 []-  x `mappend` y = makeInstances (is_instances x ++ is_instances y)+  mappend = (<>)  -- Create a single instance. inst :: Typeable a => a -> Instances-inst x = instValue (toPolyValue x)+inst x = valueInst (toValue (Identity x))++valueInst :: Value Identity -> Instances+valueInst x = polyInst (poly x)   where-    instValue :: Poly (Value Identity) -> Instances-    instValue x =+    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)) ->-          instValue (apply uncur x)+          polyInst (apply uncur x)         App (F Arrow) _ ->           makeInstances [x]         -- A plain old value x (not a function) turns into \() -> x.@@ -66,14 +72,14 @@  -- Construct a value of a particular type. -- If the type is polymorphic, may return an instance of it.-findValue :: Instances -> Type -> [Value Identity]-findValue = is_find+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 -> [Value f]+findInstance :: forall f. Typeable f => Instances -> Type -> Maybe (Value f) findInstance insts ty =-  map (unwrapFunctor runIdentity) (findValue insts ty')+  unwrapFunctor runIdentity <$> findValue insts ty'   where     ty' = typeRep (Proxy :: Proxy f) `applyType` ty @@ -89,12 +95,12 @@ find_ _ (App (F unit) Empty)   | unit == tyCon (Proxy :: Proxy ()) =     return (toValue (Identity ()))-find_ res (App (F pair) (Cons ty1 (Cons ty2 Empty)))+find_ insts (App (F pair) (Cons ty1 (Cons ty2 Empty)))   | pair == tyCon (Proxy :: Proxy (,)) = do-    x <- findValue res ty1+    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 <- findValue res (subst sub ty2)+    y <- is_find insts (subst sub ty2)     sub <- maybeToList (match ty2 (typ y))     return (pairValues (liftM2 (,)) (typeSubst sub x) y) find_ insts ty = do@@ -106,6 +112,6 @@   fun <- return (typeSubst sub fun)   arg <- return (typeSubst sub arg)   -- Find an argument for that function and apply the function.-  val <- findValue insts arg+  val <- is_find insts arg   sub <- maybeToList (match arg (typ val))   return (apply (typeSubst sub fun) val)

@@ -0,0 +1,60 @@+-- | 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)

@@ -72,7 +72,8 @@     | isTrue y = pPrint x     | otherwise = pPrint x <+> text "=" <+> pPrint y     where-      isTrue x = show (pPrint x) `elem` ["true", "True"]+      -- XXX this is a hack+      isTrue x = show (pPrint x) == "True"  infix 4 === (===) :: a -> a -> Prop a

@@ -21,6 +21,6 @@ instance MonadTrans (Pruner fun) where   lift = Pruner . lift . lift . lift -run :: Monad m => Config -> Pruner fun m a -> m a+run :: (Sized fun, Monad m) => Config -> Pruner fun m a -> m a run config (Pruner x) =   Untyped.run config (Types.run (Background.run x))

@@ -13,6 +13,7 @@ import QuickSpec.Terminal import Control.Monad.IO.Class import Control.Monad.Trans.Class+import qualified Twee.Base as Twee  data Tagged fun =     Func fun@@ -27,9 +28,12 @@   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 "]"+  pPrint (Tag ty) = text "tag[" <#> pPrint ty <#> text "]"  instance PrettyTerm fun => PrettyTerm (Tagged fun) where   termStyle (Func f) = termStyle f

@@ -34,27 +34,37 @@   [("cfg_max_term_size", "lens_max_term_size"),    ("cfg_max_cp_depth", "lens_max_cp_depth")] -instance (Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Sized fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where+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 (StateT (State (Extended 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 :: Monad m => Config -> Pruner fun m a -> m a+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_max_term_size = cfg_max_term_size,+        Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),         Twee.cfg_max_cp_depth = cfg_max_cp_depth } -instance (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>+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++instance (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun, Monad m) =>   MonadPruner (Term fun) (Term fun) (Pruner fun m) where   normaliser = Pruner $ do     state <- lift get@@ -77,20 +87,20 @@   add _ =     error "twee pruner doesn't support non-unit equalities" -normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>+normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>   State (Extended fun) -> Term fun -> Term fun normaliseTwee state t =   fromTwee $     result (normaliseTerm state (simplifyTerm state (skolemise t))) -normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>+normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>   State (Extended fun) -> Term fun -> Set (Term fun) normalFormsTwee state t =   Set.map fromTwee $     Set.map result (normalForms state (skolemise t)) -addTwee :: (Ord fun, Typeable fun, Arity fun, Sized fun, PrettyTerm fun, EqualsBonus fun) =>-  Twee.Config -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun)+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

@@ -1,5 +1,6 @@--- Typed terms.-{-# OPTIONS_HADDOCK hide #-}+-- | 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 @@ -10,15 +11,16 @@ import Test.QuickCheck(CoArbitrary) import Data.DList(DList) import qualified Data.DList as DList-import Twee.Base(Sized(..), Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)+import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint) import Twee.Pretty import qualified Data.Map.Strict as Map import Data.List-import Data.Reflection +-- | 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) @@ -27,8 +29,11 @@   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@@ -40,55 +45,73 @@   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)+  --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) -subterms, properSubterms :: Term f -> [Term f]+-- | 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 _ = [] --- Introduces variables in a canonical order.--- Also makes sure that variables of different types have different numbers+-- | 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@@ -97,18 +120,15 @@         [(x, Var (V ty n))         | (x@(V ty _), n) <- zip (nub (vars t)) [0..]] -class Eval term val where-  eval :: (Var -> val) -> term -> val--instance (Typed fun, Given Type, Apply a, Eval fun a) => Eval (Term fun) a where-  eval env = evaluateTerm (eval env) env--evaluateTerm :: (Typed fun, Given Type, Apply a) => (fun -> a) -> (Var -> a) -> Term fun -> a-evaluateTerm fun var = eval+-- | 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) =-      foldl apply (fun (defaultTo given f)) (map eval ts)+    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@@ -125,10 +145,11 @@       tsub (App f ts) =         App (typeSubst_ sub f) (map tsub ts) --- A standard term ordering - size, skeleton, generality.+-- | A standard term ordering - size, skeleton, generality. -- Satisfies the property: -- if measure (schema t) < measure (schema u) then t < u. type Measure f = (Int, Int, MeasureFuns f, Int, [Var])+-- | Compute the term ordering for a term. measure :: Sized f => Term f -> Measure f measure t =   (size t, -length (vars t), MeasureFuns (skel t),@@ -137,12 +158,14 @@     skel (Var (V ty _)) = Var (V ty 0)     skel (App f ts) = App f (map skel 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 (Var x) (Var y) = compare x y compareFuns Var{} App{} = LT@@ -152,14 +175,12 @@   compare (map MeasureFuns ts) (map MeasureFuns us)  ------------------------------------------------------------------------- Data types a la carte-ish.+-- * 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 (Eval fun1 a, Eval fun2 a) => Eval (fun1 :+: fun2) a where-  eval env (Inl x) = eval env x-  eval env (Inr x) = eval env x  instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where   size (Inl x) = size x

@@ -9,9 +9,13 @@ 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 @@ -34,6 +38,10 @@   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

@@ -4,6 +4,7 @@ module QuickSpec.Testing.QuickCheck where  import QuickSpec.Testing+import QuickSpec.Pruning import QuickSpec.Prop import Test.QuickCheck import Test.QuickCheck.Gen@@ -37,7 +38,7 @@  newtype Tester testcase term result m a =   Tester (ReaderT (Environment testcase term result) m a)-  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal)+  deriving (Functor, Applicative, Monad, MonadIO, MonadTerminal, MonadPruner term' res')  instance MonadTrans (Tester testcase term result) where   lift = Tester . lift@@ -50,21 +51,31 @@   let     seeds = unfoldr (Just . split) seed     n = cfg_num_tests-    k = cfg_max_test_size-    -- Divide tests equally between all sizes.-    -- There are n total tests of k+1 different sizes.-    -- If it doesn't divide equally, the biggest size gets the-    -- left-overs.+    k = max 1 cfg_max_test_size+    bias = 3+    cfg_max_test_size = 100+    -- Bias tests towards smaller sizes.+    -- We do this by distributing the cube of the size uniformly.     sizes =-      concat [replicate (n `div` (k+1)) i | i <- [0..k-1]] ++-      replicate (n `divRoundUp` (k+1)) k-    m `divRoundUp` n = (m-1) `div` n + 1+      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 (MonadTerminal m, Eq result) => MonadTester testcase term (Tester testcase term result m) where   test prop =

@@ -1,26 +1,28 @@+-- | This module is internal to QuickSpec.+-- -- Polymorphic types and dynamic values.-{-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE DeriveDataTypeable, ScopedTypeVariables, EmptyDataDecls, TypeSynonymInstances, FlexibleInstances, GeneralizedNewtypeDeriving, Rank2Types, ExistentialQuantification, PolyKinds, TypeFamilies, FlexibleContexts, StandaloneDeriving, PatternGuards, MultiParamTypeClasses, ConstraintKinds, DataKinds #-}+{-# 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.+  -- * Types   Typeable,-  Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, SymA, typeVar, isTypeVar,-  typeOf, typeRep, applyType, fromTypeRep,-  arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity, oneTypeVar, defaultTo, skolemiseTypeVars,-  isDictionary, getDictionary, pPrintType,-  -- Things that have types.-  Typed(..), typeSubst, typesDL, tyVars, cast,+  Type, TyCon(..), tyCon, fromTyCon, A, B, C, D, E, ClassA, ClassB, ClassC, ClassD, ClassE, ClassF, SymA, typeVar, isTypeVar,+  typeOf, typeRep, typeFromTyCon, applyType, fromTypeRep,+  arrowType, unpackArrow, typeArgs, typeRes, typeDrop, typeArity,+  isDictionary, getDictionary, splitConstrainedType, dictArity, pPrintType,+  -- * Things that have types+  Typed(..), typeSubst, typesDL, tyVars, cast, matchType,   TypeView(..),   Apply(..), apply, canApply,-  -- Polymorphic types.+  oneTypeVar, defaultTo, skolemiseTypeVars,+  -- * Polymorphic types   canonicaliseType,-  Poly, toPolyValue, poly, unPoly, polyTyp, polyMap, polyRename, polyApply, polyPair, polyList, polyMgu,-  -- Dynamic values.-  Value, toValue, fromValue,-  Unwrapped(..), unwrap, Wrapper(..),-  mapValue, forValue, ofValue, withValue, pairValues, wrapFunctor, unwrapFunctor) where+  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)@@ -35,11 +37,21 @@ import Data.Proxy import Data.List import Data.Char+import Data.Functor.Identity --- A (possibly polymorphic) type.+-- | A (possibly polymorphic) type. type Type = Term TyCon -data TyCon = Arrow | String String | TyCon Ty.TyCon deriving (Eq, Ord, Show)+-- | 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 "->"@@ -84,9 +96,13 @@ 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),@@ -99,45 +115,65 @@    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]) +-- | 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))) =@@ -145,20 +181,26 @@ 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 =@@ -167,11 +209,13 @@     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 (,))@@ -181,17 +225,31 @@ 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@@ -202,27 +260,36 @@   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 = pPrint . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise+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 --- Things with types.+-- | A class for things that have a type. class Typed a where-  -- The type.+  -- | The type.   typ :: a -> Type-  -- Any other types that may appear in subterms etc-  -- (enough at least to collect all type variables and type constructors).+  -- | 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.+  -- | 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 --- Using the normal term machinery on types.+-- | 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@@ -231,22 +298,39 @@ 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) --- Typed things that support function application.+-- | 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.+  -- | 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 =@@ -257,6 +341,7 @@         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) @@ -290,38 +375,47 @@   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+-- | 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) -polyMap :: (Typed a, Typed b) => (a -> b) -> Poly a -> Poly b-polyMap f (Poly x) = poly (f 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)@@ -340,10 +434,13 @@     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.+-- | Dynamic values inside an applicative functor.+--+-- For example, a value of type @Value Maybe@ represents a @Maybe something@. data Value f =   Value {     valueType :: Type,@@ -358,9 +455,11 @@ 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))@@ -374,14 +473,7 @@     ty <- tryApply (typ f) (typ x)     return (Value ty (fromAny (value f) <*> value x)) --- Unwrap a value to get at the thing inside, while still being able--- to wrap it up again.-data Unwrapped f = forall a. f a `In` Wrapper a-data Wrapper a =-  Wrapper {-    wrap :: forall g. g a -> Value g,-    reunwrap :: forall g. Value g -> g a }-+-- | Unwrap a value to get at the thing inside, with an existential type. unwrap :: Value f -> Unwrapped f unwrap x =   value x `In`@@ -392,22 +484,40 @@         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`@@ -440,3 +550,9 @@     _ -> 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

@@ -5,6 +5,7 @@  import Control.Arrow((&&&)) import Control.Exception+import Control.Spoon import Data.List(groupBy, sortBy) #if !MIN_VERSION_base(4,8,0) import Data.Monoid@@ -84,30 +85,8 @@     (hSetBuffering stdout buf)     x -newtype Max a = Max { getMax :: Maybe a }--getMaxWith :: Ord a => a -> Max a -> a-getMaxWith x (Max (Just y)) = x `max` y-getMaxWith x (Max Nothing)  = x--instance Ord a => Monoid (Max a) where-  mempty = Max Nothing-  Max (Just x) `mappend` y = Max (Just (getMaxWith x y))-  Max Nothing  `mappend` y = y--newtype Min a = Min { getMin :: Maybe a }--getMinWith :: Ord a => a -> Min a -> a-getMinWith x (Min (Just y)) = x `min` y-getMinWith x (Min Nothing)  = x--minimumBy :: (a -> a -> Bool) -> [a] -> a-minimumBy f = foldr1 (\x y -> if f x y then x else y)--instance Ord a => Monoid (Min a) where-  mempty = Min Nothing-  Min (Just x) `mappend` y = Min (Just (getMinWith x y))-  Min Nothing  `mappend` y = y+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) })@@ -120,3 +99,8 @@   | 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