{-# 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.Internal.SymPrim.Prim.Model
-- Copyright   :   (c) Sirui Lu 2021-2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.SymPrim.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.Internal.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.Internal.Core.Data.MemoUtils (htmemo)
import Grisette.Internal.SymPrim.GeneralFun (type (-->) (GeneralFun))
import Grisette.Internal.SymPrim.Prim.ModelValue
  ( ModelValue,
    toModelValue,
    unsafeFromModelValue,
  )
import Grisette.Internal.SymPrim.Prim.SomeTerm
  ( SomeTerm (SomeTerm),
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( BinaryOp (pevalBinary),
    PEvalApplyTerm (pevalApplyTerm),
    PEvalBVSignConversionTerm (pevalBVToSignedTerm, pevalBVToUnsignedTerm),
    PEvalBVTerm (pevalBVConcatTerm, pevalBVExtendTerm, pevalBVSelectTerm),
    PEvalBitwiseTerm
      ( pevalAndBitsTerm,
        pevalComplementBitsTerm,
        pevalOrBitsTerm,
        pevalXorBitsTerm
      ),
    PEvalDivModIntegralTerm
      ( pevalDivIntegralTerm,
        pevalModIntegralTerm,
        pevalQuotIntegralTerm,
        pevalRemIntegralTerm
      ),
    PEvalNumTerm
      ( pevalAbsNumTerm,
        pevalAddNumTerm,
        pevalMulNumTerm,
        pevalNegNumTerm,
        pevalSignumNumTerm
      ),
    PEvalOrdTerm (pevalLeOrdTerm, pevalLtOrdTerm),
    PEvalRotateTerm
      ( pevalRotateLeftTerm,
        pevalRotateRightTerm
      ),
    PEvalShiftTerm (pevalShiftLeftTerm, pevalShiftRightTerm),
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim (defaultValue, defaultValueDynamic, pevalITETerm),
    Term
      ( AbsNumTerm,
        AddNumTerm,
        AndBitsTerm,
        AndTerm,
        ApplyTerm,
        BVConcatTerm,
        BVExtendTerm,
        BVSelectTerm,
        BinaryTerm,
        ComplementBitsTerm,
        ConTerm,
        DivIntegralTerm,
        EqTerm,
        ITETerm,
        LeOrdTerm,
        LtOrdTerm,
        ModIntegralTerm,
        MulNumTerm,
        NegNumTerm,
        NotTerm,
        OrBitsTerm,
        OrTerm,
        QuotIntegralTerm,
        RemIntegralTerm,
        RotateLeftTerm,
        RotateRightTerm,
        ShiftLeftTerm,
        ShiftRightTerm,
        SignumNumTerm,
        SymTerm,
        TernaryTerm,
        ToSignedTerm,
        ToUnsignedTerm,
        UnaryTerm,
        XorBitsTerm
      ),
    TernaryOp (pevalTernary),
    TypedSymbol (TypedSymbol, unTypedSymbol),
    UnaryOp (pevalUnary),
    conTerm,
    pevalAndTerm,
    pevalEqTerm,
    pevalNotTerm,
    pevalOrTerm,
    showUntyped,
    someTypedSymbol,
    symTerm,
    withSymbolSupported,
  )
import Grisette.Internal.Utils.Parameterized (unsafeAxiom)
import Type.Reflection
  ( TypeRep,
    eqTypeRep,
    typeRep,
    pattern App,
    type (:~:) (Refl),
    type (:~~:) (HRefl),
  )
import Unsafe.Coerce (unsafeCoerce)

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

-- | Symbolic constant set.
newtype SymbolSet = SymbolSet {SymbolSet -> HashSet SomeTypedSymbol
unSymbolSet :: S.HashSet SomeTypedSymbol}
  deriving (SymbolSet -> SymbolSet -> Bool
(SymbolSet -> SymbolSet -> Bool)
-> (SymbolSet -> SymbolSet -> Bool) -> Eq SymbolSet
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SymbolSet -> SymbolSet -> Bool
== :: SymbolSet -> SymbolSet -> Bool
$c/= :: SymbolSet -> SymbolSet -> Bool
/= :: SymbolSet -> SymbolSet -> Bool
Eq, (forall x. SymbolSet -> Rep SymbolSet x)
-> (forall x. Rep SymbolSet x -> SymbolSet) -> Generic SymbolSet
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
$cfrom :: forall x. SymbolSet -> Rep SymbolSet x
from :: forall x. SymbolSet -> Rep SymbolSet x
$cto :: forall x. Rep SymbolSet x -> SymbolSet
to :: forall x. Rep SymbolSet x -> SymbolSet
Generic, Eq SymbolSet
Eq SymbolSet =>
(Int -> SymbolSet -> Int)
-> (SymbolSet -> Int) -> Hashable SymbolSet
Int -> SymbolSet -> Int
SymbolSet -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> SymbolSet -> Int
hashWithSalt :: Int -> SymbolSet -> Int
$chash :: SymbolSet -> Int
hash :: SymbolSet -> Int
Hashable, NonEmpty SymbolSet -> SymbolSet
SymbolSet -> SymbolSet -> SymbolSet
(SymbolSet -> SymbolSet -> SymbolSet)
-> (NonEmpty SymbolSet -> SymbolSet)
-> (forall b. Integral b => b -> SymbolSet -> SymbolSet)
-> Semigroup 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
$c<> :: SymbolSet -> SymbolSet -> SymbolSet
<> :: SymbolSet -> SymbolSet -> SymbolSet
$csconcat :: NonEmpty SymbolSet -> SymbolSet
sconcat :: NonEmpty SymbolSet -> SymbolSet
$cstimes :: forall b. Integral b => b -> SymbolSet -> SymbolSet
stimes :: forall b. Integral b => b -> SymbolSet -> SymbolSet
Semigroup, Semigroup SymbolSet
SymbolSet
Semigroup SymbolSet =>
SymbolSet
-> (SymbolSet -> SymbolSet -> SymbolSet)
-> ([SymbolSet] -> SymbolSet)
-> Monoid SymbolSet
[SymbolSet] -> SymbolSet
SymbolSet -> SymbolSet -> SymbolSet
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: SymbolSet
mempty :: SymbolSet
$cmappend :: SymbolSet -> SymbolSet -> SymbolSet
mappend :: SymbolSet -> SymbolSet -> SymbolSet
$cmconcat :: [SymbolSet] -> SymbolSet
mconcat :: [SymbolSet] -> SymbolSet
Monoid)

instance Show SymbolSet where
  showsPrec :: Int -> SymbolSet -> ShowS
showsPrec Int
prec (SymbolSet HashSet SomeTypedSymbol
s) = Bool -> ShowS -> ShowS
showParen (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ \String
x ->
    String
"SymbolSet {"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [String] -> String
go0 ([String] -> [String]
forall a. Ord a => [a] -> [a]
sort ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol -> String
forall a. Show a => a -> String
show (SomeTypedSymbol -> String) -> [SomeTypedSymbol] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet SomeTypedSymbol -> [SomeTypedSymbol]
forall a. HashSet a -> [a]
S.toList HashSet SomeTypedSymbol
s)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
      String -> ShowS
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 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
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
(Model -> Model -> Bool) -> (Model -> Model -> Bool) -> Eq Model
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
/= :: Model -> Model -> Bool
Eq, (forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
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
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic, Eq Model
Eq Model =>
(Int -> Model -> Int) -> (Model -> Int) -> Hashable Model
Int -> Model -> Int
Model -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
$chashWithSalt :: Int -> Model -> Int
hashWithSalt :: Int -> Model -> Int
$chash :: Model -> Int
hash :: Model -> Int
Hashable, NonEmpty Model -> Model
Model -> Model -> Model
(Model -> Model -> Model)
-> (NonEmpty Model -> Model)
-> (forall b. Integral b => b -> Model -> Model)
-> Semigroup 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
$c<> :: Model -> Model -> Model
<> :: Model -> Model -> Model
$csconcat :: NonEmpty Model -> Model
sconcat :: NonEmpty Model -> Model
$cstimes :: forall b. Integral b => b -> Model -> Model
stimes :: forall b. Integral b => b -> Model -> Model
Semigroup, Semigroup Model
Model
Semigroup Model =>
Model
-> (Model -> Model -> Model) -> ([Model] -> Model) -> Monoid Model
[Model] -> Model
Model -> Model -> Model
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: Model
mempty :: Model
$cmappend :: Model -> Model -> Model
mappend :: Model -> Model -> Model
$cmconcat :: [Model] -> Model
mconcat :: [Model] -> Model
Monoid)

instance Show Model where
  showsPrec :: Int -> Model -> ShowS
showsPrec Int
prec (Model HashMap SomeTypedSymbol ModelValue
m) = Bool -> ShowS -> ShowS
showParen (Int
prec Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
10) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ \String
x ->
    String
"Model {"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ [(SomeTypedSymbol, ModelValue)] -> String
forall {b}. Show b => [(SomeTypedSymbol, b)] -> String
go0 (((SomeTypedSymbol, ModelValue) -> String)
-> [(SomeTypedSymbol, ModelValue)]
-> [(SomeTypedSymbol, ModelValue)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\(SomeTypedSymbol
x, ModelValue
_) -> SomeTypedSymbol -> String
forall a. Show a => a -> String
show SomeTypedSymbol
x) ([(SomeTypedSymbol, ModelValue)]
 -> [(SomeTypedSymbol, ModelValue)])
-> [(SomeTypedSymbol, ModelValue)]
-> [(SomeTypedSymbol, ModelValue)]
forall a b. (a -> b) -> a -> b
$ HashMap SomeTypedSymbol ModelValue
-> [(SomeTypedSymbol, ModelValue)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SomeTypedSymbol ModelValue
m)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
    where
      go0 :: [(SomeTypedSymbol, b)] -> String
go0 [] = String
""
      go0 [(SomeTypedSymbol TypeRep t
_ TypedSymbol t
s, b
v)] = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
v
      go0 ((SomeTypedSymbol TypeRep t
_ TypedSymbol t
s, b
v) : [(SomeTypedSymbol, b)]
xs) = TypedSymbol t -> String
forall t. TypedSymbol t -> String
showUntyped TypedSymbol t
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
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 tsym :: TypedSymbol a
tsym@(TypedSymbol {}) Model
m = TypedSymbol a
-> (SupportedPrim a => Maybe (Term Bool)) -> Maybe (Term Bool)
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol a
tsym ((SupportedPrim a => Maybe (Term Bool)) -> Maybe (Term Bool))
-> (SupportedPrim a => Maybe (Term Bool)) -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
  case TypedSymbol a -> Model -> Maybe a
forall t. TypedSymbol t -> Model -> Maybe t
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> model -> Maybe t
valueOf TypedSymbol a
tsym Model
m of
    Just a
v -> Term Bool -> Maybe (Term Bool)
forall a. a -> Maybe a
Just (Term Bool -> Maybe (Term Bool)) -> Term Bool -> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$ Term a -> Term a -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm (Symbol -> Term a
forall t. (SupportedPrim t, Typeable t) => Symbol -> Term t
symTerm (Symbol -> Term a) -> Symbol -> Term a
forall a b. (a -> b) -> a -> b
$ TypedSymbol a -> Symbol
forall t. TypedSymbol t -> Symbol
unTypedSymbol TypedSymbol a
tsym) (a -> Term a
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm a
v)
    Maybe a
Nothing -> Maybe (Term Bool)
forall a. Maybe a
Nothing

instance SymbolSetOps SymbolSet TypedSymbol where
  emptySet :: SymbolSet
emptySet = HashSet SomeTypedSymbol -> SymbolSet
SymbolSet HashSet SomeTypedSymbol
forall a. HashSet a
S.empty
  isEmptySet :: SymbolSet -> Bool
isEmptySet (SymbolSet HashSet SomeTypedSymbol
s) = HashSet SomeTypedSymbol -> Bool
forall a. HashSet a -> Bool
S.null HashSet SomeTypedSymbol
s
  containsSymbol :: forall a. TypedSymbol a -> SymbolSet -> Bool
containsSymbol TypedSymbol a
s =
    SomeTypedSymbol -> HashSet SomeTypedSymbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
s) (HashSet SomeTypedSymbol -> Bool)
-> (SymbolSet -> HashSet SomeTypedSymbol) -> SymbolSet -> Bool
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 (HashSet SomeTypedSymbol -> SymbolSet)
-> (SymbolSet -> HashSet SomeTypedSymbol) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
s) (HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol)
-> (SymbolSet -> HashSet SomeTypedSymbol)
-> SymbolSet
-> HashSet SomeTypedSymbol
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 (HashSet SomeTypedSymbol -> SymbolSet)
-> HashSet SomeTypedSymbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Eq 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 (HashSet SomeTypedSymbol -> SymbolSet)
-> HashSet SomeTypedSymbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
forall a. Eq 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 (HashSet SomeTypedSymbol -> SymbolSet)
-> HashSet SomeTypedSymbol -> SymbolSet
forall a b. (a -> b) -> a -> b
$ HashSet SomeTypedSymbol
-> HashSet SomeTypedSymbol -> HashSet SomeTypedSymbol
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 = TypedSymbol t -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol t
sym SymbolSet
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) =
    TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol d -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol e -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol f -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol g -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol g
sym7
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol f -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
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) =
    TypedSymbol h -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol h
sym8
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol g -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol g
sym7
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol f -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol f
sym6
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol e
sym5
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol d
sym4
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol c
sym3
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol b
sym2
      (SymbolSet -> SymbolSet)
-> (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> SymbolSet -> SymbolSet
forall a. TypedSymbol a -> SymbolSet -> SymbolSet
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol a
sym1
      (SymbolSet -> SymbolSet) -> SymbolSet -> SymbolSet
forall a b. (a -> b) -> a -> b
$ SymbolSet
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance ModelOps Model SymbolSet TypedSymbol where
  emptyModel :: Model
emptyModel = HashMap SomeTypedSymbol ModelValue -> Model
Model HashMap SomeTypedSymbol ModelValue
forall k v. HashMap k v
M.empty
  isEmptyModel :: Model -> Bool
isEmptyModel (Model HashMap SomeTypedSymbol ModelValue
m) = HashMap SomeTypedSymbol ModelValue -> Bool
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) =
    TypedSymbol t -> (SupportedPrim t => Maybe t) -> Maybe t
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
sym ((SupportedPrim t => Maybe t) -> Maybe t)
-> (SupportedPrim t => Maybe t) -> Maybe t
forall a b. (a -> b) -> a -> b
$
      (forall a. Typeable a => ModelValue -> a
unsafeFromModelValue @t)
        (ModelValue -> t) -> Maybe ModelValue -> Maybe t
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (TypedSymbol t -> SomeTypedSymbol
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) = SomeTypedSymbol -> HashMap SomeTypedSymbol ModelValue -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (TypedSymbol a -> SomeTypedSymbol
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 (HashMap SomeTypedSymbol ModelValue -> Model)
-> HashMap SomeTypedSymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$ (HashMap SomeTypedSymbol ModelValue
 -> SomeTypedSymbol -> HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
-> HashSet SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' ((SomeTypedSymbol
 -> HashMap SomeTypedSymbol ModelValue
 -> HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
-> SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
forall a b c. (a -> b -> c) -> b -> a -> c
flip SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
-> HashMap SomeTypedSymbol ModelValue
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 (HashMap SomeTypedSymbol ModelValue -> Model)
-> HashMap SomeTypedSymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
-> HashMap SomeTypedSymbol ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (TypedSymbol t -> SomeTypedSymbol
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 (HashMap SomeTypedSymbol ModelValue -> Model)
-> HashMap SomeTypedSymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
      (HashMap SomeTypedSymbol ModelValue
 -> SomeTypedSymbol -> HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
-> HashSet SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
        ( \HashMap SomeTypedSymbol ModelValue
acc SomeTypedSymbol
sym -> case SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue -> Maybe ModelValue
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 -> SomeTypedSymbol
-> ModelValue
-> HashMap SomeTypedSymbol ModelValue
-> HashMap SomeTypedSymbol ModelValue
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
        )
        HashMap SomeTypedSymbol ModelValue
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 (HashMap SomeTypedSymbol ModelValue -> Model)
-> HashMap SomeTypedSymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
      (HashMap SomeTypedSymbol ModelValue
 -> SomeTypedSymbol -> HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
-> HashSet SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue
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 SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue -> Maybe ModelValue
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 -> TypedSymbol t
-> (SupportedPrim t => HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
tsym ((SupportedPrim t => HashMap SomeTypedSymbol ModelValue)
 -> HashMap SomeTypedSymbol ModelValue)
-> (SupportedPrim t => HashMap SomeTypedSymbol ModelValue)
-> HashMap SomeTypedSymbol ModelValue
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol
-> ModelValue
-> HashMap SomeTypedSymbol ModelValue
-> HashMap SomeTypedSymbol ModelValue
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTypedSymbol
sym (Proxy t -> ModelValue
forall t (proxy :: * -> *).
SupportedPrim t =>
proxy t -> ModelValue
forall (proxy :: * -> *). proxy t -> ModelValue
defaultValueDynamic (forall t. Proxy t
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) =
    TypedSymbol t -> (SupportedPrim t => Model) -> Model
forall t a. TypedSymbol t -> (SupportedPrim t => a) -> a
withSymbolSupported TypedSymbol t
sym ((SupportedPrim t => Model) -> Model)
-> (SupportedPrim t => Model) -> Model
forall a b. (a -> b) -> a -> b
$
      HashMap SomeTypedSymbol ModelValue -> Model
Model (HashMap SomeTypedSymbol ModelValue -> Model)
-> HashMap SomeTypedSymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
        SomeTypedSymbol
-> ModelValue
-> HashMap SomeTypedSymbol ModelValue
-> HashMap SomeTypedSymbol ModelValue
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (TypedSymbol t -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol t
sym) (t -> ModelValue
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 = (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
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 (Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term a
a) of
      SomeTerm Term a
v -> Term a -> Term a
forall a b. a -> b
unsafeCoerce Term a
v
    go :: SomeTerm -> SomeTerm
go c :: SomeTerm
c@(SomeTerm (ConTerm Int
_ a
cv :: Term v)) =
      case (TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep :: TypeRep v) of
        App (App TypeRep a
gf TypeRep b
_) TypeRep b
_ ->
          case TypeRep a -> TypeRep (-->) -> Maybe (a :~~: (-->))
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
forall (a :: * -> * -> *). Typeable a => TypeRep a
typeRep @(-->)) of
            Just a :~~: (-->)
HRefl -> case a
cv of
              GeneralFun TypedSymbol b
sym (Term b
tm :: Term r) ->
                if TypedSymbol b -> Model -> Bool
forall a. TypedSymbol a -> Model -> Bool
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 (TypedSymbol b -> Model -> Model
forall t. TypedSymbol t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> model -> model
exceptFor' TypedSymbol b
sym Model
m) (Term b -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm Term b
tm) of
                    SomeTerm (Term a
tm' :: Term r1) ->
                      case forall {k} (a :: k) (b :: k). a :~: b
forall a b. a :~: b
unsafeAxiom @r @r1 of
                        b :~: a
Refl -> Term (b --> a) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (b --> a) -> SomeTerm) -> Term (b --> a) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ (b --> a) -> Term (b --> a)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm ((b --> a) -> Term (b --> a)) -> (b --> a) -> Term (b --> a)
forall a b. (a -> b) -> a -> b
$ TypedSymbol b -> Term a -> b --> a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym Term a
tm' -- stm
                  else Term (b --> b) -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term (b --> b) -> SomeTerm) -> Term (b --> b) -> SomeTerm
forall a b. (a -> b) -> a -> b
$ (b --> b) -> Term (b --> b)
forall t.
(SupportedPrim t, Typeable t, Hashable t, Eq t, Show t) =>
t -> Term t
conTerm ((b --> b) -> Term (b --> b)) -> (b --> b) -> Term (b --> b)
forall a b. (a -> b) -> a -> b
$ TypedSymbol b -> Term b -> b --> b
forall a b.
(SupportedPrim a, SupportedPrim b) =>
TypedSymbol a -> Term b -> a --> b
GeneralFun TypedSymbol b
sym (Term b -> Term b
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 SomeTypedSymbol
-> HashMap SomeTypedSymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (TypedSymbol a -> SomeTypedSymbol
forall t. TypedSymbol t -> SomeTypedSymbol
someTypedSymbol TypedSymbol a
sym) HashMap SomeTypedSymbol ModelValue
ma of
        Maybe ModelValue
Nothing -> if Bool
fillDefault then Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ a -> Term a
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 -> Term a -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term a -> SomeTerm) -> Term a -> SomeTerm
forall a b. (a -> b) -> a -> b
$ a -> Term a
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))) = (Term arg -> Term a) -> Term arg -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (tag -> Term arg -> Term a
forall tag arg t.
(UnaryOp tag arg t, Typeable tag, Typeable t) =>
tag -> Term arg -> Term t
pevalUnary tag
tag) Term arg
arg
    go (SomeTerm (BinaryTerm Int
_ tag
tag (Term arg1
arg1 :: Term a1) (Term arg2
arg2 :: Term a2))) =
      (Term arg1 -> Term arg2 -> Term a)
-> Term arg1 -> Term arg2 -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary (tag -> Term arg1 -> Term arg2 -> Term a
forall tag arg1 arg2 t.
(BinaryOp tag arg1 arg2 t, Typeable tag, Typeable t) =>
tag -> Term arg1 -> Term arg2 -> Term t
pevalBinary 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
      (Term arg1 -> Term arg2 -> Term arg3 -> Term a)
-> Term arg1 -> Term arg2 -> Term arg3 -> SomeTerm
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 (tag -> Term arg1 -> Term arg2 -> Term arg3 -> Term a
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
pevalTernary tag
tag) Term arg1
arg1 Term arg2
arg2 Term arg3
arg3
    go (SomeTerm (NotTerm Int
_ Term Bool
arg)) = (Term Bool -> Term Bool) -> Term Bool -> SomeTerm
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)) =
      (Term Bool -> Term Bool -> Term Bool)
-> Term Bool -> Term Bool -> SomeTerm
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)) =
      (Term Bool -> Term Bool -> Term Bool)
-> Term Bool -> Term Bool -> SomeTerm
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 (EqTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (Term t1 -> Term t1 -> Term Bool) -> Term t1 -> Term t1 -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term t1 -> Term t1 -> Term Bool
forall t. SupportedPrim t => Term t -> Term t -> Term Bool
pevalEqTerm Term t1
arg1 Term t1
arg2
    go (SomeTerm (ITETerm Int
_ Term Bool
cond Term a
arg1 Term a
arg2)) =
      (Term Bool -> Term a -> Term a -> Term a)
-> Term Bool -> Term a -> Term a -> SomeTerm
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 Bool -> Term a -> Term a -> Term a
forall t.
SupportedPrim t =>
Term Bool -> Term t -> Term t -> Term t
pevalITETerm Term Bool
cond Term a
arg1 Term a
arg2
    go (SomeTerm (AddNumTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalAddNumTerm Term a
arg1 Term a
arg2
    go (SomeTerm (NegNumTerm Int
_ Term a
arg)) = (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalNegNumTerm Term a
arg
    go (SomeTerm (MulNumTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t -> Term t
pevalMulNumTerm Term a
arg1 Term a
arg2
    go (SomeTerm (AbsNumTerm Int
_ Term a
arg)) = (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalAbsNumTerm Term a
arg
    go (SomeTerm (SignumNumTerm Int
_ Term a
arg)) = (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term a -> Term a
forall t. PEvalNumTerm t => Term t -> Term t
pevalSignumNumTerm Term a
arg
    go (SomeTerm (LtOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (Term t1 -> Term t1 -> Term Bool) -> Term t1 -> Term t1 -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLtOrdTerm Term t1
arg1 Term t1
arg2
    go (SomeTerm (LeOrdTerm Int
_ Term t1
arg1 Term t1
arg2)) =
      (Term t1 -> Term t1 -> Term Bool) -> Term t1 -> Term t1 -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term t1 -> Term t1 -> Term Bool
forall t. PEvalOrdTerm t => Term t -> Term t -> Term Bool
pevalLeOrdTerm Term t1
arg1 Term t1
arg2
    go (SomeTerm (AndBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalAndBitsTerm Term a
arg1 Term a
arg2
    go (SomeTerm (OrBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalOrBitsTerm Term a
arg1 Term a
arg2
    go (SomeTerm (XorBitsTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t -> Term t
pevalXorBitsTerm Term a
arg1 Term a
arg2
    go (SomeTerm (ComplementBitsTerm Int
_ Term a
arg)) = (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term a -> Term a
forall t. PEvalBitwiseTerm t => Term t -> Term t
pevalComplementBitsTerm Term a
arg
    go (SomeTerm (ShiftLeftTerm Int
_ Term a
arg Term a
n)) = (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftLeftTerm Term a
arg Term a
n
    go (SomeTerm (RotateLeftTerm Int
_ Term a
arg Term a
n)) = (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateLeftTerm Term a
arg Term a
n
    go (SomeTerm (ShiftRightTerm Int
_ Term a
arg Term a
n)) = (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalShiftTerm t => Term t -> Term t -> Term t
pevalShiftRightTerm Term a
arg Term a
n
    go (SomeTerm (RotateRightTerm Int
_ Term a
arg Term a
n)) = (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalRotateTerm t => Term t -> Term t -> Term t
pevalRotateRightTerm Term a
arg Term a
n
    go (SomeTerm (ToSignedTerm Int
_ Term (u n)
arg)) =
      (Term (u n) -> Term (s n)) -> Term (u n) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term (u n) -> Term (s n)
forall (n :: Natural).
(KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
forall (u :: Natural -> *) (s :: Natural -> *) (n :: Natural).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (u n) -> Term (s n)
pevalBVToSignedTerm Term (u n)
arg
    go (SomeTerm (ToUnsignedTerm Int
_ Term (s n)
arg)) =
      (Term (s n) -> Term (u n)) -> Term (s n) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary Term (s n) -> Term (u n)
forall (n :: Natural).
(KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
forall (u :: Natural -> *) (s :: Natural -> *) (n :: Natural).
(PEvalBVSignConversionTerm u s, KnownNat n, 1 <= n) =>
Term (s n) -> Term (u n)
pevalBVToUnsignedTerm Term (s n)
arg
    go (SomeTerm (BVConcatTerm Int
_ Term (bv l)
arg1 Term (bv r)
arg2)) =
      (Term (bv l) -> Term (bv r) -> Term (bv (l + r)))
-> Term (bv l) -> Term (bv r) -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (l :: Natural) (r :: Natural).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r) =>
Term (bv l) -> Term (bv r) -> Term (bv (l + r))
pevalBVConcatTerm Term (bv l)
arg1 Term (bv r)
arg2
    go (SomeTerm (BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv n)
arg)) =
      (Term (bv n) -> Term (bv w)) -> Term (bv n) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (TypeRep ix -> TypeRep w -> Term (bv n) -> Term (bv w)
forall (n :: Natural) (ix :: Natural) (w :: Natural)
       (p :: Natural -> *) (q :: Natural -> *).
(KnownNat n, KnownNat ix, KnownNat w, 1 <= n, 1 <= w,
 (ix + w) <= n) =>
p ix -> q w -> Term (bv n) -> Term (bv w)
forall (bv :: Natural -> *) (n :: Natural) (ix :: Natural)
       (w :: Natural) (p :: Natural -> *) (q :: Natural -> *).
(PEvalBVTerm bv, KnownNat n, KnownNat ix, KnownNat w, 1 <= n,
 1 <= w, (ix + w) <= n) =>
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)) =
      (Term (bv l) -> Term (bv r)) -> Term (bv l) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (Bool -> TypeRep r -> Term (bv l) -> Term (bv r)
forall (l :: Natural) (r :: Natural) (proxy :: Natural -> *).
(KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
forall (bv :: Natural -> *) (l :: Natural) (r :: Natural)
       (proxy :: Natural -> *).
(PEvalBVTerm bv, KnownNat l, KnownNat r, 1 <= l, 1 <= r, l <= r) =>
Bool -> proxy r -> Term (bv l) -> Term (bv r)
pevalBVExtendTerm Bool
n TypeRep r
signed) Term (bv l)
arg
    go (SomeTerm (ApplyTerm Int
_ Term f
f Term a
arg)) =
      (Term f -> Term a -> Term a) -> Term f -> Term a -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term f -> Term a -> Term a
forall f a b. PEvalApplyTerm f a b => Term f -> Term a -> Term b
pevalApplyTerm Term f
f Term a
arg
    go (SomeTerm (DivIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalDivIntegralTerm Term a
arg1 Term a
arg2
    go (SomeTerm (ModIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalModIntegralTerm Term a
arg1 Term a
arg2
    go (SomeTerm (QuotIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalQuotIntegralTerm Term a
arg1 Term a
arg2
    go (SomeTerm (RemIntegralTerm Int
_ Term a
arg1 Term a
arg2)) =
      (Term a -> Term a -> Term a) -> Term a -> Term a -> SomeTerm
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 a -> Term a
forall t. PEvalDivModIntegralTerm t => Term t -> Term t -> Term t
pevalRemIntegralTerm 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 = Term b -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term b -> SomeTerm) -> Term b -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term b
f (Term a -> Term a
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 = Term c -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term c -> SomeTerm) -> Term c -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term c
f (Term a -> Term a
forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a) (Term b -> Term b
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 = Term d -> SomeTerm
forall a. SupportedPrim a => Term a -> SomeTerm
SomeTerm (Term d -> SomeTerm) -> Term d -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> Term b -> Term c -> Term d
f (Term a -> Term a
forall a. SupportedPrim a => Term a -> Term a
gotyped Term a
a) (Term b -> Term b
forall a. SupportedPrim a => Term a -> Term a
gotyped Term b
b) (Term c -> Term c
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 (SomeTerm -> SomeTerm) -> SomeTerm -> SomeTerm
forall a b. (a -> b) -> a -> b
$ Term a -> SomeTerm
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
[ModelValuePair t] -> ShowS
ModelValuePair t -> String
(Int -> ModelValuePair t -> ShowS)
-> (ModelValuePair t -> String)
-> ([ModelValuePair t] -> ShowS)
-> Show (ModelValuePair t)
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
$cshowsPrec :: forall t. Show t => Int -> ModelValuePair t -> ShowS
showsPrec :: Int -> ModelValuePair t -> ShowS
$cshow :: forall t. Show t => ModelValuePair t -> String
show :: ModelValuePair t -> String
$cshowList :: forall t. Show t => [ModelValuePair t] -> ShowS
showList :: [ModelValuePair t] -> ShowS
Show)

instance ModelRep (ModelValuePair t) Model where
  buildModel :: ModelValuePair t -> Model
buildModel (TypedSymbol t
sym ::= t
val) = TypedSymbol t -> t -> Model -> Model
forall t. TypedSymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol t
sym t
val Model
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) = a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
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) = a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
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) =
    a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel c
c Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> d -> Model
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) =
    a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel c
c Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> d -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel d
d Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> e -> Model
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) =
    a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel c
c
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> d -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel d
d
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> e -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel e
e
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> f -> Model
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) =
    a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel c
c
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> d -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel d
d
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> e -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel e
e
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> f -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel f
f
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> g -> Model
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) =
    a -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel a
a
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> b -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel b
b
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> c -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel c
c
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> d -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel d
d
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> e -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel e
e
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> f -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel f
f
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> g -> Model
forall rep model. ModelRep rep model => rep -> model
buildModel g
g
      Model -> Model -> Model
forall a. Semigroup a => a -> a -> a
<> h -> Model
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

-}