{-# LANGUAGE DeriveGeneric #-}
{-# 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.Integer
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
(SymbolSet -> SymbolSet -> Bool)
-> (SymbolSet -> SymbolSet -> Bool) -> Eq SymbolSet
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. 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
$cto :: forall x. Rep SymbolSet x -> SymbolSet
$cfrom :: forall x. SymbolSet -> Rep SymbolSet x
Generic, Int -> SymbolSet -> Int
SymbolSet -> Int
(Int -> SymbolSet -> Int)
-> (SymbolSet -> Int) -> Hashable SymbolSet
forall 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
(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
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
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
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 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
/= :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c== :: 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
$cto :: forall x. Rep Model x -> Model
$cfrom :: forall x. Model -> Rep Model x
Generic, Int -> Model -> Int
Model -> Int
(Int -> Model -> Int) -> (Model -> Int) -> Hashable Model
forall a. (Int -> a -> Int) -> (a -> Int) -> Hashable a
hash :: Model -> Int
$chash :: Model -> Int
hashWithSalt :: Int -> Model -> Int
$chashWithSalt :: Int -> Model -> Int
Hashable)

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 TypedSymbol a
tsym 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 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 a. SupportedPrim a => Term a -> Term a -> Term Bool
pevalEqvTerm (TypedSymbol a -> Term a
forall t. (SupportedPrim t, Typeable t) => TypedSymbol t -> Term t
symTerm 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, 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 (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.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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 ExtractSymbolics SymbolSet where
  extractSymbolics :: SymbolSet -> SymbolSet
extractSymbolics = SymbolSet -> SymbolSet
forall a. a -> a
id

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
  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
  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
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 (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 {}) = 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
partialEvalUnary 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
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
      (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
partialEvalTernary 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 (EqvTerm 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 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)) =
      (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 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)) =
      (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 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)) = (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 a. (Num a, SupportedPrim a) => Term a -> Term a
pevalUMinusNumTerm Term a
arg
    go (SomeTerm (TimesNumTerm 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 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)) = (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 a. (SupportedPrim a, Num a) => Term a -> Term a
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 a. (Num a, SupportedPrim a) => Term a -> Term a
pevalSignumNumTerm Term a
arg
    go (SomeTerm (LTNumTerm 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 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)) =
      (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 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)) =
      (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 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)) =
      (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 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)) =
      (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 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)) = (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 a. (Bits a, SupportedPrim a) => Term a -> Term a
pevalComplementBitsTerm Term a
arg
    go (SomeTerm (ShiftBitsTerm Int
_ Term a
arg Int
n)) =
      (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (Term a -> Int -> Term a
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)) =
      (Term a -> Term a) -> Term a -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (Term a -> Int -> Term a
forall a. (Bits a, SupportedPrim a) => Term a -> Int -> Term a
`pevalRotateBitsTerm` Int
n) Term a
arg
    go (SomeTerm (BVConcatTerm Int
_ Term (bv a)
arg1 Term (bv b)
arg2)) =
      (Term (bv a) -> Term (bv b) -> Term (bv c))
-> Term (bv a) -> Term (bv b) -> 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 a) -> Term (bv b) -> Term (bv c)
forall (s :: Nat -> *) (w :: Nat) (w' :: Nat) (w'' :: Nat).
(SupportedPrim (s w), SupportedPrim (s w'), SupportedPrim (s w''),
 KnownNat w, KnownNat w', KnownNat w'',
 BVConcat (s w) (s w') (s w'')) =>
Term (s w) -> Term (s w') -> Term (s w'')
pevalBVConcatTerm Term (bv a)
arg1 Term (bv b)
arg2
    go (SomeTerm (BVSelectTerm Int
_ TypeRep ix
ix TypeRep w
w Term (bv a)
arg)) =
      (Term (bv a) -> Term (bv w)) -> Term (bv a) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (TypeRep ix -> TypeRep w -> Term (bv a) -> Term (bv w)
forall (bv :: Nat -> *) (a :: Nat) (ix :: Nat) (w :: Nat)
       (proxy :: Nat -> *).
(SupportedPrim (bv a), SupportedPrim (bv w), KnownNat a,
 KnownNat w, KnownNat ix, BVSelect (bv a) ix w (bv w)) =>
proxy ix -> proxy w -> Term (bv a) -> Term (bv w)
pevalBVSelectTerm TypeRep ix
ix TypeRep w
w) Term (bv a)
arg
    go (SomeTerm (BVExtendTerm Int
_ Bool
n TypeRep n
signed Term (bv a)
arg)) =
      (Term (bv a) -> Term (bv b)) -> Term (bv a) -> SomeTerm
forall a b.
(SupportedPrim a, SupportedPrim b) =>
(Term a -> Term b) -> Term a -> SomeTerm
goUnary (Bool -> TypeRep n -> Term (bv a) -> Term (bv b)
forall (proxy :: Nat -> *) (a :: Nat) (n :: Nat) (b :: Nat)
       (bv :: Nat -> *).
(KnownNat a, KnownNat b, KnownNat n, BVExtend (bv a) n (bv b),
 SupportedPrim (bv a), SupportedPrim (bv b)) =>
Bool -> proxy n -> Term (bv a) -> Term (bv b)
pevalBVExtendTerm Bool
n TypeRep n
signed) Term (bv a)
arg
    go (SomeTerm (TabularFunApplyTerm Int
_ Term (a =-> a)
f Term a
arg)) =
      (Term (a =-> a) -> Term a -> Term a)
-> Term (a =-> 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 =-> a) -> Term a -> Term a
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)) =
      (Term (a --> a) -> Term a -> Term a)
-> Term (a --> 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 --> a) -> Term a -> Term a
forall a b.
(SupportedPrim a, SupportedPrim b) =>
Term (a --> b) -> Term a -> Term b
pevalGeneralFunApplyTerm Term (a --> a)
f Term a
arg
    go (SomeTerm (DivIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2)) =
      (Term Integer -> Term Integer -> Term Integer)
-> Term Integer -> Term Integer -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term Integer -> Term Integer -> Term Integer
pevalDivIntegerTerm Term Integer
arg1 Term Integer
arg2
    go (SomeTerm (ModIntegerTerm Int
_ Term Integer
arg1 Term Integer
arg2)) =
      (Term Integer -> Term Integer -> Term Integer)
-> Term Integer -> Term Integer -> SomeTerm
forall a b c.
(SupportedPrim a, SupportedPrim b, SupportedPrim c) =>
(Term a -> Term b -> Term c) -> Term a -> Term b -> SomeTerm
goBinary Term Integer -> Term Integer -> Term Integer
pevalModIntegerTerm Term Integer
arg1 Term Integer
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
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 SymbolSet TypedSymbol where
  buildModel :: ModelValuePair t -> Model
buildModel (TypedSymbol t
sym ::= t
val) = 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
    ( ModelValuePair a,
      ModelValuePair b
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelValuePair a, ModelValuePair b) -> Model
buildModel
    ( TypedSymbol a
sym1 ::= a
val1,
      TypedSymbol b
sym2 ::= b
val2
      ) =
      TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c) -> Model
buildModel
    ( TypedSymbol a
sym1 ::= a
val1,
      TypedSymbol b
sym2 ::= b
val2,
      TypedSymbol c
sym3 ::= c
val3
      ) =
      TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c,
 ModelValuePair d)
-> Model
buildModel
    ( TypedSymbol a
sym1 ::= a
val1,
      TypedSymbol b
sym2 ::= b
val2,
      TypedSymbol c
sym3 ::= c
val3,
      TypedSymbol d
sym4 ::= d
val4
      ) =
      TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c,
 ModelValuePair d, ModelValuePair e)
-> Model
buildModel
    ( TypedSymbol a
sym1 ::= a
val1,
      TypedSymbol b
sym2 ::= b
val2,
      TypedSymbol c
sym3 ::= c
val3,
      TypedSymbol d
sym4 ::= d
val4,
      TypedSymbol e
sym5 ::= e
val5
      ) =
      TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

instance
  ModelRep
    ( ModelValuePair a,
      ModelValuePair b,
      ModelValuePair c,
      ModelValuePair d,
      ModelValuePair e,
      ModelValuePair f
    )
    Model
    SymbolSet
    TypedSymbol
  where
  buildModel :: (ModelValuePair a, ModelValuePair b, ModelValuePair c,
 ModelValuePair d, ModelValuePair e, ModelValuePair f)
-> Model
buildModel
    ( TypedSymbol a
sym1 ::= a
val1,
      TypedSymbol b
sym2 ::= b
val2,
      TypedSymbol c
sym3 ::= c
val3,
      TypedSymbol d
sym4 ::= d
val4,
      TypedSymbol e
sym5 ::= e
val5,
      TypedSymbol f
sym6 ::= f
val6
      ) =
      TypedSymbol f -> f -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol f
sym6 f
val6
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol e -> e -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol e
sym5 e
val5
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol d -> d -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol d
sym4 d
val4
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol c -> c -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol c
sym3 c
val3
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol b -> b -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol b
sym2 b
val2
        (Model -> Model) -> (Model -> Model) -> Model -> Model
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol a -> a -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedSymbol a
sym1 a
val1
        (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

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

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