Implement firstification

Better support for higher-order funcs

CHANGES.md

@@ -5,13 +5,15 @@
 
   * Generalize the signatures of the default project-embed implementations of the Queriable class.
 
-  * Generalize support for higher-order functions. These are still experimental, as SMTLib's higher-order
-    function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which
-    is not released yet.) Currently, SBV can handle higher order versions of any, all, and filter, all
-    exported from Data.SBV.List module. These functions take as arguments lambda-functions, and SBV
-    translates them carefully for Z3 and CVC5 which has preliminary support. Proof-support in backend
-    solvers for higher-order functions is still quite weak, though KnuckleDragger makes things easier.
-    See Documentation.SBV.Examples.KnuckleDragger.Lists for several examples.
+  * Generalize support for polyorphic and higher-order functions. These are still experimental, as SMTLib's
+    higher-order function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which
+    is not released yet.) Currently, SBV can handle polymorphic and higher-order usage of: 'reverse', 'any', 'all', 'filter',
+    'map', 'foldl', 'foldr', 'zip', and 'zipWith'; all exported from the 'Data.SBV.List' module. These functions are supported
+    polymporphically, and (except reverse and zip) all take a function as an argument. SBV firstifies these
+    functions, and the resulting code is compatible with Z3 and CVC5. (Firstification might change in the
+    future, as SMTLib gains support for more higher-order features itself.) Proof-support in backend solvers
+    for higher-order functions is still quite weak, though KnuckleDragger makes things easier. See
+    Documentation.SBV.Examples.KnuckleDragger.Lists for several examples.
 
   * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These
     can now be defined by the user as we have proper support for fold and map using lambdas.

Data/SBV/Core/Model.hs

@@ -2510,7 +2510,7 @@ retrieveConstCode (UICodeC (v, _)) = Just v
 -- Plain constants
 instance HasKind a => SMTDefinable (SBV a) where
   sbv2smt a = do st <- mkNewState defaultSMTCfg (LambdaGen 0)
-                 s <- lambdaStr st (kindOf a) a
+                 s <- lambdaStr st True (kindOf a) a
                  pure $ intercalate "\n" [ "; Automatically generated by SBV. Do not modify!"
                                          , "; Type: " ++ smtType (kindOf a)
                                          , show s
@@ -3273,7 +3273,7 @@ lambdaArray :: forall a b. (SymVal a, HasKind b) => (SBV a -> SBV b) -> SArray a
 lambdaArray f = SBV . SVal k . Right $ cache g
   where k = KArray (kindOf (Proxy @a)) (kindOf (Proxy @b))
 
-        g st = do def <- lambdaStr st (kindOf (Proxy @b)) f
+        g st = do def <- lambdaStr st True (kindOf (Proxy @b)) f
                   newExpr st k (SBVApp (ArrayLambda def) [])
 
 -- | Turn a constant association-list and a default into a symbolic array.

Data/SBV/Core/Symbolic.hs

@@ -541,15 +541,15 @@ data SeqOp = SeqConcat                           -- ^ See StrConcat
            | SeqSuffixOf                         -- ^ See StrSuffixOf
            | SeqReplace                          -- ^ See StrReplace
            -- Polymorphic and higher order functions
-           | SBVReverse Kind                     -- ^ reverse k.       Where k is either [a] or String. Reverses the argument, accordingly.
-           | SBVZip     Kind Kind                -- ^ zip k1 k2.       Where we zip [k1] and [k2] to produce [(k1, k2)]
+           | SBVReverse Kind                     -- ^ reverse k.         Where k is either [a] or String. Reverses the argument, accordingly.
+           | SBVZip     Kind Kind                -- ^ zip k1 k2.         Where we zip [k1] and [k2] to produce [(k1, k2)]
            | SBVZipWith Kind Kind Kind SMTLambda -- ^ zipWith a b c fun. Where fun :: a -> b -> c, and zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]
-           | SBVMap     Kind Kind SMTLambda      -- ^ map    a b fun.  Where fun :: a -> b,      and map    :: (a -> b) -> [a] -> [b]
-           | SBVFoldl   Kind Kind SMTLambda      -- ^ foldl  a b fun.  Where fun :: b -> a -> b, and foldl  :: (b -> a -> b) -> b -> [a] -> b
-           | SBVFoldr   Kind Kind SMTLambda      -- ^ foldr  a b fun.  Where fun :: a -> b -> b, and foldr  :: (a -> b -> b) -> b -> [a] -> b
-           | SBVFilter  Kind      SMTLambda      -- ^ filter a fun.    Where fun :: a -> Bool,   and filter :: (a -> Bool) -> [a] -> [a]
-           | SBVAll     Kind      SMTLambda      -- ^ all    a fun.    Where fun :: a -> Bool,   and all    :: (a -> Bool) -> [a] -> Bool
-           | SBVAny     Kind      SMTLambda      -- ^ any    a fun.    Where fun :: a -> Bool,   and any    :: (a -> Bool) -> [a] -> Bool
+           | SBVMap     Kind Kind SMTLambda      -- ^ map    a b fun.    Where fun :: a -> b,      and map    :: (a -> b) -> [a] -> [b]
+           | SBVFoldl   Kind Kind SMTLambda      -- ^ foldl  a b fun.    Where fun :: b -> a -> b, and foldl  :: (b -> a -> b) -> b -> [a] -> b
+           | SBVFoldr   Kind Kind SMTLambda      -- ^ foldr  a b fun.    Where fun :: a -> b -> b, and foldr  :: (a -> b -> b) -> b -> [a] -> b
+           | SBVFilter  Kind      SMTLambda      -- ^ filter a fun.      Where fun :: a -> Bool,   and filter :: (a -> Bool) -> [a] -> [a]
+           | SBVAll     Kind      SMTLambda      -- ^ all    a fun.      Where fun :: a -> Bool,   and all    :: (a -> Bool) -> [a] -> Bool
+           | SBVAny     Kind      SMTLambda      -- ^ any    a fun.      Where fun :: a -> Bool,   and any    :: (a -> Bool) -> [a] -> Bool
   deriving (Eq, Ord, G.Data, NFData, Generic)
 
 -- | Show instance for SeqOp. Again, mapping is important.
@@ -2284,6 +2284,7 @@ data SMTConfig = SMTConfig {
        , ignoreExitCode              :: Bool                -- ^ If true, we shall ignore the exit code upon exit. Otherwise we require ExitSuccess.
        , redirectVerbose             :: Maybe FilePath      -- ^ Redirect the verbose output to this file if given. If Nothing, stdout is implied.
        , kdRibbonLength              :: Int                 -- ^ Line length for KD proofs
+       , firstifyUniqueLen           :: Int                 -- ^ Unique length used for firstified names.
        }
 
 -- | Ignore internal names and those the user told us to

Data/SBV/Lambda.hs

@@ -126,17 +126,35 @@ extractAllUniversals other      = error $ unlines [ ""
 
 
 -- | Generic creator for anonymous lamdas.
-lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b
-lambdaGen trans inState fk f = inSubState inState $ \st -> trans <$> convert st fk (mkLambda st f)
+lambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => Bool -> (Defn -> b) -> State -> Kind -> a -> m b
+lambdaGen allowFreeVars trans inState fk f = inSubState inState $ \st -> handle <$> convert st fk (mkLambda st f)
+  where handle d@(Defn frees _ _ _)
+          | allowFreeVars || null frees
+          = trans d
+          | True
+          = error $ unlines [ ""
+                            , "*** Data.SBV.Lambda: Detected free variables passed to a lambda."
+                            , "***"
+                            , "***  Free vars : " ++ unwords frees
+                            , "***  Definition: " ++ sh d
+                            , "***"
+                            , "*** In certain contexts, SBV only allows closed-lambdas, i.e., those that do not have any free variables in."
+                            , "***"
+                            , "*** Please rewrite your program to pass the free variable as an explicit argument to the lambda if possible."
+                            , "*** If this workaround isn't applicable, please report this as a use-case for further possible enhancements."
+                            ]
+
+        sh (Defn _frees Nothing       _ops body) = body 0
+        sh (Defn _frees (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")"
 
 -- | Create an SMTLib lambda, in the given state.
-lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTDef
-lambda inState fk = lambdaGen mkLam inState fk
+lambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Bool -> Kind -> a -> m SMTDef
+lambda inState allowFreeVars fk = lambdaGen allowFreeVars mkLam inState fk
    where mkLam (Defn frees params ops body) = SMTLam fk frees ops (extractAllUniversals <$> params) body
 
 -- | Create an anonymous lambda, rendered as n SMTLib string. The kind passed is the kind of the final result.
-lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Kind -> a -> m SMTLambda
-lambdaStr st k a = SMTLambda <$> lambdaGen mkLam st k a
+lambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> Bool -> Kind -> a -> m SMTLambda
+lambdaStr st allowFreeVars k a = SMTLambda <$> lambdaGen allowFreeVars mkLam st k a
    where mkLam (Defn _frees Nothing       _ops body) = body 0
          mkLam (Defn _frees (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")"
 
@@ -336,7 +354,7 @@ toLambda level curProgInfo cfg expectedKind result@Result{resAsgns = SBVPgm asgn
                  where mkAsgn (sv, e@(SBVApp (Label l) _)) = ((sv, converter e), Just l)
                        mkAsgn (sv, e)                      = ((sv, converter e), Nothing)
 
-                       converter = cvtExp curProgInfo (capabilities (solver cfg)) rm tableMap
+                       converter = cvtExp cfg curProgInfo (capabilities (solver cfg)) rm tableMap
 
 
                out :: SV

Data/SBV/List.hs

@@ -414,7 +414,7 @@ map f l
         kb  = kindOf (Proxy @b)
         klb = kindOf (Proxy @(SList b))
         r st = do sva <- sbvToSV st l
-                  lam <- lambdaStr st kb f
+                  lam <- lambdaStr st False kb f
                   let op = SeqOp (SBVMap ka kb lam)
                   registerSpecialFunction st op
                   newExpr st klb (SBVApp op [sva])
@@ -448,7 +448,7 @@ foldl f base l
         kb = kindOf (Proxy @b)
         r st = do svb <- sbvToSV st base
                   svl <- sbvToSV st l
-                  lam <- lambdaStr st kb f
+                  lam <- lambdaStr st False kb f
                   let op = SeqOp (SBVFoldl ka kb lam)
                   registerSpecialFunction st op
                   newExpr st kb (SBVApp op [svb, svl])
@@ -476,7 +476,7 @@ foldr f base l
         kb = kindOf (Proxy @b)
         r st = do svb <- sbvToSV st base
                   svl <- sbvToSV st l
-                  lam <- lambdaStr st kb f
+                  lam <- lambdaStr st False kb f
                   let op = SeqOp (SBVFoldr ka kb lam)
                   registerSpecialFunction st op
                   newExpr st kb (SBVApp op [svb, svl])
@@ -529,7 +529,7 @@ zipWith f xs ys
 
        r st = do svxs <- sbvToSV st xs
                  svys <- sbvToSV st ys
-                 lam <- lambdaStr st kb f
+                 lam <- lambdaStr st False kb f
                  let op = SeqOp (SBVZipWith ka kb kc lam)
                  registerSpecialFunction st op
                  newExpr st kr (SBVApp op [svxs, svys])
@@ -558,7 +558,7 @@ all f l
  | True
  = SBV $ SVal KBool $ Right $ cache r
  where r st = do sva <- sbvToSV st l
-                 lam <- lambdaStr st KBool f
+                 lam <- lambdaStr st False KBool f
                  let op = SeqOp (SBVAll (kindOf (Proxy @a)) lam)
                  registerSpecialFunction st op
                  newExpr st KBool (SBVApp op [sva])
@@ -577,7 +577,7 @@ any f l
  | True
  = SBV $ SVal KBool $ Right $ cache r
  where r st = do sva <- sbvToSV st l
-                 lam <- lambdaStr st KBool f
+                 lam <- lambdaStr st False KBool f
                  let op = SeqOp (SBVAny (kindOf (Proxy @a)) lam)
                  registerSpecialFunction st op
                  newExpr st KBool (SBVApp op [sva])
@@ -600,7 +600,7 @@ filter f l
 
         k = kindOf (Proxy @(SList a))
         r st = do sva <- sbvToSV st l
-                  lam <- lambdaStr st KBool f
+                  lam <- lambdaStr st False KBool f
                   let op = SeqOp (SBVFilter (kindOf (Proxy @a)) lam)
                   registerSpecialFunction st op
                   newExpr st k (SBVApp op [sva])

Data/SBV/Provers/Prover.hs

@@ -107,6 +107,7 @@ mkConfig s smtVersion startOpts = SMTConfig { verbose                     = Fals
                                             , ignoreExitCode              = False
                                             , redirectVerbose             = Nothing
                                             , kdRibbonLength              = 40
+                                            , firstifyUniqueLen           = 6
                                             }
 
 -- | If supported, this makes all output go to stdout, which works better with SBV