Handle remaining casts

Fixes #804

Author: LeventErkok

Data/SBV/SMT/SMTLib2.hs

@@ -1250,14 +1250,34 @@ handleADT caps op args = case args of
 
         ascribe nm k = "(as " <> nm <> " " <> smtType k <> ")"
 
--- Various casts
+-- | Handle a kind-cast. This function only needs to cover the conversions that the type-safe API can actually
+-- produce; the dynamic 'svFromIntegral' can request other combinations, which we reject with an error.
+--
+-- The type-safe generators of a 'KindCast' are:
+--
+--     * 'sFromIntegral' : @Integral a => SBV a -> SBV b@. The source is 'Integral', so it is always 'KBounded'
+--       or 'KUnbounded'; the target is any @Num@/@SymVal@ kind (bounded, unbounded, real, rational, or float/double/FP).
+--     * 'sRealToSInteger': only ever emits @KReal -> KUnbounded@.
+--     * shift-amount adjustment: only ever emits @KBounded -> KBounded@.
+--
+-- So the reachable (from, to) pairs are exactly:
+--
+--     * @KBounded   -> {KBounded, KUnbounded, KReal, KRational, KFloat/KDouble/KFP}@
+--     * @KUnbounded -> {KBounded, KUnbounded, KReal, KRational, KFloat/KDouble/KFP}@
+--     * @KReal      -> KUnbounded@
+--
+-- All of these are handled below (float/double/FP targets are routed through 'handleFPCast' via 'tryFPCast'). Note
+-- that a real or rational can never be a source (reals only appear via 'sRealToSInteger', which targets 'KUnbounded';
+-- rationals are not 'Integral'), so those directions are unreachable and left to 'error'.
 handleKindCast :: Kind -> Kind -> Text -> Text
 handleKindCast kFrom kTo a
   | kFrom == kTo
   = a
   | True
   = case kFrom of
       KBounded s m -> case kTo of
+                        KReal        -> handleKindCast KUnbounded KReal     (handleKindCast kFrom KUnbounded a)
+                        KRational    -> handleKindCast KUnbounded KRational (handleKindCast kFrom KUnbounded a)
                         KBounded _ n -> fromBV (if s then signExtend else zeroExtend) m n
                         KUnbounded   -> if s then "(sbv_to_int " <> a <> ")"
                                              else "(ubv_to_int " <> a <> ")"
@@ -1266,6 +1286,7 @@ handleKindCast kFrom kTo a
       KUnbounded   -> case kTo of
                         KReal        -> "(to_real " <> a <> ")"
                         KBounded _ n -> "((_ int_to_bv " <> showText n <> ") " <> a <> ")"
+                        KRational    -> "(SBV.Rational " <> a <> " 1)"
                         _            -> tryFPCast
 
       KReal        -> case kTo of

SBVTestSuite/TestSuite/Basics/ArithSolver.hs

@@ -928,11 +928,21 @@ realRatConvs = [ testCase "realConv1" $ assertIsThm $ respectsLe sRealToSInteger
                , testCase "realConv3" $ assertIsThm realFloorCorrect2
                , testCase "realConv4" $ assertIsThm realCeilingCorrect
                , testCase "realConv5" $ assertIsThm realCeilingCorrect2
+
                , testCase "ratConv1"  $ assertIsThm $ respectsLe sRationalToSIntegerRM
                , testCase "ratConv2"  $ assertIsThm rationalFloorCorrect
                , testCase "ratConv3"  $ assertIsThm rationalFloorCorrect2
                , testCase "ratConv4"  $ assertIsThm rationalCeilingCorrect
                , testCase "ratConv5"  $ assertIsThm rationalCeilingCorrect2
+
+               , testCase "convertCov1" $ assertIsSat (\x y -> sFromIntegral @Word8   @Integer  x .== y)
+               , testCase "convertCov2" $ assertIsSat (\x y -> sFromIntegral @Integer @Word8    x .== y)
+               , testCase "convertCov3" $ assertIsSat (\x y -> sFromIntegral @Integer @AlgReal  x .== y)
+               , testCase "convertCov4" $ assertIsSat (\x y -> sFromIntegral @Integer @Float    x .== y)
+               , testCase "convertCov5" $ assertIsSat (\x y -> sFromIntegral @Word8   @Float    x .== y)
+               , testCase "convertCov6" $ assertIsSat (\x y -> sFromIntegral @Integer @Rational x .== y)
+               , testCase "convertCov7" $ assertIsSat (\x y -> sFromIntegral @Word8   @AlgReal  x .== y)
+               , testCase "convertCov8" $ assertIsSat (\x y -> sFromIntegral @Word8   @Rational x .== y)
                ]
  where -- (x <= y) ==> (round x <= round y)
        respectsLe :: OrdSymbolic a => (SRoundingMode -> a -> SInteger) -> SRoundingMode -> a -> a -> SBool