some prettyprinting improvements

Author: MaximilianAlgehed

src/Constrained/AbstractSyntax.hs

@@ -377,7 +377,7 @@ instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (WithPrec (Spec
     ExplainSpec es z -> "ExplainSpec" <+> viaShow es <+> "$" /> pretty z
     ErrorSpec es -> "ErrorSpec" /> vsep' (map fromString (NE.toList es))
     TrueSpec -> fromString $ "TrueSpec @(" ++ showType @a ++ ")"
-    MemberSpec xs -> "MemberSpec" <+> short (NE.toList xs)
+    MemberSpec xs -> "MemberSpec" <+> viaShow (NE.toList xs)
     SuspendedSpec x p -> parensIf (d > 10) $ "constrained $ \\" <+> viaShow x <+> "->" /> pretty p
     -- TODO: require pretty for `TypeSpec` to make this much nicer
     TypeSpecD ts cant ->

src/Constrained/Env.hs

@@ -20,6 +20,7 @@ module Constrained.Env (
 
 import Constrained.Core
 import Constrained.GenT
+import Constrained.PrettyUtils
 import Data.Map (Map)
 import Data.Map qualified as Map
 import Data.Typeable
@@ -85,6 +86,6 @@ instance Pretty EnvKey where
   pretty (EnvKey x) = viaShow x
 
 instance Pretty Env where
-  pretty (Env m) = vsep ("Env" : (map f (Map.toList m)))
+  pretty (Env m) = "Env" /> vsep (map f (Map.toList m))
     where
       f (k, v) = hsep [pretty k, "->", pretty v]

src/Constrained/Generation.hs

@@ -121,7 +121,7 @@ genFromSpecT (simplifySpec -> spec) = case spec of
           [ "genFromSpecT on (TypeSpec tspec cant) at type " ++ showType @a
           , "tspec = "
           , show s
-          , "cant = " ++ show (short cant)
+          , "cant = " ++ show cant
           , "with mode " ++ show mode
           ]
       )
@@ -830,21 +830,21 @@ mergeSolverStage :: SolverStage -> [SolverStage] -> [SolverStage]
 mergeSolverStage (SolverStage x ps spec relevant) plan =
   [ case eqVar x y of
       Just Refl ->
-        SolverStage
-          y
-          (ps ++ ps')
-          ( addToErrorSpec
-              ( NE.fromList
-                  ( [ "Solving var " ++ show x ++ " fails."
-                    , "Merging the Specs"
-                    , "   1. " ++ show spec
-                    , "   2. " ++ show spec'
-                    ]
-                  )
-              )
-              (spec <> spec')
-          )
-          (relevant <> relevant')
+        normalizeSolverStage $ SolverStage
+            y
+            (ps ++ ps')
+            ( addToErrorSpec
+                ( NE.fromList
+                    ( [ "Solving var " ++ show x ++ " fails."
+                      , "Merging the Specs"
+                      , "   1. " ++ show spec
+                      , "   2. " ++ show spec'
+                      ]
+                    )
+                )
+                (spec <> spec')
+            )
+            (relevant <> relevant')
       Nothing -> stage
   | stage@(SolverStage y ps' spec' relevant') <- plan
   ]
@@ -856,49 +856,20 @@ stepPlan :: MonadGenError m => SolverPlan -> Env -> SolverPlan -> GenT m (Env, S
 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 original plan: " /> pretty narrowedOrigPlan
-                             , "Relevant parts of the env: " /> pretty narrowedEnv
-                             , "Current stage: " /> pretty stage
+                        vsep [ "Relevant parts of original plan:" //> pretty narrowedOrigPlan
+                             , "Relevant parts of the env:" //> pretty narrowedEnv
+                             , "Current stage:" //> pretty stage
                              ]
       -- TODO: tests for this, including tests for transitive behaviour
       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'))
   explain (show errorMessage) $ do
-    (spec', specs) <- runGE
-      $ explain
-        ( show
-            ( "Computing specs for variable "
-                <> pretty x
-                  /> vsep' (map pretty ps)
-            )
-        )
-      $ do
-        ispecs <- mapM (computeSpec x) ps
-        pure $ (fold ispecs, ispecs)
-    val <-
-      genFromSpecT
-        ( addToErrorSpec
-            ( NE.fromList
-                ( ( "\nStepPlan for variable: "
-                      ++ show x
-                      ++ "::"
-                      ++ showType @a
-                      ++ " fails to produce Specification, probably overconstrained."
-                      ++ "PS = "
-                      ++ unlines (map show ps)
-                  )
-                    : ("Relevant variables " ++ show relevant)
-                    : ("Original spec " ++ show spec)
-                    : "Predicates"
-                    : zipWith
-                      (\pred specx -> "  pred " ++ show pred ++ " -> " ++ show specx)
-                      ps
-                      specs
-                )
-            )
-            (spec <> spec')
-        )
+    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"
+    val <- genFromSpecT spec
     let env1 = Env.extend x val env
     pure (env1, backPropagation relevant' $ SolverPlan (substStage relevant' x val <$> pl) )
 

src/Constrained/PrettyUtils.hs

@@ -23,8 +23,8 @@ module Constrained.PrettyUtils (
   prettyType,
   vsep',
   (/>),
+  (//>),
   showType,
-  short,
 ) where
 
 import Constrained.List
@@ -73,26 +73,13 @@ h /> cont = hang 2 $ sep [h, align cont]
 
 infixl 5 />
 
+-- | Lay the header (first argument) out above the body
+-- and and indent the body by 2
+(//>) :: Doc ann -> Doc ann -> Doc ann
+h //> cont = hang 2 $ vsep [h, align cont]
+
+infixl 5 //>
+
 -- | Show a `Typeable` thing's type
 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 || verboseShort then raw else take 20 raw ++ " ... "
-   in "[" <+> fromString refined <+> "]"
-short xs =
-  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/List.hs

@@ -358,8 +358,8 @@ instance Semantics ListW where
   semantics AppendW = (++)
 
 instance Syntax ListW where
-  prettySymbol AppendW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> short n <+> prettyPrec 10 y
-  prettySymbol AppendW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> prettyPrec 10 y <+> short n
+  prettySymbol AppendW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> viaShow n <+> prettyPrec 10 y
+  prettySymbol AppendW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "append_" <+> prettyPrec 10 y <+> viaShow n
   prettySymbol _ _ _ = Nothing
 
 instance Show (ListW d r) where

src/Constrained/Spec/Set.hs

@@ -87,7 +87,7 @@ prettySetSpec :: HasSpec a => SetSpec a -> Doc ann
 prettySetSpec (SetSpec must elemS size) =
   parens
     ( "SetSpec"
-        /> sep ["must=" <> short (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]
+        /> sep ["must=" <> viaShow (Set.toList must), "elem=" <> pretty elemS, "size=" <> pretty size]
     )
 
 instance HasSpec a => Show (SetSpec a) where
@@ -163,7 +163,7 @@ instance (Ord a, HasSpec a) => HasSpec (Set a) where
       ( NE.fromList
           [ "Choose size = " ++ show chosenSize
           , "szSpec' = " ++ show szSpec'
-          , "Picking items not in must = " ++ show (short (Set.toList must))
+          , "Picking items not in must = " ++ show (Set.toList must)
           , "that also meet the element test: "
           , "  " ++ show elemS
           ]
@@ -251,13 +251,13 @@ instance Semantics SetW where
   semantics = setSem
 
 instance Syntax SetW where
-  prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> short (Set.toList n) <+> prettyPrec 10 y
-  prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 10 y <+> short (Set.toList n)
-  prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 10 y <+> short (Set.toList n)
+  prettySymbol SubsetW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> viaShow (Set.toList n) <+> prettyPrec 10 y
+  prettySymbol SubsetW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "subset_" <+> prettyPrec 10 y <+> viaShow (Set.toList n)
+  prettySymbol DisjointW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> viaShow (Set.toList n) <+> prettyPrec 10 y
+  prettySymbol DisjointW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "disjoint_" <+> prettyPrec 10 y <+> viaShow (Set.toList n)
+  prettySymbol UnionW (Lit n :> y :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> viaShow (Set.toList n) <+> prettyPrec 10 y
+  prettySymbol UnionW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "union_" <+> prettyPrec 10 y <+> viaShow (Set.toList n)
+  prettySymbol MemberW (y :> Lit n :> Nil) p = Just $ parensIf (p > 10) $ "member_" <+> prettyPrec 10 y <+> viaShow (Set.toList n)
   prettySymbol _ _ _ = Nothing
 
 instance (Ord a, HasSpec a, HasSpec (Set a)) => Semigroup (Term (Set a)) where