From d5a1cc5a2aae996453d6aef4891f67b01f87ac83 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Tue, 3 Dec 2024 08:47:04 -0800 Subject: [PATCH] Use a better field name --- Data/SBV/Lambda.hs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Data/SBV/Lambda.hs b/Data/SBV/Lambda.hs index 76779491..cf8d1d98 100644 --- a/Data/SBV/Lambda.hs +++ b/Data/SBV/Lambda.hs @@ -144,19 +144,19 @@ lambdaGen allowFreeVars trans inState fk f = inSubState inState $ \st -> handle , "*** 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 ++ ")" + sh (Defn _unints Nothing _ops body) = body 0 + sh (Defn _unints (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 -> 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 + where mkLam (Defn unints params ops body) = SMTLam fk unints 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 -> 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 ++ ")" + where mkLam (Defn _unints Nothing _ops body) = body 0 + mkLam (Defn _unints (Just params) _ops body) = "(lambda " ++ extractAllUniversals params ++ "\n" ++ body 2 ++ ")" -- | Generaic creator for named functions, namedLambdaGen :: (MonadIO m, Lambda (SymbolicT m) a) => (Defn -> b) -> State -> Kind -> a -> m b @@ -165,12 +165,12 @@ namedLambdaGen trans inState fk f = inSubState inState $ \st -> trans <$> conver -- | Create a named SMTLib function, in the given state. namedLambda :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> Kind -> a -> m SMTDef namedLambda inState nm fk = namedLambdaGen mkDef inState fk - where mkDef (Defn frees params ops body) = SMTDef nm fk frees ops (extractAllUniversals <$> params) body + where mkDef (Defn unints params ops body) = SMTDef nm fk unints ops (extractAllUniversals <$> params) body -- | Create a named SMTLib function, in the given state, string version namedLambdaStr :: (MonadIO m, Lambda (SymbolicT m) a) => State -> String -> SBVType -> a -> m String namedLambdaStr inState nm t = namedLambdaGen mkDef inState fk - where mkDef (Defn frees params ops body) = concat $ declUserFuns [(SMTDef nm fk frees ops (extractAllUniversals <$> params) body, t)] + where mkDef (Defn unints params ops body) = concat $ declUserFuns [(SMTDef nm fk unints ops (extractAllUniversals <$> params) body, t)] fk = case t of SBVType [] -> error $ "namedLambdaStr: Invalid type for " ++ show nm ++ ", empty!" SBVType xs -> last xs