packages feed

quickspec 2.2 → 2.2.1

raw patch · 20 files changed

+360/−222 lines, 20 filesdep +hashabledep ~twee-lib

Dependencies added: hashable

Dependency ranges changed: twee-lib

Files

LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2009-2018, Nick Smallbone+Copyright (c) 2009-2026, Nick Smallbone  All rights reserved.
quickspec.cabal view
@@ -1,5 +1,5 @@ Name:                quickspec-Version:             2.2+Version:             2.2.1 Cabal-version:       >= 1.10 Build-type:          Simple @@ -9,7 +9,7 @@  License:             BSD3 License-file:        LICENSE-Copyright:           2009-2019 Nick Smallbone+Copyright:           2009-2026 Nick Smallbone  Category:            Testing @@ -67,7 +67,7 @@  source-repository head   type:     git-  location: git://github.com/nick8325/quickspec.git+  location: https://github.com/nick8325/quickspec.git   branch:   master  library@@ -92,6 +92,7 @@     QuickSpec.Internal.Pruning.Types     QuickSpec.Internal.Pruning.UntypedTwee     QuickSpec.Internal.Pruning.PartialApplication+    QuickSpec.Internal.Pruning.Conditionals     QuickSpec.Internal.Term     QuickSpec.Internal.Terminal     QuickSpec.Internal.Testing@@ -108,9 +109,10 @@     containers,     data-lens-light >= 0.1.1,     dlist,+    hashable >= 1.5,     random,     spoon,     template-haskell,     transformers,-    twee-lib,+    twee-lib >= 2.6,     uglymemo
src/QuickSpec.hs view
@@ -94,10 +94,10 @@   type (==>), liftC, instanceOf,    -- * Customising QuickSpec-  withMaxTermSize, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,+  withMaxTermSize, withMaxTermDepth, withMaxTests, withMaxTestSize, withMaxFunctions, defaultTo,   withPruningDepth, withPruningTermSize, withFixedSeed,   withInferInstanceTypes, withPrintStyle, PrintStyle(..),-  withConsistencyCheck,+  withConsistencyCheck, withBackgroundStrings,    -- * Integrating with QuickCheck   (=~=),
src/QuickSpec/Internal.hs view
@@ -56,6 +56,11 @@ addBackground props =   Sig $ \_ cfg -> cfg { Haskell.cfg_background = Haskell.cfg_background cfg ++ props } +-- | Add some properties to the background theory.+withBackgroundStrings :: [String] -> Sig+withBackgroundStrings props =+  Sig $ \_ cfg -> cfg { Haskell.cfg_background_str = Haskell.cfg_background_str cfg ++ props }+ -- | A signature. newtype Sig = Sig { unSig :: Context -> Haskell.Config -> Haskell.Config } @@ -357,6 +362,10 @@ withMaxTermSize :: Int -> Sig withMaxTermSize n = Sig (\_ -> setL Haskell.lens_max_size n) +-- | Set the maximum depth of terms to explore (default: unlimited).+withMaxTermDepth :: Int -> Sig+withMaxTermDepth n = Sig (\_ -> setL Haskell.lens_max_depth n)+ withMaxCommutativeSize :: Int -> Sig withMaxCommutativeSize n = Sig (\_ -> setL Haskell.lens_max_commutative_size n) @@ -417,6 +426,11 @@ -- false laws withConsistencyCheck :: Sig withConsistencyCheck = Sig (\_ -> setL (Haskell.lens_check_consistency) True)++-- | (Experimental) Still return laws even if a resource limit+-- occurred (memory exhaustion, timeout caused by System.Timeout)+withResourceLimitHandling :: Sig+withResourceLimitHandling = Sig (\_ -> setL (Haskell.lens_handle_resource_limit) True)  -- | A signature containing boolean functions: -- @(`||`)@, @(`&&`)@, `not`, `True`, `False`.
src/QuickSpec/Internal/Explore.hs view
@@ -61,7 +61,7 @@   mapEnumerator (sortBy' measure) e  quickSpec ::-  (Ord fun, Ord norm, Sized fun, Typed fun, Ord result, PrettyTerm fun,+  (Ord fun, Ord norm, FuncSized fun, Typed fun, Ord result, PrettyTerm fun,   MonadPruner (Term fun) norm m, MonadTester testcase (Term fun) m, MonadTerminal m) =>   (Prop (Term fun) -> m ()) ->   (Term fun -> testcase -> Maybe result) ->
src/QuickSpec/Internal/Explore/Conditionals.hs view
@@ -30,34 +30,22 @@   deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal) instance MonadTrans Conditionals where   lift = Conditionals-instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+instance (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>   MonadPruner (Term fun) norm (Conditionals m) where-  normaliser = lift $ do-    norm <- normaliser-    return (norm . fmap Normal)-  add prop = do-    redundant <- conditionallyRedundant prop-    if redundant then return False else do-      res <- lift (add (Prop.mapFun Normal prop))-      considerConditionalising prop-      return res--  decodeNormalForm hole t = lift $ do-    t <- decodeNormalForm (fmap (fmap Normal) . hole) t-    let f (Normal x) = Just x-        f _ = Nothing-    return $ t >>= sequence . Term.mapFun f+  normaliser = lift normaliser+  add = lift . add . conditionalise+  decodeNormalForm hole t = lift (decodeNormalForm hole t)  conditionalsUniverse :: (Typed fun, Predicate fun) => [Type] -> [fun] -> Universe conditionalsUniverse tys funs =   universe $     tys ++-    (map typ $-      map Normal funs ++-      [ Constructor pred clas_test_case | pred <- funs, Predicate{..} <- [classify pred] ])+    (map typ funs)+      -- 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) =>+  (PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>   [fun] -> Conditionals m a -> m a runConditionals preds mx =   run (mapM_ considerPredicate preds >> mx)@@ -73,42 +61,19 @@   | Function   deriving (Eq, Ord, Functor) +{- data WithConstructor fun =     Constructor fun Type   | Normal fun   deriving (Eq, Ord)--instance Sized fun => Sized (WithConstructor fun) where-  size Constructor{} = 0-  size (Normal f) = size f--instance Pretty fun => Pretty (WithConstructor fun) where-  pPrintPrec l p (Constructor f _) = pPrintPrec l p f <#> text "_con"-  pPrintPrec l p (Normal f) = pPrintPrec l p f--instance PrettyTerm fun => PrettyTerm (WithConstructor fun) where-  termStyle (Constructor _ _) = curried-  termStyle (Normal f) = termStyle f--instance (Predicate fun, Background fun) => Background (WithConstructor fun) where-  background (Normal f) = map (Prop.mapFun Normal) (background f)-  background _ = []--instance Typed fun => Typed (WithConstructor fun) where-  typ (Constructor pred ty) =-    arrowType (typeArgs (typ pred)) ty-  typ (Normal f) = typ f-  otherTypesDL (Constructor pred _) = typesDL pred-  otherTypesDL (Normal f) = otherTypesDL f-  typeSubst_ sub (Constructor pred ty) = Constructor (typeSubst_ sub pred) (typeSubst_ sub ty)-  typeSubst_ sub (Normal f) = Normal (typeSubst_ sub f)+-}  predType :: TyCon -> [Type] -> Type predType name tys =-  Twee.build (Twee.app (Twee.fun name) tys)+  Twee.build (Twee.app (Twee.Sym name) tys)  considerPredicate ::-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  (PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>   fun -> Conditionals m () considerPredicate f =   case classify f of@@ -116,75 +81,14 @@       let         x = Var (V ty 0)         eqns =-          [Fun (Constructor f ty) :@: [Fun (Normal sel) :$: x | sel <- sels] === x,-           Fun (Normal f) :@: [Fun (Normal sel) :$: x | sel <- sels] === fmap Normal true]+          [Fun f :@: [Fun sel :$: x | sel <- sels] === true]       mapM_ (lift . add) eqns     _ -> return ()  considerConditionalising ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>+  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term fun) norm m, Predicate fun, MonadTerminal m) =>   Prop (Term fun) -> Conditionals m ()-considerConditionalising (lhs :=>: t :=: u) = do-  norm <- normaliser-  -- If we have discovered that "somePredicate x_1 x_2 ... x_n = True"-  -- we should add the axiom "get_x_n (toSomePredicate x_1 x_2 ... x_n) = x_n"-  -- to the set of known equations-  case t of-    Fun f :@: ts | Predicate{..} <- classify f -> -- It is an interesting predicate, i.e. it was added by the user-      when (norm u == norm clas_true) $-        addPredicate lhs f ts-    _ -> return ()--conditionallyRedundant ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  Prop (Term fun) -> Conditionals m Bool-conditionallyRedundant (lhs :=>: t :=: u) = do-  t' <- normalise t-  u' <- normalise u-  conditionallyRedundant' lhs t u t' u'--conditionallyRedundant' ::-  (Typed fun, Ord fun, PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  [Equation (Term fun)] -> Term fun -> Term fun -> norm -> norm -> Conditionals m Bool-conditionallyRedundant' lhs t u t' u' = do-  forM_ (usort (funs [t, u])) $ \f ->-    case classify f of-      Selector{..} -> do-        let-          Predicate{..} = classify clas_pred-          tys = typeArgs (typ clas_pred)-          argss = sequence [ [ arg | arg <- terms [t, u] >>= subterms, typ arg == ty ] | ty <- tys ]-        forM_ argss $ \args -> do-          norm <- normaliser-          let p = Fun clas_pred :@: args-          when (norm p == norm clas_true) $ do-            addPredicate lhs clas_pred args-      _ -> return ()--  t'' <- normalise t-  u'' <- normalise u-  if t'' == u'' then-    return True-   else if t'' == t' && u'' == u' then-     return False-    else-     conditionallyRedundant' lhs t u t'' u''--addPredicate ::-  (PrettyTerm fun, Ord norm, MonadPruner (Term (WithConstructor fun)) norm m, Predicate fun, MonadTerminal m) =>-  [Equation (Term fun)] -> fun -> [Term fun] -> Conditionals m ()-addPredicate lhs f ts = do-  let Predicate{..} = classify f-      ts' = map (fmap Normal) ts-      lhs' = map (fmap (fmap Normal)) lhs-      -- The "to_p x1 x2 ... xm" term-      construction = Fun (Constructor f clas_test_case) :@: ts'-      -- The "p_n (to_p x1 x2 ... xn ... xm) = xn"-      -- equations-      equations = [ lhs' :=>: Fun (Normal (clas_selectors !! i)) :$: construction :=: x | (x, i) <- zip ts' [0..]]--  -- Declare the relevant equations as axioms-  mapM_ (lift . add) equations+considerConditionalising (lhs :=>: t :=: u) = return ()  conditionalise :: (PrettyTerm fun, Typed fun, Ord fun, Predicate fun) => Prop (Term fun) -> Prop (Term fun) conditionalise (lhs :=>: t :=: u) =@@ -212,3 +116,4 @@      replaceMany subs t =       foldr (uncurry replace) t subs+
src/QuickSpec/Internal/Explore/Polymorphic.hs view
@@ -173,7 +173,7 @@      genType = Twee.build . aux 0 . Twee.singleton       where-        aux !_ Twee.Empty = mempty+        aux !_ Twee.Nil = mempty         aux n (Twee.Cons (Twee.Var _) ts) =           Twee.var (Twee.V n) `mappend` aux (n+1) ts         aux n (Twee.Cons (Twee.App f ts) us) =
src/QuickSpec/Internal/Explore/Schemas.hs view
@@ -22,7 +22,7 @@ import Data.Set(Set) import Data.Maybe import Control.Monad-import Data.Label+import Data.Intern  -- | Constrains how variables of a particular type may occur in a term. data VariableUse =@@ -157,7 +157,7 @@   -- 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)))+    m = fromIntegral (symId (intern (ty, n)))  -- | Instantiate a schema by making all the variables different. mostGeneral :: (Type -> VariableUse) -> Term f -> Term f
src/QuickSpec/Internal/Haskell.hs view
@@ -65,6 +65,12 @@ import qualified Data.Map.Strict as Map import Test.QuickCheck.Gen import Test.QuickCheck.Random+import Data.IORef+import Control.Monad.IO.Class+import Control.Exception+import QuickSpec.Internal.Parse+import Text.ParserCombinators.ReadP(ReadP, string)+import Data.Hashable  baseInstances :: Instances baseInstances =@@ -403,6 +409,10 @@     comparing $ \con ->       (typeArity (typ con), typ con, con_name con) +instance Hashable Constant where+  hashWithSalt s con =+    s `hashWithSalt` con_name con `hashWithSalt` typ (con_value con)+ instance Background Constant  con :: Typeable a => String -> a -> Constant@@ -479,6 +489,9 @@ instance Sized Constant where   size = con_size +instance FuncSized Constant where+  sizeApp f ts = size f + sum ts+ instance Predicate Constant where   classify = con_classify @@ -617,6 +630,7 @@     cfg_quickCheck :: QuickCheck.Config,     cfg_twee :: Twee.Config,     cfg_max_size :: Int,+    cfg_max_depth :: Int,     cfg_max_commutative_size :: Int,     cfg_max_functions :: Int,     cfg_instances :: Instances,@@ -627,14 +641,17 @@     cfg_default_to :: Type,     cfg_infer_instance_types :: Bool,     cfg_background :: [Prop (Term Constant)],+    cfg_background_str :: [String],     cfg_print_filter :: Prop (Term Constant) -> Bool,     cfg_print_style :: PrintStyle,-    cfg_check_consistency :: Bool+    cfg_check_consistency :: Bool,+    cfg_handle_resource_limit :: Bool     }  lens_quickCheck = lens cfg_quickCheck (\x y -> y { cfg_quickCheck = x }) lens_twee = lens cfg_twee (\x y -> y { cfg_twee = x }) lens_max_size = lens cfg_max_size (\x y -> y { cfg_max_size = x })+lens_max_depth = lens cfg_max_depth (\x y -> y { cfg_max_depth = x }) lens_max_commutative_size = lens cfg_max_commutative_size (\x y -> y { cfg_max_commutative_size = x }) lens_max_functions = lens cfg_max_functions (\x y -> y { cfg_max_functions = x }) lens_instances = lens cfg_instances (\x y -> y { cfg_instances = x })@@ -642,9 +659,11 @@ lens_default_to = lens cfg_default_to (\x y -> y { cfg_default_to = x }) lens_infer_instance_types = lens cfg_infer_instance_types (\x y -> y { cfg_infer_instance_types = x }) lens_background = lens cfg_background (\x y -> y { cfg_background = x })+lens_background_str = lens cfg_background_str (\x y -> y { cfg_background_str = 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 }) lens_check_consistency = lens cfg_check_consistency (\x y -> y { cfg_check_consistency = x })+lens_handle_resource_limit = lens cfg_handle_resource_limit (\x y -> y { cfg_handle_resource_limit = x })  defaultConfig :: Config defaultConfig =@@ -652,6 +671,7 @@     cfg_quickCheck = QuickCheck.Config { QuickCheck.cfg_num_tests = 1000, QuickCheck.cfg_max_test_size = 100, QuickCheck.cfg_fixed_seed = Nothing },     cfg_twee = Twee.Config { Twee.cfg_max_term_size = minBound, Twee.cfg_max_cp_depth = maxBound },     cfg_max_size = 7,+    cfg_max_depth = maxBound,     cfg_max_commutative_size = 5,     cfg_max_functions = maxBound,     cfg_instances = mempty,@@ -659,9 +679,11 @@     cfg_default_to = typeRep (Proxy :: Proxy Int),     cfg_infer_instance_types = False,     cfg_background = [],+    cfg_background_str = [],     cfg_print_filter = \_ -> True,     cfg_print_style = ForHumans,-    cfg_check_consistency = False }+    cfg_check_consistency = False,+    cfg_handle_resource_limit = False }  -- Extra types for the universe that come from in-scope instances. instanceTypes :: Instances -> Config -> [Type]@@ -682,10 +704,10 @@     groundInstances =       [ dict       | -- () :- dict-        Twee.App tc (Twee.Cons (Twee.App unit Twee.Empty) (Twee.Cons dict Twee.Empty)) <-+        Twee.App (Twee.Sym tc) (Twee.Cons (Twee.App (Twee.Sym unit) Twee.Nil) (Twee.Cons dict Twee.Nil)) <-         map (typeRes . typ) (is_instances insts),-        Twee.fun_value tc == tyCon (Proxy :: Proxy (:-)),-        Twee.fun_value unit == tyCon (Proxy :: Proxy (() :: Constraint)),+        tc == tyCon (Proxy :: Proxy (:-)),+        unit == tyCon (Proxy :: Proxy (() :: Constraint)),         Twee.isGround dict ]  data Warnings =@@ -731,6 +753,9 @@  quickSpec :: Config -> IO [Prop (Term Constant)] quickSpec cfg@Config{..} = do+  propNo <- newIORef 1+  props <- newIORef ([] :: [Prop (Term Constant)])+   let     constantsOf f =       usort (concatMap funs $@@ -752,8 +777,8 @@       norm <- normaliser       let prop' = prettierProp funs norm prop       when (not (hasBackgroundPredicates prop') && not (isBackgroundProp prop') && cfg_print_filter prop) $ do-        (n :: Int, props) <- get-        put (n+1, props)+        n <- liftIO $ readIORef propNo+        liftIO $ writeIORef propNo (n+1)         putLine $           case cfg_print_style of             ForHumans ->@@ -795,6 +820,7 @@       sortTerms measure $       filterEnumerator (all constraintsOk . funs) $       filterEnumerator (\t -> length (usort (funs t)) <= cfg_max_functions) $+      filterEnumerator (\t -> depth t <= cfg_max_depth) $       filterEnumerator (\t -> size t + length (conditions t) <= cfg_max_size) $       enumerateConstants atomic `mappend` enumerateApplications       where@@ -819,7 +845,7 @@           putLine "quickspec_laws ="       let         pres prop = do-          modify $ \(k, props) -> (k, prop:props)+          liftIO $ modifyIORef props (prop:)           if n == 0 then return () else present (constantsOf f) prop       QuickSpec.Internal.Explore.quickSpec pres (flip eval) cfg_max_size cfg_max_commutative_size use univ         (enumerator (map Fun (constantsOf g)))@@ -830,11 +856,18 @@     main = do       forM_ cfg_background $ \prop -> do         add prop+      forM_ cfg_background_str $ \prop_str -> do+        add (parseProp parseFun prop_str)+       mapM_ round [0..rounds-1]       where         round n = mainOf n (concat . take 1 . drop n) (concat . take (n+1))         rounds = length cfg_constants +    -- Used in adding background functions from strings+    parseFun :: ReadP Constant+    parseFun = msum [do { string (con_name c); return c } | c <- constants ]+     -- Used in checkConsistency. Generate a term to be used when a     -- Twee proof contains a hole ("?"), i.e. a don't-care variable.     hole ty = do@@ -877,12 +910,22 @@           putLine (printf "  %s is false" (prettyShow (prettiestProp constants norm inst)))         putLine "" -  join $-    fmap withStdioTerminal $-    generate $-    QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $-    Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $-    runConditionals constants $ do-      result <- fmap (reverse . snd) $ flip execStateT (1, []) main-      when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty-      return result+  handleJust (\ex -> if cfg_handle_resource_limit && isResourceLimitException ex then Just () else Nothing) return $+    join $+      fmap withStdioTerminal $+      generate $+      QuickCheck.run cfg_quickCheck (arbitraryTestCase cfg_default_to instances) eval $+      Twee.run cfg_twee { Twee.cfg_max_term_size = Twee.cfg_max_term_size cfg_twee `max` cfg_max_size } $+      runConditionals constants $ do+        main+        when cfg_check_consistency $ void $ execStateT checkConsistency Map.empty++  let maybeConditionalise prop+        | prop == prop' = [prop]+        | otherwise = [prop, prop']+        where prop' = conditionalise prop++  -- Return conditional properties both in conditionalised and raw form.+  -- Raw form is needed if the properties will be passed to addBackground,+  -- but conditionalised is better for other uses.+  concatMap maybeConditionalise . reverse <$> readIORef props
src/QuickSpec/Internal/Haskell/Resolve.hs view
@@ -61,9 +61,9 @@       -- (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)) ->+        App (Sym Arrow) (Cons _ (Cons (App (Sym Arrow) _) Nil)) ->           polyInst (apply uncur x)-        App (F _ Arrow) _ ->+        App (Sym Arrow) _ ->           makeInstances [x]         -- A plain old value x (not a function) turns into \() -> x.         _ ->@@ -94,10 +94,10 @@ -- -- Invariant: the type of the returned value is an instance of the argument type. find_ :: Instances -> Type -> [Value Identity]-find_ _ (App (F _ unit) Empty)+find_ _ (App (Sym unit) Nil)   | unit == tyCon (Proxy :: Proxy ()) =     return (toValue (Identity ()))-find_ insts (App (F _ pair) (Cons ty1 (Cons ty2 Empty)))+find_ insts (App (Sym pair) (Cons ty1 (Cons ty2 Nil)))   | pair == tyCon (Proxy :: Proxy (,)) = do     x <- is_find insts ty1     sub <- maybeToList (match ty1 (typ x))@@ -109,7 +109,7 @@   -- Find a function whose result type unifies with ty.   -- Rename it to avoid clashes with ty.   fun <- fmap (polyRename ty) (is_instances insts)-  App (F _ Arrow) (Cons arg (Cons res Empty)) <- return (typ fun)+  App (Sym Arrow) (Cons arg (Cons res Nil)) <- return (typ fun)   sub <- maybeToList (unify ty res)   fun <- return (typeSubst sub fun)   arg <- return (typeSubst sub arg)
src/QuickSpec/Internal/Parse.hs view
@@ -9,7 +9,7 @@ import QuickSpec.Internal.Prop import QuickSpec.Internal.Term hiding (char) import QuickSpec.Internal.Type-import qualified Data.Label as Label+import qualified Data.Intern as Intern import Text.ParserCombinators.ReadP  class Parse fun a where@@ -20,8 +20,8 @@     x <- satisfy isUpper     xs <- munch isAlphaNum     let name = x:xs-    -- Use Data.Label as an easy way to generate a variable number-    return (V typeVar (fromIntegral (Label.labelNum (Label.label name))))+    -- Use Data.Intern as an easy way to generate a variable number+    return (V typeVar (fromIntegral (Intern.symId (Intern.intern name))))  instance (fun1 ~ fun, Apply (Term fun)) => Parse fun1 (Term fun) where   parse pfun =
src/QuickSpec/Internal/Prop.hs view
@@ -48,6 +48,14 @@   where     both f (t :=: u) = f t :=: f u +mapTermM :: Monad m => (Term fun1 -> m (Term fun2)) -> Prop (Term fun1) -> m (Prop (Term fun2))+mapTermM f (lhs :=>: rhs) = do+  lhs <- mapM (both f) lhs+  rhs <- both f rhs+  return (lhs :=>: rhs)+  where+    both f (t :=: u) = liftM2 (:=:) (f t) (f u)+ instance Typed a => Typed (Prop a) where   typ _ = typeOf True   otherTypesDL p = DList.fromList (literals p) >>= typesDL
+ src/QuickSpec/Internal/Pruning/Conditionals.hs view
@@ -0,0 +1,102 @@+-- Encode conditionals during pruning.+{-# OPTIONS_HADDOCK hide #-}+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances, DeriveGeneric #-}+module QuickSpec.Internal.Pruning.Conditionals where++import QuickSpec.Internal.Pruning+import QuickSpec.Internal.Pruning.Background(Background(..))+import QuickSpec.Internal.Testing+import QuickSpec.Internal.Term+import QuickSpec.Internal.Type+import QuickSpec.Internal.Prop hiding (mapFun)+import QuickSpec.Internal.Terminal+import QuickSpec.Internal.Utils+import Control.Monad.IO.Class+import Control.Monad.Trans.Class+import GHC.Generics+import Data.Hashable+import Data.Hashable.Generic++data Conditionals fun =+    Func fun+  | Guard Type (UnconditionalTerm fun) (UnconditionalTerm fun) (UnconditionalTerm fun) (UnconditionalTerm fun) [Var]+  deriving (Eq, Ord, Show, Typeable, Generic)++instance Hashable fun => Hashable (Conditionals fun) where+  hashWithSalt = genericHashWithSalt++instance Arity fun => Arity (Conditionals fun) where+  arity (Func f) = arity f+  arity (Guard _ _ _ _ _ vs) = length vs + 1++instance Sized fun => Sized (Conditionals fun) where+  size (Func f) = size f+  size Guard{} = 0++instance Sized fun => FuncSized (Conditionals fun) where+  -- Note: since there is no FuncSized instance for PartiallyApplied+  -- we just assume that Func f is adding the size of its arguments+  sizeApp (Func f) ts = size f + sum ts+  sizeApp Guard{} ts = penalty + maximum ts+    where+      penalty = 3++instance Pretty fun => Pretty (Conditionals fun) where+  pPrint (Func f) = pPrint f+  pPrint Guard{} = text "guard"++instance PrettyTerm fun => PrettyTerm (Conditionals fun) where+  termStyle (Func f) = termStyle f+  termStyle Guard{} = uncurried++instance Typed fun => Typed (Conditionals fun) where+  typ (Func f) = typ f+  typ (Guard ty t _ _ _ vs) = arrowType (typ t:map typ vs) ty++  typeSubst_ sub (Func f) = Func (typeSubst_ sub f)+  typeSubst_ sub (Guard ty t u v w vs) = Guard (typeSubst_ sub ty) (typeSubst_ sub t) (typeSubst_ sub u) (typeSubst_ sub v) (typeSubst_ sub w) (typeSubst_ sub vs)++instance EqualsBonus (Conditionals fun) where++type ConditionalTerm fun = Term fun+type UnconditionalTerm fun = Term (Conditionals fun)++newtype Pruner fun pruner a =+  Pruner { run :: pruner a }+  deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term, MonadTerminal)++instance MonadTrans (Pruner fun) where+  lift = Pruner++instance (PrettyTerm fun, Typed fun, MonadPruner (UnconditionalTerm fun) norm pruner) => MonadPruner (ConditionalTerm fun) norm (Pruner fun pruner) where+  normaliser =+    Pruner $ do+      norm <- normaliser :: pruner (UnconditionalTerm fun -> norm)++      return $ \t ->+        norm . mapFun Func $ t++  add prop = and <$> lift (mapM add (conditionalise' (canonicalise prop)))++  decodeNormalForm hole t =+    Pruner $ do+      t <- decodeNormalForm (fmap (fmap Func) . hole) t+      let elimIfEq (Func f) = Just f+          elimIfEq Guard{} = Nothing+      return $ t >>= mapFunM elimIfEq++instance (Typed fun, Arity fun, Background fun) => Background (Conditionals fun) where+  background (Func f) = concatMap conditionalise' (background f)+  background Guard{} = []++conditionalise :: Typed fun => Prop (UnconditionalTerm fun) -> [Prop (UnconditionalTerm fun)]+conditionalise prop@([] :=>: _) = [prop]+conditionalise ((t :=: u):lhs :=>: v :=: w) =+  ([] :=>: guarded t v):conditionalise (lhs :=>: guarded u w)+  where+    guarded x y = Fun (Guard ty t u v w vs) :@: (x:map Var vs) :=: y+    vs = usort (concatMap vars [t, u, v, w])+    ty = typ t++conditionalise' :: Typed fun => Prop (ConditionalTerm fun) -> [Prop (UnconditionalTerm fun)]+conditionalise' = conditionalise . mapTerm (mapFun Func)
src/QuickSpec/Internal/Pruning/PartialApplication.hs view
@@ -1,6 +1,6 @@ -- Pruning support for partial application and the like. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor #-}+{-# LANGUAGE FlexibleInstances, TypeSynonymInstances, RecordWildCards, MultiParamTypeClasses, FlexibleContexts, GeneralizedNewtypeDeriving, UndecidableInstances, DeriveFunctor, DeriveGeneric #-} module QuickSpec.Internal.Pruning.PartialApplication where  import QuickSpec.Internal.Term as Term@@ -12,6 +12,9 @@ import QuickSpec.Internal.Testing import Control.Monad.IO.Class import Control.Monad.Trans.Class+import GHC.Generics+import Data.Hashable+import Data.Hashable.Generic  data PartiallyApplied f =     -- A partially-applied function symbol.@@ -20,7 +23,10 @@     -- The ($) operator, for oversaturated applications.     -- The type argument is the type of the first argument to ($).   | Apply Type-  deriving (Eq, Ord, Functor)+  deriving (Eq, Ord, Functor, Generic)++instance Hashable f => Hashable (PartiallyApplied f) where+  hashWithSalt = genericHashWithSalt  instance Sized f => Sized (PartiallyApplied f) where   size (Partial f _) = size f
src/QuickSpec/Internal/Pruning/Twee.hs view
@@ -15,17 +15,19 @@ import Control.Monad.Trans.Class import Control.Monad.IO.Class import qualified QuickSpec.Internal.Pruning.UntypedTwee as Untyped+import qualified QuickSpec.Internal.Pruning.Conditionals as Conditionals+import QuickSpec.Internal.Pruning.Conditionals(Conditionals) import QuickSpec.Internal.Pruning.UntypedTwee(Config(..))-import Data.Typeable+import Data.Intern  newtype Pruner fun m a =-  Pruner (PartialApplication.Pruner fun (Types.Pruner (PartiallyApplied fun) (Background.Pruner (Tagged (PartiallyApplied fun)) (Untyped.Pruner (Tagged (PartiallyApplied fun)) m))) a)+  Pruner (PartialApplication.Pruner fun (Conditionals.Pruner (PartiallyApplied fun) (Types.Pruner (Conditionals (PartiallyApplied fun)) (Background.Pruner (Tagged (Conditionals (PartiallyApplied fun))) (Untyped.Pruner (Tagged (Conditionals (PartiallyApplied fun))) m)))) a)   deriving (Functor, Applicative, Monad, MonadIO, MonadTester testcase term,-            MonadPruner (Term fun) (Untyped.Norm (Tagged (PartiallyApplied fun))), MonadTerminal)+            MonadPruner (Term fun) (Untyped.Norm (Tagged (Conditionals (PartiallyApplied fun)))), MonadTerminal)  instance MonadTrans (Pruner fun) where-  lift = Pruner . lift . lift . lift . lift+  lift = Pruner . lift . lift . lift . lift . lift -run :: (Sized fun, Typeable fun, Ord fun, Monad m) => Config -> Pruner fun m a -> m a+run :: (Sized fun, Intern fun, Ord fun, PrettyTerm fun, Monad m) => Config -> Pruner fun m a -> m a run config (Pruner x) =-  Untyped.run config (Background.run (Types.run (PartialApplication.run x)))+  Untyped.run config (Background.run (Types.run (Conditionals.run (PartialApplication.run x))))
src/QuickSpec/Internal/Pruning/Types.hs view
@@ -1,6 +1,6 @@ -- Encode monomorphic types during pruning. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances #-}+{-# LANGUAGE FlexibleInstances, GeneralizedNewtypeDeriving, MultiParamTypeClasses, FlexibleContexts, ScopedTypeVariables, UndecidableInstances, DeriveGeneric #-} module QuickSpec.Internal.Pruning.Types where  import QuickSpec.Internal.Pruning@@ -12,12 +12,18 @@ import QuickSpec.Internal.Terminal import Control.Monad.IO.Class import Control.Monad.Trans.Class+import GHC.Generics+import Data.Hashable+import Data.Hashable.Generic  data Tagged fun =     Func fun   | Tag Type-  deriving (Eq, Ord, Show, Typeable)+  deriving (Eq, Ord, Show, Typeable, Generic) +instance Hashable fun => Hashable (Tagged fun) where+  hashWithSalt = genericHashWithSalt+ instance Arity fun => Arity (Tagged fun) where   arity (Func f) = arity f   arity (Tag _) = 1@@ -25,6 +31,10 @@ instance Sized fun => Sized (Tagged fun) where   size (Func f) = size f   size (Tag _) = 0++instance FuncSized fun => FuncSized (Tagged fun) where+  sizeApp (Func f) ts = sizeApp f ts+  sizeApp (Tag t) ts = sum ts  instance Pretty fun => Pretty (Tagged fun) where   pPrint (Func f) = pPrint f
src/QuickSpec/Internal/Pruning/UntypedTwee.hs view
@@ -1,6 +1,6 @@ -- A pruner that uses twee. Does not respect types. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances #-}+{-# LANGUAGE RecordWildCards, FlexibleContexts, FlexibleInstances, GADTs, PatternSynonyms, GeneralizedNewtypeDeriving, MultiParamTypeClasses, UndecidableInstances, DeriveGeneric #-} module QuickSpec.Internal.Pruning.UntypedTwee where  import QuickSpec.Internal.Testing@@ -16,7 +16,7 @@ import Twee hiding (Config(..)) import Twee.Rule hiding (normalForms) import Twee.Proof hiding (Config, defaultConfig)-import Twee.Base(Ordered(..), Labelled)+import Twee.Base(Ordered(..)) import Control.Monad.Trans.Reader import Control.Monad.Trans.State.Strict hiding (State) import Control.Monad.Trans.Class@@ -27,6 +27,9 @@ import qualified Data.Map.Strict as Map import qualified Data.IntMap as IntMap import Control.Monad+import GHC.Generics+import Data.Hashable+import Data.Hashable.Generic  data Config =   Config {@@ -37,37 +40,42 @@ lens_max_cp_depth = lens cfg_max_cp_depth (\x y -> y { cfg_max_cp_depth = x })  data Extended fun = Minimal | Skolem Twee.Var | Function fun-  deriving (Eq, Ord, Typeable)+  deriving (Eq, Ord, Typeable, Generic) -instance (Ord fun, Typeable fun) => Labelled (Extended fun)+instance Hashable fun => Hashable (Extended fun) where+  hashWithSalt = genericHashWithSalt  instance Sized fun => Sized (Extended fun) where   size (Function f) = size f   size _ = 1+  --sizeMode (Function f) = sizeMode f+  --sizeMode _ = AddArgs +instance FuncSized fun => FuncSized (Extended fun) where+  sizeApp (Function f) ts = sizeApp f ts+  sizeApp _ [] = 1++instance Twee.Weighted (Extended fun)+instance KBO.ArgWeighted fun where+  argWeight _ = 1 instance KBO.Sized (Extended fun) where   size _ = 1 -instance Arity fun => Arity (Extended fun) where-  arity (Function f) = arity f-  arity (Skolem _) = 0-  arity Minimal = 0--instance (Ord fun, Typeable fun) => Twee.Minimal (Extended fun) where-  minimal = Twee.fun Minimal+instance Twee.Intern fun => Twee.Minimal (Extended fun) where+  minimal = Twee.Sym Minimal+  skolem = Twee.Sym . Skolem . Twee.V  instance EqualsBonus (Extended fun)--instance (Ord fun, Typeable fun, Pretty fun) => Pretty (Extended fun) where+instance (Twee.Intern fun, Pretty fun) => Pretty (Extended fun) where   pPrintPrec l p (Function f) = pPrintPrec l p f   pPrintPrec _ _ Minimal = text "?"   pPrintPrec _ _ (Skolem (Twee.V x)) = text ("sk" ++ show x) -instance (Ord fun, Typeable fun, PrettyTerm fun) => PrettyTerm (Extended fun) where+instance (Twee.Intern fun, PrettyTerm fun) => PrettyTerm (Extended fun) where   termStyle (Function f) = termStyle f   termStyle _ = curried -instance (Sized fun, Pretty fun, PrettyTerm fun, Ord fun, Typeable fun, Arity fun, EqualsBonus fun) => Ordered (Extended fun) where+instance (Ord fun, Pretty fun, PrettyTerm fun, Twee.Intern fun) => Ordered (Extended fun) where   lessEq = KBO.lessEq   lessIn = KBO.lessIn   lessEqSkolem = KBO.lessEqSkolem@@ -79,26 +87,23 @@ instance MonadTrans (Pruner fun) where   lift = Pruner . lift . lift -run :: (Typeable fun, Ord fun, Sized fun, Monad m) => Config -> Pruner fun m a -> m a+run :: (Twee.Intern fun, Ord fun, PrettyTerm fun, FuncSized fun, Monad m) => Config -> Pruner fun m a -> m a run Config{..} (Pruner x) =   evalStateT (runReaderT x config) (initialState config)   where     config =       defaultConfig {-        Twee.cfg_accept_term = Just (\t -> size t <= cfg_max_term_size),+        Twee.cfg_accept_term = Just (\t -> termSize t <= cfg_max_term_size),         Twee.cfg_max_cp_depth = cfg_max_cp_depth } -instance (Labelled fun, 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 KBO.Weighted (Extended fun) where-  argWeight _ = 1+termSize :: (Twee.Intern fun, FuncSized fun) => Twee.Term fun -> Int+termSize (Twee.Var _) = 1+termSize (Twee.App (Twee.Sym f) ts) =+  sizeApp f (map termSize (Twee.unpack ts))  type Norm fun = Twee.Term (Extended fun) -instance (Ord fun, Typed fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>+instance (Ord fun, Typed fun, Twee.Intern fun, PrettyTerm fun, EqualsBonus fun, Sized fun, Monad m) =>   MonadPruner (Term fun) (Norm fun) (Pruner fun m) where   normaliser = Pruner $ do     state <- lift get@@ -125,11 +130,11 @@     where       decode (Twee.Var (Twee.V n)) ty =         Just (Var (V ty n))-      decode (Twee.App (Twee.F _ Minimal) Twee.Empty) ty =+      decode (Twee.App (Twee.Sym Minimal) Twee.Nil) ty =         hole ty-      decode (Twee.App (Twee.F _ (Skolem (Twee.V n))) Twee.Empty) ty =+      decode (Twee.App (Twee.Sym (Skolem (Twee.V n))) Twee.Nil) ty =         Just (Var (V ty n))-      decode (Twee.App (Twee.F _ (Function f)) ts) _ =+      decode (Twee.App (Twee.Sym (Function f)) ts) _ =         (Fun f :@:) <$> zipWithM decode (Twee.unpack ts) args         where           args = typeArgs (typ f)@@ -153,19 +158,19 @@      return (map toTheorem actives) -normaliseTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>+normaliseTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   State (Extended fun) -> Term fun -> Norm fun normaliseTwee state t =   result u (normaliseTerm state u)   where     u = simplifyTerm state (skolemise t) -normalFormsTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>+normalFormsTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   State (Extended fun) -> Term fun -> Set (Norm fun) normalFormsTwee state t =   Set.fromList . Map.elems $ Map.mapWithKey result (normalForms state (skolemise t)) -addTwee :: (Ord fun, Typeable fun, Arity fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>+addTwee :: (Twee.Intern fun, Ord fun, PrettyTerm fun, EqualsBonus fun, Sized fun) =>   Twee.Config (Extended fun) -> Term fun -> Term fun -> State (Extended fun) -> State (Extended fun) addTwee config t u state =   interreduce config $@@ -174,22 +179,22 @@   where     axiom = Axiom 0 (prettyShow (t :=: u)) (toTwee t Twee.:=: toTwee u) -toTwee :: (Ord f, Typeable f) =>+toTwee :: (Ord f, Twee.Intern f) =>   Term f -> Twee.Term (Extended f) toTwee = Twee.build . tt   where     tt (Var (V _ x)) =       Twee.var (Twee.V x)     tt (Fun f :@: ts) =-      Twee.app (Twee.fun (Function f)) (map tt ts)+      Twee.app (Twee.Sym (Function f)) (map tt ts)     tt _ = error "partially applied term" -skolemise :: (Ord f, Typeable f) =>+skolemise :: (Ord f, Twee.Intern f) =>   Term f -> Twee.Term (Extended f) skolemise = Twee.build . sk   where     sk (Var (V _ x)) =-      Twee.con (Twee.fun (Skolem (Twee.V x)))+      Twee.con (Twee.Sym (Skolem (Twee.V x)))     sk (Fun f :@: ts) =-      Twee.app (Twee.fun (Function f)) (map sk ts)+      Twee.app (Twee.Sym (Function f)) (map sk ts)     sk _ = error "partially applied term"
src/QuickSpec/Internal/Term.hs view
@@ -18,15 +18,15 @@ import Data.Map(Map) import Data.List import Data.Ord-import Data.Maybe+import Data.Hashable  -- | A typed term. data Term f = Var {-# UNPACK #-} !Var | Fun !f | !(Term f) :$: !(Term f)-  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)+  deriving (Eq, Ord, Show, Functor, Foldable, Traversable, Generic, Hashable)  -- | A variable, which has a type and a number. data Var = V { var_ty :: !Type, var_id :: {-# UNPACK #-} !Int }-  deriving (Eq, Ord, Show, Generic)+  deriving (Eq, Ord, Show, Generic, Hashable)  instance CoArbitrary Var where   coarbitrary = coarbitrary . var_id@@ -87,16 +87,16 @@ class Sized a where   size :: a -> Int -instance Sized f => Sized (Term f) where+class FuncSized a where+  sizeApp :: a -> [Int] -> Int++instance FuncSized f => Sized (Term f) where   size (Var _) = 1-  size (Fun f) = size f-  size (t :$: u) =-    size t + size u ++  size (Var _ :@: ts) =     -- Penalise applied function variables, because they can be used     -- to build many many terms without any constants at all-    case t of-      Var _ -> 1-      _ -> 0+    2 + sum (map size ts)+  size (Fun f :@: ts) = sizeApp f (map size ts)  instance Pretty Var where   pPrint x = parens $ text "X" <#> pPrint (var_id x+1) <+> text "::" <+> pPrint (var_ty x)@@ -157,6 +157,12 @@ mapFun f (t :$: u) = mapFun f t :$: mapFun f u  -- | Map a function over function symbols.+mapFunM :: Monad m => (f -> m g) -> Term f -> m (Term g)+mapFunM _ (Var x) = return (Var x)+mapFunM f (Fun x) = Fun <$> f x+mapFunM f (t :$: u) = liftM2 (:$:) (mapFunM f t) (mapFunM f u)++-- | Map a function over function symbols. flatMapFun :: (f -> Term g) -> Term f -> Term g flatMapFun _ (Var x) = Var x flatMapFun f (Fun x) = f x@@ -251,7 +257,7 @@ -- if measure (schema t) < measure (schema u) then t < u. 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 :: (FuncSized f, Typed f) => Term f -> Measure f measure t =   (depth t, size t, missing t, -length (vars t), MeasureFuns (skel t),    -length (usort (vars t)), vars t)@@ -296,6 +302,10 @@ instance (Sized fun1, Sized fun2) => Sized (fun1 :+: fun2) where   size (Inl x) = size x   size (Inr x) = size x++instance (FuncSized fun1, FuncSized fun2) => FuncSized (fun1 :+: fun2) where+  sizeApp (Inl x) = sizeApp x+  sizeApp (Inr x) = sizeApp x  instance (Typed fun1, Typed fun2) => Typed (fun1 :+: fun2) where   typ (Inl x) = typ x
src/QuickSpec/Internal/Type.hs view
@@ -39,6 +39,8 @@ import Data.List hiding (singleton) import Data.Char import Data.Functor.Identity+import Data.Intern+import Data.Hashable  -- | A (possibly polymorphic) type. type Type = Term TyCon@@ -54,7 +56,10 @@   | String String   deriving (Eq, Ord, Show, Typeable) -instance Labelled TyCon+instance Hashable TyCon where+  hashWithSalt s Arrow = s `hashWithSalt` (0 :: Int)+  hashWithSalt s (TyCon tc) = s `hashWithSalt` (1 :: Int) `hashWithSalt` Ty.tyConFingerprint tc+  hashWithSalt s (String xs) = s `hashWithSalt` (2 :: Int) `hashWithSalt` xs  instance Pretty TyCon where   pPrint Arrow = text "->"@@ -79,6 +84,8 @@     | take 2 (show con) == "(," ||       take 3 (show con) == "(%," =       fixedArity (1+length (filter (== ',') (show con))) tupleStyle+    | Just n <- Data.List.lookup con tupleTyCons =+      fixedArity n tupleStyle     | isAlphaNum (head (show con)) = curried     | otherwise = infixStyle 5 @@ -139,7 +146,7 @@  -- | Turn a `TyCon` into a type. typeFromTyCon :: TyCon -> Type-typeFromTyCon tc = build (con (fun tc))+typeFromTyCon tc = build (con (Sym tc))  -- | Function application for type constructors. --@@ -152,7 +159,7 @@ arrowType :: [Type] -> Type -> Type arrowType [] res = res arrowType (arg:args) res =-  build (app (fun Arrow) [arg, arrowType args res])+  build (app (Sym Arrow) [arg, arrowType args res])  -- | Is a given type a function type? isArrowType :: Type -> Bool@@ -162,20 +169,20 @@ -- -- For multiple-argument functions, unpacks one argument. unpackArrow :: Type -> Maybe (Type, Type)-unpackArrow (App (F _ Arrow) (Cons t (Cons u Empty))) =+unpackArrow (App (Sym Arrow) (Cons t (Cons u Nil))) =   Just (t, u) unpackArrow _ =   Nothing  -- | The arguments of a function type. typeArgs :: Type -> [Type]-typeArgs (App (F _ Arrow) (Cons arg (Cons res Empty))) =+typeArgs (App (Sym Arrow) (Cons arg (Cons res Nil))) =   arg:typeArgs res typeArgs _ = []  -- | The result of a function type. typeRes :: Type -> Type-typeRes (App (F _ Arrow) (Cons _ (Cons res Empty))) =+typeRes (App (Sym Arrow) (Cons _ (Cons res Nil))) =   typeRes res typeRes ty = ty @@ -183,7 +190,7 @@ -- @n@ arguments. Crashes if the type does not have enough arguments. typeDrop :: Int -> Type -> Type typeDrop 0 ty = ty-typeDrop n (App (F _ Arrow) (Cons _ (Cons ty Empty))) =+typeDrop n (App (Sym Arrow) (Cons _ (Cons ty Nil))) =   typeDrop (n-1) ty typeDrop _ _ =   error "typeDrop on non-function type"@@ -205,7 +212,7 @@ skolemiseTypeVars :: Typed a => a -> a skolemiseTypeVars = typeSubst (const aTy)   where-    aTy = build (con (fun (tyCon (Proxy :: Proxy A))))+    aTy = build (con (Sym (tyCon (Proxy :: Proxy A))))  -- | Construct a type from a `Ty.TypeRep`. fromTypeRep :: Ty.TypeRep -> Type@@ -214,7 +221,7 @@       build (var (V n))   | otherwise =     let (tyCon, tys) = Ty.splitTyConApp ty in-    build (app (fun (fromTyCon tyCon)) (map fromTypeRep tys))+    build (app (Sym (fromTyCon tyCon)) (map fromTypeRep tys))  -- | Construct a `TyCon` type from a "Data.Typeable" `Ty.TyCon`. fromTyCon :: Ty.TyCon -> TyCon@@ -223,11 +230,19 @@   | otherwise = TyCon ty  -- | Some built-in type consructors.-arrowTyCon, commaTyCon, listTyCon, dictTyCon :: Ty.TyCon+arrowTyCon, unitTyCon, tuple2TyCon, tuple3TyCon, tuple4TyCon, tuple5TyCon, tuple6TyCon, tuple7TyCon, listTyCon, dictTyCon :: Ty.TyCon arrowTyCon = mkCon (Proxy :: Proxy (->))-commaTyCon = mkCon (Proxy :: Proxy (,))+unitTyCon = mkCon (Proxy :: Proxy ())+tuple2TyCon = mkCon (Proxy :: Proxy (,))+tuple3TyCon = mkCon (Proxy :: Proxy (,,))+tuple4TyCon = mkCon (Proxy :: Proxy (,,,))+tuple5TyCon = mkCon (Proxy :: Proxy (,,,,))+tuple6TyCon = mkCon (Proxy :: Proxy (,,,,,))+tuple7TyCon = mkCon (Proxy :: Proxy (,,,,,,)) listTyCon  = mkCon (Proxy :: Proxy []) dictTyCon  = mkCon (Proxy :: Proxy Dict)+tupleTyCons :: [(Ty.TyCon, Int)]+tupleTyCons = [(unitTyCon, 0), (tuple2TyCon, 2), (tuple3TyCon, 3), (tuple4TyCon, 4), (tuple5TyCon, 5), (tuple6TyCon, 6), (tuple7TyCon, 7)]  mkCon :: Typeable a => proxy a -> Ty.TyCon mkCon = fst . Ty.splitTyConApp . Ty.typeRep@@ -238,7 +253,7 @@  -- | 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))+getDictionary (App (Sym (TyCon dict)) (Cons ty Nil))   | dict == dictTyCon = Just ty getDictionary _ = Nothing @@ -261,16 +276,16 @@ instance CoArbitrary Type where   coarbitrary = coarbitrary . singleton instance CoArbitrary (TermList TyCon) where-  coarbitrary Empty = variant 0+  coarbitrary Nil = variant 0   coarbitrary ConsSym{hd = Var (V x), rest = ts} =     variant 1 . coarbitrary x . coarbitrary ts   coarbitrary ConsSym{hd = App f _, rest = ts} =-    variant 2 . coarbitrary (fun_id f) . coarbitrary ts+    variant 2 . coarbitrary (symId f) . coarbitrary ts  -- | Pretty-print a type. Differs from the `Pretty` instance by printing type -- variables in lowercase. pPrintType :: Type -> Doc-pPrintType = ppr . typeSubst (\(V x) -> build (con (fun (String (as !! x))))) . canonicalise+pPrintType = ppr . typeSubst (\(V x) -> build (con (Sym (String (as !! x))))) . canonicalise   where     as = supply [[x] | x <- ['a'..'z']]     -- Print dictionary arguments specially@@ -358,12 +373,12 @@   typeSubst_ = subst  instance Apply Type where-  tryApply (App (F _ Arrow) (Cons arg (Cons res Empty))) t+  tryApply (App (Sym Arrow) (Cons arg (Cons res Nil))) t     | t == arg = Just res   tryApply _ _ = Nothing  instance (Typed a, Typed b) => Typed (a, b) where-  typ (x, y) = build (app (fun (TyCon commaTyCon)) [typ x, typ y])+  typ (x, y) = build (app (Sym (TyCon tuple2TyCon)) [typ x, typ y])   otherTypesDL (x, y) = otherTypesDL x `mplus` otherTypesDL y   typeSubst_ f (x, y) = (typeSubst_ f x, typeSubst_ f y)
src/QuickSpec/Internal/Utils.hs view
@@ -1,6 +1,6 @@ -- | Miscellaneous utility functions. {-# OPTIONS_HADDOCK hide #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE CPP, ScopedTypeVariables #-} module QuickSpec.Internal.Utils where  import Control.Arrow((&&&))@@ -20,6 +20,7 @@ import Twee.Base hiding (lookup) import Control.Monad.Trans.State.Strict import Control.Monad+import Data.Typeable  (#) :: Category.Category cat => cat b c -> cat a b -> cat a c (#) = (Category..)@@ -136,3 +137,18 @@       | otherwise = fxp y       where         y = f x++isResourceLimitException :: SomeException -> Bool+isResourceLimitException ex =+  fromException ex == Just StackOverflow ||+  fromException ex == Just HeapOverflow ||+  isTimeout ex ||+  case fromException ex of+    Just (SomeAsyncException ex) -> isResourceLimitException (SomeException ex)+    Nothing -> False+  where+    -- The Timeout type wasn't exported until GHC 8.10,+    -- otherwise we could just do:+    -- isJust (fromException ex :: Maybe Timeout)+    isTimeout (SomeException ex) =+      tyConModule (typeRepTyCon (typeOf ex)) == "System.Timeout"