Skip to content

Commit

Permalink
Use a better field name
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Dec 3, 2024
1 parent b4e03ad commit d5a1cc5
Showing 1 changed file with 7 additions and 7 deletions.
14 changes: 7 additions & 7 deletions Data/SBV/Lambda.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down

0 comments on commit d5a1cc5

Please sign in to comment.