Remove some minor cruft

Author: MaximilianAlgehed

src/Constrained/Base.hs

@@ -72,7 +72,6 @@ module Constrained.Base (
   -- * Building `Pred`, `Specification`, `Term` etc.
   bind,
   name,
-  named,
 
   -- * TODO: documentme
   propagateSpec,
@@ -772,12 +771,6 @@ 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/Generation.hs

@@ -51,7 +51,6 @@ module Constrained.Generation (
   pattern SumSpec,
 ) where
 
--- import Debug.Trace
 import Constrained.AbstractSyntax
 import Constrained.Base
 import Constrained.Conformance
@@ -98,40 +97,39 @@ 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

src/Constrained/Spec/Map.hs

@@ -186,7 +186,6 @@ 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
                 Result (k, v) ->

src/Constrained/Syntax.hs

@@ -211,6 +211,7 @@ 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
@@ -222,9 +223,9 @@ reifyWithName ::
   (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))
+  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