{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
module Grisette.IR.SymPrim.Data.Prim.Model
( SymbolSet (..),
Model (..),
ModelValuePair (..),
equation,
evaluateTerm,
)
where
import qualified Data.HashMap.Strict as M
import qualified Data.HashSet as S
import Data.Hashable (Hashable)
import Data.List (sort, sortOn)
import Data.Proxy (Proxy (Proxy))
import GHC.Generics (Generic)
import Grisette.Core.Data.Class.ExtractSymbolics
( ExtractSymbolics (extractSymbolics),
)
import Grisette.Core.Data.Class.ModelOps
( ModelOps
( emptyModel,
exceptFor,
exceptFor',
extendTo,
insertValue,
isEmptyModel,
modelContains,
restrictTo,
valueOf
),
ModelRep (buildModel),
SymbolSetOps
( containsSymbol,
differenceSet,
emptySet,
insertSymbol,
intersectionSet,
isEmptySet,
unionSet
),
SymbolSetRep (buildSymbolSet),
)
import Grisette.Core.Data.MemoUtils (htmemo)
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
( BinaryOp (partialEvalBinary),
SomeTypedSymbol (SomeTypedSymbol),
SupportedPrim (defaultValue, defaultValueDynamic),
Term
( AbsNumTerm,
AddNumTerm,
AndBitsTerm,
AndTerm,
BVConcatTerm,
BVExtendTerm,
BVSelectTerm,
BVToSignedTerm,
BVToUnsignedTerm,
BinaryTerm,
ComplementBitsTerm,
ConTerm,
DivBoundedIntegralTerm,
DivIntegralTerm,
EqvTerm,
GeneralFunApplyTerm,
ITETerm,
LENumTerm,
LTNumTerm,
ModBoundedIntegralTerm,
ModIntegralTerm,
NotTerm,
OrBitsTerm,
OrTerm,
QuotBoundedIntegralTerm,
QuotIntegralTerm,
RemBoundedIntegralTerm,
RemIntegralTerm,
RotateBitsTerm,
ShiftBitsTerm,
SignumNumTerm,
SymTerm,
TabularFunApplyTerm,
TernaryTerm,
TimesNumTerm,
UMinusNumTerm,
UnaryTerm,
XorBitsTerm
),
TernaryOp (partialEvalTernary),
TypedSymbol,
UnaryOp (partialEvalUnary),
showUntyped,
someTypedSymbol,
withSymbolSupported,
type (-->) (GeneralFun),
)
import Grisette.IR.SymPrim.Data.Prim.ModelValue
( ModelValue,
toModelValue,
unsafeFromModelValue,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
( pevalBVConcatTerm,
pevalBVExtendTerm,
pevalBVSelectTerm,
pevalBVToSignedTerm,
pevalBVToUnsignedTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
( pevalAndBitsTerm,
pevalComplementBitsTerm,
pevalOrBitsTerm,
pevalRotateBitsTerm,
pevalShiftBitsTerm,
pevalXorBitsTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
( pevalAndTerm,
pevalEqvTerm,
pevalITETerm,
pevalNotTerm,
pevalOrTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
( pevalGeneralFunApplyTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
( pevalDivBoundedIntegralTerm,
pevalDivIntegralTerm,
pevalModBoundedIntegralTerm,
pevalModIntegralTerm,
pevalQuotBoundedIntegralTerm,
pevalQuotIntegralTerm,
pevalRemBoundedIntegralTerm,
pevalRemIntegralTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
( pevalAbsNumTerm,
pevalAddNumTerm,
pevalLeNumTerm,
pevalLtNumTerm,
pevalSignumNumTerm,
pevalTimesNumTerm,
pevalUMinusNumTerm,
)
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
( pevalTabularFunApplyTerm,
)
import Type.Reflection
( TypeRep,
eqTypeRep,
typeRep,
pattern App,
type (:~~:) (HRefl),
)
import Unsafe.Coerce (unsafeCoerce)
newtype SymbolSet = SymbolSet {SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet :: S.HashSet SomeTypedSymbol}
deriving (SymbolSet -> SymbolSet -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SymbolSet -> SymbolSet -> Bool
$c/= :: SymbolSet -> SymbolSet -> Bool
== :: SymbolSet -> SymbolSet -> Bool
$c== :: SymbolSet -> SymbolSet -> Bool
Eq, forall x. Rep SymbolSet x -> SymbolSet
forall x. SymbolSet -> Rep SymbolSet x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep SymbolSet x -> SymbolSet
$cfrom :: forall x. SymbolSet -> Rep SymbolSet x
Generic, Eq SymbolSet
Int -> SymbolSet -> Int
SymbolSet -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: SymbolSet -> Int
$chash :: SymbolSet -> Int
hashWithSalt :: Int -> SymbolSet -> Int
$chashWithSalt :: Int -> SymbolSet -> Int
Hashable, NonEmpty SymbolSet -> SymbolSet
SymbolSet -> SymbolSet -> SymbolSet
forall b. Integral b => b -> SymbolSet -> SymbolSet
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> SymbolSet -> SymbolSet
$cstimes :: forall b. Integral b => b -> SymbolSet -> SymbolSet
sconcat :: NonEmpty SymbolSet -> SymbolSet
$csconcat :: NonEmpty SymbolSet -> SymbolSet
<> :: SymbolSet -> SymbolSet -> SymbolSet
$c<> :: SymbolSet -> SymbolSet -> SymbolSet
Semigroup, Semigroup SymbolSet
SymbolSet
[SymbolSet] -> SymbolSet
SymbolSet -> SymbolSet -> SymbolSet
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [SymbolSet] -> SymbolSet
$cmconcat :: [SymbolSet] -> SymbolSet
mappend :: SymbolSet -> SymbolSet -> SymbolSet
$cmappend :: SymbolSet -> SymbolSet -> SymbolSet
mempty :: SymbolSet
$cmempty :: SymbolSet
Monoid)
instance Show SymbolSet where
showsPrec :: Int -> SymbolSet -> ShowS
showsPrec Int
prec (SymbolSet HashSet SomeTypedSymbol
s) = Bool -> ShowS -> ShowS
showParen (Int
prec forall a. Ord a => a -> a -> Bool
>= Int
10) forall a b. (a -> b) -> a -> b
$ \String
x ->
String
"SymbolSet {"
forall a. [a] -> [a] -> [a]
++ [String] -> String
go0 (forall a. Ord a => [a] -> [a]
sort forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> String
show forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HashSet a -> [a]
S.toList HashSet SomeTypedSymbol
s)
forall a. [a] -> [a] -> [a]
++ String
"}"
forall a. [a] -> [a] -> [a]
++ String
x
where
go0 :: [String] -> String
go0 [] = String
""
go0 [String
x] = String
x
go0 (String
x : [String]
xs) = String
x forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ [String] -> String
go0 [String]
xs
newtype Model = Model {Model -> HashMap SomeTypedSymbol ModelValue
unModel :: M.HashMap SomeTypedSymbol ModelValue} deriving (Model -> Model -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c== :: Model -> Model -> Bool
Eq, forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Model x -> Model
$cfrom :: forall x. Model -> Rep Model x
Generic, Eq Model
Int -> Model -> Int
Model -> Int
forall a. Eq a -> (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Model -> Int
$chash :: Model -> Int
hashWithSalt :: Int -> Model -> Int
$chashWithSalt :: Int -> Model -> Int
Hashable, NonEmpty Model -> Model
Model -> Model -> Model
forall b. Integral b => b -> Model -> Model
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
stimes :: forall b. Integral b => b -> Model -> Model
$cstimes :: forall b. Integral b => b -> Model -> Model
sconcat :: NonEmpty Model -> Model
$csconcat :: NonEmpty Model -> Model
<> :: Model -> Model -> Model
$c<> :: Model -> Model -> Model
Semigroup, Semigroup Model
Model
[Model] -> Model
Model -> Model -> Model
forall a.
Semigroup a -> a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
mconcat :: [Model] -> Model
$cmconcat :: [Model] -> Model
mappend :: Model -> Model -> Model
$cmappend :: Model -> Model -> Model
mempty :: Model
$cmempty :: Model
Monoid)
instance Show Model where
showsPrec :: Int -> Model -> ShowS
showsPrec Int
prec (Model HashMap SomeTypedSymbol ModelValue
m) = Bool -> ShowS -> ShowS
showParen (Int
prec forall a. Ord a => a -> a -> Bool
>= Int
10) forall a b. (a -> b) -> a -> b
$ \String
x ->
String
"Model {"
forall a. [a] -> [a] -> [a]
++ forall {b}. Show b => [(SomeTypedSymbol, b)] -> String
go0 (forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\(SomeTypedSymbol
x, ModelValue
_) -> forall a. Show a => a -> String
show SomeTypedSymbol
x) forall a b. (a -> b) -> a -> b
$ forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SomeTypedSymbol ModelValue
m)
forall a. [a] -> [a] -> [a]
++ String
"}"
forall a. [a] -> [a] -> [a]
++ String
x
where
go0 :: [(SomeTypedSymbol, b)] -> String
go0 [] = String
""
go0 [(SomeTypedSymbol TypeRep t
_ TypedSymbol t
s, b
v)] = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
v
go0 ((SomeTypedSymbol TypeRep t
_ TypedSymbol t
s, b
v) : [(SomeTypedSymbol, b)]
xs) = forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show b
v forall a. [a] -> [a] -> [a]
++ String
", " forall a. [a] -> [a] -> [a]
++ [(SomeTypedSymbol, b)] -> String
go0 [(SomeTypedSymbol, b)]
xs
equation :: TypedSymbol a -> Model -> Maybe (Term Bool)
equation :: forall a. TypedSymbol a -> Model -> Maybe (Term Bool)
equation TypedSymbol a
tsym Model
m = forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol a
tsym forall a b. (a -> b) -> a -> b
$
case forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> model -> Maybe t
valueOf TypedSymbol a
tsym Model
m of
Just a
v -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm TypedSymbol a
tsym) (forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v)
Maybe a
Nothing -> forall a. Maybe a
Nothing
instance SymbolSetOps SymbolSet TypedSymbol where
emptySet :: SymbolSet
emptySet = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall a. HashSet a
S.empty
isEmptySet :: SymbolSet -> Bool
isEmptySet (SymbolSet HashSet SomeTypedSymbol
s) = forall a. HashSet a -> Bool
S.null HashSet SomeTypedSymbol
s
containsSymbol :: forall a. TypedSymbol a -> SymbolSet -> Bool
containsSymbol TypedSymbol a
s =
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
s) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet
insertSymbol :: forall a. TypedSymbol a -> SymbolSet -> SymbolSet
insertSymbol TypedSymbol a
s = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
s) forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet
intersectionSet :: SymbolSet -> SymbolSet -> SymbolSet
intersectionSet (SymbolSet HashSet SomeTypedSymbol
s1) (SymbolSet HashSet SomeTypedSymbol
s2) = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet SomeTypedSymbol
s1 HashSet SomeTypedSymbol
s2
unionSet :: SymbolSet -> SymbolSet -> SymbolSet
unionSet (SymbolSet HashSet SomeTypedSymbol
s1) (SymbolSet HashSet SomeTypedSymbol
s2) = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.union HashSet SomeTypedSymbol
s1 HashSet SomeTypedSymbol
s2
differenceSet :: SymbolSet -> SymbolSet -> SymbolSet
differenceSet (SymbolSet HashSet SomeTypedSymbol
s1) (SymbolSet HashSet SomeTypedSymbol
s2) = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet forall a b. (a -> b) -> a -> b
$ forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet SomeTypedSymbol
s1 HashSet SomeTypedSymbol
s2
instance SymbolSetRep (TypedSymbol t) SymbolSet TypedSymbol where
buildSymbolSet :: TypedSymbol t -> SymbolSet
buildSymbolSet TypedSymbol t
sym = forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol t
sym forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b) -> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c) -> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c,
TypedSymbol d
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d)
-> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3, TypedSymbol d
sym4) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c,
TypedSymbol d,
TypedSymbol e
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d,
TypedSymbol e)
-> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3, TypedSymbol d
sym4, TypedSymbol e
sym5) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c,
TypedSymbol d,
TypedSymbol e,
TypedSymbol f
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d,
TypedSymbol e, TypedSymbol f)
-> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3, TypedSymbol d
sym4, TypedSymbol e
sym5, TypedSymbol f
sym6) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c,
TypedSymbol d,
TypedSymbol e,
TypedSymbol f,
TypedSymbol g
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d,
TypedSymbol e, TypedSymbol f, TypedSymbol g)
-> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3, TypedSymbol d
sym4, TypedSymbol e
sym5, TypedSymbol f
sym6, TypedSymbol g
sym7) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol g
sym7
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance
SymbolSetRep
( TypedSymbol a,
TypedSymbol b,
TypedSymbol c,
TypedSymbol d,
TypedSymbol e,
TypedSymbol f,
TypedSymbol g,
TypedSymbol h
)
SymbolSet
TypedSymbol
where
buildSymbolSet :: (TypedSymbol a, TypedSymbol b, TypedSymbol c, TypedSymbol d,
TypedSymbol e, TypedSymbol f, TypedSymbol g, TypedSymbol h)
-> SymbolSet
buildSymbolSet (TypedSymbol a
sym1, TypedSymbol b
sym2, TypedSymbol c
sym3, TypedSymbol d
sym4, TypedSymbol e
sym5, TypedSymbol f
sym6, TypedSymbol g
sym7, TypedSymbol h
sym8) =
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol h
sym8
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol g
sym7
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
forall a b. (a -> b) -> a -> b
$ forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet
instance ExtractSymbolics SymbolSet where
extractSymbolics :: SymbolSet -> SymbolSet
extractSymbolics = forall a. a -> a
id
instance ModelOps Model SymbolSet TypedSymbol where
emptyModel :: Model
emptyModel = HashMap SomeTypedSymbol ModelValue -> Model
Model forall k v. HashMap k v
M.empty
isEmptyModel :: Model -> Bool
isEmptyModel (Model HashMap SomeTypedSymbol ModelValue
m) = forall k v. HashMap k v -> Bool
M.null HashMap SomeTypedSymbol ModelValue
m
valueOf :: forall t. TypedSymbol t -> Model -> Maybe t
valueOf :: forall t. TypedSymbol t -> Model -> Maybe t
valueOf TypedSymbol t
sym (Model HashMap SomeTypedSymbol ModelValue
m) =
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
sym forall a b. (a -> b) -> a -> b
$
(forall a. Typeable a => ModelValue -> a
unsafeFromModelValue @t)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol t
sym) HashMap SomeTypedSymbol ModelValue
m
modelContains :: forall a. TypedSymbol a -> Model -> Bool
modelContains TypedSymbol a
sym (Model HashMap SomeTypedSymbol ModelValue
m) = forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym) HashMap SomeTypedSymbol ModelValue
m
exceptFor :: SymbolSet -> Model -> Model
exceptFor (SymbolSet HashSet SomeTypedSymbol
s) (Model HashMap SomeTypedSymbol ModelValue
m) = HashMap SomeTypedSymbol ModelValue -> Model
Model forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete) HashMap SomeTypedSymbol ModelValue
m HashSet SomeTypedSymbol
s
exceptFor' :: forall t. TypedSymbol t -> Model -> Model
exceptFor' TypedSymbol t
s (Model HashMap SomeTypedSymbol ModelValue
m) = HashMap SomeTypedSymbol ModelValue -> Model
Model forall a b. (a -> b) -> a -> b
$ forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol t
s) HashMap SomeTypedSymbol ModelValue
m
restrictTo :: SymbolSet -> Model -> Model
restrictTo (SymbolSet HashSet SomeTypedSymbol
s) (Model HashMap SomeTypedSymbol ModelValue
m) =
HashMap SomeTypedSymbol ModelValue -> Model
Model forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
( \HashMap SomeTypedSymbol ModelValue
acc SomeTypedSymbol
sym -> case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTypedSymbol
sym HashMap SomeTypedSymbol ModelValue
m of
Just ModelValue
v -> forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTypedSymbol
sym ModelValue
v HashMap SomeTypedSymbol ModelValue
acc
Maybe ModelValue
Nothing -> HashMap SomeTypedSymbol ModelValue
acc
)
forall k v. HashMap k v
M.empty
HashSet SomeTypedSymbol
s
extendTo :: SymbolSet -> Model -> Model
extendTo (SymbolSet HashSet SomeTypedSymbol
s) (Model HashMap SomeTypedSymbol ModelValue
m) =
HashMap SomeTypedSymbol ModelValue -> Model
Model forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
( \HashMap SomeTypedSymbol ModelValue
acc sym :: SomeTypedSymbol
sym@(SomeTypedSymbol TypeRep t
_ (TypedSymbol t
tsym :: TypedSymbol t)) -> case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTypedSymbol
sym HashMap SomeTypedSymbol ModelValue
acc of
Just ModelValue
_ -> HashMap SomeTypedSymbol ModelValue
acc
Maybe ModelValue
Nothing -> forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
tsym forall a b. (a -> b) -> a -> b
$ forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTypedSymbol
sym (forall t (proxy :: * -> *).
SupportedPrim t =>
proxy t -> ModelValue
defaultValueDynamic (forall {k} (t :: k). Proxy t
Proxy @t)) HashMap SomeTypedSymbol ModelValue
acc
)
HashMap SomeTypedSymbol ModelValue
m
HashSet SomeTypedSymbol
s
insertValue :: forall t. TypedSymbol t -> t -> Model -> Model
insertValue TypedSymbol t
sym (t
v :: t) (Model HashMap SomeTypedSymbol ModelValue
m) =
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
sym forall a b. (a -> b) -> a -> b
$
HashMap SomeTypedSymbol ModelValue -> Model
Model forall a b. (a -> b) -> a -> b
$
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol t
sym) (forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue t
v) HashMap SomeTypedSymbol ModelValue
m
evaluateSomeTerm :: Bool -> Model -> SomeTerm -> SomeTerm
evaluateSomeTerm :: Bool -> Model -> SomeTerm -> SomeTerm
evaluateSomeTerm Bool
fillDefault m :: Model
m@(Model HashMap SomeTypedSymbol ModelValue
ma) = SomeTerm -> SomeTerm
gomemo
where
gomemo :: SomeTerm -> SomeTerm
gomemo = forall k a. (Eq k, Hashable k) => (k -> a) -> k -> a
htmemo SomeTerm -> SomeTerm
go
gotyped :: (SupportedPrim a) => Term a -> Term a
gotyped :: forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a = case SomeTerm -> SomeTerm
gomemo (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
a) of
SomeTerm Term a
v -> forall a b. a -> b
unsafeCoerce Term a
v
go :: SomeTerm -> SomeTerm
go c :: SomeTerm
c@(SomeTerm (ConTerm Int
_ a
cv :: Term v)) =
case (forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
case forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep a
gf (forall {k} (a :: k). Typeable a => TypeRep a
typeRep @(-->)) of
Just a :~~: (-->)
HRefl -> case a
cv of
GeneralFun TypedSymbol b
sym Term b
tm ->
if forall model symbolSet (typedSymbol :: * -> *) a.
ModelOps model symbolSet typedSymbol =>
typedSymbol a -> model -> Bool
modelContains TypedSymbol b
sym Model
m
then case Bool -> Model -> SomeTerm -> SomeTerm
evaluateSomeTerm Bool
fillDefault (forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> model -> model
exceptFor' TypedSymbol b
sym Model
m) (forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term b
tm) of
SomeTerm Term a
tm' -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym Term a
tm'
else forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm forall a b. (a -> b) -> a -> b
$ forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym (forall a. SupportedPrim a => Term a -> Term a
gotyped Term b
tm)
Maybe (a :~~: (-->))
Nothing -> SomeTerm
c
TypeRep a
_ -> SomeTerm
c
go c :: SomeTerm
c@(SomeTerm ((SymTerm Int
_ TypedSymbol a
sym) :: Term a)) =
case forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym) HashMap SomeTypedSymbol ModelValue
ma of
Maybe ModelValue
Nothing -> if Bool
fillDefault then forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (forall t. SupportedPrim t => t
defaultValue @a) else SomeTerm
c
Just ModelValue
dy -> forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm (forall a. Typeable a => ModelValue -> a
unsafeFromModelValue @a ModelValue
dy)
go (SomeTerm (UnaryTerm Int
_ tag
tag (Term arg
arg :: Term a))) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
partialEvalUnary tag
tag) Term arg
arg
go (SomeTerm (BinaryTerm Int
_ tag
tag (Term arg1
arg1 :: Term a1) (Term arg2
arg2 :: Term a2))) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary (forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
partialEvalBinary tag
tag) Term arg1
arg1 Term arg2
arg2
go (SomeTerm (TernaryTerm Int
_ tag
tag (Term arg1
arg1 :: Term a1) (Term arg2
arg2 :: Term a2) (Term arg3
arg3 :: Term a3))) = do
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c,
SupportedPrim d) =>
(Term a -> Term b -> Term c -> Term d)
-> Term a -> Term b -> Term c -> SomeTerm
goTernary (forall tag arg1 arg2 arg3 t.
(TernaryOp tag arg1 arg2 arg3 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term t
partialEvalTernary tag
tag) Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
go (SomeTerm (NotTerm Int
_ Term Bool
arg)) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term Bool -> Term Bool
pevalNotTerm Term Bool
arg
go (SomeTerm (OrTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term Bool -> Term Bool -> Term Bool
pevalOrTerm Term Bool
arg1 Term Bool
arg2
go (SomeTerm (AndTerm Int
_ Term Bool
arg1 Term Bool
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term Bool -> Term Bool -> Term Bool
pevalAndTerm Term Bool
arg1 Term Bool
arg2
go (SomeTerm (EqvTerm Int
_ Term t1
arg1 Term t1
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm Term t1
arg1 Term t1
arg2
go (SomeTerm (ITETerm Int
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c,
SupportedPrim d) =>
(Term a -> Term b -> Term c -> Term d)
-> Term a -> Term b -> Term c -> SomeTerm
goTernary forall a.
SupportedPrim a =>
Term Bool -> Term a -> Term a -> Term a
pevalITETerm Term Bool
cond Term a
arg1 Term a
arg2
go (SomeTerm (AddNumTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAddNumTerm Term a
arg1 Term a
arg2
go (SomeTerm (UMinusNumTerm Int
_ Term a
arg)) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
arg
go (SomeTerm (TimesNumTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. (Num a, SupportedPrim a) => Term a -> Term a -> Term a
pevalTimesNumTerm Term a
arg1 Term a
arg2
go (SomeTerm (AbsNumTerm Int
_ Term a
arg)) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall a. (SupportedPrim a, Num a) => Term a -> Term a
pevalAbsNumTerm Term a
arg
go (SomeTerm (SignumNumTerm Int
_ Term a
arg)) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term a
arg
go (SomeTerm (LTNumTerm Int
_ Term t1
arg1 Term t1
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLtNumTerm Term t1
arg1 Term t1
arg2
go (SomeTerm (LENumTerm Int
_ Term t1
arg1 Term t1
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(Num a, Ord a, SupportedPrim a) =>
Term a -> Term a -> Term Bool
pevalLeNumTerm Term t1
arg1 Term t1
arg2
go (SomeTerm (AndBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalAndBitsTerm Term a
arg1 Term a
arg2
go (SomeTerm (OrBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalOrBitsTerm Term a
arg1 Term a
arg2
go (SomeTerm (XorBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a. (Bits a, SupportedPrim a) => Term a -> Term a -> Term a
pevalXorBitsTerm Term a
arg1 Term a
arg2
go (SomeTerm (ComplementBitsTerm Int
_ Term a
arg)) = forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
arg
go (SomeTerm (ShiftBitsTerm Int
_ Term a
arg Int
n)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
`pevalShiftBitsTerm` Int
n) Term a
arg
go (SomeTerm (RotateBitsTerm Int
_ Term a
arg Int
n)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
`pevalRotateBitsTerm` Int
n) Term a
arg
go (SomeTerm (BVToSignedTerm Int
_ Term (ubv n)
arg)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (ubv n1),
forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (sbv n1),
Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
BVSignConversion (ubv n) (sbv n)) =>
Term (ubv n) -> Term (sbv n)
pevalBVToSignedTerm Term (ubv n)
arg
go (SomeTerm (BVToUnsignedTerm Int
_ Term (sbv n)
arg)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary forall (ubv :: Nat -> *) (sbv :: Nat -> *) (n :: Nat).
(forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (ubv n1),
forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (sbv n1),
Typeable ubv, Typeable sbv, KnownNat n, 1 <= n,
BVSignConversion (ubv n) (sbv n)) =>
Term (sbv n) -> Term (ubv n)
pevalBVToUnsignedTerm Term (sbv n)
arg
go (SomeTerm (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall (bv :: Nat -> *) (a :: Nat) (b :: Nat).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv, KnownNat a, KnownNat b, KnownNat (a + b), 1 <= a,
1 <= b, 1 <= (a + b), SizedBV bv) =>
Term (bv a) -> Term (bv b) -> Term (bv (a + b))
pevalBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2
go (SomeTerm (BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (forall (bv :: Nat -> *) (n :: Nat) (ix :: Nat) (w :: Nat)
(p :: Nat -> *) (q :: Nat -> *).
(forall (n1 :: Nat).
(KnownNat n1, 1 <= n1) =>
SupportedPrim (bv n1),
Typeable bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
(ix + w) <= n, SizedBV bv) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w) Term (bv n)
arg
go (SomeTerm (BVExtendTerm Int
_ Bool
n TypeRep r
signed Term (bv l)
arg)) =
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (forall (proxy :: Nat -> *) (l :: Nat) (r :: Nat) (bv :: Nat -> *).
(forall (n :: Nat). (KnownNat n, 1 <= n) => SupportedPrim (bv n),
Typeable bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r,
SizedBV bv) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed) Term (bv l)
arg
go (SomeTerm (TabularFunApplyTerm Int
_ Term (a =-> a)
f Term a
arg)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a =-> b) -> Term a -> Term b
pevalTabularFunApplyTerm Term (a =-> a)
f Term a
arg
go (SomeTerm (GeneralFunApplyTerm Int
_ Term (a --> a)
f Term a
arg)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> a)
f Term a
arg
go (SomeTerm (DivIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalDivIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (ModIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (QuotIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (RemIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalRemIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (DivBoundedIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalDivBoundedIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (ModBoundedIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Integral a) =>
Term a -> Term a -> Term a
pevalModBoundedIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (QuotBoundedIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalQuotBoundedIntegralTerm Term a
arg1 Term a
arg2
go (SomeTerm (RemBoundedIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary forall a.
(SupportedPrim a, Bounded a, Integral a) =>
Term a -> Term a -> Term a
pevalRemBoundedIntegralTerm Term a
arg1 Term a
arg2
goUnary :: (SupportedPrim a, SupportedPrim b) => (Term a -> Term b) -> Term a -> SomeTerm
goUnary :: forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term a -> Term b
f Term a
a = forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term a -> Term b
f (forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a)
goBinary ::
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) ->
Term a ->
Term b ->
SomeTerm
goBinary :: forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term a -> Term b -> Term c
f Term a
a Term b
b = forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term c
f (forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a) (forall a. SupportedPrim a => Term a -> Term a
gotyped Term b
b)
goTernary ::
(SupportedPrim a, SupportedPrim b, SupportedPrim c, SupportedPrim d) =>
(Term a -> Term b -> Term c -> Term d) ->
Term a ->
Term b ->
Term c ->
SomeTerm
goTernary :: forall a b c d.
(SupportedPrim a, SupportedPrim b, SupportedPrim c,
SupportedPrim d) =>
(Term a -> Term b -> Term c -> Term d)
-> Term a -> Term b -> Term c -> SomeTerm
goTernary Term a -> Term b -> Term c -> Term d
f Term a
a Term b
b Term c
c = forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term c -> Term d
f (forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a) (forall a. SupportedPrim a => Term a -> Term a
gotyped Term b
b) (forall a. SupportedPrim a => Term a -> Term a
gotyped Term c
c)
evaluateTerm :: forall a. (SupportedPrim a) => Bool -> Model -> Term a -> Term a
evaluateTerm :: forall a. SupportedPrim a => Bool -> Model -> Term a -> Term a
evaluateTerm Bool
fillDefault Model
m Term a
t = case Bool -> Model -> SomeTerm -> SomeTerm
evaluateSomeTerm Bool
fillDefault Model
m forall a b. (a -> b) -> a -> b
$ forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
t of
SomeTerm (Term a
t1 :: Term b) -> forall a b. a -> b
unsafeCoerce @(Term b) @(Term a) Term a
t1
data ModelValuePair t = (TypedSymbol t) ::= t deriving (Int -> ModelValuePair t -> ShowS
forall t. Show t => Int -> ModelValuePair t -> ShowS
forall t. Show t => [ModelValuePair t] -> ShowS
forall t. Show t => ModelValuePair t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ModelValuePair t] -> ShowS
$cshowList :: forall t. Show t => [ModelValuePair t] -> ShowS
show :: ModelValuePair t -> String
$cshow :: forall t. Show t => ModelValuePair t -> String
showsPrec :: Int -> ModelValuePair t -> ShowS
$cshowsPrec :: forall t. Show t => Int -> ModelValuePair t -> ShowS
Show)
instance ModelRep (ModelValuePair t) Model where
buildModel :: ModelValuePair t -> Model
buildModel (TypedSymbol t
sym ::= t
val) = forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
sym t
val forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel
instance (ModelRep a Model, ModelRep b Model) => ModelRep (a, b) Model where
buildModel :: (a, b) -> Model
buildModel (a
a, b
b) = forall rep model. ModelRep rep model => rep -> model
buildModel a
a forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model
) =>
ModelRep (a, b, c) Model
where
buildModel :: (a, b, c) -> Model
buildModel (a
a, b
b, c
c) = forall rep model. ModelRep rep model => rep -> model
buildModel a
a forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model,
ModelRep d Model
) =>
ModelRep (a, b, c, d) Model
where
buildModel :: (a, b, c, d) -> Model
buildModel (a
a, b
b, c
c, d
d) =
forall rep model. ModelRep rep model => rep -> model
buildModel a
a forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel d
d
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model,
ModelRep d Model,
ModelRep e Model
) =>
ModelRep (a, b, c, d, e) Model
where
buildModel :: (a, b, c, d, e) -> Model
buildModel (a
a, b
b, c
c, d
d, e
e) =
forall rep model. ModelRep rep model => rep -> model
buildModel a
a forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel d
d forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel e
e
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model,
ModelRep d Model,
ModelRep e Model,
ModelRep f Model
) =>
ModelRep (a, b, c, d, e, f) Model
where
buildModel :: (a, b, c, d, e, f) -> Model
buildModel (a
a, b
b, c
c, d
d, e
e, f
f) =
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel d
d
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel e
e
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel f
f
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model,
ModelRep d Model,
ModelRep e Model,
ModelRep f Model,
ModelRep g Model
) =>
ModelRep (a, b, c, d, e, f, g) Model
where
buildModel :: (a, b, c, d, e, f, g) -> Model
buildModel (a
a, b
b, c
c, d
d, e
e, f
f, g
g) =
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel d
d
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel e
e
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel f
f
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel g
g
instance
( ModelRep a Model,
ModelRep b Model,
ModelRep c Model,
ModelRep d Model,
ModelRep e Model,
ModelRep f Model,
ModelRep g Model,
ModelRep h Model
) =>
ModelRep (a, b, c, d, e, f, g, h) Model
where
buildModel :: (a, b, c, d, e, f, g, h) -> Model
buildModel (a
a, b
b, c
c, d
d, e
e, f
f, g
g, h
h) =
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel b
b
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel c
c
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel d
d
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel e
e
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel f
f
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel g
g
forall a. Semigroup a => a -> a -> a
<> forall rep model. ModelRep rep model => rep -> model
buildModel h
h