packages feed

quickspec 2.1.2 → 2.1.3

raw patch · 17 files changed

+408/−213 lines, 17 files

Files

examples/HugeLists.hs view
@@ -1,7 +1,7 @@ -- A stress test using lots and lots of list functions. {-# LANGUAGE ScopedTypeVariables, ConstraintKinds, RankNTypes, ConstraintKinds, FlexibleContexts #-} import QuickSpec-import QuickSpec.Utils+import QuickSpec.Internal.Utils import Data.List import Control.Monad
examples/IntSet.hs view
@@ -6,6 +6,7 @@  main = quickSpec [   monoType (Proxy :: Proxy IntSet),+  withMaxTests 10000,    series [sig1, sig2, sig3]]   where
quickspec.cabal view
@@ -1,6 +1,6 @@ Name:                quickspec-Version:             2.1.2-Cabal-version:       >= 1.6+Version:             2.1.3+Cabal-version:       >= 1.10 Build-type:          Simple  Homepage:            https://github.com/nick8325/quickspec@@ -71,6 +71,7 @@   branch:   master  library+  default-language: Haskell2010   ghc-options: -W   hs-source-dirs: src   Exposed-modules:@@ -111,5 +112,5 @@     spoon,     template-haskell,     transformers,-    twee-lib == 2.1.5,+    twee-lib == 2.2,     uglymemo
src/QuickSpec.hs view
@@ -74,7 +74,12 @@   A, B, C, D, E,    -- * Declaring types-  monoType, monoTypeObserve, vars, monoTypeWithVars, inst, Observe(..),+  monoType, monoTypeObserve, Observe(..), inst,+  vars, monoTypeWithVars, monoTypeObserveWithVars,+  variableUse, VariableUse(..),+  +  -- * Declaring types: @TypeApplication@-friendly variants+  mono, monoObserve, monoVars, monoObserveVars,    -- * Standard signatures   -- | The \"prelude\": a standard signature containing useful functions@@ -90,14 +95,18 @@   -- * Customising QuickSpec   withMaxTermSize, withMaxTests, withMaxTestSize, defaultTo,   withPruningDepth, withPruningTermSize, withFixedSeed,-  withInferInstanceTypes,+  withInferInstanceTypes, withPrintStyle, PrintStyle(..), +  -- * Integrating with QuickCheck+  (=~=),+   -- * Re-exported functionality   Typeable, (:-)(..), Dict(..), Proxy(..), Arbitrary) where  import QuickSpec.Internal-import QuickSpec.Internal.Haskell(Observe(..))+import QuickSpec.Internal.Haskell(Observe(..), PrintStyle(..), (=~=)) import QuickSpec.Internal.Type(A, B, C, D, E)+import QuickSpec.Internal.Explore.Schemas(VariableUse(..)) import Data.Typeable import Data.Constraint import Test.QuickCheck
src/QuickSpec/Internal.hs view
@@ -8,15 +8,17 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE TypeApplications #-} module QuickSpec.Internal where -import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..))+import QuickSpec.Internal.Haskell(Predicateable, PredicateTestCase, Names(..), Observe(..), Use(..)) import qualified QuickSpec.Internal.Haskell as Haskell import qualified QuickSpec.Internal.Haskell.Resolve as Haskell import qualified QuickSpec.Internal.Testing.QuickCheck as QuickCheck import qualified QuickSpec.Internal.Pruning.UntypedTwee as Twee import QuickSpec.Internal.Prop import QuickSpec.Internal.Term(Term)+import QuickSpec.Internal.Explore.Schemas(VariableUse(..)) import Test.QuickCheck import Test.QuickCheck.Random import Data.Constraint@@ -156,6 +158,16 @@     inst (Sub Dict :: () :- Ord a),     inst (Sub Dict :: () :- Arbitrary a)] +-- | Like 'monoType', but designed to be used with TypeApplications directly.+--+-- For example, you can add 'Foo' to your signature via:+--+-- @+-- `mono` @Foo+-- @+mono :: forall a. (Ord a, Arbitrary a, Typeable a) => Sig+mono = monoType (Proxy @a)+ -- | Declare a new monomorphic type using observational equivalence. -- The type must implement `Observe` and `Arbitrary`. monoTypeObserve :: forall proxy test outcome a.@@ -166,16 +178,63 @@     inst (Sub Dict :: () :- Observe test outcome a),     inst (Sub Dict :: () :- Arbitrary a)] +-- | Like 'monoTypeObserve', but designed to be used with TypeApplications directly.+--+-- For example, you can add 'Foo' to your signature via:+--+-- @+-- `monoObserve` @Foo+-- @+monoObserve :: forall a test outcome.+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>+  Sig+monoObserve = monoTypeObserve (Proxy @a)++-- | Declare a new monomorphic type using observational equivalence, saying how you want variables of that type to be named.+monoTypeObserveWithVars :: forall proxy test outcome a.+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>+  [String] -> proxy a -> Sig+monoTypeObserveWithVars xs proxy =+  monoTypeObserve proxy `mappend` vars xs proxy++-- | Like 'monoTypeObserveWithVars', but designed to be used with TypeApplications directly.+--+-- For example, you can add 'Foo' to your signature via:+--+-- @+-- `monoObserveVars` @Foo ["foo"]+-- @+monoObserveVars :: forall a test outcome.+  (Observe test outcome a, Arbitrary test, Ord outcome, Arbitrary a, Typeable test, Typeable outcome, Typeable a) =>+  [String] -> Sig+monoObserveVars xs = monoTypeObserveWithVars xs (Proxy @a)+ -- | Declare a new monomorphic type, saying how you want variables of that type to be named. monoTypeWithVars :: forall proxy a. (Ord a, Arbitrary a, Typeable a) => [String] -> proxy a -> Sig monoTypeWithVars xs proxy =   monoType proxy `mappend` vars xs proxy +-- | Like 'monoTypeWithVars' designed to be used with TypeApplications directly.+--+-- For example, you can add 'Foo' to your signature via:+--+-- @+-- `monoVars` @Foo ["foo"]+-- @+monoVars :: forall a. (Ord a, Arbitrary a, Typeable a) => [String] -> Sig+monoVars xs = monoTypeWithVars xs (Proxy @a)+ -- | Customize how variables of a particular type are named. vars :: forall proxy a. Typeable a => [String] -> proxy a -> Sig vars xs _ = instFun (Names xs :: Names a) +-- | Constrain how variables of a particular type may occur in a term.+-- The default value is @'UpTo' 4@.+variableUse :: forall proxy a. Typeable a => VariableUse -> proxy a -> Sig+variableUse x _ = instFun (Use x :: Use a)+ -- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and+-- | Declare a typeclass instance. QuickSpec needs to have an `Ord` and -- `Arbitrary` instance for each type you want it to test. -- -- For example, if you are testing @`Data.Map.Map` k v@, you will need to add@@ -235,7 +294,7 @@ -- -- Here is an example which first tests @0@ and @+@ and then adds @++@ and @length@: ----- > main = quickSpec [sig1, sig2]+-- > main = quickSpec (series [sig1, sig2]) -- >   where -- >     sig1 = [ -- >       con "0" (0 :: Int),@@ -271,6 +330,13 @@ -- | Set which type polymorphic terms are tested at. defaultTo :: Typeable a => proxy a -> Sig defaultTo proxy = Sig (\_ -> setL Haskell.lens_default_to (typeRep proxy))++-- | Set how QuickSpec should display its discovered equations (default: 'ForHumans').+--+-- If you'd instead like to turn QuickSpec's output into QuickCheck tests, set+-- this to 'ForQuickCheck'.+withPrintStyle :: Haskell.PrintStyle -> Sig+withPrintStyle style = Sig (\_ -> setL Haskell.lens_print_style style)  -- | Set how hard QuickSpec tries to filter out redundant equations (default: no limit). --
src/QuickSpec/Internal/Explore.hs view
@@ -1,5 +1,5 @@ {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleContexts, PatternGuards #-} module QuickSpec.Internal.Explore where  import QuickSpec.Internal.Explore.Polymorphic@@ -15,6 +15,7 @@ import Control.Monad.Trans.State.Strict import Text.Printf import Data.Semigroup(Semigroup(..))+import Data.List  newtype Enumerator a = Enumerator { enumerate :: Int -> [[a]] -> [a] } @@ -62,10 +63,10 @@   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>   (Prop (Term fun) -> m ()) ->   (Term fun -> testcase -> result) ->-  Int -> Int -> (Type -> Bool) -> Universe -> Enumerator (Term fun) -> m ()-quickSpec present eval maxSize maxCommutativeSize singleUse univ enum = do+  Int -> Int -> (Type -> VariableUse) -> Universe -> Enumerator (Term fun) -> m ()+quickSpec present eval maxSize maxCommutativeSize use univ enum = do   let-    state0 = initialState singleUse univ (\t -> size t <= maxCommutativeSize) eval+    state0 = initialState use univ (\t -> size t <= maxCommutativeSize) eval      loop m n _ | m > n = return ()     loop m n tss = do@@ -87,6 +88,11 @@    evalStateT (loop 0 maxSize (repeat [])) state0 +----------------------------------------------------------------------+-- Functions that are not really to do with theory exploration,+-- but are useful for printing the output nicely.+----------------------------------------------------------------------+ pPrintSignature :: (Pretty a, Typed a) => [a] -> Doc pPrintSignature funs =   text "== Functions ==" $$@@ -97,3 +103,40 @@     pad xs = nest (maxWidth - length xs) (text xs)     pPrintDecl (name, ty) =       pad name <+> text "::" <+> ty++-- 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+prettyDefinition :: Eq fun => [fun] -> Prop (Term fun) -> Prop (Term fun)+prettyDefinition cons (lhs :=>: t :=: u)+  | Just (f, ts) <- defines u,+    f `notElem` funs t,+    null (usort (vars t) \\ vars ts) =+    lhs :=>: u :=: t+    -- In the case where t defines f, the equation is already oriented correctly+  | otherwise = lhs :=>: t :=: u+  where+    defines (Fun f :@: ts)+      | f `elem` cons,+        all (`notElem` cons) (funs ts) = Just (f, ts)+    defines _ = Nothing++-- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative+prettyAC :: (Eq f, Eq norm) => (Term f -> norm) -> Prop (Term f) -> Prop (Term f)+prettyAC norm (lhs :=>: Fun f :@: [Var x, Fun f1 :@: [Var y, Var z]] :=: Fun f2 :@: [Var y1, Fun f3 :@: [Var x1, Var z1]])+  | f == f1, f1 == f2, f2 == f3,+    x == x1, y == y1, z == z1,+    x /= y, y /= z, x /= z,+    norm (Fun f :@: [Var x, Var y]) == norm (Fun f :@: [Var y, Var x]) =+      lhs :=>: Fun f :@: [Fun f :@: [Var x, Var y], Var z] :=: Fun f :@: [Var x, Fun f :@: [Var y, Var z]]+prettyAC _ prop = prop++-- Add a type signature when printing the equation x = y.+disambiguatePropType :: Prop (Term fun) -> Doc+disambiguatePropType (_ :=>: (Var x) :=: Var _) =+  text "::" <+> pPrintType (typ x)+disambiguatePropType _ = pPrintEmpty
src/QuickSpec/Internal/Explore/Conditionals.hs view
@@ -19,7 +19,7 @@ import QuickSpec.Internal.Testing import QuickSpec.Internal.Terminal import QuickSpec.Internal.Utils-import QuickSpec.Internal.Explore.Polymorphic+import QuickSpec.Internal.Explore.Polymorphic hiding (Normal) import qualified Twee.Base as Twee import Data.List import Control.Monad@@ -37,10 +37,9 @@     return (norm . fmap Normal)   add prop = do     redundant <- conditionallyRedundant prop-    if redundant then return False else do-      res <- lift (add (mapFun Normal prop))-      when res (considerConditionalising prop)-      return res+    unless redundant $ do+      lift (add (mapFun Normal prop))+      considerConditionalising prop  conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe conditionalsUniverse tys funs =@@ -76,10 +75,6 @@   size Constructor{} = 0   size (Normal f) = size f -instance Arity fun => Arity (WithConstructor fun) where-  arity Constructor{} = 1-  arity (Normal f) = arity f- instance Pretty fun => Pretty (WithConstructor fun) where   pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"   pPrintPrec l p (Normal f) = pPrintPrec l p f@@ -87,10 +82,6 @@ instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where   termStyle (Constructor _ _) = curried   termStyle (Normal f) = termStyle f--instance PrettyArity fun => PrettyArity (WithConstructor fun) where-  prettyArity (Constructor _ _) = 1-  prettyArity (Normal f) = prettyArity f  instance (Predicate fun, Background fun) => Background (WithConstructor fun) where   background (Normal f) = map (mapFun Normal) (background f)
src/QuickSpec/Internal/Explore/Polymorphic.hs view
@@ -9,10 +9,14 @@ {-# LANGUAGE RankNTypes #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE RecordWildCards #-}-module QuickSpec.Internal.Explore.Polymorphic(module QuickSpec.Internal.Explore.Polymorphic, Result(..), Universe(..)) where+module QuickSpec.Internal.Explore.Polymorphic(+  module QuickSpec.Internal.Explore.Polymorphic,+  Result(..),+  Universe(..),+  VariableUse(..)) where  import qualified QuickSpec.Internal.Explore.Schemas as Schemas-import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..))+import QuickSpec.Internal.Explore.Schemas(Schemas, Result(..), VariableUse(..)) import QuickSpec.Internal.Term import QuickSpec.Internal.Type import QuickSpec.Internal.Testing@@ -53,14 +57,14 @@ univ = lens pm_universe (\x y -> y { pm_universe = x })  initialState ::-  (Type -> Bool) ->+  (Type -> VariableUse) ->   Universe ->   (Term fun -> Bool) ->   (Term fun -> testcase -> result) ->   Polymorphic testcase result fun norm-initialState singleUse univ inst eval =+initialState use univ inst eval =   Polymorphic {-    pm_schemas = Schemas.initialState singleUse (inst . fmap fun_specialised) (eval . fmap fun_specialised),+    pm_schemas = Schemas.initialState use (inst . fmap fun_specialised) (eval . fmap fun_specialised),     pm_universe = univ }  polyFun :: Typed fun => fun -> PolyFun fun@@ -75,7 +79,7 @@   typeSubst_ _ x = x -- because it's supposed to be monomorphic  newtype PolyM testcase result fun norm m a = PolyM { unPolyM :: StateT (Polymorphic testcase result fun norm) m a }-  deriving (Functor, Applicative, Monad)+  deriving (Functor, Applicative, Monad, MonadTerminal)  explore ::   (PrettyTerm fun, Ord result, Ord norm, Typed fun, Ord fun, Apply (Term fun),@@ -121,7 +125,7 @@   add prop = PolyM $ do     univ <- access univ     let insts = typeInstances univ (canonicalise (regeneralise (mapFun fun_original prop)))-    or <$> mapM add insts+    mapM_ add insts  instance MonadTester testcase (Term fun) m =>   MonadTester testcase (Term (PolyFun fun)) (PolyM testcase result fun norm m) where@@ -219,13 +223,17 @@             ho <- arrows fun,             sub <- typeInstancesList univBase (components fun) ]   -    -- Add antiunifiers of all pairs of types, so that each equation-    -- has a most general type-    univ = usort $ oneTypeVar $ fixpoint antiunifiers univHo+    -- Now close the type universe under "anti-substitution":+    -- if u = typeSubst sub t, and u is in the universe, then+    -- oneTypeVar t should be in the universe.+    -- In practice this means replacing arbitrary subterms of+    -- each type with a type variable.+    univ = fixpoint (usort . oneTypeVar . concatMap antisubst) univHo       where-        antiunifiers tys =-          usort $ map (unPoly . poly) $-            tys ++ [antiunify ty1 ty2 | ty1 <- tys, ty2 <- tys]+        antisubst ty =+          ty:+          [ Twee.build (Twee.replacePosition n (Twee.var (Twee.V 0)) (Twee.singleton ty))+          | n <- [0..Twee.len ty-1] ]      components ty =       case unpackArrow ty of
src/QuickSpec/Internal/Explore/Schemas.hs view
@@ -11,6 +11,7 @@ import QuickSpec.Internal.Type import QuickSpec.Internal.Testing import QuickSpec.Internal.Utils+import QuickSpec.Internal.Terminal import qualified QuickSpec.Internal.Explore.Terms as Terms import QuickSpec.Internal.Explore.Terms(Terms) import Control.Monad.Trans.State.Strict hiding (State)@@ -23,9 +24,16 @@ import Control.Monad import Twee.Label +-- | Constrains how variables of a particular type may occur in a term.+data VariableUse =+    UpTo Int -- ^ @UpTo n@: terms may contain up to @n@ distinct variables of this type+             -- (in some cases, laws with more variables may still be found)+  | Linear   -- ^ Each variable in the term must be distinct+  deriving (Eq, Show)+ data Schemas testcase result fun norm =   Schemas {-    sc_single_use :: Type -> Bool,+    sc_use :: Type -> VariableUse,     sc_instantiate_singleton :: Term fun -> Bool,     sc_empty :: Terms testcase result (Term fun) norm,     sc_classes :: Terms testcase result (Term fun) norm,@@ -33,7 +41,7 @@     sc_instances :: Map (Term fun) (Terms testcase result (Term fun) norm) }  classes = lens sc_classes (\x y -> y { sc_classes = x })-single_use = lens sc_single_use (\x y -> y { sc_single_use = x })+use = lens sc_use (\x y -> y { sc_use = x }) instances = lens sc_instances (\x y -> y { sc_instances = x }) instantiated = lens sc_instantiated (\x y -> y { sc_instantiated = x }) @@ -41,13 +49,13 @@ instance_ t = reading (\Schemas{..} -> keyDefault t sc_empty # instances)  initialState ::-  (Type -> Bool) ->+  (Type -> VariableUse) ->   (Term fun -> Bool) ->   (Term fun -> testcase -> result) ->   Schemas testcase result fun norm-initialState singleUse inst eval =+initialState use inst eval =   Schemas {-    sc_single_use = singleUse,+    sc_use = use,     sc_instantiate_singleton = inst,     sc_empty = Terms.initialState eval,     sc_classes = Terms.initialState eval,@@ -61,37 +69,38 @@ -- The schema is represented as a term where there is only one distinct variable of each type explore ::   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>   Term fun -> StateT (Schemas testcase result fun norm) m (Result fun) explore t0 = do-  let t = mostSpecific t0-  res <- zoom classes (Terms.explore t)-  singleUse <- access single_use-  case res of-    Terms.Singleton -> do-      inst <- gets sc_instantiate_singleton-      if inst t then-        instantiateRep t-       else do-        -- Add the most general instance of the schema-        zoom (instance_ t) (Terms.explore (mostGeneral singleUse t0))-        return (Accepted [])-    Terms.Discovered ([] :=>: _ :=: u) ->-      exploreIn u t-    Terms.Knew ([] :=>: _ :=: u) ->-      exploreIn u t-    _ -> error "term layer returned non-equational property"+  use <- access use+  if or [use ty == UpTo 0 | ty <- usort (map typ (vars t0))] then return (Rejected []) else do+    let t = mostSpecific t0+    res <- zoom classes (Terms.explore t)+    case res of+      Terms.Singleton -> do+        inst <- gets sc_instantiate_singleton+        if inst t then+          instantiateRep t+         else do+          -- Add the most general instance of the schema+          zoom (instance_ t) (Terms.explore (mostGeneral use t0))+          return (Accepted [])+      Terms.Discovered ([] :=>: _ :=: u) ->+        exploreIn u t+      Terms.Knew ([] :=>: _ :=: u) ->+        exploreIn u t+      _ -> error "term layer returned non-equational property"  {-# INLINEABLE exploreIn #-} exploreIn ::   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>   Term fun -> Term fun ->   StateT (Schemas testcase result fun norm) m (Result fun) exploreIn rep t = do   -- First check if schema is redundant-  singleUse <- access single_use-  res <- zoom (instance_ rep) (Terms.explore (mostGeneral singleUse t))+  use <- access use+  res <- zoom (instance_ rep) (Terms.explore (mostGeneral use t))   case res of     Terms.Discovered prop -> do       add prop@@ -111,7 +120,7 @@ {-# INLINEABLE instantiateRep #-} instantiateRep ::   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>   Term fun ->   StateT (Schemas testcase result fun norm) m (Result fun) instantiateRep t = do@@ -121,13 +130,13 @@ {-# INLINEABLE instantiate #-} instantiate ::   (PrettyTerm fun, Ord result, Ord fun, Ord norm, Typed fun,-  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m) =>+  MonadTester testcase (Term fun) m, MonadPruner (Term fun) norm m, MonadTerminal m) =>   Term fun -> Term fun ->   StateT (Schemas testcase result fun norm) m (Result fun) instantiate rep t = do-  singleUse <- access single_use+  use <- access use   zoom (instance_ rep) $ do-    let instances = sortBy (comparing generality) (allUnifications singleUse (mostGeneral singleUse t))+    let instances = sortBy (comparing generality) (allUnifications use (mostGeneral use t))     Accepted <$> catMaybes <$> forM instances (\t -> do       res <- Terms.explore t       case res of@@ -140,30 +149,46 @@ generality :: Term f -> (Int, [Var]) generality t = (-length (usort (vars t)), vars t) +mkVar :: Type -> Int -> Var+mkVar ty n = V ty m+  -- Try to make sure that variables of different types don't end up with the+  -- same number. It would be better to deal with this in QuickSpec.Term.+  -- (Note: the problem we are trying to avoid is that, if two variables have+  -- the same number and different but unifiable types, then a type substitution+  -- can turn them into the same variable.)+  where+    m = fromIntegral (labelNum (label (ty, n)))+ -- | Instantiate a schema by making all the variables different.-mostGeneral :: (Type -> Bool) -> Term f -> Term f-mostGeneral singleUse s = evalState (aux s) Map.empty+mostGeneral :: (Type -> VariableUse) -> Term f -> Term f+mostGeneral use s = evalState (aux s) Map.empty   where     aux (Var (V ty _)) = do       m <- get       let n :: Int           n = Map.findWithDefault 0 ty m-      unless (singleUse ty) $+      unless (use ty == UpTo 1) $         put $! Map.insert ty (n+1) m-      let m = fromIntegral (labelNum (label (ty, n)))-      return (Var (V ty m))+      return (Var (mkVar ty n))     aux (Fun f) = return (Fun f)     aux (t :$: u) = liftM2 (:$:) (aux t) (aux u)  mostSpecific :: Term f -> Term f-mostSpecific = subst (\(V ty _) -> Var (V ty 0))+mostSpecific = subst (\(V ty _) -> Var (mkVar ty 0)) -allUnifications :: (Type -> Bool) -> Term fun -> [Term fun]-allUnifications singleUse t = map f ss+allUnifications :: (Type -> VariableUse) -> Term fun -> [Term fun]+allUnifications use t =+  [ subst (\x -> Var (Map.findWithDefault undefined x s)) t | s <- ss ]   where-    vs = [ map (x,) (select xs) | xs <- partitionBy typ (usort (vars t)), x <- xs ]-    ss = map Map.fromList (sequence vs)-    go s x = Map.findWithDefault undefined x s-    f s = subst (Var . go s) t-    select [V ty x] | not (singleUse ty) = [V ty x, V ty (succ x)]-    select xs = take 4 xs+    ss =+      map Map.fromList $ map concat $ sequence+        [substsFor xs (typ y) | xs@(y:_) <- partitionBy typ (usort (vars t))]++    substsFor xs ty =+      case use ty of+        UpTo k ->+          sequence [[(x, v) | v <- take k vs] | x <- xs]+        Linear ->+          map (zip xs) (permutations (take (length xs) vs))+      where+        vs = map (mkVar ty) [0..]
src/QuickSpec/Internal/Explore/Terms.hs view
@@ -14,6 +14,7 @@ import Control.Monad.Trans.State.Strict hiding (State) import Data.Lens.Light import QuickSpec.Internal.Utils+import QuickSpec.Internal.Terminal  data Terms testcase result term norm =   Terms {@@ -56,14 +57,14 @@ -- The representatives of the equivalence classes are guaranteed not to change. -- -- Discovered properties are not added to the pruner.-explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>+explore :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m, MonadTerminal m) =>   term -> StateT (Terms testcase result term norm) m (Result term) explore t = do   res <- explore' t-  -- case res of-  --   Discovered prop -> traceM ("discovered " ++ prettyShow prop)-  --   Knew prop -> traceM ("knew " ++ prettyShow prop)-  --   Singleton -> traceM ("singleton " ++ prettyShow t)+  --case res of+  --  Discovered prop -> putLine ("discovered " ++ prettyShow prop)+  --  Knew prop -> putLine ("knew " ++ prettyShow prop)+  --  Singleton -> putLine ("singleton " ++ prettyShow t)   return res explore' :: (Pretty term, Typed term, Ord norm, Ord result, MonadTester testcase term m, MonadPruner term norm m) =>   term -> StateT (Terms testcase result term norm) m (Result term)
src/QuickSpec/Internal/Haskell.hs view
@@ -22,7 +22,6 @@ import QuickSpec.Internal.Pruning import Test.QuickCheck hiding (total, classify, subterms, Fun) import Data.Constraint hiding ((\\))-import Data.List import Data.Proxy import qualified Twee.Base as Twee import QuickSpec.Internal.Term@@ -36,7 +35,7 @@ import qualified QuickSpec.Internal.Pruning.Twee as Twee import QuickSpec.Internal.Explore hiding (quickSpec) import qualified QuickSpec.Internal.Explore-import QuickSpec.Internal.Explore.Polymorphic(Universe(..))+import QuickSpec.Internal.Explore.Polymorphic(Universe(..), VariableUse(..)) import QuickSpec.Internal.Pruning.Background(Background) import Control.Monad import Control.Monad.Trans.State.Strict@@ -45,7 +44,7 @@ import QuickSpec.Internal.Utils import Data.Lens.Light import GHC.TypeLits-import QuickSpec.Internal.Explore.Conditionals+import QuickSpec.Internal.Explore.Conditionals hiding (Normal) import Control.Spoon import qualified Data.Set as Set import qualified Test.QuickCheck.Poly as Poly@@ -76,6 +75,8 @@     inst (Names ["f", "g", "h"] :: Names (A -> B)),     inst (Names ["dict"] :: Names (Dict ClassA)),     inst (Names ["x", "y", "z", "w"] :: Names A),+    -- Allow up to 4 variables per type by default+    inst (Use (UpTo 4) :: Use A),     -- Standard instances     baseType (Proxy :: Proxy ()),     baseType (Proxy :: Proxy Int),@@ -125,6 +126,7 @@     -- From Arbitrary to Gen     inst $ \(Dict :: Dict (Arbitrary A)) -> arbitrary :: Gen A,     -- Observation functions+    inst $ \(Dict :: Dict (Ord A)) -> OrdInstance :: OrdInstance A,     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),@@ -134,10 +136,13 @@     -- Needed for typeclass-polymorphic predicates to work currently     inst (\(Dict :: Dict ClassA) -> Dict :: Dict (Arbitrary (Dict ClassA)))] +data OrdInstance a where+  OrdInstance :: Ord a => OrdInstance a+ -- A token used in the instance list for types that shouldn't generate warnings data NoWarnings a = NoWarnings -data SingleUse a = SingleUse+data Use a = Use VariableUse  instance c => Arbitrary (Dict c) where   arbitrary = return Dict@@ -166,6 +171,10 @@ instance (Arbitrary a, Observe test outcome b) => Observe (a, test) outcome (a -> b) where   observe (x, obs) f = observe obs (f x) +-- | Like 'Test.QuickCheck.===', but using the 'Observe' typeclass instead of 'Eq'.+(=~=) :: (Show test, Show outcome, Observe test outcome a) => a -> a -> Property+a =~= b = property $ \test -> observe test a Test.QuickCheck.=== observe test b+ -- 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@@ -240,6 +249,9 @@ findGenerator def insts ty =   bringFunctor <$> (findInstance insts (defaultTo def ty) :: Maybe (Value Gen)) +findOrdInstance :: Instances -> Type -> Maybe (Value OrdInstance)+findOrdInstance insts ty = findInstance insts ty+ findObserver :: Instances -> Type -> Maybe (Gen (Value Identity -> Value Ordy)) findObserver insts ty = do   inst <- findInstance insts ty :: Maybe (Value WrappedObserveData)@@ -274,13 +286,23 @@   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 } +makeQuickcheckFun :: String -> Constant+makeQuickcheckFun nm = Constant+  { con_name  = nm+  , con_style = infixStyle 9  -- high precedence to always force parens+  , con_value = undefined+  , con_type = undefined+  , con_constraints = undefined+  , con_size = 1+  , con_classify = Function+  }+ instance Eq Constant where   x == y =     con_name x == con_name y && typ (con_value x) == typ (con_value y)@@ -288,12 +310,7 @@ instance Ord Constant where   compare =     comparing $ \con ->-      (con_name con, twiddle (arity con), typ con)-      where-        -- This trick comes from Prover9 and improves the ordering somewhat-        twiddle 1 = 2-        twiddle 2 = 1-        twiddle x = x+      (typeArity (typ con), typ con, con_name con)  instance Background Constant @@ -313,11 +330,6 @@           | isOp name && typeArity (typ val) >= 2 -> infixStyle 5           | isOp name -> prefix           | otherwise -> curried,-    con_pretty_arity =-      case () of-        _ | isOp name && typeArity (typ val) >= 2 -> 2-          | isOp name -> 1-          | otherwise -> typeArity (typ val),     con_value = val,     con_type = ty,     con_constraints = constraints,@@ -372,15 +384,9 @@ instance PrettyTerm Constant where   termStyle = con_style -instance PrettyArity Constant where-  prettyArity = con_pretty_arity- instance Sized Constant where   size = con_size -instance Arity Constant where-  arity = typeArity . typ- instance Predicate Constant where   classify = con_classify @@ -478,6 +484,12 @@     inst :: Dict (Arbitrary (PredicateTestCase a)) -> Gen (PredicateTestCase a)     inst Dict = arbitrary `suchThat` uncrry pred +-- | How QuickSpec should style equations.+data PrintStyle+  = ForHumans+  | ForQuickCheck+  deriving (Eq, Ord, Show, Read, Bounded, Enum)+ data Config =   Config {     cfg_quickCheck :: QuickCheck.Config,@@ -492,7 +504,8 @@     cfg_default_to :: Type,     cfg_infer_instance_types :: Bool,     cfg_background :: [Prop (Term Constant)],-    cfg_print_filter :: Prop (Term Constant) -> Bool+    cfg_print_filter :: Prop (Term Constant) -> Bool,+    cfg_print_style :: PrintStyle     }  lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x })@@ -505,6 +518,7 @@ lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x }) lens_background = lens cfg_background (\x y -> y { cfg_background = x }) lens_print_filter = lens cfg_print_filter (\x y -> y { cfg_print_filter = x })+lens_print_style = lens cfg_print_style (\x y -> y { cfg_print_style = x })  defaultConfig :: Config defaultConfig =@@ -518,7 +532,8 @@     cfg_default_to = typeRep (Proxy :: Proxy Int),     cfg_infer_instance_types = False,     cfg_background = [],-    cfg_print_filter = \_ -> True }+    cfg_print_filter = \_ -> True,+    cfg_print_style = ForHumans }  -- Extra types for the universe that come from in-scope instances. instanceTypes :: Instances -> Config -> [Type]@@ -593,55 +608,33 @@       [true | any (/= Function) (map classify (f cfg_constants))] ++       f cfg_constants ++ concatMap selectors (f cfg_constants)     constants = constantsOf concat-    +     univ = conditionalsUniverse (instanceTypes instances cfg) constants     instances = cfg_instances `mappend` baseInstances      eval = evalHaskell cfg_default_to instances+    was_observed = isNothing . findOrdInstance instances  -- it was observed if there is no Ord instance directly in scope      present funs prop = do       norm <- normaliser-      let prop' = makeDefinition funs (ac norm (conditionalise prop))+      let prop' = prettyDefinition funs (prettyAC norm (conditionalise prop))       when (cfg_print_filter prop) $ do         (n :: Int, props) <- get         put (n+1, prop':props)         putLine $-          printf "%3d. %s" n $ show $-            prettyProp (names instances) prop' <+> maybeType prop--    -- Put an equation that defines the function f into the form f lhs = rhs.-    -- An equation defines f if:-    --   * it is of the form f lhs = rhs (or vice versa).-    --   * f is not a background function.-    --   * lhs only contains background functions.-    --   * rhs does not contain f.-    --   * all vars in rhs appear in lhs-    makeDefinition cons (lhs :=>: t :=: u)-      | Just (f, ts) <- defines u,-        f `notElem` funs t,-        null (usort (vars t) \\ vars ts) =-        lhs :=>: u :=: t-        -- In the case where t defines f, the equation is already oriented correctly-      | otherwise = lhs :=>: t :=: u-      where-        defines (Fun f :@: ts)-          | f `elem` cons,-            all (`notElem` cons) (funs ts) = Just (f, ts)-        defines _ = Nothing--    -- Transform x+(y+z) = y+(x+z) into associativity, if + is commutative-    ac norm (lhs :=>: Fun f :@: [Var x, Fun f1 :@: [Var y, Var z]] :=: Fun f2 :@: [Var y1, Fun f3 :@: [Var x1, Var z1]])-      | f == f1, f1 == f2, f2 == f3,-        x == x1, y == y1, z == z1,-        x /= y, y /= z, x /= z,-        norm (Fun f :@: [Var x, Var y]) == norm (Fun f :@: [Var y, Var x]) =-          lhs :=>: Fun f :@: [Fun f :@: [Var x, Var y], Var z] :=: Fun f :@: [Var x, Fun f :@: [Var y, Var z]]-    ac _ prop = prop--    -- Add a type signature when printing the equation x = y.-    maybeType (_ :=>: x@(Var _) :=: Var _) =-      text "::" <+> pPrintType (typ x)-    maybeType _ = pPrintEmpty+          case cfg_print_style of+            ForHumans ->+              printf "%3d. %s" n $ show $+                prettyProp (names instances) prop' <+> disambiguatePropType prop+            ForQuickCheck ->+              renderStyle (style {lineLength = 78}) $ nest 2 $+                prettyPropQC+                  was_observed+                  makeQuickcheckFun+                  n+                  (names instances)+                  prop'+                  <+> disambiguatePropType prop      -- XXX do this during testing     constraintsOk = memo $ \con ->@@ -659,8 +652,9 @@      conditions t = usort [p | f <- funs t, Selector _ p _ <- [classify f]] -    singleUse ty =-      isJust (findInstance instances ty :: Maybe (Value SingleUse))+    use ty =+      ofValue (\(Use x) -> x) $ fromJust $+      (findInstance instances ty :: Maybe (Value Use))      mainOf n f g = do       unless (null (f cfg_constants)) $ do@@ -670,10 +664,14 @@       when (n > 0) $ do         putText (prettyShow (warnings univ instances cfg))         putLine "== Laws =="+        when (cfg_print_style == ForQuickCheck) $ do+          putLine "quickspec_laws :: [(String, Property)]"+          putLine "quickspec_laws ="       let pres = if n == 0 then \_ -> return () else present (constantsOf f)-      QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size singleUse univ+      QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ         (enumerator (map Fun (constantsOf g)))       when (n > 0) $ do+        when (cfg_print_style == ForQuickCheck) $ putLine "  ]"         putLine ""      main = do
src/QuickSpec/Internal/Prop.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE DeriveGeneric, TypeFamilies, DeriveFunctor, FlexibleInstances, MultiParamTypeClasses, UndecidableInstances, FlexibleContexts, TypeOperators #-} module QuickSpec.Internal.Prop where +import Data.Bool (bool) import Control.Monad import qualified Data.DList as DList import Data.Ord@@ -10,7 +11,6 @@ import QuickSpec.Internal.Term import GHC.Generics(Generic) import qualified Data.Map.Strict as Map-import qualified Data.Set as Set import Control.Monad.Trans.State.Strict import Data.List @@ -83,19 +83,44 @@ -- Making properties look pretty (naming variables, etc.) ---------------------------------------------------------------------- -class PrettyArity fun where-  prettyArity :: fun -> Int-  prettyArity _ = 0--instance (PrettyArity fun1, PrettyArity fun2) => PrettyArity (fun1 :+: fun2) where-  prettyArity (Inl x) = prettyArity x-  prettyArity (Inr x) = prettyArity x- prettyProp ::-  (Typed fun, Apply (Term fun), PrettyTerm fun, PrettyArity fun) =>+  (Typed fun, Apply (Term fun), PrettyTerm fun) =>   (Type -> [String]) -> Prop (Term fun) -> Doc-prettyProp cands = pPrint . nameVars cands+prettyProp cands = pPrint . snd . nameVars cands +prettyPropQC ::+  (Typed fun, Apply (Term fun), PrettyTerm fun) =>+  (Type -> Bool) -> (String -> fun) -> Int -> (Type -> [String]) -> Prop (Term fun) -> Doc+prettyPropQC was_observed mk_fun nth cands x+  = hang (text first_char <+> text "(" <+> ((text $ show $ show $ pPrint law))) 2+  $ hang (hsep [text ",", text "property", text "$"]) 4+  $ hang ppr_binds 4+  $ ppr_ctx <+> (pPrint (eq_fn :$: lhs :$: rhs) <> text ")")++  where+    eq = mk_fun "==="+    obs_eq = mk_fun "=~="+    eq_fn = Fun $ Ordinary $ bool eq obs_eq $ was_observed $ typ lhs_for_type+++    first_char =+      case nth of+        1 -> "["+        _ -> ","+    ppr_ctx =+      case length ctx of+        0 -> pPrintEmpty+        _ -> (hsep $ punctuate (text " &&") $ fmap (parens . pPrint) ctx) <+> text "==>"++    (_ :=>: (lhs_for_type :=: _)) = x+    (var_defs, law@(ctx :=>: (lhs :=: rhs))) = nameVars cands x+    print_sig name ty = parens $ text name <+> text "::" <+> pPrintType ty+    ppr_binds =+      case Map.size var_defs of+        0 -> pPrintEmpty+        _ -> (text "\\ " <> sep (fmap (uncurry print_sig) (Map.assocs var_defs))) <+> text "->"++ data Named fun = Name String | Ordinary fun instance Pretty fun => Pretty (Named fun) where   pPrintPrec _ _ (Name name) = text name@@ -104,14 +129,16 @@   termStyle Name{} = curried   termStyle (Ordinary fun) = termStyle fun -nameVars :: (Type -> [String]) -> Prop (Term fun) -> Prop (Term (Named fun))+nameVars :: (Type -> [String]) -> Prop (Term fun) -> (Map.Map String Type, Prop (Term (Named fun))) nameVars cands p =-  subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Ordinary) p)+  (var_defs, subst (\x -> Map.findWithDefault undefined x sub) (fmap (fmap Ordinary) p))   where-    sub = Map.fromList (evalState (mapM assign (nub (vars p))) Set.empty)+    sub = Map.fromList sub_map+    (sub_map, var_defs) = (runState (mapM assign (nub (vars p))) Map.empty)     assign x = do       s <- get-      let names = supply (cands (typ x))-          name = head (filter (`Set.notMember` s) names)-      modify (Set.insert name)+      let ty = typ x+          names = supply (cands ty)+          name = head (filter (`Map.notMember` s) names)+      modify (Map.insert name ty)       return (x, Fun (Name name))
src/QuickSpec/Internal/Pruning.hs view
@@ -13,12 +13,12 @@  class Monad m => MonadPruner term norm m | m -> term norm where   normaliser :: m (term -> norm)-  add :: Prop term -> m Bool+  add :: Prop term -> m ()    default normaliser :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => m (term -> norm)   normaliser = lift normaliser -  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m Bool+  default add :: (MonadTrans t, MonadPruner term norm m', m ~ t m') => Prop term -> m ()   add = lift . add  instance MonadPruner term norm m => MonadPruner term norm (StateT s m)@@ -37,7 +37,7 @@  instance MonadPruner term norm m => MonadPruner term norm (ReadOnlyPruner m) where   normaliser = ReadOnlyPruner normaliser-  add _ = return True+  add _ = return ()  newtype WatchPruner term m a = WatchPruner (StateT [Prop term] m a)   deriving (Functor, Applicative, Monad, MonadTrans, MonadIO, MonadTester testcase term)@@ -46,7 +46,7 @@   normaliser = lift normaliser   add prop = do     res <- lift (add prop)-    when res (WatchPruner (modify (prop:)))+    WatchPruner (modify (prop:))     return res  watchPruner :: Monad m => WatchPruner term m a -> m (a, [Prop term])
src/QuickSpec/Internal/Pruning/PartialApplication.hs view
@@ -12,6 +12,7 @@ import QuickSpec.Internal.Testing import Control.Monad.IO.Class import Control.Monad.Trans.Class+import Twee.Base(Arity(..))  data PartiallyApplied f =     -- A partially-applied function symbol.@@ -31,16 +32,12 @@   arity (Apply _) = 2  instance Pretty f => Pretty (PartiallyApplied f) where-  pPrint (Partial f _) = pPrint f+  pPrint (Partial f n) = pPrint f <#> text "@" <#> pPrint n   pPrint (Apply _) = text "$"  instance PrettyTerm f => PrettyTerm (PartiallyApplied f) where   termStyle (Partial f _) = termStyle f-  termStyle (Apply _) = invisible--instance PrettyArity f => PrettyArity (PartiallyApplied f) where-  prettyArity (Partial f _) = prettyArity f-  prettyArity (Apply _) = 1+  termStyle (Apply _) = infixStyle 2  instance Typed f => Typed (PartiallyApplied f) where   typ (Apply ty) = arrowType [ty] ty@@ -50,10 +47,6 @@   typeSubst_ sub (Apply ty) = Apply (typeSubst_ sub ty)   typeSubst_ sub (Partial f n) = Partial (typeSubst_ sub f) n -getTotal :: Arity f => PartiallyApplied f -> Maybe f-getTotal (Partial f n) | arity f == n = Just f-getTotal _ = Nothing- partial :: f -> Term (PartiallyApplied f) partial f = Fun (Partial f 0) @@ -61,8 +54,8 @@ total f = Partial f (arity f)  smartApply ::-  (Arity f, Typed f) => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)-smartApply (Fun (Partial f n) :@: ts) u | n < arity f =+  Typed f => Term (PartiallyApplied f) -> Term (PartiallyApplied f) -> Term (PartiallyApplied f)+smartApply (Fun (Partial f n) :@: ts) u =   Fun (Partial f (n+1)) :@: (ts ++ [u]) smartApply t u = simpleApply t u @@ -72,12 +65,13 @@ simpleApply t u =   Fun (Apply (typ t)) :@: [t, u] -instance (Arity f, Typed f, Background f) => Background (PartiallyApplied f) where+instance (Typed f, Background f) => Background (PartiallyApplied f) where   background (Partial f _) =-    map (mapFun (\f -> Partial f (arity f))) (background f) +++    map (mapFun (\f -> Partial f arity)) (background f) ++     [ simpleApply (partial n) (vs !! n) === partial (n+1)-    | n <- [0..arity f-1] ]+    | n <- [0..arity-1] ]     where+      arity = typeArity (typ f)       partial i =         Fun (Partial f i) :@: take i vs       vs = map Var (zipWith V (typeArgs (typ f)) [0..])@@ -90,7 +84,7 @@ instance MonadTrans (Pruner fun) where   lift = Pruner -instance (PrettyTerm fun, Typed fun, Arity fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where+instance (PrettyTerm fun, Typed fun, MonadPruner (Term (PartiallyApplied fun)) norm pruner) => MonadPruner (Term fun) norm (Pruner fun pruner) where   normaliser =     Pruner $ do       norm <- normaliser@@ -101,7 +95,7 @@     Pruner $ do       add (encode <$> canonicalise prop) -encode :: (Typed fun, Arity fun) => Term fun -> Term (PartiallyApplied fun)+encode :: Typed fun => Term fun -> Term (PartiallyApplied fun) encode (Var x) = Var x encode (Fun f) = partial f encode (t :$: u) = smartApply (encode t) (encode u)
src/QuickSpec/Internal/Pruning/Types.hs view
@@ -4,8 +4,7 @@ module QuickSpec.Internal.Pruning.Types where  import QuickSpec.Internal.Pruning-import qualified QuickSpec.Internal.Pruning.Background as Background-import QuickSpec.Internal.Pruning.Background(Background)+import QuickSpec.Internal.Pruning.Background(Background(..)) import QuickSpec.Internal.Testing import QuickSpec.Internal.Term import QuickSpec.Internal.Type@@ -14,6 +13,7 @@ import Control.Monad.IO.Class import Control.Monad.Trans.Class import qualified Twee.Base as Twee+import Twee.Base(Arity(..))  data Tagged fun =     Func fun@@ -66,11 +66,11 @@    add prop = lift (add (encode <$> canonicalise prop)) -instance (Typed fun, Arity fun) => Background (Tagged fun) where+instance (Typed fun, Twee.Arity fun, Background fun) => Background (Tagged fun) where   background = typingAxioms  -- Compute the typing axioms for a function or type tag.-typingAxioms :: (Typed fun, Arity fun) =>+typingAxioms :: (Typed fun, Twee.Arity fun, Background fun) =>   Tagged fun -> [Prop (UntypedTerm fun)] typingAxioms (Tag ty) =   [tag ty (tag ty x) === tag ty x]@@ -78,7 +78,8 @@     x = Var (V ty 0) typingAxioms (Func func) =   [tag res t === t] ++-  [tagArg i ty === t | (i, ty) <- zip [0..] args]+  [tagArg i ty === t | (i, ty) <- zip [0..] args] +++  map (fmap encode) (background func)   where     f = Fun (Func func)     xs = take n (map (Var . V typeVar) [0..])
src/QuickSpec/Internal/Pruning/UntypedTwee.hs view
@@ -16,7 +16,7 @@ import Twee hiding (Config(..)) import Twee.Rule hiding (normalForms) import Twee.Proof hiding (Config, defaultConfig)-import Twee.Base(Ordered(..), Extended(..), EqualsBonus)+import Twee.Base(Ordered(..), Extended(..), Arity(..), EqualsBonus) import Control.Monad.Trans.Reader import Control.Monad.Trans.State.Strict hiding (State) import Control.Monad.Trans.Class@@ -77,16 +77,10 @@   add ([] :=>: t :=: u) = Pruner $ do     state <- lift get     config <- ask-    let-      t' = normalFormsTwee state t-      u' = normalFormsTwee state u-    -- Add the property anyway in case it could only be joined-    -- by considering all normal forms     lift (put $! addTwee config t u state)-    return (Set.null (Set.intersection t' u'))    add _ =-    return True+    return ()     --error "twee pruner doesn't support non-unit equalities"  normaliseTwee :: (Ord fun, Typeable fun, Arity fun, Twee.Sized fun, PrettyTerm fun, EqualsBonus fun) =>
src/QuickSpec/Internal/Term.hs view
@@ -9,12 +9,13 @@ import QuickSpec.Internal.Utils import Control.Monad import GHC.Generics(Generic)-import Test.QuickCheck(CoArbitrary)+import Test.QuickCheck(CoArbitrary(..)) import Data.DList(DList) import qualified Data.DList as DList-import Twee.Base(Arity(..), Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint)+import Twee.Base(Pretty(..), PrettyTerm(..), TermStyle(..), EqualsBonus, prettyPrint) import Twee.Pretty import qualified Data.Map.Strict as Map+import Data.Map(Map) import Data.List import Data.Ord @@ -24,13 +25,47 @@  -- | 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)+  deriving (Eq, Ord, Show, Generic) +instance CoArbitrary Var where+  coarbitrary = coarbitrary . var_id+ instance Typed Var where   typ x = var_ty x   otherTypesDL _ = mzero   typeSubst_ sub (V ty x) = V (typeSubst_ sub ty) x +match :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))+match (Var x) t = Just (Map.singleton x t)+match (Fun f) (Fun g)+  | f == g = Just Map.empty+  | otherwise = Nothing+match (f :$: x) (g :$: y) = do+  m1 <- match f g+  m2 <- match x y+  guard (and [t == u | (t, u) <- Map.elems (Map.intersectionWith (,) m1 m2)])+  return (Map.union m1 m2)++unify :: Eq f => Term f -> Term f -> Maybe (Map Var (Term f))+unify t u = loop Map.empty [(t, u)]+  where+    loop sub [] = Just sub+    loop sub ((Fun f, Fun g):xs)+      | f == g = loop sub xs+    loop sub ((f :$: x, g :$: y):xs) =+      loop sub ((f, g):(x, y):xs)+    loop sub ((Var x, t):xs)+      | t == Var x = loop sub xs+      | x `elem` vars t = Nothing+      | otherwise =+        loop+          (Map.insert x t (fmap (replace x t) sub))+          [(replace x t u, replace x t v) | (u, v) <- xs]+    loop sub ((t, Var x):xs) = loop sub ((Var x, t):xs)++    replace x t (Var y) | x == y = t+    replace _ _ t = t+ -- | A class for things that contain terms. class Symbolic f a | a -> f where   -- | A different list of all terms contained in the thing.@@ -169,14 +204,19 @@     tryApply (typ t) (typ u)     return (t :$: u) +depth :: Term f -> Int+depth Var{} = 1+depth Fun{} = 1+depth (t :$: u) = depth t `max` (1+depth u)+ -- | A standard term ordering - size, skeleton, generality. -- Satisfies the property: -- if measure (schema t) < measure (schema u) then t < u.-type Measure f = (Int, Int, Int, MeasureFuns f, Int, [Var])+type Measure f = (Int, Int, Int, Int, MeasureFuns f, Int, [Var]) -- | Compute the term ordering for a term. measure :: (Sized f, Typed f) => Term f -> Measure f measure t =-  (size t, missing t, -length (vars t), MeasureFuns (skel t),+  (depth t, size t, missing t, -length (vars t), MeasureFuns (skel t),    -length (usort (vars t)), vars t)   where     skel (Var (V ty _)) = Var (V ty 0)@@ -219,10 +259,6 @@ instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where   size (Inl x) = size x   size (Inr x) = size x--instance (Arity fun1, Arity fun2) => Arity (fun1 :+: fun2) where-  arity (Inl x) = arity x-  arity (Inr x) = arity x  instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where   typ (Inl x) = typ x