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..61e7307 100644 --- a/src/Constrained/Generation.hs +++ b/src/Constrained/Generation.hs @@ -220,7 +220,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 +849,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 +867,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 +901,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 +1312,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..5edbc24 100644 --- a/src/Constrained/Spec/Map.hs +++ b/src/Constrained/Spec/Map.hs @@ -186,26 +186,39 @@ 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 - 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..2399c37 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,23 @@ 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 + , IsPred p + ) => + String -> + Term a -> + (a -> b) -> + (Term b -> p) -> + Pred +reifyWithName nam t f body = + 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 assertReified :: HasSpec a => Term a -> (a -> Bool) -> Pred -- Note, it is necessary to introduce the extra variable from the `exists` here