Add some debugging features and better explanations

src/Constrained/GenT.hs

@@ -40,6 +40,7 @@ module Constrained.GenT (
 
   -- * So far undocumented
   fatalError,
+  getMessages,
   catMessages,
   catMessageList,
   explain,

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]

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

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 <> ")"

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

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