{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.Model
-- 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.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
import Data.List
import Data.Proxy
import GHC.Generics
import Grisette.Core.Data.Class.ExtractSymbolics
import Grisette.Core.Data.Class.ModelOps
import Grisette.Core.Data.MemoUtils
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term
import Grisette.IR.SymPrim.Data.Prim.ModelValue
import Grisette.IR.SymPrim.Data.Prim.PartialEval.BV
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bits
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool
import Grisette.IR.SymPrim.Data.Prim.PartialEval.GeneralFun
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Integral
import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num
import Grisette.IR.SymPrim.Data.Prim.PartialEval.TabularFun
import Type.Reflection
import Unsafe.Coerce

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.IR.SymPrim
-- >>> :set -XFlexibleContexts

-- | Symbolic constant set.
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

-- | Model returned by the solver.
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 -- someTypedSymbol sym1 == someTypedSymbol sym
                  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' -- stm
                  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

-- |
-- A type used for building a model by hand.
--
-- >>> buildModel ("x" ::= (1 :: Integer), "y" ::= True) :: Model
-- Model {x -> 1 :: Integer, y -> True :: Bool}
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

{-
instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2
      ) =
      insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3
      ) =
      insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3,
      sym4 ::= val4
      ) =
      insertValue sym4 val4
        . insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3,
      sym4 ::= val4,
      sym5 ::= val5
      ) =
      insertValue sym5 val5
        . insertValue sym4 val4
        . insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e,
      ModelValuePair f
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3,
      sym4 ::= val4,
      sym5 ::= val5,
      sym6 ::= val6
      ) =
      insertValue sym6 val6
        . insertValue sym5 val5
        . insertValue sym4 val4
        . insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e,
      ModelValuePair f,
      ModelValuePair g
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3,
      sym4 ::= val4,
      sym5 ::= val5,
      sym6 ::= val6,
      sym7 ::= val7
      ) =
      insertValue sym7 val7
        . insertValue sym6 val6
        . insertValue sym5 val5
        . insertValue sym4 val4
        . insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e,
      ModelValuePair f,
      ModelValuePair g,
      ModelValuePair h
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel
    ( sym1 ::= val1,
      sym2 ::= val2,
      sym3 ::= val3,
      sym4 ::= val4,
      sym5 ::= val5,
      sym6 ::= val6,
      sym7 ::= val7,
      sym8 ::= val8
      ) =
      insertValue sym8 val8
        . insertValue sym7 val7
        . insertValue sym6 val6
        . insertValue sym5 val5
        . insertValue sym4 val4
        . insertValue sym3 val3
        . insertValue sym2 val2
        . insertValue sym1 val1
        $ emptyModel

-}