Add Tim's changes

Author: lehins

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

src/Constrained/GenT.hs

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

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]

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,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

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