diff --git a/.github/workflows/haskell-ci.yml b/.github/workflows/haskell-ci.yml index 1fdaa76..e10b883 100644 --- a/.github/workflows/haskell-ci.yml +++ b/.github/workflows/haskell-ci.yml @@ -23,6 +23,18 @@ concurrency: cancel-in-progress: true jobs: + check-formatting: + name: Check formatting + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: install fourmolu + run: | + wget https://github.com/fourmolu/fourmolu/releases/download/v0.17.0.0/fourmolu-0.17.0.0-linux-x86_64 + chmod +x fourmolu-0.17.0.0-linux-x86_64 + mv fourmolu-0.17.0.0-linux-x86_64 fourmolu + - run: ./fourmolu -c . + test-with-cabal: name: Haskell-CI - Linux - ${{ matrix.ghc-version }} diff --git a/bench/Constrained/Bench.hs b/bench/Constrained/Bench.hs index 93b4745..a3010ba 100644 --- a/bench/Constrained/Bench.hs +++ b/bench/Constrained/Bench.hs @@ -10,11 +10,10 @@ module Constrained.Bench where import Constrained.API -import Constrained.Generation -import Constrained.Examples.Set -import Constrained.Examples.Map import Constrained.Examples.Basic - +import Constrained.Examples.Map +import Constrained.Examples.Set +import Constrained.Generation import Control.DeepSeq import Criterion import Data.Map (Map) diff --git a/examples/Constrained/Examples/Basic.hs b/examples/Constrained/Examples/Basic.hs index fda7fbe..05f2a4f 100644 --- a/examples/Constrained/Examples/Basic.hs +++ b/examples/Constrained/Examples/Basic.hs @@ -346,23 +346,24 @@ manyInconsistentTrans = constrained' $ \ [var| a |] [var| b |] c d e [var| f |] complicatedEither :: Specification (Either Int Int, (Either Int Int, Int, Int)) complicatedEither = constrained' $ \ [var| i |] [var| t |] -> - [ caseOn i - (branch $ \ a -> a `elem_` lit [1..10]) - (branch $ \ b -> b `elem_` lit [1..10]) + [ caseOn + i + (branch $ \a -> a `elem_` lit [1 .. 10]) + (branch $ \b -> b `elem_` lit [1 .. 10]) , match t $ \ [var| k |] _ _ -> - [ k ==. i - , not_ $ k `elem_` lit [ Left j | j <- [1..9] ] - ] + [ k ==. i + , not_ $ k `elem_` lit [Left j | j <- [1 .. 9]] + ] ] pairCant :: Specification (Int, (Int, Int)) pairCant = constrained' $ \ [var| i |] [var| p |] -> - [ assert $ i `elem_` lit [1..10] + [ assert $ i `elem_` lit [1 .. 10] , match p $ \ [var| k |] _ -> - [ k ==. i - , not_ $ k `elem_` lit [1..9] - ] + [ k ==. i + , not_ $ k `elem_` lit [1 .. 9] + ] ] signumPositive :: Specification Rational -signumPositive = constrained $ \ x -> signum (x * 30) >=. 1 +signumPositive = constrained $ \x -> signum (x * 30) >=. 1 diff --git a/examples/Constrained/Examples/Fold.hs b/examples/Constrained/Examples/Fold.hs index 804b25d..a29eb64 100644 --- a/examples/Constrained/Examples/Fold.hs +++ b/examples/Constrained/Examples/Fold.hs @@ -36,10 +36,10 @@ evenSpec = explainSpec ["even via (x+x)"] $ (\ [var|somey|] -> [assert $ evenx ==. somey + somey]) composeEvenSpec :: Specification Int -composeEvenSpec = constrained $ \ x -> [satisfies x evenSpec, assert $ x >. 10] +composeEvenSpec = constrained $ \x -> [satisfies x evenSpec, assert $ x >. 10] composeOddSpec :: Specification Int -composeOddSpec = constrained $ \ x -> [satisfies x oddSpec, assert $ x >. 10] +composeOddSpec = constrained $ \x -> [satisfies x oddSpec, assert $ x >. 10] sum3WithLength :: Integer -> Specification ([Int], Int, Int, Int) sum3WithLength n = diff --git a/examples/Constrained/Examples/Map.hs b/examples/Constrained/Examples/Map.hs index 0cbaba6..1f899e7 100644 --- a/examples/Constrained/Examples/Map.hs +++ b/examples/Constrained/Examples/Map.hs @@ -128,24 +128,27 @@ mapIsJust = constrained' $ \ [var| x |] [var| y |] -> eitherKeys :: Specification ([Int], [Int], Map (Either Int Int) Int) eitherKeys = constrained' $ \ [var| as |] [var| bs |] [var| m |] -> - [ - forAll' m $ \ [var| k |] _v -> - [ caseOn k - (branch $ \ a -> a `elem_` as) - (branch $ \ b -> b `elem_` bs) - , reify as (map Left) $ \ ls -> - reify bs (map Right) $ \ rs -> - k `elem_` ls ++. rs + [ forAll' m $ \ [var| k |] _v -> + [ caseOn + k + (branch $ \a -> a `elem_` as) + (branch $ \b -> b `elem_` bs) + , reify as (map Left) $ \ls -> + reify bs (map Right) $ \rs -> + k `elem_` ls ++. rs ] ] keysExample :: Specification (Either Int Int) -keysExample = constrained $ \ k -> - [ caseOn k - (branch $ \ a -> a `elem_` as) - (branch $ \ b -> b `elem_` bs) - , reify as (map Left) $ \ ls -> - reify bs (map Right) $ \ rs -> - k `elem_` ls ++. rs - ] where as = lit [ 1 .. 10] - bs = lit [ 11 .. 20 ] +keysExample = constrained $ \k -> + [ caseOn + k + (branch $ \a -> a `elem_` as) + (branch $ \b -> b `elem_` bs) + , reify as (map Left) $ \ls -> + reify bs (map Right) $ \rs -> + k `elem_` ls ++. rs + ] + where + as = lit [1 .. 10] + bs = lit [11 .. 20] diff --git a/fourmolu.yaml b/fourmolu.yaml new file mode 100644 index 0000000..6a9d739 --- /dev/null +++ b/fourmolu.yaml @@ -0,0 +1,16 @@ +indentation: 2 +function-arrows: trailing +comma-style: leading +import-export-style: diff-friendly +indent-wheres: true +record-brace-space: true +newlines-between-decls: 1 +haddock-style: single-line +haddock-style-module: +let-style: auto +in-style: right-align +unicode: never +respectful: false +fixities: [] +single-constraint-parens: never +column-limit: 100 diff --git a/scripts/fourmolize.sh b/scripts/fourmolize.sh new file mode 100755 index 0000000..34d1739 --- /dev/null +++ b/scripts/fourmolize.sh @@ -0,0 +1 @@ +fourmolu -i . diff --git a/src/Constrained/Base.hs b/src/Constrained/Base.hs index 74db146..4e491bc 100644 --- a/src/Constrained/Base.hs +++ b/src/Constrained/Base.hs @@ -32,7 +32,7 @@ module Constrained.Base ( pattern (:<:), pattern (:>:), pattern Unary, - Ctx(..), + Ctx (..), toCtx, flipCtx, fromListCtx, @@ -675,7 +675,7 @@ instance Show (BaseW d r) where show ToGenericW = "toSimpleRep" show FromGenericW = "fromSimpleRep" -instance Syntax BaseW where +instance Syntax BaseW instance Semantics BaseW where semantics FromGenericW = fromSimpleRep diff --git a/src/Constrained/Conformance.hs b/src/Constrained/Conformance.hs index 8ff615c..04ce2df 100644 --- a/src/Constrained/Conformance.hs +++ b/src/Constrained/Conformance.hs @@ -31,9 +31,9 @@ import Constrained.Syntax import Data.List (intersect, nub) import Data.List.NonEmpty qualified as NE import Data.Maybe +import Data.Semigroup (sconcat) import Data.Set (Set) import Data.Set qualified as Set -import Data.Semigroup (sconcat) import Prettyprinter hiding (cat) import Test.QuickCheck (Property, Testable, property) diff --git a/src/Constrained/Env.hs b/src/Constrained/Env.hs index 7794fc9..b0a32ad 100644 --- a/src/Constrained/Env.hs +++ b/src/Constrained/Env.hs @@ -1,9 +1,9 @@ {-# LANGUAGE DerivingVia #-} -{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE ImpredicativeTypes #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE StandaloneDeriving #-} @@ -76,7 +76,7 @@ find env var = do -- | Filter the keys in an env, useful for removing irrelevant variables in -- error messages filterKeys :: Env -> (forall a. Typeable a => Var a -> Bool) -> Env -filterKeys (Env m) f = Env $ Map.filterWithKey (\ (EnvKey k) _ -> f k) m +filterKeys (Env m) f = Env $ Map.filterWithKey (\(EnvKey k) _ -> f k) m instance Pretty EnvValue where pretty (EnvValue x) = viaShow x diff --git a/src/Constrained/GenT.hs b/src/Constrained/GenT.hs index 974892c..77143b0 100644 --- a/src/Constrained/GenT.hs +++ b/src/Constrained/GenT.hs @@ -60,7 +60,9 @@ module Constrained.GenT ( listFromGE, ) where +import Control.Arrow (second) import Control.Monad +import Control.Monad.Trans import Data.Foldable import Data.List.NonEmpty (NonEmpty ((:|)), (<|)) import Data.List.NonEmpty qualified as NE @@ -70,8 +72,6 @@ import System.Random import Test.QuickCheck hiding (Args, Fun) import Test.QuickCheck.Gen import Test.QuickCheck.Random -import Control.Arrow (second) -import Control.Monad.Trans -- ============================================================== -- The GE Monad @@ -127,27 +127,27 @@ runThreadingGen g = MkGen $ \seed size -> do snd <$> unThreadingGen g seed size strictGetSize :: Applicative m => ThreadingGenT m Int -strictGetSize = ThreadingGen $ \ seed size -> pure (seed, size) +strictGetSize = ThreadingGen $ \seed size -> pure (seed, size) scaleThreading :: (Int -> Int) -> ThreadingGenT m a -> ThreadingGenT m a -scaleThreading f sg = ThreadingGen $ \ seed size -> unThreadingGen sg seed (f size) +scaleThreading f sg = ThreadingGen $ \seed size -> unThreadingGen sg seed (f size) -newtype ThreadingGenT m a = ThreadingGen { unThreadingGen :: QCGen -> Int -> m (QCGen, a) } +newtype ThreadingGenT m a = ThreadingGen {unThreadingGen :: QCGen -> Int -> m (QCGen, a)} instance Functor m => Functor (ThreadingGenT m) where - fmap f (ThreadingGen g) = ThreadingGen $ \ seed size -> second f <$> g seed size + fmap f (ThreadingGen g) = ThreadingGen $ \seed size -> second f <$> g seed size instance Monad m => Applicative (ThreadingGenT m) where - pure a = ThreadingGen $ \ seed _ -> pure (seed, a) + pure a = ThreadingGen $ \seed _ -> pure (seed, a) (<*>) = ap instance Monad m => Monad (ThreadingGenT m) where - ThreadingGen g >>= k = ThreadingGen $ \ seed size -> do + ThreadingGen g >>= k = ThreadingGen $ \seed size -> do (seed', a) <- g seed size unThreadingGen (k a) seed' size instance MonadTrans ThreadingGenT where - lift m = ThreadingGen $ \ seed _ -> (seed,) <$> m + lift m = ThreadingGen $ \seed _ -> (seed,) <$> m ------------------------------------------------------------------------ -- The GenT monad @@ -233,7 +233,7 @@ instance MonadGenError m => MonadGenError (GenT m) where fatalErrors es = GenT $ \_ xs -> lift $ fatalErrors (cat es xs) -- Perhaps we want to turn fatalError into genError, if mode_ is Loose? - explainNE e (GenT f) = GenT $ \mode es -> ThreadingGen $ \ seed size -> explainNE e $ unThreadingGen (f mode es) seed size + explainNE e (GenT f) = GenT $ \mode es -> ThreadingGen $ \seed size -> explainNE e $ unThreadingGen (f mode es) seed size -- ==================================================== -- useful operations on NonEmpty @@ -454,7 +454,7 @@ sizeT = GenT $ \_ _ -> strictGetSize -- | Always succeeds, but returns the internal GE structure for analysis inspect :: forall m a. MonadGenError m => GenT GE a -> GenT m (GE a) -inspect (GenT f) = GenT $ \ mode msgs -> liftGenToThreading $ runThreadingGen $ f mode msgs +inspect (GenT f) = GenT $ \mode msgs -> liftGenToThreading $ runThreadingGen $ f mode msgs -- | Ignore all kinds of Errors, by squashing them into Nothing tryGenT :: MonadGenError m => GenT GE a -> GenT m (Maybe a) diff --git a/src/Constrained/Generation.hs b/src/Constrained/Generation.hs index 07932ce..1a8cf89 100644 --- a/src/Constrained/Generation.hs +++ b/src/Constrained/Generation.hs @@ -50,7 +50,6 @@ module Constrained.Generation ( EqW (..), SumSpec (..), pattern SumSpec, - mapSpec, forwardPropagateSpec, ) where @@ -159,10 +158,10 @@ shrinkWithSpec (ExplainSpec _ s) a = shrinkWithSpec s a shrinkWithSpec (simplifySpec -> spec) a = case spec of -- TODO: It would be nice to avoid the extra `conformsToSpec` check here and only look -- at the cant set instead - TypeSpec s _ -> [ a' | a' <- shrinkWithTypeSpec s a, a' `conformsToSpec` spec ] + TypeSpec s _ -> [a' | a' <- shrinkWithTypeSpec s a, a' `conformsToSpec` spec] SuspendedSpec x p -> shrinkFromPreds p x a -- TODO: it would be nice if there was some better way of doing this - MemberSpec as -> [ a' | a' <- unconstrainedShrink a, a' `elem` as ] + MemberSpec as -> [a' | a' <- unconstrainedShrink a, a' `elem` as] TrueSpec -> unconstrainedShrink a ErrorSpec {} -> [] -- Should be impossible? @@ -176,22 +175,22 @@ shrinkFromPreds p Nothing -> pure () Just err -> explainNE err $ fatalError "Trying to shrink a bad value, don't do that!" if not $ Name x `appearsIn` p -- NOTE: this is safe because we just checked that p is SAT above - then return $ unconstrainedShrink a - else do - -- Get an `env` for the original value - initialEnv <- envFromPred (Env.singleton x a) p - return - [ a' - | -- Shrink the initialEnv - env' <- shrinkEnvFromPlan initialEnv plan - , -- Get the value of the constrained variable `x` in the shrunk env - Just a' <- [Env.lookup env' x] - , -- NOTE: this is necessary because it's possible that changing - -- a particular value in the env during shrinking might not result - -- in the value of `x` changing and there is no better way to know than - -- to do this. - a' /= a - ] + then return $ unconstrainedShrink a + else do + -- Get an `env` for the original value + initialEnv <- envFromPred (Env.singleton x a) p + return + [ a' + | -- Shrink the initialEnv + env' <- shrinkEnvFromPlan initialEnv plan + , -- Get the value of the constrained variable `x` in the shrunk env + Just a' <- [Env.lookup env' x] + , -- NOTE: this is necessary because it's possible that changing + -- a particular value in the env during shrinking might not result + -- in the value of `x` changing and there is no better way to know than + -- to do this. + a' /= a + ] | otherwise = error "Bad pred" -- Start with a valid Env for the plan and try to shrink it @@ -226,7 +225,7 @@ fixupWithSpec spec a | a `conformsToSpec` spec = Just a | otherwise = case spec of MemberSpec (a' :| _) -> Just a' - TypeSpec ts _ -> fixupWithTypeSpec ts a >>= \ a' -> a' <$ guard (conformsToSpec a' spec) + TypeSpec ts _ -> fixupWithTypeSpec ts a >>= \a' -> a' <$ guard (conformsToSpec a' spec) _ -> listToMaybe $ filter (`conformsToSpec` spec) (shrinkWithSpec TrueSpec a) -- Debugging -------------------------------------------------------------- @@ -269,9 +268,11 @@ unsafeSubstStage env (SolverStage y ps spec relevant) = substStage :: HasSpec a => Set Name -> Var a -> a -> SolverStage -> SolverStage substStage rel' x val (SolverStage y ps spec relevant) = normalizeSolverStage $ SolverStage y (substPred env <$> ps) spec relevant' - where env = Env.singleton x val - relevant' | Name x `appearsIn` ps = rel' <> relevant - | otherwise = relevant + where + env = Env.singleton x val + relevant' + | Name x `appearsIn` ps = rel' <> relevant + | otherwise = relevant normalizeSolverStage :: SolverStage -> SolverStage normalizeSolverStage (SolverStage x ps spec relevant) = SolverStage x ps'' (spec <> spec') relevant @@ -376,7 +377,7 @@ linearize preds graph = do ] go (n@(Name x) : ns) ps = do let (nps, ops) = partition (isLastVariable n . fst) ps - (normalizeSolverStage (SolverStage x (map snd nps) mempty mempty):) <$> go ns ops + (normalizeSolverStage (SolverStage x (map snd nps) mempty mempty) :) <$> go ns ops isLastVariable n set = n `Set.member` set && solvableFrom n (Set.delete n set) graph @@ -902,7 +903,8 @@ mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage] mergeSolverStage (SolverStage x ps spec relevant) plan = [ case eqVar x y of Just Refl -> - normalizeSolverStage $ SolverStage + normalizeSolverStage $ + SolverStage y (ps ++ ps') (spec <> spec') @@ -917,38 +919,41 @@ isEmptyPlan (SolverPlan plan) = null plan stepPlan :: MonadGenError m => SolverPlan -> Env -> SolverPlan -> GenT m (Env, SolverPlan) stepPlan _ env plan@(SolverPlan []) = pure (env, plan) stepPlan (SolverPlan origStages) env (SolverPlan (stage@(SolverStage (x :: Var a) ps spec relevant) : pl)) = do - let errorMessage = "Failed to step the plan" /> - vsep [ "Relevant parts of the original plan:" //> pretty narrowedOrigPlan - , "Already generated variables:" //> pretty narrowedEnv - , "Current stage:" //> pretty stage - ] + let errorMessage = + "Failed to step the plan" + /> vsep + [ "Relevant parts of the original plan:" //> pretty narrowedOrigPlan + , "Already generated variables:" //> pretty narrowedEnv + , "Current stage:" //> pretty stage + ] relevant' = Set.insert (Name x) relevant - narrowedOrigPlan = SolverPlan $ [ st | st@(SolverStage v _ _ _) <- origStages, Name v `Set.member` relevant' ] - narrowedEnv = Env.filterKeys env (\v -> nameOf v `Set.member` (Set.map (\ (Name n) -> nameOf n) relevant')) + narrowedOrigPlan = SolverPlan $ [st | st@(SolverStage v _ _ _) <- origStages, Name v `Set.member` relevant'] + narrowedEnv = Env.filterKeys env (\v -> nameOf v `Set.member` (Set.map (\(Name n) -> nameOf n) relevant')) explain (show errorMessage) $ do when (isErrorLike spec) $ genError "The specification in the current stage is unsatisfiable, giving up." when (not $ null ps) $ - fatalError "Something went wrong and not all predicates have been discharged. Report this as a bug in Constrained.Generation" + fatalError + "Something went wrong and not all predicates have been discharged. Report this as a bug in Constrained.Generation" val <- genFromSpecT spec let env1 = Env.extend x val env - pure (env1, backPropagation relevant' $ SolverPlan (substStage relevant' x val <$> pl) ) + pure (env1, backPropagation relevant' $ SolverPlan (substStage relevant' x val <$> pl)) -- | Generate a satisfying `Env` for a `p : Pred fn`. The `Env` contains values for -- all the free variables in `flattenPred p`. genFromPreds :: forall m. MonadGenError m => Env -> Pred -> GenT m Env -- TODO: remove this once optimisePred does a proper fixpoint computation genFromPreds env0 (optimisePred . optimisePred -> preds) = do - -- NOTE: this is just lazy enough that the work of flattening, - -- computing dependencies, and linearizing is memoized in - -- properties that use `genFromPreds`. - origPlan <- runGE $ prepareLinearization preds - let go :: Env -> SolverPlan -> GenT m Env - go env plan | isEmptyPlan plan = pure env - go env plan = do - (env', plan') <- stepPlan origPlan env plan - go env' plan' - go env0 origPlan + -- NOTE: this is just lazy enough that the work of flattening, + -- computing dependencies, and linearizing is memoized in + -- properties that use `genFromPreds`. + origPlan <- runGE $ prepareLinearization preds + let go :: Env -> SolverPlan -> GenT m Env + go env plan | isEmptyPlan plan = pure env + go env plan = do + (env', plan') <- stepPlan origPlan env plan + go env' plan' + go env0 origPlan -- | Push as much information we can backwards through the plan. backPropagation :: Set Name -> SolverPlan -> SolverPlan @@ -967,11 +972,23 @@ backPropagation relevant (SolverPlan initplan) = SolverPlan (go [] (reverse init , [Name xr] <- Set.toList $ freeVarSet tr , Name x `elem` [Name xl, Name xr] , Result ctxL <- toCtx xl tl - , Result ctxR <- toCtx xr tr - = case (eqVar x xl, eqVar x xr) of - (Just Refl, _) -> [SolverStage xr [] (propagateSpec (forwardPropagateSpec spec ctxL) ctxR) (Set.insert (Name x) relevant)] - (_, Just Refl) -> [SolverStage xl [] (propagateSpec (forwardPropagateSpec spec ctxR) ctxL) (Set.insert (Name x) relevant)] - _ -> error "The impossible happened" + , Result ctxR <- toCtx xr tr = + case (eqVar x xl, eqVar x xr) of + (Just Refl, _) -> + [ SolverStage + xr + [] + (propagateSpec (forwardPropagateSpec spec ctxL) ctxR) + (Set.insert (Name x) relevant) + ] + (_, Just Refl) -> + [ SolverStage + xl + [] + (propagateSpec (forwardPropagateSpec spec ctxR) ctxL) + (Set.insert (Name x) relevant) + ] + _ -> error "The impossible happened" newStage _ = [] -- | Function symbols for `(==.)` @@ -1372,7 +1389,7 @@ instance Pretty SolverStage where ++ ["_" | null stagePreds && isTrueSpec stageSpec] ) -newtype SolverPlan = SolverPlan { solverPlan :: [SolverStage] } +newtype SolverPlan = SolverPlan {solverPlan :: [SolverStage]} instance Pretty SolverPlan where pretty SolverPlan {..} = @@ -1418,4 +1435,3 @@ forwardPropagateSpec s CtxHOLE = s forwardPropagateSpec s (CtxApp f (c :? Nil)) | Evidence <- ctxHasSpec c = mapSpec f (forwardPropagateSpec s c) forwardPropagateSpec _ _ = TrueSpec - diff --git a/src/Constrained/Generic.hs b/src/Constrained/Generic.hs index 5e68faf..dd97482 100644 --- a/src/Constrained/Generic.hs +++ b/src/Constrained/Generic.hs @@ -25,10 +25,10 @@ module Constrained.Generic ( Sum (..), (:::), SOP, - SOPLike(..), + SOPLike (..), SOPOf, ALG, - Inject(..), + Inject (..), ProdOver, ConstrOf, inject, diff --git a/src/Constrained/Graph.hs b/src/Constrained/Graph.hs index 232d4bd..eead5ca 100644 --- a/src/Constrained/Graph.hs +++ b/src/Constrained/Graph.hs @@ -25,6 +25,8 @@ module Constrained.Graph ( import Control.Monad import Data.Foldable +-- TODO: consider using more of this +import Data.Graph qualified as G import Data.List (nub) import Data.Map (Map) import Data.Map qualified as Map @@ -33,8 +35,6 @@ import Data.Set (Set) import Data.Set qualified as Set import Prettyprinter import Test.QuickCheck --- TODO: consider using more of this -import Data.Graph qualified as G -- | A graph with unlabeled edges for keeping track of dependencies data Graph node = Graph @@ -63,33 +63,51 @@ instance Pretty n => Pretty (Graph n) where -- | Construct a graph mkGraph :: Ord node => Map node (Set node) -> Graph node -mkGraph e0 = Graph e $ Map.unionsWith (<>) - [ Map.fromList $ (p, mempty) : [ (c, Set.singleton p) - | c <- Set.toList cs - ] - | (p, cs) <- Map.toList e - ] - where e = Map.unionWith (<>) e0 (Map.fromList [ (c, mempty) | (_, cs) <- Map.toList e0 - , c <- Set.toList cs - ]) +mkGraph e0 = + Graph e $ + Map.unionsWith + (<>) + [ Map.fromList $ + (p, mempty) + : [ (c, Set.singleton p) + | c <- Set.toList cs + ] + | (p, cs) <- Map.toList e + ] + where + e = + Map.unionWith + (<>) + e0 + ( Map.fromList + [ (c, mempty) + | (_, cs) <- Map.toList e0 + , c <- Set.toList cs + ] + ) instance (Arbitrary node, Ord node) => Arbitrary (Graph node) where arbitrary = - frequency [ (1, mkGraph <$> arbitrary) - , (3, do order <- nub <$> arbitrary - mkGraph <$> buildGraph order - ) - ] - where buildGraph [] = return mempty - buildGraph [n] = return (Map.singleton n mempty) - buildGraph (n:ns) = do - deps <- listOf (elements ns) - Map.insert n (Set.fromList deps) <$> buildGraph ns + frequency + [ (1, mkGraph <$> arbitrary) + , + ( 3 + , do + order <- nub <$> arbitrary + mkGraph <$> buildGraph order + ) + ] + where + buildGraph [] = return mempty + buildGraph [n] = return (Map.singleton n mempty) + buildGraph (n : ns) = do + deps <- listOf (elements ns) + Map.insert n (Set.fromList deps) <$> buildGraph ns shrink g = [ mkGraph e' | e <- shrink (edges g) - -- If we don't do this it's very easy to introduce a shrink-loop - , let e' = fmap (\ xs -> Set.filter (`Map.member` e) xs) e + , -- If we don't do this it's very easy to introduce a shrink-loop + let e' = fmap (\xs -> Set.filter (`Map.member` e) xs) e ] -- | Get all the nodes of a graph @@ -142,7 +160,7 @@ transitiveDependencies :: Ord node => node -> Graph node -> Set node transitiveDependencies x (Graph e _) = go mempty (Set.toList $ fromMaybe mempty $ Map.lookup x e) where go deps [] = deps - go deps (y:ys) + go deps (y : ys) | y `Set.member` deps = go deps ys | otherwise = go (Set.insert y deps) (ys ++ Set.toList (fromMaybe mempty $ Map.lookup y e)) @@ -174,16 +192,16 @@ topsort gr@(Graph e _) = go [] e findCycle :: Ord node => Graph node -> [node] findCycle g@(Graph e _) = mkCycle . concat . take 1 . filter isCyclic . map (map tr) . concatMap cycles . G.scc $ gr where - edgeList = [ (n, n, Set.toList es) | (n, es) <- Map.toList e ] + edgeList = [(n, n, Set.toList es) | (n, es) <- Map.toList e] (gr, tr0, _) = G.graphFromEdges edgeList tr x = let (n, _, _) = tr0 x in n cycles (G.Node a []) = [[a]] - cycles (G.Node a as) = (a:) <$> concatMap cycles as + cycles (G.Node a as) = (a :) <$> concatMap cycles as isCyclic [] = False isCyclic [a] = dependsOn a a g isCyclic _ = True -- Removes a non-dependent stem from the start of the dependencies - mkCycle ns = let l = last ns in dropWhile (\ n -> not $ dependsOn l n g) ns + mkCycle ns = let l = last ns in dropWhile (\n -> not $ dependsOn l n g) ns -- | Get the dependencies of a node in the graph, `mempty` if the node is not -- in the graph diff --git a/src/Constrained/NumOrd.hs b/src/Constrained/NumOrd.hs index f391dc8..0066613 100644 --- a/src/Constrained/NumOrd.hs +++ b/src/Constrained/NumOrd.hs @@ -1,6 +1,6 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-} +{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DerivingVia #-} @@ -744,8 +744,9 @@ instance {-# OVERLAPPABLE #-} (HasSpec a, MaybeBounded a, Integral a, TypeSpec a divideSpec 0 _ = TrueSpec divideSpec a (NumSpecInterval (unionWithMaybe max lowerBound -> ml) (unionWithMaybe min upperBound -> mu)) = typeSpec ts where - ts | a > 0 = NumSpecInterval ml' mu' - | otherwise = NumSpecInterval mu' ml' + ts + | a > 0 = NumSpecInterval ml' mu' + | otherwise = NumSpecInterval mu' ml' ml' = adjustLowerBound <$> ml mu' = adjustUpperBound <$> mu @@ -755,19 +756,19 @@ instance {-# OVERLAPPABLE #-} (HasSpec a, MaybeBounded a, Integral a, TypeSpec a | a == 1 = l | a == -1 = negate l | otherwise = - let r = l `div` a in - if toInteger r * toInteger a < toInteger l - then r + signum a - else r + let r = l `div` a + in if toInteger r * toInteger a < toInteger l + then r + signum a + else r adjustUpperBound u - | a == 1 = u + | a == 1 = u | a == -1 = negate u | otherwise = - let r = u `div` a in - if toInteger r * toInteger a > toInteger u - then r - signum a - else r + let r = u `div` a + in if toInteger r * toInteger a > toInteger u + then r - signum a + else r instance HasDivision (Ratio Integer) where doDivide = (/) @@ -775,26 +776,24 @@ instance HasDivision (Ratio Integer) where divideSpec 0 _ = TrueSpec divideSpec a (NumSpecInterval ml mu) = typeSpec ts where - ts | a > 0 = NumSpecInterval ml' mu' - | otherwise = NumSpecInterval mu' ml' + ts + | a > 0 = NumSpecInterval ml' mu' + | otherwise = NumSpecInterval mu' ml' ml' = adjustLowerBound <$> ml mu' = adjustUpperBound <$> mu adjustLowerBound l = let r = l / a l' = r * a - in - if l' < l - then r + (l - l') * 2 / a - else r + in if l' < l + then r + (l - l') * 2 / a + else r adjustUpperBound u = let r = u / a u' = r * a - in - if u < u' - then r - (u' - u) * 2 / a - else r - + in if u < u' + then r - (u' - u) * 2 / a + else r instance HasDivision Float where doDivide = (/) @@ -802,25 +801,24 @@ instance HasDivision Float where divideSpec 0 _ = TrueSpec divideSpec a (NumSpecInterval ml mu) = typeSpec ts where - ts | a > 0 = NumSpecInterval ml' mu' - | otherwise = NumSpecInterval mu' ml' + ts + | a > 0 = NumSpecInterval ml' mu' + | otherwise = NumSpecInterval mu' ml' ml' = adjustLowerBound <$> ml mu' = adjustUpperBound <$> mu adjustLowerBound l = let r = l / a l' = r * a - in - if l' < l - then r + (l - l') * 2 / a - else r + in if l' < l + then r + (l - l') * 2 / a + else r adjustUpperBound u = let r = u / a u' = r * a - in - if u < u' - then r - (u' - u) * 2 / a - else r + in if u < u' + then r - (u' - u) * 2 / a + else r instance HasDivision Double where doDivide = (/) @@ -828,25 +826,24 @@ instance HasDivision Double where divideSpec 0 _ = TrueSpec divideSpec a (NumSpecInterval ml mu) = typeSpec ts where - ts | a > 0 = NumSpecInterval ml' mu' - | otherwise = NumSpecInterval mu' ml' + ts + | a > 0 = NumSpecInterval ml' mu' + | otherwise = NumSpecInterval mu' ml' ml' = adjustLowerBound <$> ml mu' = adjustUpperBound <$> mu adjustLowerBound l = let r = l / a l' = r * a - in - if l' < l - then r + (l - l') * 2 / a - else r + in if l' < l + then r + (l - l') * 2 / a + else r adjustUpperBound u = let r = u / a u' = r * a - in - if u < u' - then r - (u' - u) * 2 / a - else r + in if u < u' + then r - (u' - u) * 2 / a + else r -- | A type that we can reason numerically about in constraints type Numeric a = (HasSpec a, Ord a, Num a, TypeSpec a ~ NumSpec a, MaybeBounded a, HasDivision a) @@ -913,15 +910,16 @@ instance Logic IntW where propagateTypeSpec NegateW (Unary HOLE) ts cant = negateSpec ts <> notMemberSpec (map negate cant) propagateTypeSpec MultW (HOLE :<: 0) ts cant | 0 `conformsToSpec` TypeSpec ts cant = TrueSpec - | otherwise = ErrorSpec $ NE.fromList [ "zero" ] + | otherwise = ErrorSpec $ NE.fromList ["zero"] propagateTypeSpec MultW (HOLE :<: i) ts cant = divideSpec i ts <> notMemberSpec (mapMaybe (flip invertMult i) cant) propagateTypeSpec MultW ctx ts cant = propagateTypeSpec MultW (flipCtx ctx) ts cant propagateTypeSpec SignumW (Unary HOLE) ts cant = - constrained $ \ x -> - [ x `satisfies` notMemberSpec [0] | not $ ok 0 ] ++ - [ Assert $ 0 <=. x | not $ ok (-1) ] ++ - [ Assert $ x <=. 0 | not $ ok 1 ] - where ok = flip conformsToSpec (TypeSpec ts cant) + constrained $ \x -> + [x `satisfies` notMemberSpec [0] | not $ ok 0] + ++ [Assert $ 0 <=. x | not $ ok (-1)] + ++ [Assert $ x <=. 0 | not $ ok 1] + where + ok = flip conformsToSpec (TypeSpec ts cant) propagateMemberSpec AddW (HOLE :<: i) es = memberSpec @@ -936,15 +934,16 @@ instance Logic IntW where propagateMemberSpec NegateW (Unary HOLE) es = MemberSpec $ NE.nub $ fmap negate es propagateMemberSpec MultW (HOLE :<: 0) es | 0 `elem` es = TrueSpec - | otherwise = ErrorSpec $ NE.fromList [ "zero" ] + | otherwise = ErrorSpec $ NE.fromList ["zero"] propagateMemberSpec MultW (HOLE :<: i) es = memberSpec (mapMaybe (flip invertMult i) (NE.toList es)) (NE.fromList ["propagateSpec"]) propagateMemberSpec MultW ctx es = propagateMemberSpec MultW (flipCtx ctx) es propagateMemberSpec SignumW (Unary HOLE) es - | all ((`notElem` [-1, 0, 1]) . signum) es = ErrorSpec $ NE.fromList [ "signum for invalid member spec", show es ] - | otherwise = constrained $ \ x -> - [ x `satisfies` notMemberSpec [0] | 0 `notElem` es ] ++ - [ Assert $ 0 <=. x | -1 `notElem` es ] ++ - [ Assert $ x <=. 0 | 1 `notElem` es ] + | all ((`notElem` [-1, 0, 1]) . signum) es = + ErrorSpec $ NE.fromList ["signum for invalid member spec", show es] + | otherwise = constrained $ \x -> + [x `satisfies` notMemberSpec [0] | 0 `notElem` es] + ++ [Assert $ 0 <=. x | -1 `notElem` es] + ++ [Assert $ x <=. 0 | 1 `notElem` es] rewriteRules AddW (x :> y :> Nil) _ | x == y = Just $ 2 * x rewriteRules _ _ _ = Nothing diff --git a/src/Constrained/PrettyUtils.hs b/src/Constrained/PrettyUtils.hs index 29771b3..bfdd9b6 100644 --- a/src/Constrained/PrettyUtils.hs +++ b/src/Constrained/PrettyUtils.hs @@ -1,8 +1,8 @@ {-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} diff --git a/src/Constrained/Spec/List.hs b/src/Constrained/Spec/List.hs index a8ed69c..04fc4da 100644 --- a/src/Constrained/Spec/List.hs +++ b/src/Constrained/Spec/List.hs @@ -280,8 +280,8 @@ randomInterleaving xs ys = go xs ys (length ys) go' _ xs [] _ = pure xs go' _ [] ys _ = pure ys - go' 0 (x:xs) ys l = (x:) <$> go xs ys l - go' i xs (y:ys) l = (y:) <$> go' (i-1) xs ys l + go' 0 (x : xs) ys l = (x :) <$> go xs ys l + go' i xs (y : ys) l = (y :) <$> go' (i - 1) xs ys l instance HasSpec a => HasGenHint [a] where type Hint [a] = Integer diff --git a/src/Constrained/Spec/Map.hs b/src/Constrained/Spec/Map.hs index ffd744f..ab21640 100644 --- a/src/Constrained/Spec/Map.hs +++ b/src/Constrained/Spec/Map.hs @@ -186,7 +186,13 @@ instance n <- genFromSpecT size' let go sz 0 slow kvs' m | fromInteger sz == Map.size m = pure m - | not slow = go sz (sz - fromIntegral (Map.size m)) True (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty)) m + | not slow = + go + sz + (sz - fromIntegral (Map.size m)) + True + (kvs' <> typeSpec (Cartesian (notMemberSpec (Map.keys m)) mempty)) + m | otherwise = fatalError "The impossible happened" go sz n' slow kvs' m = do mkv <- inspect $ genFromSpecT kvs' diff --git a/src/Constrained/Spec/SumProd.hs b/src/Constrained/Spec/SumProd.hs index a295ea1..e0a10a5 100644 --- a/src/Constrained/Spec/SumProd.hs +++ b/src/Constrained/Spec/SumProd.hs @@ -594,8 +594,8 @@ chooseSpec (w, s) (w', s') = p (branch $ \_ -> (x `satisfies` s)) (branch $ \_ -> (x `satisfies` s')) - -- This is a bit ugly :( - , caseOn + , -- This is a bit ugly :( + caseOn p (branchW w $ \_ -> True) (branchW w' $ \_ -> True) diff --git a/src/Constrained/Syntax.hs b/src/Constrained/Syntax.hs index 13ad890..ac09f0c 100644 --- a/src/Constrained/Syntax.hs +++ b/src/Constrained/Syntax.hs @@ -1,5 +1,5 @@ -{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} @@ -735,11 +735,11 @@ buildElemList :: List (Weighted Binder) as -> Maybe (NE.NonEmpty (SumOver as)) buildElemList Nil = Nothing buildElemList (Weighted Nothing (x :-> ElemPred True (V x') as) :> xs) | Just Refl <- eqVar x x' = - case xs of - Nil -> Just as - _ :> _ -> do - rest <- buildElemList xs - return $ fmap SumLeft as <> fmap SumRight rest + case xs of + Nil -> Just as + _ :> _ -> do + rest <- buildElemList xs + return $ fmap SumLeft as <> fmap SumRight rest buildElemList _ = Nothing -- | Run a `caseOn` diff --git a/src/Constrained/Test.hs b/src/Constrained/Test.hs index 775429d..758e0ab 100644 --- a/src/Constrained/Test.hs +++ b/src/Constrained/Test.hs @@ -25,7 +25,7 @@ module Constrained.Test ( prop_propagateSpecSound, prop_gen_sound, specType, - TestableFn(..), + TestableFn (..), ) where import Constrained.API.Extend @@ -41,16 +41,16 @@ import Constrained.Spec.List import Constrained.Spec.Map import Constrained.Spec.Set import Constrained.TheKnot +import Data.Int import Data.List (nub) import qualified Data.List.NonEmpty as NE import Data.Map (Map) import Data.Set (Set) import Data.Typeable (Typeable, typeOf) +import Data.Word import Prettyprinter import Test.QuickCheck hiding (Fun) import qualified Test.QuickCheck as QC -import Data.Word -import Data.Int -- | Check that a generator from a given `Specification` is sound, it never -- generates a bad value that doesn't satisfy the constraint @@ -76,7 +76,7 @@ prop_constrained_satisfies_sound spec = prop_sound (constrained $ \a -> satisfie prop_constrained_explained :: HasSpec a => Specification a -> QC.Property prop_constrained_explained spec = let es = NE.singleton "Dummy explanation" - in prop_sound $ constrained $ \x -> Explain es $ x `satisfies` spec + in prop_sound $ constrained $ \x -> Explain es $ x `satisfies` spec -- | `prop_complete ps` assumes that `ps` is satisfiable and checks that it doesn't crash prop_complete :: HasSpec a => Specification a -> QC.Property @@ -400,8 +400,8 @@ instance QC.Arbitrary TestableFn where , TestableFn $ MultW @Int , TestableFn $ MultW @Integer , TestableFn $ SignumW @Integer - -- These are representative of the bounded types - , TestableFn $ MultW @Word8 + , -- These are representative of the bounded types + TestableFn $ MultW @Word8 , TestableFn $ SignumW @Word8 , TestableFn $ MultW @Int8 , TestableFn $ MultW @Float diff --git a/test/Constrained/GraphSpec.hs b/test/Constrained/GraphSpec.hs index efd236a..e005df4 100644 --- a/test/Constrained/GraphSpec.hs +++ b/test/Constrained/GraphSpec.hs @@ -1,14 +1,15 @@ {-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE NumericUnderscores #-} -{-# LANGUAGE ImportQualifiedPost #-} -{-# LANGUAGE DerivingVia #-} + module Constrained.GraphSpec where -import Data.Either import Constrained.Graph +import Data.Either import Data.Set (Set) import Data.Set qualified as Set import Test.Hspec @@ -17,7 +18,7 @@ import Test.QuickCheck newtype Node = Node Int deriving (Ord, Eq) - deriving Show via Int + deriving (Show) via Int instance Arbitrary Node where arbitrary = Node <$> choose (0, 20) @@ -38,14 +39,20 @@ prop_subtract_topsort g g' = prop_subtract_union :: Graph Node -> Graph Node -> Property prop_subtract_union g g0' = let g' = subtractGraph g g0' - in subtractGraph g g' <> g' === g + in subtractGraph g g' <> g' === g prop_subtract_keeps_nodes :: Graph Node -> Graph Node -> Property prop_subtract_keeps_nodes g g' = nodes (subtractGraph g g') === nodes g prop_subtract_removes_edges :: Graph Node -> Graph Node -> Node -> Node -> Property prop_subtract_removes_edges g g' x y = - property $ not (dependsOn x y (subtractGraph (dependency x (Set.singleton y) <> g) $ dependency x (Set.singleton y) <> g')) + property $ + not + ( dependsOn + x + y + (subtractGraph (dependency x (Set.singleton y) <> g) $ dependency x (Set.singleton y) <> g') + ) prop_union_commutes :: Graph Node -> Graph Node -> Property prop_union_commutes g g' = g <> g' === g' <> g @@ -77,13 +84,13 @@ prop_transitive_dependencies g n = prop_topsort_all_nodes :: Graph Node -> Property prop_topsort_all_nodes g = case topsort g of - Left{} -> discard + Left {} -> discard Right o -> Set.fromList o === nodes g prop_topsort_sound :: Graph Node -> Property prop_topsort_sound g = case topsort g of - Left{} -> discard + Left {} -> discard Right o -> property $ go o where go [] = True @@ -95,19 +102,20 @@ prop_topsort_complete g = prop_find_cycle_sound :: Property prop_find_cycle_sound = - forAllShrink (mkGraph @Node <$> arbitrary) shrink $ \ g -> + forAllShrink (mkGraph @Node <$> arbitrary) shrink $ \g -> let c = findCycle g - in counterexample (show c) $ all (\(x, y) -> dependsOn x y g) (zip c (drop 1 $ cycle c)) + in counterexample (show c) $ all (\(x, y) -> dependsOn x y g) (zip c (drop 1 $ cycle c)) prop_find_cycle_loops :: Property prop_find_cycle_loops = - forAllShrink (mkGraph @Node <$> arbitrary) shrink $ \ g -> + forAllShrink (mkGraph @Node <$> arbitrary) shrink $ \g -> case findCycle g of [] -> property True - c@(x:_) -> cover 40 True "found cycle" $ counterexample (show c) $ dependsOn (last c) x g + c@(x : _) -> cover 40 True "found cycle" $ counterexample (show c) $ dependsOn (last c) x g return [] tests :: Bool -> Spec tests _nightly = - describe "Graph tests" $ sequence_ [ prop n (checkCoverage $ withMaxSuccess 1000 p) | (n, p) <- $allProperties ] + describe "Graph tests" $ + sequence_ [prop n (checkCoverage $ withMaxSuccess 1000 p) | (n, p) <- $allProperties] diff --git a/test/Constrained/Tests.hs b/test/Constrained/Tests.hs index 2351c96..3598a84 100644 --- a/test/Constrained/Tests.hs +++ b/test/Constrained/Tests.hs @@ -20,12 +20,12 @@ import Constrained.Examples.Basic import Constrained.Examples.Either import Constrained.Examples.Fold ( Outcome (..), - evenSpec, composeEvenSpec, + composeOddSpec, + evenSpec, listSumComplex, logishProp, oddSpec, - composeOddSpec, pickProp, sum3, sum3WithLength, diff --git a/test/Tests.hs b/test/Tests.hs index beecbcf..efbd817 100644 --- a/test/Tests.hs +++ b/test/Tests.hs @@ -1,7 +1,7 @@ module Main where -import Constrained.Tests as Tests import Constrained.GraphSpec as Graph +import Constrained.Tests as Tests import Data.Maybe import System.Environment import Test.Hspec