grisette-0.1.0.0: src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
-- |
-- Module : Grisette.Backend.SBV.Data.SMT.Lowering
-- Copyright : (c) Sirui Lu 2021-2023
-- License : BSD-3-Clause (see the LICENSE file)
--
-- Maintainer : siruilu@cs.washington.edu
-- Stability : Experimental
-- Portability : GHC only
module Grisette.Backend.SBV.Data.SMT.Lowering
( lowerSinglePrim,
lowerSinglePrim',
parseModel,
SymBiMap,
)
where
import Control.Monad.State.Strict
import Data.Bifunctor
import Data.Bits
import Data.Dynamic
import Data.Foldable
import Data.Kind
import Data.Maybe
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBVI
import Data.Type.Equality (type (~~))
import Data.Typeable
import GHC.Exts (sortWith)
import GHC.Natural
import GHC.Stack
import GHC.TypeNats
import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving
import Grisette.Backend.SBV.Data.SMT.SymBiMap
import Grisette.Core.Data.Class.ModelOps
import Grisette.IR.SymPrim.Data.BV
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
import Grisette.IR.SymPrim.Data.Prim.Model as PM
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.TabularFun
import qualified Type.Reflection as R
import Unsafe.Coerce
newtype NatRepr (n :: Nat) = NatRepr Natural
withKnownNat :: forall n r. NatRepr n -> (KnownNat n => r) -> r
withKnownNat (NatRepr nVal) v =
case someNatVal nVal of
SomeNat (Proxy :: Proxy n') ->
case unsafeAxiom :: n :~: n' of
Refl -> v
data LeqProof (m :: Nat) (n :: Nat) where
LeqProof :: m <= n => LeqProof m n
-- | Assert a proof of equality between two types.
-- This is unsafe if used improperly, so use this with caution!
unsafeAxiom :: forall a b. a :~: b
unsafeAxiom = unsafeCoerce (Refl @a)
{-# NOINLINE unsafeAxiom #-} -- Note [Mark unsafe axioms as NOINLINE]
unsafeLeqProof :: forall m n. LeqProof m n
unsafeLeqProof = unsafeCoerce (LeqProof @0 @0)
{-# NOINLINE unsafeLeqProof #-} -- Note [Mark unsafe axioms as NOINLINE]
cachedResult ::
forall integerBitWidth a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a ->
State SymBiMap (Maybe (TermTy integerBitWidth a))
cachedResult t = gets $ \m -> do
d <- lookupTerm (SomeTerm t) m
Just $ fromDyn d undefined
addResult ::
forall integerBitWidth a.
(SupportedPrim a, Typeable (TermTy integerBitWidth a)) =>
Term a ->
TermTy integerBitWidth a ->
State SymBiMap ()
addResult tm sbvtm = modify $ addBiMapIntermediate (SomeTerm tm) (toDyn sbvtm)
lowerSinglePrim' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
(TermTy integerBitWidth a, SymBiMap)
lowerSinglePrim' config t = runState (lowerSinglePrimCached' config t)
lowerSinglePrimCached' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimCached' config t = introSupportedPrimConstraint t $
case (config, R.typeRep @a) of
ResolvedDeepType -> do
r <- cachedResult @integerBitWidth t
case r of
Just v -> return v
_ -> lowerSinglePrimImpl' config t
_ -> translateTypeError (R.typeRep @a)
lowerUnaryTerm' ::
forall integerBitWidth a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, x1 ~ TermTy integerBitWidth x) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
(a1 -> x1) ->
State SymBiMap (TermTy integerBitWidth x)
lowerUnaryTerm' config orig t1 f = do
l1 <- lowerSinglePrimCached' config t1
let g = f l1
addResult @integerBitWidth orig g
return g
lowerBinaryTerm' ::
forall integerBitWidth a b a1 b1 x.
( Typeable (TermTy integerBitWidth x),
a1 ~ TermTy integerBitWidth a,
b1 ~ TermTy integerBitWidth b,
SupportedPrim x
) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
Term b ->
(a1 -> b1 -> TermTy integerBitWidth x) ->
State SymBiMap (TermTy integerBitWidth x)
lowerBinaryTerm' config orig t1 t2 f = do
l1 <- lowerSinglePrimCached' config t1
l2 <- lowerSinglePrimCached' config t2
let g = f l1 l2
addResult @integerBitWidth orig g
return g
lowerSinglePrimImpl' ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
State SymBiMap (TermTy integerBitWidth a)
lowerSinglePrimImpl' ResolvedConfig {} (ConTerm _ v) =
case R.typeRep @a of
BoolType -> return $ if v then SBV.sTrue else SBV.sFalse
IntegerType -> return $ fromInteger v
SignedBVType _ -> case v of
IntN x -> return $ fromInteger x
UnsignedBVType _ -> case v of
WordN x -> return $ fromInteger x
_ -> translateTypeError (R.typeRep @a)
lowerSinglePrimImpl' _ t@SymTerm {} =
error $
"The symbolic term should have already been lowered "
++ show t
++ " to SMT with collectedPrims.\n"
++ "We don't support adding new symbolics after collectedPrims with SBV backend"
lowerSinglePrimImpl' _ (UnaryTerm _ op (_ :: Term x)) = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateUnaryError (show op) (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl' _ (BinaryTerm _ op (_ :: Term x) (_ :: Term y)) = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateBinaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)
lowerSinglePrimImpl' ResolvedConfig {} (TernaryTerm _ op (_ :: Term x) (_ :: Term y) (_ :: Term z)) = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateTernaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @z) (R.typeRep @a)
lowerSinglePrimImpl' config t@(NotTerm _ arg) = lowerUnaryTerm' config t arg SBV.sNot
lowerSinglePrimImpl' config t@(OrTerm _ arg1 arg2) = lowerBinaryTerm' config t arg1 arg2 (SBV..||)
lowerSinglePrimImpl' config t@(AndTerm _ arg1 arg2) = lowerBinaryTerm' config t arg1 arg2 (SBV..&&)
lowerSinglePrimImpl' config t@(EqvTerm _ (arg1 :: Term x) arg2) =
case (config, R.typeRep @x) of
ResolvedSimpleType -> lowerBinaryTerm' config t arg1 arg2 (SBV..==)
_ -> translateBinaryError "(==)" (R.typeRep @x) (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl' config t@(ITETerm _ cond arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedSimpleType -> do
l1 <- lowerSinglePrimCached' config cond
l2 <- lowerSinglePrimCached' config arg1
l3 <- lowerSinglePrimCached' config arg2
let g = SBV.ite l1 l2 l3
addResult @integerBitWidth t g
return g
_ -> translateTernaryError "ite" (R.typeRep @Bool) (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(AddNumTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerBinaryTerm' config t arg1 arg2 (+)
_ -> translateBinaryError "(+)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(UMinusNumTerm _ arg) =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm' config t arg negate
_ -> translateUnaryError "negate" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(TimesNumTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerBinaryTerm' config t arg1 arg2 (*)
_ -> translateBinaryError "(*)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(AbsNumTerm _ arg) =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm' config t arg abs
_ -> translateUnaryError "abs" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(SignumNumTerm _ arg) =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm' config t arg signum
_ -> translateUnaryError "signum" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(LTNumTerm _ (arg1 :: Term arg) arg2) =
case (config, R.typeRep @arg) of
ResolvedNumOrdType -> lowerBinaryTerm' config t arg1 arg2 (SBV..<)
_ -> translateBinaryError "(<)" (R.typeRep @arg) (R.typeRep @arg) (R.typeRep @Bool)
lowerSinglePrimImpl' config t@(LENumTerm _ (arg1 :: Term arg) arg2) =
case (config, R.typeRep @arg) of
ResolvedNumOrdType -> lowerBinaryTerm' config t arg1 arg2 (SBV..<=)
_ -> translateBinaryError "(<=)" (R.typeRep @arg) (R.typeRep @arg) (R.typeRep @Bool)
lowerSinglePrimImpl' config t@(AndBitsTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 (.&.)
_ -> translateBinaryError "(.&.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(OrBitsTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 (.|.)
_ -> translateBinaryError "(.|.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(XorBitsTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm' config t arg1 arg2 xor
_ -> translateBinaryError "xor" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(ComplementBitsTerm _ arg) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm' config t arg complement
_ -> translateUnaryError "complement" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(ShiftBitsTerm _ arg n) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm' config t arg (`shift` n)
_ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl' config t@(RotateBitsTerm _ arg n) =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm' config t arg (`rotate` n)
_ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl' config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) =
case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->
case (unsafeAxiom @(nx + ny) @na) of
Refl -> lowerBinaryTerm' config t bv1 bv2 (SBV.#)
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx), SignedBVType (_ :: Proxy ny)) ->
case (unsafeAxiom @(nx + ny) @na) of
Refl ->
lowerBinaryTerm'
config
t
bv1
bv2
( \(x :: SBV.SInt xn) (y :: SBV.SInt yn) ->
SBV.sFromIntegral $
(SBV.sFromIntegral x :: SBV.SWord xn) SBV.# (SBV.sFromIntegral y :: SBV.SWord yn)
)
_ -> translateBinaryError "bvconcat" (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)
lowerSinglePrimImpl' config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) =
case (R.typeRep @a, R.typeRep @x) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->
withKnownNat n1 $
case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
unsafeLeqProof @(na + ix - 1 + 1) @xn,
unsafeLeqProof @ix @(na + ix - 1)
) of
(Refl, LeqProof, LeqProof) ->
lowerUnaryTerm' config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix))
where
n1 :: NatRepr (na + ix - 1)
n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->
withKnownNat n1 $
case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
unsafeLeqProof @(na + ix - 1 + 1) @xn,
unsafeLeqProof @ix @(na + ix - 1)
) of
(Refl, LeqProof, LeqProof) ->
lowerUnaryTerm' config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix))
where
n1 :: NatRepr (na + ix - 1)
n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
_ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl' config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) =
case (R.typeRep @a, R.typeRep @x) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
(LeqProof, LeqProof) ->
bvIsNonZeroFromGEq1 @(na - nx) $
lowerUnaryTerm' config t bv (if signed then SBV.signExtend else SBV.zeroExtend)
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
(LeqProof, LeqProof) ->
bvIsNonZeroFromGEq1 @(na - nx) $
lowerUnaryTerm'
config
t
bv
( if signed
then SBV.signExtend
else \x ->
SBV.sFromIntegral
(SBV.zeroExtend (SBV.sFromIntegral x :: SBV.SBV (SBV.WordN nx)) :: SBV.SBV (SBV.WordN na))
)
_ -> translateTernaryError "bvextend" (R.typeRep @Bool) n (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl' config t@(TabularFunApplyTerm _ (f :: Term (b =-> a)) (arg :: Term b)) =
case (config, R.typeRep @a) of
ResolvedDeepType -> do
l1 <- lowerSinglePrimCached' config f
l2 <- lowerSinglePrimCached' config arg
let g = l1 l2
addResult @integerBitWidth t g
return g
_ -> translateBinaryError "tabularApply" (R.typeRep @(b =-> a)) (R.typeRep @b) (R.typeRep @a)
lowerSinglePrimImpl' config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg :: Term b)) =
case (config, R.typeRep @a) of
ResolvedDeepType -> do
l1 <- lowerSinglePrimCached' config f
l2 <- lowerSinglePrimCached' config arg
let g = l1 l2
addResult @integerBitWidth t g
return g
_ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)
lowerSinglePrimImpl' config t@(DivIntegerTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
(ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sDiv
_ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' config t@(ModIntegerTerm _ arg1 arg2) =
case (config, R.typeRep @a) of
(ResolvedConfig {}, IntegerType) -> lowerBinaryTerm' config t arg1 arg2 SBV.sMod
_ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl' _ _ = undefined
buildUTFun11 ::
forall integerBitWidth s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2)))
buildUTFun11 config ta tb term@(SymTerm _ ts) m = case ((config, ta), (config, tb)) of
(ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f = SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) name
in Just $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun11 _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun111 ::
forall integerBitWidth s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3)))
buildUTFun111 config ta tb tc term@(SymTerm _ ts) m = case ((config, ta), (config, tb), (config, tc)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)
name
in Just $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun11 ::
forall integerBitWidth s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2)))
buildUGFun11 config ta tb term@(SymTerm _ ts) m = case ((config, ta), (config, tb)) of
(ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f = SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2) name
in Just $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun11 _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun111 ::
forall integerBitWidth s1 s2 s3 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3)))
buildUGFun111 config ta tb tc term@(SymTerm _ ts) m = case ((config, ta), (config, tb), (config, tc)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3)
name
in Just $ return (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"
lowerSinglePrimUFun ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))
lowerSinglePrimUFun config t@(SymTerm _ _) m =
case R.typeRep @a of
TFun3Type (t1 :: R.TypeRep a1) (t2 :: R.TypeRep a2) (t3 :: R.TypeRep a3) -> buildUTFun111 config t1 t2 t3 t m
TFunType (ta :: R.TypeRep b) (tb :: R.TypeRep b1) -> buildUTFun11 config ta tb t m
GFun3Type (t1 :: R.TypeRep a1) (t2 :: R.TypeRep a2) (t3 :: R.TypeRep a3) -> buildUGFun111 config t1 t2 t3 t m
GFunType (ta :: R.TypeRep b) (tb :: R.TypeRep b1) -> buildUGFun11 config ta tb t m
_ -> Nothing
lowerSinglePrimUFun _ _ _ = error "Should not call this function"
lowerUnaryTerm ::
forall integerBitWidth a a1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
(a1 -> x1) ->
SymBiMap ->
SBV.Symbolic (SymBiMap, x1)
lowerUnaryTerm config orig t1 f m = do
(m1, l1) <- lowerSinglePrimCached config t1 m
let g = f l1
return (addBiMapIntermediate (SomeTerm orig) (toDyn g) m1, g)
lowerBinaryTerm ::
forall integerBitWidth a b a1 b1 x x1.
(Typeable x1, a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
Term b ->
(a1 -> b1 -> x1) ->
SymBiMap ->
SBV.Symbolic (SymBiMap, x1)
lowerBinaryTerm config orig t1 t2 f m = do
(m1, l1) <- lowerSinglePrimCached config t1 m
(m2, l2) <- lowerSinglePrimCached config t2 m1
let g = f l1 l2
return (addBiMapIntermediate (SomeTerm orig) (toDyn g) m2, g)
lowerSinglePrimCached ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimCached config t m =
introSupportedPrimConstraint t $
case (config, R.typeRep @a) of
ResolvedDeepType ->
case lookupTerm (SomeTerm t) m of
Just x -> return (m, fromDyn x undefined)
Nothing -> lowerSinglePrimImpl config t m
_ -> translateTypeError (R.typeRep @a)
lowerSinglePrim ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim config t = lowerSinglePrimCached config t emptySymBiMap
translateTypeError :: HasCallStack => R.TypeRep a -> b
translateTypeError ta =
error $
"Don't know how to translate the type " ++ show ta ++ " to SMT"
translateUnaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> c
translateUnaryError op ta tb =
error $
"Don't know how to translate the op "
++ show op
++ " :: "
++ show ta
++ " -> "
++ show tb
++ " to SMT"
translateBinaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> d
translateBinaryError op ta tb tc =
error $
"Don't know how to translate the op "
++ show op
++ " :: "
++ show ta
++ " -> "
++ show tb
++ " -> "
++ show tc
++ " to SMT"
translateTernaryError :: HasCallStack => String -> R.TypeRep a -> R.TypeRep b -> R.TypeRep c -> R.TypeRep d -> e
translateTernaryError op ta tb tc td =
error $
"Don't know how to translate the op "
++ show op
++ " :: "
++ show ta
++ " -> "
++ show tb
++ " -> "
++ show tc
++ " -> "
++ show td
++ " to SMT"
lowerSinglePrimImpl ::
forall integerBitWidth a.
HasCallStack =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimImpl ResolvedConfig {} (ConTerm _ v) m =
case R.typeRep @a of
BoolType -> return (m, if v then SBV.sTrue else SBV.sFalse)
IntegerType -> return (m, fromInteger v)
SignedBVType _ -> case v of
IntN x -> return (m, fromInteger x)
UnsignedBVType _ -> case v of
WordN x -> return (m, fromInteger x)
_ -> translateTypeError (R.typeRep @a)
lowerSinglePrimImpl config t@(SymTerm _ ts) m =
fromMaybe errorMsg $ asum [simple, ufunc]
where
errorMsg :: forall x. x
errorMsg = translateTypeError (R.typeRep @a)
simple :: Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a))
simple = case (config, R.typeRep @a) of
ResolvedSimpleType -> Just $ do
let name = show ts
(g :: TermTy integerBitWidth a) <- SBV.free name
return (addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m, g)
_ -> Nothing
ufunc :: (Maybe (SBV.Symbolic (SymBiMap, TermTy integerBitWidth a)))
ufunc = lowerSinglePrimUFun config t m
lowerSinglePrimImpl _ (UnaryTerm _ op (_ :: Term x)) _ = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateUnaryError (show op) (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl _ (BinaryTerm _ op (_ :: Term x) (_ :: Term y)) _ = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateBinaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)
lowerSinglePrimImpl ResolvedConfig {} (TernaryTerm _ op (_ :: Term x) (_ :: Term y) (_ :: Term z)) _ = errorMsg
where
errorMsg :: forall t1. t1
errorMsg = translateTernaryError (show op) (R.typeRep @x) (R.typeRep @y) (R.typeRep @z) (R.typeRep @a)
lowerSinglePrimImpl config t@(NotTerm _ arg) m = lowerUnaryTerm config t arg SBV.sNot m
lowerSinglePrimImpl config t@(OrTerm _ arg1 arg2) m = lowerBinaryTerm config t arg1 arg2 (SBV..||) m
lowerSinglePrimImpl config t@(AndTerm _ arg1 arg2) m = lowerBinaryTerm config t arg1 arg2 (SBV..&&) m
lowerSinglePrimImpl config t@(EqvTerm _ (arg1 :: Term x) arg2) m =
case (config, R.typeRep @x) of
ResolvedSimpleType -> lowerBinaryTerm config t arg1 arg2 (SBV..==) m
_ -> translateBinaryError "(==)" (R.typeRep @x) (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl config t@(ITETerm _ cond arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSimpleType -> do
(m1, l1) <- lowerSinglePrimCached config cond m
(m2, l2) <- lowerSinglePrimCached config arg1 m1
(m3, l3) <- lowerSinglePrimCached config arg2 m2
let g = SBV.ite l1 l2 l3
return (addBiMapIntermediate (SomeTerm t) (toDyn g) m3, g)
_ -> translateBinaryError "ite" (R.typeRep @Bool) (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(AddNumTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerBinaryTerm config t arg1 arg2 (+) m
_ -> translateBinaryError "(+)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(UMinusNumTerm _ arg) m =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm config t arg negate m
_ -> translateUnaryError "negate" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(TimesNumTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerBinaryTerm config t arg1 arg2 (*) m
_ -> translateBinaryError "(*)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(AbsNumTerm _ arg) m =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm config t arg abs m
_ -> translateUnaryError "abs" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(SignumNumTerm _ arg) m =
case (config, R.typeRep @a) of
ResolvedNumType -> lowerUnaryTerm config t arg signum m
_ -> translateUnaryError "signum" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(LTNumTerm _ (arg1 :: Term arg) arg2) m =
case (config, R.typeRep @arg) of
ResolvedNumOrdType -> lowerBinaryTerm config t arg1 arg2 (SBV..<) m
_ -> translateBinaryError "(<)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @Bool)
lowerSinglePrimImpl config t@(LENumTerm _ (arg1 :: Term arg) arg2) m =
case (config, R.typeRep @arg) of
ResolvedNumOrdType -> lowerBinaryTerm config t arg1 arg2 (SBV..<=) m
_ -> translateBinaryError "(<=)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @Bool)
lowerSinglePrimImpl config t@(AndBitsTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 (.&.) m
_ -> translateBinaryError "(.&.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(OrBitsTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 (.|.) m
_ -> translateBinaryError "(.|.)" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(XorBitsTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm config t arg1 arg2 xor m
_ -> translateBinaryError "xor" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(ComplementBitsTerm _ arg) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm config t arg complement m
_ -> translateUnaryError "complement" (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(ShiftBitsTerm _ arg n) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm config t arg (`shift` n) m
_ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl config t@(RotateBitsTerm _ arg n) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m
_ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =
case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->
case (unsafeAxiom @(nx + ny) @na) of
Refl -> lowerBinaryTerm config t bv1 bv2 (SBV.#) m
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx), SignedBVType (_ :: Proxy ny)) ->
case (unsafeAxiom @(nx + ny) @na) of
Refl ->
lowerBinaryTerm
config
t
bv1
bv2
( \(x :: SBV.SInt xn) (y :: SBV.SInt yn) ->
SBV.sFromIntegral $
(SBV.sFromIntegral x :: SBV.SWord xn) SBV.# (SBV.sFromIntegral y :: SBV.SWord yn)
)
m
_ -> translateBinaryError "bvconcat" (R.typeRep @x) (R.typeRep @y) (R.typeRep @a)
lowerSinglePrimImpl config t@(BVSelectTerm _ (ix :: R.TypeRep ix) w (bv :: Term x)) m =
case (R.typeRep @a, R.typeRep @x) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy xn)) ->
withKnownNat n1 $
case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
unsafeLeqProof @(na + ix - 1 + 1) @xn,
unsafeLeqProof @ix @(na + ix - 1)
) of
(Refl, LeqProof, LeqProof) ->
lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m
where
n1 :: NatRepr (na + ix - 1)
n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->
withKnownNat n1 $
case ( unsafeAxiom @(na + ix - 1 - ix + 1) @na,
unsafeLeqProof @(na + ix - 1 + 1) @xn,
unsafeLeqProof @ix @(na + ix - 1)
) of
(Refl, LeqProof, LeqProof) ->
lowerUnaryTerm config t bv (SBV.bvExtract (Proxy @(na + ix - 1)) (Proxy @ix)) m
where
n1 :: NatRepr (na + ix - 1)
n1 = NatRepr (natVal (Proxy @na) + natVal (Proxy @ix) - 1)
_ -> translateTernaryError "bvselect" ix w (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl config t@(BVExtendTerm _ signed (n :: R.TypeRep n) (bv :: Term x)) m =
case (R.typeRep @a, R.typeRep @x) of
(UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
(LeqProof, LeqProof) ->
bvIsNonZeroFromGEq1 @(na - nx) $
lowerUnaryTerm config t bv (if signed then SBV.signExtend else SBV.zeroExtend) m
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
withKnownNat (NatRepr (natVal (Proxy @na) - natVal (Proxy @nx)) :: NatRepr (na - nx)) $
case (unsafeLeqProof @(nx + 1) @na, unsafeLeqProof @1 @(na - nx)) of
(LeqProof, LeqProof) ->
bvIsNonZeroFromGEq1 @(na - nx) $
lowerUnaryTerm
config
t
bv
( if signed
then SBV.signExtend
else \x ->
SBV.sFromIntegral
(SBV.zeroExtend (SBV.sFromIntegral x :: SBV.SBV (SBV.WordN nx)) :: SBV.SBV (SBV.WordN na))
)
m
_ -> translateTernaryError "bvextend" (R.typeRep @Bool) n (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl config t@(TabularFunApplyTerm _ (f :: Term (b =-> a)) (arg :: Term b)) m =
case (config, R.typeRep @a) of
ResolvedDeepType -> do
(m1, l1) <- lowerSinglePrimCached config f m
(m2, l2) <- lowerSinglePrimCached config arg m1
let g = l1 l2
return (addBiMapIntermediate (SomeTerm t) (toDyn g) m2, g)
_ -> translateBinaryError "tabularApply" (R.typeRep @(b =-> a)) (R.typeRep @b) (R.typeRep @a)
lowerSinglePrimImpl config t@(GeneralFunApplyTerm _ (f :: Term (b --> a)) (arg :: Term b)) m =
case (config, R.typeRep @a) of
ResolvedDeepType -> do
(m1, l1) <- lowerSinglePrimCached config f m
(m2, l2) <- lowerSinglePrimCached config arg m1
let g = l1 l2
return (addBiMapIntermediate (SomeTerm t) (toDyn g) m2, g)
_ -> translateBinaryError "generalApply" (R.typeRep @(b --> a)) (R.typeRep @b) (R.typeRep @a)
lowerSinglePrimImpl config t@(DivIntegerTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
(ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
_ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(ModIntegerTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
(ResolvedConfig {}, IntegerType) -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
_ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl _ _ _ = error "Should never happen"
unsafeMkNatRepr :: Int -> NatRepr w
unsafeMkNatRepr x = NatRepr (fromInteger $ toInteger x)
unsafeWithNonZeroKnownNat :: forall w r. Int -> ((KnownNat w, 1 <= w) => r) -> r
unsafeWithNonZeroKnownNat i r
| i <= 0 = error "Not an nonzero natural number"
| otherwise = withKnownNat @w (unsafeMkNatRepr i) $ unsafeBVIsNonZero r
where
unsafeBVIsNonZero :: ((1 <= w) => r) -> r
unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of
Refl -> r1
bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
Refl -> r1
parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model
parseModel _ (SBVI.SMTModel _ _ assoc uifuncs) mp = foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
where
goassoc :: (String, SBVI.CV) -> PM.Model -> PM.Model
goassoc (name, cv) m = case findStringToSymbol name mp of
Just (SomeTypedSymbol tr s) ->
insertValue s (resolveSingle tr cv) m
Nothing -> error "Bad"
resolveSingle :: R.TypeRep a -> SBVI.CV -> a
resolveSingle t (SBVI.CV SBVI.KBool (SBVI.CInteger n)) =
case R.eqTypeRep t (R.typeRep @Bool) of
Just R.HRefl -> n /= 0
Nothing -> error "Bad type"
resolveSingle t (SBVI.CV SBVI.KUnbounded (SBVI.CInteger i)) =
case R.eqTypeRep t (R.typeRep @Integer) of
Just R.HRefl -> i
Nothing -> error "Bad type"
resolveSingle t (SBVI.CV (SBVI.KBounded _ bitWidth) (SBVI.CInteger i)) =
case R.eqTypeRep t (R.typeRep @Integer) of
Just R.HRefl -> i
_ -> case t of
R.App a (n :: R.TypeRep w) ->
case R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat) of
Just R.HRefl ->
unsafeWithNonZeroKnownNat @w bitWidth $
case (R.eqTypeRep a (R.typeRep @IntN), R.eqTypeRep a (R.typeRep @WordN)) of
(Just R.HRefl, _) ->
fromInteger i
(_, Just R.HRefl) -> fromInteger i
_ -> error "Bad type"
_ -> error "Bad type"
_ -> error "Bad type"
resolveSingle _ _ = error "Unknown cv"
buildConstFun :: (SupportedPrim a, SupportedPrim r) => R.TypeRep a -> R.TypeRep r -> SBVI.CV -> a =-> r
buildConstFun _ tr v = case tr of
TFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) -> TabularFun [] $ buildConstFun ta2' tr2' v
_ -> TabularFun [] $ resolveSingle tr v
goutfuncResolve ::
forall a r.
(SupportedPrim a, SupportedPrim r) =>
R.TypeRep a ->
R.TypeRep r ->
([([SBVI.CV], SBVI.CV)], SBVI.CV) ->
(a =-> r)
goutfuncResolve ta1 ta2 (l, s) =
case ta2 of
TFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) ->
TabularFun
(second (\r -> goutfuncResolve ta2' tr2' (r, s)) <$> partition ta1 l)
(buildConstFun ta2' tr2' s)
_ ->
TabularFun
(bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l)
(resolveSingle ta2 s)
gougfuncResolve ::
forall a r.
(SupportedPrim a, SupportedPrim r) =>
Int ->
R.TypeRep a ->
R.TypeRep r ->
([([SBVI.CV], SBVI.CV)], SBVI.CV) ->
(a --> r)
gougfuncResolve idx ta1 ta2 (l, s) =
case ta2 of
GFunType (ta2' :: R.TypeRep a2) (tr2' :: R.TypeRep r2) ->
let sym = WithInfo (IndexedSymbol "arg" idx) FunArg
funs = second (\r -> gougfuncResolve (idx + 1) ta2' tr2' (r, s)) <$> partition ta1 l
def = gougfuncResolve (idx + 1) ta2' tr2' ([], s)
body =
foldl'
( \acc (v, f) ->
pevalITETerm
(pevalEqvTerm (iinfosymTerm "arg" idx FunArg) (conTerm v))
(conTerm f)
acc
)
(conTerm def)
funs
in GeneralFun sym body
_ ->
let sym = WithInfo (IndexedSymbol "arg" idx) FunArg
vs = bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l
def = resolveSingle ta2 s
body =
foldl'
( \acc (v, a) ->
pevalITETerm
(pevalEqvTerm (iinfosymTerm "arg" idx FunArg) (conTerm v))
(conTerm a)
acc
)
(conTerm def)
vs
in GeneralFun sym body
partition :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
partition t = case (R.eqTypeRep t (R.typeRep @Bool), R.eqTypeRep t (R.typeRep @Integer)) of
(Just R.HRefl, _) -> partitionWithOrd . resolveFirst t
(_, Just R.HRefl) -> partitionWithOrd . resolveFirst t
_ -> case t of
R.App bv _ -> case (R.eqTypeRep bv (R.typeRep @IntN), R.eqTypeRep bv (R.typeRep @WordN)) of
(Just R.HRefl, _) -> fmap (first IntN) . partitionWithOrd . fmap (first unIntN) . resolveFirst t
(_, Just R.HRefl) -> partitionWithOrd . resolveFirst t
_ -> error "Unknown type"
_ -> error "Unknown type"
resolveFirst :: R.TypeRep a -> [([SBVI.CV], SBVI.CV)] -> [(a, [([SBVI.CV], SBVI.CV)])]
resolveFirst tf = fmap (\case (x : xs, v) -> (resolveSingle tf x, [(xs, v)]); _ -> error "impossible")
partitionWithOrd :: forall a. Ord a => [(a, [([SBVI.CV], SBVI.CV)])] -> [(a, [([SBVI.CV], SBVI.CV)])]
partitionWithOrd v = go sorted
where
sorted = sortWith fst v
go (x : x1 : xs) =
if fst x == fst x1
then go $ (fst x, snd x ++ snd x1) : xs
else x : go (x1 : xs)
go x = x
gouifuncs :: (String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV))) -> PM.Model -> PM.Model
gouifuncs (name, (SBVI.SBVType _, l)) m = case findStringToSymbol name mp of
Just (SomeTypedSymbol tr s) -> withSymbolSupported s $ case tr of
t@(TFunType a r) -> R.withTypeable t $ insertValue s (goutfuncResolve a r l) m
t@(GFunType a r) -> R.withTypeable t $ insertValue s (gougfuncResolve 0 a r l) m
_ -> error "Bad"
Nothing -> error "Bad"
-- helpers
data BVTypeContainer bv k where
BVTypeContainer :: (SBV.BVIsNonZero n, KnownNat n, 1 <= n, k ~ bv n) => Proxy n -> BVTypeContainer bv k
signedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer IntN t)
signedBVTypeView t = case t of
R.App s (n :: R.TypeRep w) ->
case (R.eqTypeRep s (R.typeRep @IntN), R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat)) of
(Just R.HRefl, Just R.HRefl) ->
Just $ unsafeBVIsNonZero @w $ withPrim (Proxy @t) (BVTypeContainer Proxy)
_ -> Nothing
_ -> Nothing
where
unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r
unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of
Refl -> r1
pattern SignedBVType ::
forall t.
(SupportedPrim t) =>
forall (n :: Nat).
(t ~~ IntN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>
Proxy n ->
R.TypeRep t
pattern SignedBVType p <- (signedBVTypeView @t -> Just (BVTypeContainer p))
unsignedBVTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (BVTypeContainer WordN t)
unsignedBVTypeView t = case t of
R.App s (n :: R.TypeRep w) ->
case (R.eqTypeRep s (R.typeRep @WordN), R.eqTypeRep (R.typeRepKind n) (R.typeRep @Nat)) of
(Just R.HRefl, Just R.HRefl) ->
Just $ unsafeBVIsNonZero @w $ withPrim (Proxy @t) (BVTypeContainer Proxy)
_ -> Nothing
_ -> Nothing
where
unsafeBVIsNonZero :: forall w r. ((SBV.BVIsNonZero w) => r) -> r
unsafeBVIsNonZero r1 = case unsafeAxiom :: w :~: 1 of
Refl -> r1
pattern UnsignedBVType ::
forall t.
(SupportedPrim t) =>
forall (n :: Nat).
(t ~~ WordN n, KnownNat n, 1 <= n, SBV.BVIsNonZero n) =>
Proxy n ->
R.TypeRep t
pattern UnsignedBVType p <- (unsignedBVTypeView @t -> Just (BVTypeContainer p))
data TFunTypeContainer :: forall k. k -> Type where
TFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> TFunTypeContainer (a =-> b)
tFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (TFunTypeContainer t)
tFunTypeView t = case t of
R.App (R.App arr (ta2' :: R.TypeRep a2)) (tr2' :: R.TypeRep r2) ->
case R.eqTypeRep arr (R.typeRep @(=->)) of
Just R.HRefl -> Just $ withPrim (Proxy @t) $ TFunTypeContainer ta2' tr2'
Nothing -> Nothing
_ -> Nothing
pattern TFunType ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type).
(t ~~ (a =-> b), SupportedPrim a, SupportedPrim b) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep t
pattern TFunType a b <-
(tFunTypeView -> Just (TFunTypeContainer a b))
where
TFunType a b = R.App (R.App (R.typeRep @(=->)) a) b
pattern TFun3Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type).
(t ~~ (a =-> b =-> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep t
pattern TFun3Type a b c = TFunType a (TFunType b c)
data GFunTypeContainer :: forall k. k -> Type where
GFunTypeContainer :: (SupportedPrim a, SupportedPrim b) => R.TypeRep a -> R.TypeRep b -> GFunTypeContainer (a --> b)
gFunTypeView :: forall t. (SupportedPrim t) => R.TypeRep t -> Maybe (GFunTypeContainer t)
gFunTypeView t = case t of
R.App (R.App arr (ta2' :: R.TypeRep a2)) (tr2' :: R.TypeRep r2) ->
case R.eqTypeRep arr (R.typeRep @(-->)) of
Just R.HRefl -> Just $ withPrim (Proxy @t) $ GFunTypeContainer ta2' tr2'
Nothing -> Nothing
_ -> Nothing
pattern GFunType ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type).
(t ~~ (a --> b), SupportedPrim a, SupportedPrim b) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep t
pattern GFunType a b <-
(gFunTypeView -> Just (GFunTypeContainer a b))
where
GFunType a b = R.App (R.App (R.typeRep @(-->)) a) b
pattern GFun3Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type).
(t ~~ (a --> b --> c), SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep t
pattern GFun3Type a b c = GFunType a (GFunType b c)
pattern BoolType ::
forall t.
() =>
(t ~~ Bool) =>
R.TypeRep t
pattern BoolType <- (R.eqTypeRep (R.typeRep @Bool) -> Just R.HRefl)
pattern IntegerType ::
forall t.
() =>
(t ~~ Integer) =>
R.TypeRep t
pattern IntegerType <- (R.eqTypeRep (R.typeRep @Integer) -> Just R.HRefl)
type ConfigConstraint integerBitWidth s =
( SBV.SBV s ~ TermTy integerBitWidth Integer,
SBV.SymVal s,
SBV.HasKind s,
Typeable s,
Num (SBV.SBV s),
Num s,
SBV.OrdSymbolic (SBV.SBV s),
Ord s,
SBV.SDivisible (SBV.SBV s),
SBV.OrdSymbolic (SBV.SBV s),
SBV.Mergeable (SBV.SBV s)
)
data DictConfig integerBitWidth where
DictConfig ::
forall s integerBitWidth.
(ConfigConstraint integerBitWidth s) =>
SBV.SMTConfig ->
DictConfig integerBitWidth
resolveConfigView ::
forall integerBitWidth.
GrisetteSMTConfig integerBitWidth ->
DictConfig integerBitWidth
resolveConfigView config = case config of
UnboundedReasoning c -> DictConfig c
BoundedReasoning c -> DictConfig c
pattern ResolvedConfig ::
forall integerBitWidth.
() =>
forall s.
ConfigConstraint integerBitWidth s =>
SBV.SMTConfig ->
GrisetteSMTConfig integerBitWidth
pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)
type SimpleTypeConstraint integerBitWidth s s' =
( SBV.SBV s' ~ TermTy integerBitWidth s,
SBV.SymVal s',
SBV.HasKind s',
Typeable s',
SBV.OrdSymbolic (SBV.SBV s'),
SBV.Mergeable (SBV.SBV s')
)
type TypeResolver dictType =
forall integerBitWidth s.
(SupportedPrim s) =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s) ->
Maybe (dictType integerBitWidth s)
-- has to declare this because GHC does not support impredicative polymorphism
data DictSimpleType integerBitWidth s where
DictSimpleType ::
forall integerBitWidth s s'.
(SimpleTypeConstraint integerBitWidth s s') =>
DictSimpleType integerBitWidth s
resolveSimpleTypeView :: TypeResolver DictSimpleType
resolveSimpleTypeView (ResolvedConfig {}, s) = case s of
BoolType -> Just DictSimpleType
IntegerType -> Just DictSimpleType
SignedBVType _ -> Just DictSimpleType
UnsignedBVType _ -> Just DictSimpleType
_ -> Nothing
resolveSimpleTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedSimpleType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
SimpleTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedSimpleType <- (resolveSimpleTypeView -> Just DictSimpleType)
type DeepTypeConstraint integerBitWidth s s' =
( s' ~ TermTy integerBitWidth s,
Typeable s',
SBV.Mergeable s'
)
data DictDeepType integerBitWidth s where
DictDeepType ::
forall integerBitWidth s s'.
(DeepTypeConstraint integerBitWidth s s') =>
DictDeepType integerBitWidth s
resolveDeepTypeView :: TypeResolver DictDeepType
resolveDeepTypeView r = case r of
ResolvedSimpleType -> Just DictDeepType
(config, TFunType (ta :: R.TypeRep a) (tb :: R.TypeRep b)) ->
case (resolveDeepTypeView (config, ta), resolveDeepTypeView (config, tb)) of
(Just DictDeepType, Just DictDeepType) -> Just DictDeepType
_ -> Nothing
(config, GFunType (ta :: R.TypeRep a) (tb :: R.TypeRep b)) ->
case (resolveDeepTypeView (config, ta), resolveDeepTypeView (config, tb)) of
(Just DictDeepType, Just DictDeepType) -> Just DictDeepType
_ -> Nothing
_ -> Nothing
pattern ResolvedDeepType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
DeepTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedDeepType <- (resolveDeepTypeView -> Just DictDeepType)
type NumTypeConstraint integerBitWidth s s' =
( SimpleTypeConstraint integerBitWidth s s',
Num (SBV.SBV s'),
Num s',
Num s
)
data DictNumType integerBitWidth s where
DictNumType ::
forall integerBitWidth s s'.
(NumTypeConstraint integerBitWidth s s') =>
DictNumType integerBitWidth s
resolveNumTypeView :: TypeResolver DictNumType
resolveNumTypeView (ResolvedConfig {}, s) = case s of
IntegerType -> Just DictNumType
SignedBVType _ -> Just DictNumType
UnsignedBVType _ -> Just DictNumType
_ -> Nothing
resolveNumTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedNumType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
NumTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedNumType <- (resolveNumTypeView -> Just DictNumType)
type NumOrdTypeConstraint integerBitWidth s s' =
( NumTypeConstraint integerBitWidth s s',
SBV.OrdSymbolic (SBV.SBV s'),
Ord s',
Ord s
)
data DictNumOrdType integerBitWidth s where
DictNumOrdType ::
forall integerBitWidth s s'.
(NumOrdTypeConstraint integerBitWidth s s') =>
DictNumOrdType integerBitWidth s
resolveNumOrdTypeView :: TypeResolver DictNumOrdType
resolveNumOrdTypeView (ResolvedConfig {}, s) = case s of
IntegerType -> Just DictNumOrdType
SignedBVType _ -> Just DictNumOrdType
UnsignedBVType _ -> Just DictNumOrdType
_ -> Nothing
resolveNumOrdTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedNumOrdType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
NumOrdTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedNumOrdType <- (resolveNumOrdTypeView -> Just DictNumOrdType)
type BitsTypeConstraint integerBitWidth s s' =
( SimpleTypeConstraint integerBitWidth s s',
Bits (SBV.SBV s'),
Bits s',
Bits s
)
data DictBitsType integerBitWidth s where
DictBitsType ::
forall integerBitWidth s s'.
(BitsTypeConstraint integerBitWidth s s') =>
DictBitsType integerBitWidth s
resolveBitsTypeView :: TypeResolver DictBitsType
resolveBitsTypeView (ResolvedConfig {}, s) = case s of
SignedBVType _ -> Just DictBitsType
UnsignedBVType _ -> Just DictBitsType
_ -> Nothing
resolveBitsTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedBitsType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
BitsTypeConstraint integerBitWidth s s' =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedBitsType <- (resolveBitsTypeView -> Just DictBitsType)