From afb58d6d6372301aa0621521740b571b904e9cbb Mon Sep 17 00:00:00 2001 From: Alexey Kuleshevich Date: Wed, 16 Jul 2025 19:47:03 -0600 Subject: [PATCH 1/2] Add Tim's changes --- src/Constrained/Base.hs | 7 +++ src/Constrained/GenT.hs | 1 + src/Constrained/Generation.hs | 86 +++++++++++++++++++--------------- src/Constrained/NumOrd.hs | 1 - src/Constrained/PrettyUtils.hs | 17 +++++-- src/Constrained/Spec/Map.hs | 36 +++++++++----- src/Constrained/Syntax.hs | 17 +++++++ 7 files changed, 111 insertions(+), 54 deletions(-) diff --git a/src/Constrained/Base.hs b/src/Constrained/Base.hs index 62fa7db..85f9aa4 100644 --- a/src/Constrained/Base.hs +++ b/src/Constrained/Base.hs @@ -72,6 +72,7 @@ module Constrained.Base ( -- * Building `Pred`, `Specification`, `Term` etc. bind, name, + named, -- * TODO: documentme propagateSpec, @@ -771,6 +772,12 @@ name :: String -> Term a -> Term a name nh (V (Var i _)) = V (Var i nh) name _ _ = error "applying name to non-var thing! Shame on you!" +-- | Give a Term a nameHint, if its a Var, and doesn't already have one, +-- otherwise return the Term unchanged. +named :: String -> Term a -> Term a +named nh t@(V (Var i x)) = if x /= "v" then t else V (Var i nh) +named _ t = t + -- | Create a `Binder` with a fresh variable, used in e.g. `constrained` bind :: (HasSpec a, IsPred p) => (Term a -> p) -> Binder a bind bodyf = newv :-> bodyPred diff --git a/src/Constrained/GenT.hs b/src/Constrained/GenT.hs index d2a2bef..39d5bfd 100644 --- a/src/Constrained/GenT.hs +++ b/src/Constrained/GenT.hs @@ -40,6 +40,7 @@ module Constrained.GenT ( -- * So far undocumented fatalError, + getMessages, catMessages, catMessageList, explain, diff --git a/src/Constrained/Generation.hs b/src/Constrained/Generation.hs index 888477f..8e791ac 100644 --- a/src/Constrained/Generation.hs +++ b/src/Constrained/Generation.hs @@ -51,6 +51,7 @@ module Constrained.Generation ( pattern SumSpec, ) where +-- import Debug.Trace import Constrained.AbstractSyntax import Constrained.Base import Constrained.Conformance @@ -97,39 +98,40 @@ import Prelude hiding (cycle, pred) -- generators are not flexible enough. genFromSpecT :: forall a m. (HasCallStack, HasSpec a, MonadGenError m) => Specification a -> GenT m a -genFromSpecT (simplifySpec -> spec) = case spec of - ExplainSpec [] s -> genFromSpecT s - ExplainSpec es s -> push es (genFromSpecT s) - MemberSpec as -> explain ("genFromSpecT on spec" ++ show spec) $ pureGen (elements (NE.toList as)) - TrueSpec -> genFromSpecT (typeSpec $ emptySpec @a) - SuspendedSpec x p - -- NOTE: If `x` isn't free in `p` we still have to try to generate things - -- from `p` to make sure `p` is sat and then we can throw it away. A better - -- approach would be to only do this in the case where we don't know if `p` - -- is sat. The proper way to implement such a sat check is to remove - -- sat-but-unnecessary variables in the optimiser. - | not $ Name x `appearsIn` p -> do - !_ <- genFromPreds mempty p - genFromSpecT TrueSpec - | otherwise -> do - env <- genFromPreds mempty p - Env.find env x - TypeSpec s cant -> do - mode <- getMode - explainNE - ( NE.fromList - [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a - , "tspec = " - , show s - , "cant = " ++ show (short cant) - , "with mode " ++ show mode - ] - ) - $ - -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this - -- starts giving us trouble. - genFromTypeSpec s `suchThatT` (`notElem` cant) - ErrorSpec e -> genErrorNE e +genFromSpecT (simplifySpec -> spec) = + case spec of + ExplainSpec [] s -> genFromSpecT s + ExplainSpec es s -> push es (genFromSpecT s) + MemberSpec as -> explain ("genFromSpecT on spec" ++ show spec) $ pureGen (elements (NE.toList as)) + TrueSpec -> genFromSpecT (typeSpec $ emptySpec @a) + SuspendedSpec x p + -- NOTE: If `x` isn't free in `p` we still have to try to generate things + -- from `p` to make sure `p` is sat and then we can throw it away. A better + -- approach would be to only do this in the case where we don't know if `p` + -- is sat. The proper way to implement such a sat check is to remove + -- sat-but-unnecessary variables in the optimiser. + | not $ Name x `appearsIn` p -> do + !_ <- genFromPreds mempty p + genFromSpecT TrueSpec + | otherwise -> do + env <- genFromPreds mempty p + Env.find env x + TypeSpec s cant -> do + mode <- getMode + explainNE + ( NE.fromList + [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a + , "tspec = " + , show s + , "cant = " ++ show (short cant) + , "with mode " ++ show mode + ] + ) + $ + -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this + -- starts giving us trouble. + genFromTypeSpec s `suchThatT` (`notElem` cant) + ErrorSpec e -> genErrorNE e -- | A version of `genFromSpecT` that simply errors if the generator fails genFromSpec :: forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a @@ -220,7 +222,10 @@ prepareLinearization p = do explainNE ( NE.fromList [ "Linearizing" - , show $ " preds: " <> pretty preds + , show $ + " preds: " + <> pretty (take 3 preds) + <> (if length preds > 3 then fromString (" ... " ++ show (length preds - 3) ++ " more.") else "") , show $ " graph: " <> pretty graph ] ) @@ -846,7 +851,7 @@ isEmptyPlan (SolverPlan plan _) = null plan stepPlan :: MonadGenError m => Env -> SolverPlan -> GenT m (Env, SolverPlan) stepPlan env plan@(SolverPlan [] _) = pure (env, plan) -stepPlan env (SolverPlan (SolverStage x ps spec : pl) gr) = do +stepPlan env (SolverPlan (SolverStage (x :: Var a) ps spec : pl) gr) = do (spec', specs) <- runGE $ explain ( show @@ -864,6 +869,8 @@ stepPlan env (SolverPlan (SolverStage x ps spec : pl) gr) = do ( NE.fromList ( ( "\nStepPlan for variable: " ++ show x + ++ "::" + ++ showType @a ++ " fails to produce Specification, probably overconstrained." ++ "PS = " ++ unlines (map show ps) @@ -896,8 +903,10 @@ genFromPreds env0 (optimisePred . optimisePred -> preds) = go :: Env -> SolverPlan -> GenT m Env go env plan | isEmptyPlan plan = pure env go env plan = do + (mess :: String) <- (unlines . map NE.head) <$> getMessages (env', plan') <- - explain (show $ "Stepping the plan:" /> vsep [pretty plan, pretty env]) $ stepPlan env plan + explain (show (fromString (mess ++ "Stepping the plan:") /> vsep [pretty plan, pretty env])) $ + stepPlan env plan go env' plan' -- | Push as much information we can backwards through the plan. @@ -1305,9 +1314,12 @@ data SolverStage where } -> SolverStage +docVar :: Typeable a => Var a -> Doc h +docVar (v :: Var a) = fromString (show v ++ " :: " ++ showType @a) + instance Pretty SolverStage where pretty SolverStage {..} = - viaShow stageVar + docVar stageVar <+> "<-" /> vsep' ( [pretty stageSpec | not $ isTrueSpec stageSpec] diff --git a/src/Constrained/NumOrd.hs b/src/Constrained/NumOrd.hs index 95705e9..44fb4ce 100644 --- a/src/Constrained/NumOrd.hs +++ b/src/Constrained/NumOrd.hs @@ -51,7 +51,6 @@ module Constrained.NumOrd ( import Constrained.AbstractSyntax import Constrained.Base import Constrained.Conformance -import Constrained.Conformance () import Constrained.Core (Value (..), unionWithMaybe) import Constrained.FunctionSymbol import Constrained.GenT diff --git a/src/Constrained/PrettyUtils.hs b/src/Constrained/PrettyUtils.hs index d8462e2..e8598b5 100644 --- a/src/Constrained/PrettyUtils.hs +++ b/src/Constrained/PrettyUtils.hs @@ -77,15 +77,22 @@ infixl 5 /> showType :: forall t. Typeable t => String showType = show (typeRep (Proxy @t)) +-- | Set to True if you need to see everything while debugging +verboseShort :: Bool +verboseShort = True + -- | Pretty-print a short list in full and truncate longer lists short :: forall a x. (Show a, Typeable a) => [a] -> Doc x short [] = "[]" short [x] = let raw = show x - refined = if length raw <= 20 then raw else take 20 raw ++ " ... " + refined = if length raw <= 20 || verboseShort then raw else take 20 raw ++ " ... " in "[" <+> fromString refined <+> "]" short xs = - let raw = show xs - in if length raw <= 50 - then fromString raw - else "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <> ")" + if verboseShort + then fromString $ unlines (map show xs) + else + let raw = show xs + in if length raw <= 50 + then fromString raw + else "([" <+> viaShow (length xs) <+> "elements ...] @" <> prettyType @a <> ")" diff --git a/src/Constrained/Spec/Map.hs b/src/Constrained/Spec/Map.hs index 8d3a91c..5fb7691 100644 --- a/src/Constrained/Spec/Map.hs +++ b/src/Constrained/Spec/Map.hs @@ -186,26 +186,40 @@ instance n <- genFromSpecT size' let go 0 _ m = pure m go n' kvs' m = do - mkv <- tryGenT $ genFromSpecT kvs' + -- mkv <- tryGenT $ genFromSpecT kvs' + mkv <- inspect $ genFromSpecT kvs' case mkv of - Nothing - | sizeOf m `conformsToSpec` size -> pure m - Just (k, v) -> + Result (k, v) -> go (n' - 1) (kvs' <> typeSpec (Cartesian (notEqualSpec k) mempty)) (Map.insert k v m) - _ -> + GenError msgs -> + if sizeOf m `conformsToSpec` size + then pure m + else + genErrorNE + (pure "Gen error while trying to generate enough elements for a Map." <> catMessageList msgs) + FatalError msgs -> genErrorNE ( NE.fromList - [ "Failed to generate enough elements for the map:" - , " m = " ++ show m - , " n' = " ++ show n' - , show $ " kvs' = " <> pretty kvs' - , show $ " simplifySpec kvs' = " <> pretty (simplifySpec kvs') + [ "Fatal error while trying to generate enough elements for a map:" + , " The ones we have generated so far = " ++ show m + , " The number we need to still generate: n' = " ++ show n' + , "The original size spec " ++ show size + , "The refined size spec " ++ show size' + , "The computed target size " ++ show n + , "Fatal error messages" + , "<<<---" + -- , "The kvs Spec" + -- , " >>>> "++ show $ " kvs' = " <> pretty kvs' + -- , "The simplified kvs Spec" + -- , " >>>> "++ show(pretty (simplifySpec kvs')) ] + <> catMessageList msgs + <> (pure "--->>>") ) - explain (" n = " ++ show n) $ go n kvs mempty + explain (" The number we are trying for: n = " ++ show n) $ go n kvs mempty genFromTypeSpec (MapSpec mHint mustKeys mustVals size (simplifySpec -> kvs) foldSpec) = do !mustMap <- explain "Make the mustMap" $ forM (Set.toList mustKeys) $ \k -> do let vSpec = constrained $ \v -> satisfies (pair_ (Lit k) v) kvs diff --git a/src/Constrained/Syntax.hs b/src/Constrained/Syntax.hs index 98ad44e..84510bd 100644 --- a/src/Constrained/Syntax.hs +++ b/src/Constrained/Syntax.hs @@ -31,6 +31,7 @@ module Constrained.Syntax ( explanation, assertReified, reify, + reifyWithName, letBind, unsafeExists, forAll, @@ -210,6 +211,22 @@ reify t f body = , Explain (pure ("reify " ++ show t ++ " somef $")) $ toPred (body x) ] +reifyWithName :: + ( HasSpec a + , HasSpec b + , IsPred p + ) => + String -> + Term a -> + (a -> b) -> + (Term b -> p) -> + Pred +reifyWithName nam t f body = + exists (\eval -> pure $ f (eval t)) $ \x -> + [ reifies (named nam x) t f + , Explain (pure ("reify " ++ show t ++ " somef $")) $ toPred (body (named nam x)) + ] + -- | Like `suchThat` for constraints assertReified :: HasSpec a => Term a -> (a -> Bool) -> Pred -- Note, it is necessary to introduce the extra variable from the `exists` here From 0ab52c3b509b3e627781a17dbdbe6615efce4cd8 Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Thu, 17 Jul 2025 09:19:33 +0200 Subject: [PATCH 2/2] Remove some minor cruft --- src/Constrained/Base.hs | 7 ---- src/Constrained/Generation.hs | 68 +++++++++++++++++------------------ src/Constrained/Spec/Map.hs | 1 - src/Constrained/Syntax.hs | 7 ++-- 4 files changed, 37 insertions(+), 46 deletions(-) diff --git a/src/Constrained/Base.hs b/src/Constrained/Base.hs index 85f9aa4..62fa7db 100644 --- a/src/Constrained/Base.hs +++ b/src/Constrained/Base.hs @@ -72,7 +72,6 @@ module Constrained.Base ( -- * Building `Pred`, `Specification`, `Term` etc. bind, name, - named, -- * TODO: documentme propagateSpec, @@ -772,12 +771,6 @@ name :: String -> Term a -> Term a name nh (V (Var i _)) = V (Var i nh) name _ _ = error "applying name to non-var thing! Shame on you!" --- | Give a Term a nameHint, if its a Var, and doesn't already have one, --- otherwise return the Term unchanged. -named :: String -> Term a -> Term a -named nh t@(V (Var i x)) = if x /= "v" then t else V (Var i nh) -named _ t = t - -- | Create a `Binder` with a fresh variable, used in e.g. `constrained` bind :: (HasSpec a, IsPred p) => (Term a -> p) -> Binder a bind bodyf = newv :-> bodyPred diff --git a/src/Constrained/Generation.hs b/src/Constrained/Generation.hs index 8e791ac..61e7307 100644 --- a/src/Constrained/Generation.hs +++ b/src/Constrained/Generation.hs @@ -51,7 +51,6 @@ module Constrained.Generation ( pattern SumSpec, ) where --- import Debug.Trace import Constrained.AbstractSyntax import Constrained.Base import Constrained.Conformance @@ -98,40 +97,39 @@ import Prelude hiding (cycle, pred) -- generators are not flexible enough. genFromSpecT :: forall a m. (HasCallStack, HasSpec a, MonadGenError m) => Specification a -> GenT m a -genFromSpecT (simplifySpec -> spec) = - case spec of - ExplainSpec [] s -> genFromSpecT s - ExplainSpec es s -> push es (genFromSpecT s) - MemberSpec as -> explain ("genFromSpecT on spec" ++ show spec) $ pureGen (elements (NE.toList as)) - TrueSpec -> genFromSpecT (typeSpec $ emptySpec @a) - SuspendedSpec x p - -- NOTE: If `x` isn't free in `p` we still have to try to generate things - -- from `p` to make sure `p` is sat and then we can throw it away. A better - -- approach would be to only do this in the case where we don't know if `p` - -- is sat. The proper way to implement such a sat check is to remove - -- sat-but-unnecessary variables in the optimiser. - | not $ Name x `appearsIn` p -> do - !_ <- genFromPreds mempty p - genFromSpecT TrueSpec - | otherwise -> do - env <- genFromPreds mempty p - Env.find env x - TypeSpec s cant -> do - mode <- getMode - explainNE - ( NE.fromList - [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a - , "tspec = " - , show s - , "cant = " ++ show (short cant) - , "with mode " ++ show mode - ] - ) - $ - -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this - -- starts giving us trouble. - genFromTypeSpec s `suchThatT` (`notElem` cant) - ErrorSpec e -> genErrorNE e +genFromSpecT (simplifySpec -> spec) = case spec of + ExplainSpec [] s -> genFromSpecT s + ExplainSpec es s -> push es (genFromSpecT s) + MemberSpec as -> explain ("genFromSpecT on spec" ++ show spec) $ pureGen (elements (NE.toList as)) + TrueSpec -> genFromSpecT (typeSpec $ emptySpec @a) + SuspendedSpec x p + -- NOTE: If `x` isn't free in `p` we still have to try to generate things + -- from `p` to make sure `p` is sat and then we can throw it away. A better + -- approach would be to only do this in the case where we don't know if `p` + -- is sat. The proper way to implement such a sat check is to remove + -- sat-but-unnecessary variables in the optimiser. + | not $ Name x `appearsIn` p -> do + !_ <- genFromPreds mempty p + genFromSpecT TrueSpec + | otherwise -> do + env <- genFromPreds mempty p + Env.find env x + TypeSpec s cant -> do + mode <- getMode + explainNE + ( NE.fromList + [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a + , "tspec = " + , show s + , "cant = " ++ show (short cant) + , "with mode " ++ show mode + ] + ) + $ + -- TODO: we could consider giving `cant` as an argument to `genFromTypeSpec` if this + -- starts giving us trouble. + genFromTypeSpec s `suchThatT` (`notElem` cant) + ErrorSpec e -> genErrorNE e -- | A version of `genFromSpecT` that simply errors if the generator fails genFromSpec :: forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a diff --git a/src/Constrained/Spec/Map.hs b/src/Constrained/Spec/Map.hs index 5fb7691..5edbc24 100644 --- a/src/Constrained/Spec/Map.hs +++ b/src/Constrained/Spec/Map.hs @@ -186,7 +186,6 @@ instance n <- genFromSpecT size' let go 0 _ m = pure m go n' kvs' m = do - -- mkv <- tryGenT $ genFromSpecT kvs' mkv <- inspect $ genFromSpecT kvs' case mkv of Result (k, v) -> diff --git a/src/Constrained/Syntax.hs b/src/Constrained/Syntax.hs index 84510bd..2399c37 100644 --- a/src/Constrained/Syntax.hs +++ b/src/Constrained/Syntax.hs @@ -211,6 +211,7 @@ reify t f body = , Explain (pure ("reify " ++ show t ++ " somef $")) $ toPred (body x) ] +-- | Like `reify` but provide a @[`var`| ... |]@-style name explicitly reifyWithName :: ( HasSpec a , HasSpec b @@ -222,9 +223,9 @@ reifyWithName :: (Term b -> p) -> Pred reifyWithName nam t f body = - exists (\eval -> pure $ f (eval t)) $ \x -> - [ reifies (named nam x) t f - , Explain (pure ("reify " ++ show t ++ " somef $")) $ toPred (body (named nam x)) + exists (\eval -> pure $ f (eval t)) $ \(name nam -> x) -> + [ reifies x t f + , Explain (pure ("reify " ++ show t ++ " somef $")) $ toPred (body x) ] -- | Like `suchThat` for constraints