search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
239 stars 33 forks source link

Make OptimizeResult type dependent on OptimizeStyle #707

Closed amigalemming closed 1 month ago

amigalemming commented 2 months ago

Currently OptimizeResult has three constructors that correspond to the three constructors of OptimizeStyle. This means, I have to perform a complete case analysis on the OptimizeResult constructors after an optmize although there can be only one constructor.

I suggest that instead optimize gets a type with a Style record or GADT or TypeFamily, in order to make the result dependent on the Style option, like so:

data OptimizeStyle result

optimize :: Satisfiable a => OptimizeStyle result -> a -> IO result

lexicographic :: OptimizeStyle LexicographicResult
independent :: OptimizeStyle IndependentResult
pareto :: Maybe Int -> OptimizeStyle ParetoResult

data LexicographicResult = LexicographicResult SMTResult
data ParetoResult = ParetoResult (Bool, [SMTResult])     
data IndependentResult = IndependentResult [(String, SMTResult)]
LeventErkok commented 2 months ago

Sure. Can you implement and submit a PR please; that way it'll get done a lot quicker.

If you can't spare the time, I'll get to this sometime next week, most likely.

LeventErkok commented 1 month ago

@amigalemming

I went for a low-tech solution, adding wrappers directly within SBV. This should simplify the end-user experience, and is definitely the lowest cost:

https://github.com/LeventErkok/sbv/blob/224e89c2744bb63de5623a9072550eb0bd224ca3/Data/SBV.hs#L1712-L1751

Let me know if this handles your use case and needs.

LeventErkok commented 1 month ago

I guess you lost interest in this, and looks like the additional API takes care of this problem. Feel free to file another ticket if you run into further issues.