grisette-0.4.0.0: src/Grisette/Backend/SBV/Data/SMT/Lowering.hs
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# 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,
lowerSinglePrimCached,
parseModel,
SymBiMap,
)
where
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Reader (MonadTrans (lift), ReaderT)
import Control.Monad.State (StateT)
import Data.Bifunctor (Bifunctor (bimap, first, second))
import Data.Bits
( Bits (complement, xor, (.&.), (.|.)),
)
import Data.Dynamic (Typeable, fromDyn, toDyn)
import Data.Foldable (Foldable (foldl'), asum)
import Data.Kind (Type)
import Data.Maybe (fromMaybe)
import Data.SBV (SIntegral, sRotateLeft, sRotateRight, sShiftLeft, sShiftRight)
import qualified Data.SBV as SBV
import qualified Data.SBV.Internals as SBVI
import qualified Data.SBV.Trans as SBVT
import qualified Data.SBV.Trans.Control as SBVTC
import Data.Type.Equality (type (~~))
import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))
import GHC.Exts (sortWith)
import GHC.Stack (HasCallStack)
import GHC.TypeNats
( KnownNat,
Nat,
natVal,
type (+),
type (-),
type (<=),
)
import {-# SOURCE #-} Grisette.Backend.SBV.Data.SMT.Solving
( ApproximationConfig (Approx, NoApprox),
ExtraConfig (integerApprox),
GrisetteSMTConfig (GrisetteSMTConfig),
TermTy,
)
import Grisette.Backend.SBV.Data.SMT.SymBiMap
( SymBiMap,
addBiMap,
addBiMapIntermediate,
emptySymBiMap,
findStringToSymbol,
lookupTerm,
sizeBiMap,
)
import Grisette.Core.Data.BV (IntN (IntN, unIntN), WordN (WordN))
import Grisette.Core.Data.Class.ModelOps
( ModelOps (emptyModel, insertValue),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
( conTerm,
symTerm,
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
( SomeTerm (SomeTerm),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
( SomeTypedSymbol (SomeTypedSymbol),
SupportedPrim (withPrim),
Term
( AbsNumTerm,
AddNumTerm,
AndBitsTerm,
AndTerm,
BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
BinaryTerm,
ComplementBitsTerm,
ConTerm,
DivBoundedIntegralTerm,
DivIntegralTerm,
EqvTerm,
GeneralFunApplyTerm,
ITETerm,
LENumTerm,
LTNumTerm,
ModBoundedIntegralTerm,
ModIntegralTerm,
NotTerm,
OrBitsTerm,
OrTerm,
QuotBoundedIntegralTerm,
QuotIntegralTerm,
RemBoundedIntegralTerm,
RemIntegralTerm,
RotateLeftTerm,
RotateRightTerm,
ShiftLeftTerm,
ShiftRightTerm,
SignumNumTerm,
SymTerm,
TabularFunApplyTerm,
TernaryTerm,
TimesNumTerm,
ToSignedTerm,
ToUnsignedTerm,
UMinusNumTerm,
UnaryTerm,
XorBitsTerm
),
TypedSymbol (IndexedSymbol),
buildGeneralFun,
someTypedSymbol,
withSymbolSupported,
type (-->),
)
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils
( introSupportedPrimConstraint,
)
import Grisette.IR.SymPrim.Data.Prim.Model as PM (Model)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( pevalEqvTerm,
pevalITETerm,
)
import Grisette.IR.SymPrim.Data.TabularFun
( type (=->) (TabularFun),
)
import Grisette.Utils.Parameterized
( KnownProof (KnownProof),
LeqProof (LeqProof),
unsafeAxiom,
unsafeKnownProof,
unsafeLeqProof,
withKnownProof,
)
import qualified Type.Reflection as R
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"
lowerValue ::
forall integerBitWidth a.
(SupportedPrim a, Typeable a) =>
GrisetteSMTConfig integerBitWidth ->
a ->
TermTy integerBitWidth a
lowerValue config@ResolvedConfig {} v =
case R.typeRep @a of
BoolType -> if v then SBV.sTrue else SBV.sFalse
IntegerType -> fromInteger v
SignedBVType _ -> case v of
IntN x -> fromInteger x
UnsignedBVType _ -> case v of
WordN x -> fromInteger x
TFunType (l :: a1) (r :: a2) ->
case ((config, l), (config, r)) of
(ResolvedSimpleType, ResolvedMergeableType) ->
lowerTFunCon config v
_ -> translateTypeError (R.typeRep @a)
_ -> translateTypeError (R.typeRep @a)
lowerValue _ _ = translateTypeError (R.typeRep @a)
lowerTFunCon ::
forall integerBitWidth a b.
(SupportedPrim a, SupportedPrim b, SBV.EqSymbolic (TermTy integerBitWidth a), SBV.Mergeable (TermTy integerBitWidth b)) =>
GrisetteSMTConfig integerBitWidth ->
(a =-> b) ->
(TermTy integerBitWidth a -> TermTy integerBitWidth b)
lowerTFunCon config@ResolvedConfig {} (TabularFun l d) = go l d
where
go [] d _ = lowerValue config d
go ((x, r) : xs) d v = SBV.ite (lowerValue config x SBV..== v) (lowerValue config r) (go xs d v)
lowerTFunCon _ TabularFun {} = translateTypeError (R.typeRep @a)
buildUTFun11 ::
forall integerBitWidth s1 s2 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
Term a ->
SymBiMap ->
Maybe (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 (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 (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 (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun1111 ::
forall integerBitWidth s1 s2 s3 s4 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4))
buildUTFun1111 config ta tb tc td term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3 -> TermTy integerBitWidth s4)
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun1111 _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun11111 ::
forall integerBitWidth s1 s2 s3 s4 s5 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4, SupportedPrim s5) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5))
buildUTFun11111 config ta tb tc td te term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun11111 _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6))
buildUTFun111111 config ta tb tc td te tf term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun111111 _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun1111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6,
SupportedPrim s7
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
R.TypeRep s7 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7))
buildUTFun1111111 config ta tb tc td te tf tg term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun1111111 _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUTFun11111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 s8 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6,
SupportedPrim s7,
SupportedPrim s8
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
R.TypeRep s7 ->
R.TypeRep s8 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7 =-> s8))
buildUTFun11111111 config ta tb tc td te tf tg th term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg), (config, th)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 =-> s2 =-> s3 =-> s4 =-> s5 =-> s6 =-> s7 =-> s8))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUTFun11111111 _ _ _ _ _ _ _ _ _ _ _ = 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 (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 (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 (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 (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun111 _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun1111 ::
forall integerBitWidth s1 s2 s3 s4 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4))
buildUGFun1111 config ta tb tc td term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth s1 -> TermTy integerBitWidth s2 -> TermTy integerBitWidth s3 -> TermTy integerBitWidth s4)
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun1111 _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun11111 ::
forall integerBitWidth s1 s2 s3 s4 s5 a.
(SupportedPrim a, SupportedPrim s1, SupportedPrim s2, SupportedPrim s3, SupportedPrim s4, SupportedPrim s5) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5))
buildUGFun11111 config ta tb tc td te term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun11111 _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6))
buildUGFun111111 config ta tb tc td te tf term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun111111 _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun1111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6,
SupportedPrim s7
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
R.TypeRep s7 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7))
buildUGFun1111111 config ta tb tc td te tf tg term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun1111111 _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
buildUGFun11111111 ::
forall integerBitWidth s1 s2 s3 s4 s5 s6 s7 s8 a.
( SupportedPrim a,
SupportedPrim s1,
SupportedPrim s2,
SupportedPrim s3,
SupportedPrim s4,
SupportedPrim s5,
SupportedPrim s6,
SupportedPrim s7,
SupportedPrim s8
) =>
GrisetteSMTConfig integerBitWidth ->
R.TypeRep s1 ->
R.TypeRep s2 ->
R.TypeRep s3 ->
R.TypeRep s4 ->
R.TypeRep s5 ->
R.TypeRep s6 ->
R.TypeRep s7 ->
R.TypeRep s8 ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7 --> s8))
buildUGFun11111111 config ta tb tc td te tf tg th term@(SymTerm _ ts) m =
case ((config, ta), (config, tb), (config, tc), (config, td), (config, te), (config, tf), (config, tg), (config, th)) of
(ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType, ResolvedSimpleType) ->
let name = "ufunc_" ++ show (sizeBiMap m)
f =
SBV.uninterpret @(TermTy integerBitWidth (s1 --> s2 --> s3 --> s4 --> s5 --> s6 --> s7 --> s8))
name
in Just (addBiMap (SomeTerm term) (toDyn f) name (someTypedSymbol ts) m, f)
_ -> Nothing
buildUGFun11111111 _ _ _ _ _ _ _ _ _ _ _ = error "Should only be called on SymTerm"
lowerSinglePrimUFun ::
forall integerBitWidth a.
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
Maybe (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimUFun config t@(SymTerm _ _) m =
case R.typeRep @a of
TFun8Type t1 t2 t3 t4 t5 t6 t7 t8 -> buildUTFun11111111 config t1 t2 t3 t4 t5 t6 t7 t8 t m
TFun7Type t1 t2 t3 t4 t5 t6 t7 -> buildUTFun1111111 config t1 t2 t3 t4 t5 t6 t7 t m
TFun6Type t1 t2 t3 t4 t5 t6 -> buildUTFun111111 config t1 t2 t3 t4 t5 t6 t m
TFun5Type t1 t2 t3 t4 t5 -> buildUTFun11111 config t1 t2 t3 t4 t5 t m
TFun4Type t1 t2 t3 t4 -> buildUTFun1111 config t1 t2 t3 t4 t m
TFun3Type t1 t2 t3 -> buildUTFun111 config t1 t2 t3 t m
TFunType t1 t2 -> buildUTFun11 config t1 t2 t m
GFun8Type t1 t2 t3 t4 t5 t6 t7 t8 -> buildUGFun11111111 config t1 t2 t3 t4 t5 t6 t7 t8 t m
GFun7Type t1 t2 t3 t4 t5 t6 t7 -> buildUGFun1111111 config t1 t2 t3 t4 t5 t6 t7 t m
GFun6Type t1 t2 t3 t4 t5 t6 -> buildUGFun111111 config t1 t2 t3 t4 t5 t6 t m
GFun5Type t1 t2 t3 t4 t5 -> buildUGFun11111 config t1 t2 t3 t4 t5 t m
GFun4Type t1 t2 t3 t4 -> buildUGFun1111 config t1 t2 t3 t4 t m
GFun3Type t1 t2 t3 -> buildUGFun111 config t1 t2 t3 t m
GFunType t1 t2 -> buildUGFun11 config t1 t2 t m
_ -> Nothing
lowerSinglePrimUFun _ _ _ = error "Should not call this function"
class (Monad m) => SBVFreshMonad m where
sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a)
instance (MonadIO m) => SBVFreshMonad (SBVT.SymbolicT m) where
sbvFresh = SBVT.free
instance (MonadIO m) => SBVFreshMonad (SBVTC.QueryT m) where
sbvFresh = SBVTC.freshVar
instance (SBVFreshMonad m) => SBVFreshMonad (ReaderT r m) where
sbvFresh = lift . sbvFresh
instance (SBVFreshMonad m) => SBVFreshMonad (StateT s m) where
sbvFresh = lift . sbvFresh
lowerUnaryTerm ::
forall integerBitWidth a a1 x x1 m.
(Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
(a1 -> x1) ->
SymBiMap ->
m (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 m.
(Typeable x1, a1 ~ TermTy integerBitWidth a, b1 ~ TermTy integerBitWidth b, SupportedPrim x, HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth ->
Term x ->
Term a ->
Term b ->
(a1 -> b1 -> x1) ->
SymBiMap ->
m (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 m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
m (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 m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
m (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrim config t = lowerSinglePrimCached config t emptySymBiMap
lowerSinglePrimImpl ::
forall integerBitWidth a m.
(HasCallStack, SBVFreshMonad m) =>
GrisetteSMTConfig integerBitWidth ->
Term a ->
SymBiMap ->
m (SymBiMap, TermTy integerBitWidth a)
lowerSinglePrimImpl config@ResolvedConfig {} (ConTerm _ v) m = return (m, lowerValue config v)
lowerSinglePrimImpl config t@(SymTerm _ ts) m =
fromMaybe errorMsg $ asum [simple, ufunc]
where
errorMsg :: forall x. x
errorMsg = translateTypeError (R.typeRep @a)
simple :: Maybe (m (SymBiMap, TermTy integerBitWidth a))
simple = case (config, R.typeRep @a) of
ResolvedSimpleType -> Just $ do
let name = show ts
(g :: TermTy integerBitWidth a) <- sbvFresh name
return (addBiMap (SomeTerm t) (toDyn g) name (someTypedSymbol ts) m, g)
_ -> Nothing
ufunc :: (Maybe (m (SymBiMap, TermTy integerBitWidth a)))
ufunc = return <$> 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
ResolvedMergeableType -> 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@(ShiftLeftTerm _ arg n) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftLeft m
_ -> translateBinaryError "shiftLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl config t@(ShiftRightTerm _ arg n) m =
case (config, R.typeRep @a) of
ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftRight m
_ -> translateBinaryError "shiftRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
-- SBV's rotateLeft and rotateRight are broken for signed values, so we have to
-- do this
-- https://github.com/LeventErkok/sbv/issues/673
lowerSinglePrimImpl config t@(RotateLeftTerm _ arg n) m =
case (config, R.typeRep @a) of
(_, SignedBVType (Proxy :: Proxy n)) ->
lowerBinaryTerm
config
t
arg
n
( \x y ->
SBV.sFromIntegral $
sRotateLeft
(SBV.sFromIntegral x :: SBV.SWord n)
(SBV.sFromIntegral y :: SBV.SWord n)
)
m
ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateLeft m
_ -> translateBinaryError "rotateLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl config t@(RotateRightTerm _ arg n) m =
case (config, R.typeRep @a) of
(_, SignedBVType (Proxy :: Proxy n)) ->
lowerBinaryTerm
config
t
arg
n
( \x y ->
SBV.sFromIntegral $
sRotateRight
(SBV.sFromIntegral x :: SBV.SWord n)
(SBV.sFromIntegral y :: SBV.SWord n)
)
m
ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateRight m
_ -> translateBinaryError "rotateRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)
lowerSinglePrimImpl config t@(ToSignedTerm _ (bv :: Term x)) m =
case (R.typeRep @a, R.typeRep @x) of
(SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->
case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
Just R.HRefl ->
lowerUnaryTerm config t bv SBV.sFromIntegral m
_ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)
_ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)
lowerSinglePrimImpl config t@(ToUnsignedTerm _ (bv :: Term x)) m =
case (R.typeRep @a, R.typeRep @x) of
(UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->
case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of
Just R.HRefl ->
lowerUnaryTerm config t bv SBV.sFromIntegral m
_ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)
_ -> translateUnaryError "s2u" (R.typeRep @x) (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)) ->
withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
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
(SignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy xn)) ->
withKnownProof (unsafeKnownProof @(na + ix - 1) (natVal (Proxy @na) + natVal (Proxy @ix) - 1)) $
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
_ -> 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)) ->
withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @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)) ->
withKnownProof (unsafeKnownProof @(na - nx) (natVal (Proxy @na) - natVal (Proxy @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@(DivIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
_ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(ModIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
_ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(QuotIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m
_ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(RemIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m
_ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(DivBoundedIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sDiv m
_ -> translateBinaryError "div" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(ModBoundedIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sMod m
_ -> translateBinaryError "mod" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(QuotBoundedIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sQuot m
_ -> translateBinaryError "quot" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl config t@(RemBoundedIntegralTerm _ arg1 arg2) m =
case (config, R.typeRep @a) of
ResolvedSDivisibleType -> lowerBinaryTerm config t arg1 arg2 SBV.sRem m
_ -> translateBinaryError "rem" (R.typeRep @a) (R.typeRep @a) (R.typeRep @a)
lowerSinglePrimImpl _ _ _ = error "Should never happen"
bvIsNonZeroFromGEq1 :: forall w r. (1 <= w) => ((SBV.BVIsNonZero w) => r) -> r
bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of
Refl -> r1
#if MIN_VERSION_sbv(10,3,0)
preprocessUIFuncs ::
[(String, (Bool, SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
preprocessUIFuncs =
traverse
(\case
(a, (_, b, Right c)) -> Just (a, (b, c))
_ -> Nothing)
#elif MIN_VERSION_sbv(10,0,0)
preprocessUIFuncs ::
[(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
preprocessUIFuncs =
traverse
(\case
(a, (b, Right c)) -> Just (a, (b, c))
_ -> Nothing)
#else
preprocessUIFuncs ::
[(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->
Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]
preprocessUIFuncs = Just
#endif
parseModel :: forall integerBitWidth. GrisetteSMTConfig integerBitWidth -> SBVI.SMTModel -> SymBiMap -> PM.Model
parseModel _ (SBVI.SMTModel _ _ assoc orguifuncs) mp =
case preprocessUIFuncs orguifuncs of
Just uifuncs -> foldr gouifuncs (foldr goassoc emptyModel assoc) uifuncs
_ -> error "SBV Failed to parse model"
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 ->
case (unsafeKnownProof @w (fromIntegral bitWidth), unsafeLeqProof @1 @w) of
(KnownProof, LeqProof) ->
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 = IndexedSymbol "arg" idx
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 (symTerm sym) (conTerm v))
(conTerm f)
acc
)
(conTerm def)
funs
in buildGeneralFun sym body
_ ->
let sym = IndexedSymbol "arg" idx
vs = bimap (resolveSingle ta1 . head) (resolveSingle ta2) <$> l
def = resolveSingle ta2 s
body =
foldl'
( \acc (v, a) ->
pevalITETerm
(pevalEqvTerm (symTerm sym) (conTerm v))
(conTerm a)
acc
)
(conTerm def)
vs
in buildGeneralFun 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)
pattern TFun4Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type) (d :: Type).
( t ~~ (a =-> b =-> c =-> d),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep t
pattern TFun4Type a b c d = TFunType a (TFunType b (TFunType c d))
pattern TFun5Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type).
( t ~~ (a =-> b =-> c =-> d =-> e),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep t
pattern TFun5Type a b c d e =
TFunType
a
( TFunType
b
( TFunType
c
(TFunType d e)
)
)
pattern TFun6Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type).
( t ~~ (a =-> b =-> c =-> d =-> e =-> f),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep t
pattern TFun6Type a b c d e f =
TFunType
a
( TFunType
b
( TFunType
c
( TFunType
d
(TFunType e f)
)
)
)
pattern TFun7Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type)
(g :: Type).
( t ~~ (a =-> b =-> c =-> d =-> e =-> f =-> g),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep g ->
R.TypeRep t
pattern TFun7Type a b c d e f g =
TFunType
a
( TFunType
b
( TFunType
c
( TFunType
d
( TFunType
e
(TFunType f g)
)
)
)
)
pattern TFun8Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type)
(g :: Type)
(h :: Type).
( t ~~ (a =-> b =-> c =-> d =-> e =-> f =-> g =-> h),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g,
SupportedPrim h
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep g ->
R.TypeRep h ->
R.TypeRep t
pattern TFun8Type a b c d e f g h =
TFunType
a
( TFunType
b
( TFunType
c
( TFunType
d
( TFunType
e
( TFunType
f
(TFunType g h)
)
)
)
)
)
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 GFun4Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type) (d :: Type).
( t ~~ (a --> b --> c --> d),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep t
pattern GFun4Type a b c d = GFunType a (GFunType b (GFunType c d))
pattern GFun5Type ::
forall t.
(SupportedPrim t) =>
forall (a :: Type) (b :: Type) (c :: Type) (d :: Type) (e :: Type).
( t ~~ (a --> b --> c --> d --> e),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep t
pattern GFun5Type a b c d e =
GFunType
a
( GFunType
b
( GFunType
c
(GFunType d e)
)
)
pattern GFun6Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type).
( t ~~ (a --> b --> c --> d --> e --> f),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep t
pattern GFun6Type a b c d e f =
GFunType
a
( GFunType
b
( GFunType
c
( GFunType
d
(GFunType e f)
)
)
)
pattern GFun7Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type)
(g :: Type).
( t ~~ (a --> b --> c --> d --> e --> f --> g),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep g ->
R.TypeRep t
pattern GFun7Type a b c d e f g =
GFunType
a
( GFunType
b
( GFunType
c
( GFunType
d
( GFunType
e
(GFunType f g)
)
)
)
)
pattern GFun8Type ::
forall t.
(SupportedPrim t) =>
forall
(a :: Type)
(b :: Type)
(c :: Type)
(d :: Type)
(e :: Type)
(f :: Type)
(g :: Type)
(h :: Type).
( t ~~ (a --> b --> c --> d --> e --> f --> g --> h),
SupportedPrim a,
SupportedPrim b,
SupportedPrim c,
SupportedPrim d,
SupportedPrim e,
SupportedPrim f,
SupportedPrim g,
SupportedPrim h
) =>
R.TypeRep a ->
R.TypeRep b ->
R.TypeRep c ->
R.TypeRep d ->
R.TypeRep e ->
R.TypeRep f ->
R.TypeRep g ->
R.TypeRep h ->
R.TypeRep t
pattern GFun8Type a b c d e f g h =
GFunType
a
( GFunType
b
( GFunType
c
( GFunType
d
( GFunType
e
( GFunType
f
(GFunType g h)
)
)
)
)
)
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
GrisetteSMTConfig c extra ->
case integerApprox extra of
NoApprox -> DictConfig c
Approx _ -> DictConfig c
pattern ResolvedConfig ::
forall integerBitWidth.
() =>
forall s.
(ConfigConstraint integerBitWidth s) =>
SBV.SMTConfig ->
GrisetteSMTConfig integerBitWidth
pattern ResolvedConfig c <- (resolveConfigView -> DictConfig c)
type MergeableTypeConstraint integerBitWidth s =
( Typeable (TermTy integerBitWidth s),
SBV.Mergeable (TermTy integerBitWidth s)
)
-- has to declare this because GHC does not support impredicative polymorphism
data DictMergeableType integerBitWidth s where
DictMergeableType ::
forall integerBitWidth s.
(MergeableTypeConstraint integerBitWidth s) =>
DictMergeableType integerBitWidth s
resolveMergeableTypeView :: TypeResolver DictMergeableType
resolveMergeableTypeView (config@ResolvedConfig {}, s) = case s of
BoolType -> Just DictMergeableType
IntegerType -> Just DictMergeableType
SignedBVType _ -> Just DictMergeableType
UnsignedBVType _ -> Just DictMergeableType
TFunType l r ->
case (resolveSimpleTypeView (config, l), resolveMergeableTypeView (config, r)) of
(Just DictSimpleType, Just DictMergeableType) -> Just DictMergeableType
_ -> Nothing
GFunType l r ->
case (resolveSimpleTypeView (config, l), resolveMergeableTypeView (config, r)) of
(Just DictSimpleType, Just DictMergeableType) -> Just DictMergeableType
_ -> Nothing
_ -> Nothing
resolveMergeableTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedMergeableType ::
forall integerBitWidth s.
(SupportedPrim s) =>
(MergeableTypeConstraint integerBitWidth s) =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedMergeableType <- (resolveMergeableTypeView -> Just DictMergeableType)
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 SDivisibleTypeConstraint integerBitWidth s s' =
( SimpleTypeConstraint integerBitWidth s s',
SBV.SDivisible (SBV.SBV s'),
Integral s
)
data DictSDivisibleType integerBitWidth s where
DictSDivisibleType ::
forall integerBitWidth s s'.
(SDivisibleTypeConstraint integerBitWidth s s') =>
DictSDivisibleType integerBitWidth s
resolveSDivisibleTypeView :: TypeResolver DictSDivisibleType
resolveSDivisibleTypeView (ResolvedConfig {}, s) = case s of
IntegerType -> Just DictSDivisibleType
SignedBVType _ -> Just DictSDivisibleType
UnsignedBVType _ -> Just DictSDivisibleType
_ -> Nothing
resolveSDivisibleTypeView _ = error "Should never happen, make compiler happy"
pattern ResolvedSDivisibleType ::
forall integerBitWidth s.
(SupportedPrim s) =>
forall s'.
(SDivisibleTypeConstraint integerBitWidth s s') =>
(GrisetteSMTConfig integerBitWidth, R.TypeRep s)
pattern ResolvedSDivisibleType <- (resolveSDivisibleTypeView -> Just DictSDivisibleType)
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,
SIntegral s',
Integral 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)