Improve debuggability when a plan fails

constrained-generators.cabal

@@ -15,6 +15,11 @@ source-repository head
   type: git
   location: https://github.com/input-output-hk/constrained-generators
 
+flag devel
+  description:       Enable development mode
+  default:           False
+  manual:            True
+
 library
   exposed-modules:
     Constrained.API
@@ -46,6 +51,23 @@ library
     Constrained.TypeErrors
 
   hs-source-dirs: src
+
+  if flag(devel)
+    exposed-modules:
+      Constrained.Examples
+      Constrained.Examples.Basic
+      Constrained.Examples.BinTree
+      Constrained.Examples.CheatSheet
+      Constrained.Examples.Either
+      Constrained.Examples.Fold
+      Constrained.Examples.List
+      Constrained.Examples.ManualExamples
+      Constrained.Examples.Map
+      Constrained.Examples.Set
+      Constrained.Examples.Tree
+
+    hs-source-dirs: examples
+
   default-language: Haskell2010
   ghc-options:
     -Wall

examples/Constrained/Examples/Basic.hs

@@ -319,3 +319,27 @@ wtfSpec = constrained' $ \ [var| options |] [var| mpair |] ->
         , assert $ unit ==. lit ()
         ]
     )
+
+manyInconsistent :: Specification (Int, Int, Int, Int, Int, Int)
+manyInconsistent = constrained' $ \ [var| a |] b c d e [var| f |] ->
+  [ assert $ a <. 10
+  , assert $ b >. a
+  , assert $ c >. b
+  , assert $ d >. c
+  , assert $ e >. d
+  , f `dependsOn` e
+  , assert $ f >. 10
+  , assert $ f <. a
+  ]
+
+manyInconsistentTrans :: Specification (Int, Int, Int, Int, Int, Int)
+manyInconsistentTrans = constrained' $ \ [var| a |] [var| b |] c d e [var| f |] ->
+  [ assert $ a <. 10
+  , assert $ b <. a
+  , assert $ c >. b
+  , assert $ d >. c
+  , assert $ e >. d
+  , f `dependsOn` e
+  , assert $ f >. 10
+  , assert $ f <. b
+  ]

examples/Constrained/Examples/Map.hs

@@ -125,3 +125,16 @@ mapSetSmall = constrained $ \x ->
 mapIsJust :: Specification (Int, Int)
 mapIsJust = constrained' $ \ [var| x |] [var| y |] ->
   just_ x ==. lookup_ y (lit $ Map.fromList [(z, z) | z <- [100 .. 102]])
+
+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
+      ]
+  ]

src/Constrained/AbstractSyntax.hs

@@ -134,6 +134,7 @@ fastInequality _ _ = True
 class Syntax (t :: [Type] -> Type -> Type) where
   isInfix :: t dom rng -> Bool
   isInfix _ = False
+
   prettySymbol ::
     forall deps dom rng ann.
     t dom rng ->
@@ -305,10 +306,9 @@ instance Pretty (PredD deps) where
         sep
           [ "memberPred"
           , pretty term
-          , "(" <> viaShow (length vs) <> " items)"
-          , brackets (fillSep (punctuate "," (map viaShow (NE.toList vs))))
+          , prettyShowList (NE.toList vs)
           ]
-    ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, fillSep (punctuate "," (map viaShow (NE.toList vs)))]
+    ElemPred False term vs -> align $ sep ["notMemberPred", pretty term, prettyShowList (NE.toList vs)]
     Exists _ (x :-> p) -> align $ sep ["exists" <+> viaShow x <+> "in", pretty p]
     Let t (x :-> p) -> align $ sep ["let" <+> viaShow x <+> "=" /> pretty t <+> "in", pretty p]
     And ps -> braces $ vsep' $ map pretty ps
@@ -377,15 +377,15 @@ 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" <+> prettyShowList (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 ->
       parensIf (d > 10) $
         "TypeSpec"
           /> vsep
             [ fromString (showsPrec 11 ts "")
-            , viaShow cant
+            , prettyShowList cant
             ]
 
 instance (Show a, Typeable a, Show (TypeSpecD deps a)) => Pretty (SpecificationD deps a) where

src/Constrained/Base.hs

@@ -99,7 +99,6 @@ import Constrained.FunctionSymbol
 import Constrained.GenT
 import Constrained.Generic
 import Constrained.List hiding (toList)
-import Constrained.PrettyUtils
 import Constrained.TypeErrors
 import Control.Monad.Writer (
   Writer,
@@ -671,8 +670,6 @@ instance Show (BaseW d r) where
   show FromGenericW = "fromSimpleRep"
 
 instance Syntax BaseW where
-  prettySymbol ToGenericW (x :> Nil) p = Just $ "to" <+> pretty (WithPrec p x)
-  prettySymbol FromGenericW (x :> Nil) p = Just $ "from" <+> pretty (WithPrec p x)
 
 instance Semantics BaseW where
   semantics FromGenericW = fromSimpleRep

src/Constrained/Env.hs

@@ -1,4 +1,6 @@
 {-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ImportQualifiedPost #-}
@@ -13,6 +15,7 @@ module Constrained.Env (
   lookup,
   find,
   remove,
+  filterKeys,
 ) where
 
 import Constrained.Core
@@ -34,7 +37,7 @@ data EnvValue where
 deriving instance Show EnvValue
 
 data EnvKey where
-  EnvKey :: !(Var a) -> EnvKey
+  EnvKey :: Typeable a => !(Var a) -> EnvKey
 
 instance Eq EnvKey where
   EnvKey v == EnvKey v' = nameOf v == nameOf v'
@@ -50,7 +53,7 @@ extend :: (Typeable a, Show a) => Var a -> a -> Env -> Env
 extend v a (Env m) = Env $ Map.insert (EnvKey v) (EnvValue a) m
 
 -- | Remove a variable from an environment if it exists
-remove :: Var a -> Env -> Env
+remove :: Typeable a => Var a -> Env -> Env
 remove v (Env m) = Env $ Map.delete (EnvKey v) m
 
 -- | Create a singleton environment
@@ -70,13 +73,18 @@ find env var = do
     Just a -> pure a
     Nothing -> genError ("Couldn't find " ++ show var ++ " in " ++ show env)
 
+-- | 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
+
 instance Pretty EnvValue where
-  pretty (EnvValue x) = pretty $ take 80 (show x)
+  pretty (EnvValue x) = viaShow x
 
 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) = vsep (map f (Map.toList m))
     where
       f (k, v) = hsep [pretty k, "->", pretty v]