Runtime enums

[georgefst]

I have an application which requires dealing with user-defined enumerated types. As a simplification, suppose I have a map representing a set of enums:

e :: Map String [String]
e = Map.fromList [ ("E1", ["A","B","C"]), ("E2", ["X","Y"]) ]

and I use this to define the legal values of:

data UserEnum = String :. String

such that values include, for example, "E1" :. "A"and "E2" :. "X", but not "E1" :. "X".

I want to provide instances of HasKind UserEnum and SymVal UserEnum so that I can treat this simlarly to if I had:

data E1 = A | B | C deriving (Data, HasKind, SymVal)
data E2 = X | Y deriving (Data, HasKind, SymVal)

Is this possible? I can't find much documentation on writing manual instances of these classes.

[LeventErkok]

This is quite an unorthodox thing to do and will be brittle as you'll need to manufacture a type out of your values to make an instance of SymVal. But I'd go with something like:

{-# LANGUAGE ScopedTypeVariables #-}

import Data.SBV
import qualified Data.SBV.Internals as I

import Data.List (elemIndex)

data UEnum = UEnum String [String]
           deriving Show

uEnumKind :: UEnum -> Kind
uEnumKind (UEnum nm cstrs) = KUninterpreted nm (Right cstrs)

uEnumLit :: UEnum -> String -> SBV UEnum
uEnumLit e@(UEnum nm cstrs) l =
        let k = uEnumKind e
        in case l `elemIndex` cstrs of
             Nothing -> error $ "uEnumLit, bad value: " ++  show (e, l)
             Just i  -> I.SBV $ I.SVal k $ Left $ I.CV k $ I.CUserSort (Just i, l)

-- data E1 = A | B | C
e1 :: UEnum
e1 = UEnum "E1" ["A", "B", "C"]

-- You somehow have to manufacture this type. Template Haskell might help here.
data E1 = E1 UEnum String

instance HasKind E1 where
  kindOf (E1 ue _) = uEnumKind ue

instance SymVal E1 where
  literal (E1 ue l) = let I.SBV v = uEnumLit ue l in I.SBV v

  fromCV (I.CV (KUninterpreted nm (Right cstrs)) (I.CUserSort (_, l))) = E1 (UEnum nm cstrs) l
  fromCV x                                                             = error $ "fromCV, bad value: " ++ show x

  mkSymVal mbQ = I.mkSymSBV mbQ (uEnumKind e1)

With this, you can write:

test :: IO AllSatResult
test = allSat $ do x :: SBV E1 <- free "x"
                   y :: SBV E1 <- free "y"
                   constrain $ distinct [x, y]

When I run it, it produces:

*Main> test
Solution #1:
  x = B :: E1
  y = A :: E1
Solution #2:
  x = A :: E1
  y = B :: E1
Solution #3:
  x = C :: E1
  y = A :: E1
Solution #4:
  x = C :: E1
  y = B :: E1
Solution #5:
  x = A :: E1
  y = C :: E1
Solution #6:
  x = B :: E1
  y = C :: E1
Found 6 different solutions.

which seems to be about what you'd expect.

I'm not 100% sure if I understand what you are trying to do, but perhaps this'll get you started on the right path?

[georgefst]

Thanks for the detailed response. Unfortunately, manufacturing E1, as above, just isn't an option. These types are defined by the user at runtime (and there can be unbounded-ly many of them), so we can't have a one-to-one correspondence between user enums and Haskell types.

Therefore, I sense this isn't possible to do 'directly', and I'll have to manually create some sort of encoding in terms of, say, Int8s. Which will require some care but might not be too painful.

[LeventErkok]

This is less of an SBV question then. Imagine you want the minBound/maxBound instances for your "E1," i.e., want to make it an instance of the Bounded class. How would you do that at run-time?

The best solution I can come up with is to dump the data as a Haskell file at run-time, compile it, and start running that. That would be the absolute safest way of doing it. I don't see how you can manufacture instances like this without a datatype available.

But the good thing about this observation is that your problem is now independent of SBV. If you can figure out how to do that, you can use the same trick to solve your SBV related issue as well. You might want to ask at StackOverflow or Haskell cafe etc., to see if this might be possible. I faintly recall work around "Haskell plugins" (https://hackage.haskell.org/package/plugins) which might have some uses here; though I never used it.

In any case, this isn't really an SBV question. I'm closing it. But if you can figure out a way to do it using some other trick, please drop me a line. I'd be interested to hear.

[georgefst]

[...] make it an instance of the Bounded class. How would you do that at run-time?

I wouldn't. I haven't sussed out the details yet but I think I can get the behaviour I need by adding constraints on each enum-valued symbolic variable (which would actually be implemented as int-valued), to effectively set the correct range. This probably isn't maximally efficient for the solver, but I don't foresee it being a bottleneck.

Anything based around compiling Haskell at run-time is probably a no-go for me due to the need for ease of distribution, among other things, but I may look into it. Admittedly, the need to actually distribute anything probably distances me from the typical user of sbv...

Anyway, you're right to close this issue.

[LeventErkok]

Modeling through SWordN for some suitable N might work indeed. But this isn't in the spirit of SBV, or I'd say even Haskell. It's akin to modeling Bool as an Int. With sufficient discipline, I guess you can make it work, but you'll be leaving the type-safety on the floor. (This'll look like programming in Perl or Python..) Too bad this seems to be your only recourse.

[georgefst]

Oh, there's no question about that - this is a horrifically un-Haskell-y thing to do. But I've reached a point where I need to be pragmatic due to time constraints.

The goal here is performing various kinds of analysis of software requirements entered in a bespoke, high-level language. The tool was already written in Haskell before we decided that SMT-based analysis would be added, so we opted to use sbv, but I've been aware all along that this isn't quite aligned with the sbv synopsis:

Express properties about Haskell programs and automatically prove them using SMT solvers.

Up until now, this hadn't been a problem and the existing sbv-based code feels very elegant. Indeed I hadn't realised at the start of this project that we'd need to deal with user-defined types.

I guess perhaps what we really need is a slightly lower-level Haskell interface to smtlib, but sbv seemed by far the best option out there. I considered the direct Z3 bindings but, although we're using Z3 right now, we want to be able to easily switch solvers.

Anyway, FWIW, the tool I'm building is partly a replacement for an older one in which even Bools were modelled as Int (and that sort of thing isn't why we're replacing it, at least not directly). And there have been recent discussions about whether we should, for example, allow implicit casting between enums and Int in the requirements language. So I'm not exactly winning the 'strong types' argument...

[LeventErkok]

Best of luck with that! Feel free to ping if you run into any other SBV related issues.