{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# 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 (..),
    ConstantSymbolSet,
    AnySymbolSet,
    Model (..),
    ModelValuePair (..),
    equation,
    evalTerm,
  )
where

import Control.DeepSeq (NFData)
import qualified Data.Binary as Binary
import Data.Bytes.Serial (Serial (deserialize, serialize))
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 qualified Data.Serialize as Cereal
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.SymPrim.GeneralFun (generalSubstSomeTerm)
import Grisette.Internal.SymPrim.Prim.Internal.Term
  ( SomeTypedAnySymbol,
    SomeTypedConstantSymbol,
    SupportedPrim,
    SymbolKind (AnyKind, ConstantKind),
    Term,
    TypedAnySymbol,
  )
import Grisette.Internal.SymPrim.Prim.Term
  ( IsSymbolKind,
    ModelValue,
    SomeTypedSymbol (SomeTypedSymbol),
    SupportedPrim (defaultValue),
    TypedSymbol,
    conTerm,
    defaultValueDynamic,
    pevalEqTerm,
    showUntyped,
    someTypedSymbol,
    symTerm,
    toModelValue,
    unsafeFromModelValue,
    withSymbolSupported,
  )
import Language.Haskell.TH.Syntax (Lift)

-- $setup
-- >>> import Grisette.Core
-- >>> import Grisette.SymPrim

-- | Set of symbols.
--
-- Check 'Grisette.Core.SymbolSetOps' for operations, and
-- 'Grisette.Core.SymbolSetRep' for manual constructions.
newtype SymbolSet knd = SymbolSet
  { forall (knd :: SymbolKind).
SymbolSet knd -> HashSet (SomeTypedSymbol knd)
unSymbolSet :: S.HashSet (SomeTypedSymbol knd)
  }
  deriving (SymbolSet knd -> SymbolSet knd -> Bool
(SymbolSet knd -> SymbolSet knd -> Bool)
-> (SymbolSet knd -> SymbolSet knd -> Bool) -> Eq (SymbolSet knd)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (knd :: SymbolKind). SymbolSet knd -> SymbolSet knd -> Bool
$c== :: forall (knd :: SymbolKind). SymbolSet knd -> SymbolSet knd -> Bool
== :: SymbolSet knd -> SymbolSet knd -> Bool
$c/= :: forall (knd :: SymbolKind). SymbolSet knd -> SymbolSet knd -> Bool
/= :: SymbolSet knd -> SymbolSet knd -> Bool
Eq, (forall x. SymbolSet knd -> Rep (SymbolSet knd) x)
-> (forall x. Rep (SymbolSet knd) x -> SymbolSet knd)
-> Generic (SymbolSet knd)
forall x. Rep (SymbolSet knd) x -> SymbolSet knd
forall x. SymbolSet knd -> Rep (SymbolSet knd) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (knd :: SymbolKind) x.
Rep (SymbolSet knd) x -> SymbolSet knd
forall (knd :: SymbolKind) x.
SymbolSet knd -> Rep (SymbolSet knd) x
$cfrom :: forall (knd :: SymbolKind) x.
SymbolSet knd -> Rep (SymbolSet knd) x
from :: forall x. SymbolSet knd -> Rep (SymbolSet knd) x
$cto :: forall (knd :: SymbolKind) x.
Rep (SymbolSet knd) x -> SymbolSet knd
to :: forall x. Rep (SymbolSet knd) x -> SymbolSet knd
Generic)
  deriving newtype (Eq (SymbolSet knd)
Eq (SymbolSet knd) =>
(Int -> SymbolSet knd -> Int)
-> (SymbolSet knd -> Int) -> Hashable (SymbolSet knd)
Int -> SymbolSet knd -> Int
SymbolSet knd -> Int
forall a. Eq a => (Int -> a -> Int) -> (a -> Int) -> Hashable a
forall (knd :: SymbolKind). Eq (SymbolSet knd)
forall (knd :: SymbolKind). Int -> SymbolSet knd -> Int
forall (knd :: SymbolKind). SymbolSet knd -> Int
$chashWithSalt :: forall (knd :: SymbolKind). Int -> SymbolSet knd -> Int
hashWithSalt :: Int -> SymbolSet knd -> Int
$chash :: forall (knd :: SymbolKind). SymbolSet knd -> Int
hash :: SymbolSet knd -> Int
Hashable)
  deriving anyclass ((forall (m :: * -> *). MonadPut m => SymbolSet knd -> m ())
-> (forall (m :: * -> *). MonadGet m => m (SymbolSet knd))
-> Serial (SymbolSet knd)
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (knd :: SymbolKind) (m :: * -> *).
(IsSymbolKind knd, MonadGet m) =>
m (SymbolSet knd)
forall (knd :: SymbolKind) (m :: * -> *).
(IsSymbolKind knd, MonadPut m) =>
SymbolSet knd -> m ()
forall (m :: * -> *). MonadGet m => m (SymbolSet knd)
forall (m :: * -> *). MonadPut m => SymbolSet knd -> m ()
$cserialize :: forall (knd :: SymbolKind) (m :: * -> *).
(IsSymbolKind knd, MonadPut m) =>
SymbolSet knd -> m ()
serialize :: forall (m :: * -> *). MonadPut m => SymbolSet knd -> m ()
$cdeserialize :: forall (knd :: SymbolKind) (m :: * -> *).
(IsSymbolKind knd, MonadGet m) =>
m (SymbolSet knd)
deserialize :: forall (m :: * -> *). MonadGet m => m (SymbolSet knd)
Serial)

instance (IsSymbolKind knd) => Cereal.Serialize (SymbolSet knd) where
  put :: Putter (SymbolSet knd)
put = Putter (SymbolSet knd)
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymbolSet knd -> m ()
serialize
  get :: Get (SymbolSet knd)
get = Get (SymbolSet knd)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (SymbolSet knd)
deserialize

instance (IsSymbolKind knd) => Binary.Binary (SymbolSet knd) where
  put :: SymbolSet knd -> Put
put = SymbolSet knd -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => SymbolSet knd -> m ()
serialize
  get :: Get (SymbolSet knd)
get = Get (SymbolSet knd)
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m (SymbolSet knd)
deserialize

-- | Set of constant symbols. Excluding unintepreted functions.
type ConstantSymbolSet = SymbolSet 'ConstantKind

-- | Set of any symbols.
type AnySymbolSet = SymbolSet 'AnyKind

instance Semigroup (SymbolSet knd) where
  SymbolSet HashSet (SomeTypedSymbol knd)
s1 <> :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd
<> SymbolSet HashSet (SomeTypedSymbol knd)
s2 = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ HashSet (SomeTypedSymbol knd)
-> HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet (SomeTypedSymbol knd)
s1 HashSet (SomeTypedSymbol knd)
s2

instance Monoid (SymbolSet knd) where
  mempty :: SymbolSet knd
mempty = SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance Show (SymbolSet knd) where
  showsPrec :: Int -> SymbolSet knd -> ShowS
showsPrec Int
prec (SymbolSet HashSet (SomeTypedSymbol knd)
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 knd -> String
forall a. Show a => a -> String
show (SomeTypedSymbol knd -> String)
-> [SomeTypedSymbol knd] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> HashSet (SomeTypedSymbol knd) -> [SomeTypedSymbol knd]
forall a. HashSet a -> [a]
S.toList HashSet (SomeTypedSymbol knd)
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.
--
-- Check 'Grisette.Core.ModelOps' for operations, and 'Grisette.Core.ModelRep'
-- for manual constructions.
newtype Model = Model
  { Model -> HashMap SomeTypedAnySymbol ModelValue
unModel :: M.HashMap SomeTypedAnySymbol ModelValue
  }
  deriving stock (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, (forall (m :: * -> *). Quote m => Model -> m Exp)
-> (forall (m :: * -> *). Quote m => Model -> Code m Model)
-> Lift Model
forall t.
(forall (m :: * -> *). Quote m => t -> m Exp)
-> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
forall (m :: * -> *). Quote m => Model -> m Exp
forall (m :: * -> *). Quote m => Model -> Code m Model
$clift :: forall (m :: * -> *). Quote m => Model -> m Exp
lift :: forall (m :: * -> *). Quote m => Model -> m Exp
$cliftTyped :: forall (m :: * -> *). Quote m => Model -> Code m Model
liftTyped :: forall (m :: * -> *). Quote m => Model -> Code m Model
Lift)
  deriving newtype (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, Model -> ()
(Model -> ()) -> NFData Model
forall a. (a -> ()) -> NFData a
$crnf :: Model -> ()
rnf :: Model -> ()
NFData)
  deriving anyclass ((forall (m :: * -> *). MonadPut m => Model -> m ())
-> (forall (m :: * -> *). MonadGet m => m Model) -> Serial Model
forall a.
(forall (m :: * -> *). MonadPut m => a -> m ())
-> (forall (m :: * -> *). MonadGet m => m a) -> Serial a
forall (m :: * -> *). MonadGet m => m Model
forall (m :: * -> *). MonadPut m => Model -> m ()
$cserialize :: forall (m :: * -> *). MonadPut m => Model -> m ()
serialize :: forall (m :: * -> *). MonadPut m => Model -> m ()
$cdeserialize :: forall (m :: * -> *). MonadGet m => m Model
deserialize :: forall (m :: * -> *). MonadGet m => m Model
Serial)

instance Cereal.Serialize Model where
  put :: Putter Model
put = Putter Model
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Model -> m ()
serialize
  get :: Get Model
get = Get Model
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m Model
deserialize

instance Binary.Binary Model where
  put :: Model -> Put
put = Model -> Put
forall a (m :: * -> *). (Serial a, MonadPut m) => a -> m ()
forall (m :: * -> *). MonadPut m => Model -> m ()
serialize
  get :: Get Model
get = Get Model
forall a (m :: * -> *). (Serial a, MonadGet m) => m a
forall (m :: * -> *). MonadGet m => m Model
deserialize

instance Semigroup Model where
  Model HashMap SomeTypedAnySymbol ModelValue
m1 <> :: Model -> Model -> Model
<> Model HashMap SomeTypedAnySymbol ModelValue
m2 = HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$ HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v. Eq k => HashMap k v -> HashMap k v -> HashMap k v
M.union HashMap SomeTypedAnySymbol ModelValue
m1 HashMap SomeTypedAnySymbol ModelValue
m2

instance Monoid Model where
  mempty :: Model
mempty = Model
forall model symbolSet (typedSymbol :: * -> *).
ModelOps model symbolSet typedSymbol =>
model
emptyModel

instance Show Model where
  showsPrec :: Int -> Model -> ShowS
showsPrec Int
prec (Model HashMap SomeTypedAnySymbol 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]
++ [(SomeTypedAnySymbol, ModelValue)] -> String
forall {b} {knd :: SymbolKind}.
Show b =>
[(SomeTypedSymbol knd, b)] -> String
go0 (((SomeTypedAnySymbol, ModelValue) -> String)
-> [(SomeTypedAnySymbol, ModelValue)]
-> [(SomeTypedAnySymbol, ModelValue)]
forall b a. Ord b => (a -> b) -> [a] -> [a]
sortOn (\(SomeTypedAnySymbol
x, ModelValue
_) -> SomeTypedAnySymbol -> String
forall a. Show a => a -> String
show SomeTypedAnySymbol
x) ([(SomeTypedAnySymbol, ModelValue)]
 -> [(SomeTypedAnySymbol, ModelValue)])
-> [(SomeTypedAnySymbol, ModelValue)]
-> [(SomeTypedAnySymbol, ModelValue)]
forall a b. (a -> b) -> a -> b
$ HashMap SomeTypedAnySymbol ModelValue
-> [(SomeTypedAnySymbol, ModelValue)]
forall k v. HashMap k v -> [(k, v)]
M.toList HashMap SomeTypedAnySymbol ModelValue
m)
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"
      String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
x
    where
      go0 :: [(SomeTypedSymbol knd, b)] -> String
go0 [] = String
""
      go0 [(SomeTypedSymbol TypedSymbol knd t
s, b
v)] = TypedSymbol knd t -> String
forall (knd :: SymbolKind) t. TypedSymbol knd t -> String
showUntyped TypedSymbol knd 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 TypedSymbol knd t
s, b
v) : [(SomeTypedSymbol knd, b)]
xs) = TypedSymbol knd t -> String
forall (knd :: SymbolKind) t. TypedSymbol knd t -> String
showUntyped TypedSymbol knd 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 knd, b)] -> String
go0 [(SomeTypedSymbol knd, b)]
xs

-- | Given a typed symbol and a model, return the equation (symbol = value)
-- encoded in the model.
equation :: TypedAnySymbol a -> Model -> Maybe (Term Bool)
equation :: forall a. TypedAnySymbol a -> Model -> Maybe (Term Bool)
equation TypedAnySymbol a
tsym Model
m = TypedAnySymbol a
-> ((SupportedPrim a, Typeable a) => Maybe (Term Bool))
-> Maybe (Term Bool)
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedAnySymbol a
tsym (((SupportedPrim a, Typeable a) => Maybe (Term Bool))
 -> Maybe (Term Bool))
-> ((SupportedPrim a, Typeable a) => Maybe (Term Bool))
-> Maybe (Term Bool)
forall a b. (a -> b) -> a -> b
$
  case TypedAnySymbol a -> Model -> Maybe a
forall t. TypedSymbol 'AnyKind t -> Model -> Maybe t
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> model -> Maybe t
valueOf TypedAnySymbol 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 (TypedAnySymbol a -> Term a
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedAnySymbol a
tsym) (a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm a
v)
    Maybe a
Nothing -> Maybe (Term Bool)
forall a. Maybe a
Nothing

instance SymbolSetOps (SymbolSet knd) (TypedSymbol knd) where
  emptySet :: SymbolSet knd
emptySet = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet HashSet (SomeTypedSymbol knd)
forall a. HashSet a
S.empty
  isEmptySet :: SymbolSet knd -> Bool
isEmptySet (SymbolSet HashSet (SomeTypedSymbol knd)
s) = HashSet (SomeTypedSymbol knd) -> Bool
forall a. HashSet a -> Bool
S.null HashSet (SomeTypedSymbol knd)
s
  containsSymbol :: forall a. TypedSymbol knd a -> SymbolSet knd -> Bool
containsSymbol TypedSymbol knd a
s =
    SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd) -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (TypedSymbol knd a -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol knd a
s) (HashSet (SomeTypedSymbol knd) -> Bool)
-> (SymbolSet knd -> HashSet (SomeTypedSymbol knd))
-> SymbolSet knd
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolSet knd -> HashSet (SomeTypedSymbol knd)
forall (knd :: SymbolKind).
SymbolSet knd -> HashSet (SomeTypedSymbol knd)
unSymbolSet
  insertSymbol :: forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
insertSymbol TypedSymbol knd a
s = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> (SymbolSet knd -> HashSet (SomeTypedSymbol knd))
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SomeTypedSymbol knd
-> HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd)
forall a. (Eq a, Hashable a) => a -> HashSet a -> HashSet a
S.insert (TypedSymbol knd a -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol knd a
s) (HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd))
-> (SymbolSet knd -> HashSet (SomeTypedSymbol knd))
-> SymbolSet knd
-> HashSet (SomeTypedSymbol knd)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolSet knd -> HashSet (SomeTypedSymbol knd)
forall (knd :: SymbolKind).
SymbolSet knd -> HashSet (SomeTypedSymbol knd)
unSymbolSet
  intersectionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd
intersectionSet (SymbolSet HashSet (SomeTypedSymbol knd)
s1) (SymbolSet HashSet (SomeTypedSymbol knd)
s2) = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ HashSet (SomeTypedSymbol knd)
-> HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.intersection HashSet (SomeTypedSymbol knd)
s1 HashSet (SomeTypedSymbol knd)
s2
  unionSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd
unionSet (SymbolSet HashSet (SomeTypedSymbol knd)
s1) (SymbolSet HashSet (SomeTypedSymbol knd)
s2) = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ HashSet (SomeTypedSymbol knd)
-> HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd)
forall a. Eq a => HashSet a -> HashSet a -> HashSet a
S.union HashSet (SomeTypedSymbol knd)
s1 HashSet (SomeTypedSymbol knd)
s2
  differenceSet :: SymbolSet knd -> SymbolSet knd -> SymbolSet knd
differenceSet (SymbolSet HashSet (SomeTypedSymbol knd)
s1) (SymbolSet HashSet (SomeTypedSymbol knd)
s2) = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ HashSet (SomeTypedSymbol knd)
-> HashSet (SomeTypedSymbol knd) -> HashSet (SomeTypedSymbol knd)
forall a. (Eq a, Hashable a) => HashSet a -> HashSet a -> HashSet a
S.difference HashSet (SomeTypedSymbol knd)
s1 HashSet (SomeTypedSymbol knd)
s2

instance
  SymbolSetRep
    (SomeTypedSymbol knd)
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: SomeTypedSymbol knd -> SymbolSet knd
buildSymbolSet SomeTypedSymbol knd
sym = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SomeTypedSymbol knd -> HashSet (SomeTypedSymbol knd)
forall a. Hashable a => a -> HashSet a
S.singleton SomeTypedSymbol knd
sym

instance
  SymbolSetRep
    [SomeTypedSymbol knd]
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: [SomeTypedSymbol knd] -> SymbolSet knd
buildSymbolSet = HashSet (SomeTypedSymbol knd) -> SymbolSet knd
forall (knd :: SymbolKind).
HashSet (SomeTypedSymbol knd) -> SymbolSet knd
SymbolSet (HashSet (SomeTypedSymbol knd) -> SymbolSet knd)
-> ([SomeTypedSymbol knd] -> HashSet (SomeTypedSymbol knd))
-> [SomeTypedSymbol knd]
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [SomeTypedSymbol knd] -> HashSet (SomeTypedSymbol knd)
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList

instance
  SymbolSetRep
    [TypedSymbol knd t]
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: [TypedSymbol knd t] -> SymbolSet knd
buildSymbolSet [TypedSymbol knd t]
sym = [SomeTypedSymbol knd] -> SymbolSet knd
forall rep symbolSet (typedSymbol :: * -> *).
SymbolSetRep rep symbolSet typedSymbol =>
rep -> symbolSet
buildSymbolSet ([SomeTypedSymbol knd] -> SymbolSet knd)
-> [SomeTypedSymbol knd] -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ TypedSymbol knd t -> SomeTypedSymbol knd
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol (TypedSymbol knd t -> SomeTypedSymbol knd)
-> [TypedSymbol knd t] -> [SomeTypedSymbol knd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TypedSymbol knd t]
sym

instance
  SymbolSetRep
    (TypedSymbol knd t)
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: TypedSymbol knd t -> SymbolSet knd
buildSymbolSet TypedSymbol knd t
sym = TypedSymbol knd t -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd t
sym SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b) -> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2) =
    TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3) =
    TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c,
      TypedSymbol knd d
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c,
 TypedSymbol knd d)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3, TypedSymbol knd d
sym4) =
    TypedSymbol knd d -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd d
sym4
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c,
      TypedSymbol knd d,
      TypedSymbol knd e
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c,
 TypedSymbol knd d, TypedSymbol knd e)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3, TypedSymbol knd d
sym4, TypedSymbol knd e
sym5) =
    TypedSymbol knd e -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd e
sym5
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd d -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd d
sym4
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c,
      TypedSymbol knd d,
      TypedSymbol knd e,
      TypedSymbol knd f
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c,
 TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3, TypedSymbol knd d
sym4, TypedSymbol knd e
sym5, TypedSymbol knd f
sym6) =
    TypedSymbol knd f -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd f
sym6
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd e -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd e
sym5
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd d -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd d
sym4
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c,
      TypedSymbol knd d,
      TypedSymbol knd e,
      TypedSymbol knd f,
      TypedSymbol knd g
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c,
 TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f,
 TypedSymbol knd g)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3, TypedSymbol knd d
sym4, TypedSymbol knd e
sym5, TypedSymbol knd f
sym6, TypedSymbol knd g
sym7) =
    TypedSymbol knd g -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd g
sym7
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd f -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd f
sym6
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd e -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd e
sym5
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd d -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd d
sym4
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance
  SymbolSetRep
    ( TypedSymbol knd a,
      TypedSymbol knd b,
      TypedSymbol knd c,
      TypedSymbol knd d,
      TypedSymbol knd e,
      TypedSymbol knd f,
      TypedSymbol knd g,
      TypedSymbol knd h
    )
    (SymbolSet knd)
    (TypedSymbol knd)
  where
  buildSymbolSet :: (TypedSymbol knd a, TypedSymbol knd b, TypedSymbol knd c,
 TypedSymbol knd d, TypedSymbol knd e, TypedSymbol knd f,
 TypedSymbol knd g, TypedSymbol knd h)
-> SymbolSet knd
buildSymbolSet (TypedSymbol knd a
sym1, TypedSymbol knd b
sym2, TypedSymbol knd c
sym3, TypedSymbol knd d
sym4, TypedSymbol knd e
sym5, TypedSymbol knd f
sym6, TypedSymbol knd g
sym7, TypedSymbol knd h
sym8) =
    TypedSymbol knd h -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd h
sym8
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd g -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd g
sym7
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd f -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd f
sym6
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd e -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd e
sym5
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd d -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd d
sym4
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd c -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd c
sym3
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd b -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd b
sym2
      (SymbolSet knd -> SymbolSet knd)
-> (SymbolSet knd -> SymbolSet knd)
-> SymbolSet knd
-> SymbolSet knd
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall a. TypedSymbol knd a -> SymbolSet knd -> SymbolSet knd
forall symbolSet (typedSymbol :: * -> *) a.
SymbolSetOps symbolSet typedSymbol =>
typedSymbol a -> symbolSet -> symbolSet
insertSymbol TypedSymbol knd a
sym1
      (SymbolSet knd -> SymbolSet knd) -> SymbolSet knd -> SymbolSet knd
forall a b. (a -> b) -> a -> b
$ SymbolSet knd
forall symbolSet (typedSymbol :: * -> *).
SymbolSetOps symbolSet typedSymbol =>
symbolSet
emptySet

instance ModelOps Model AnySymbolSet TypedAnySymbol where
  emptyModel :: Model
emptyModel = HashMap SomeTypedAnySymbol ModelValue -> Model
Model HashMap SomeTypedAnySymbol ModelValue
forall k v. HashMap k v
M.empty
  isEmptyModel :: Model -> Bool
isEmptyModel (Model HashMap SomeTypedAnySymbol ModelValue
m) = HashMap SomeTypedAnySymbol ModelValue -> Bool
forall k v. HashMap k v -> Bool
M.null HashMap SomeTypedAnySymbol ModelValue
m
  valueOf :: forall t. TypedAnySymbol t -> Model -> Maybe t
  valueOf :: forall t. TypedSymbol 'AnyKind t -> Model -> Maybe t
valueOf TypedAnySymbol t
sym (Model HashMap SomeTypedAnySymbol ModelValue
m) =
    TypedAnySymbol t
-> ((SupportedPrim t, Typeable t) => Maybe t) -> Maybe t
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedAnySymbol t
sym (((SupportedPrim t, Typeable t) => Maybe t) -> Maybe t)
-> ((SupportedPrim t, Typeable 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
<$> SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (TypedAnySymbol t -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedAnySymbol t
sym) HashMap SomeTypedAnySymbol ModelValue
m
  modelContains :: forall a. TypedAnySymbol a -> Model -> Bool
modelContains TypedAnySymbol a
sym (Model HashMap SomeTypedAnySymbol ModelValue
m) = SomeTypedAnySymbol -> HashMap SomeTypedAnySymbol ModelValue -> Bool
forall k a. (Eq k, Hashable k) => k -> HashMap k a -> Bool
M.member (TypedAnySymbol a -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedAnySymbol a
sym) HashMap SomeTypedAnySymbol ModelValue
m
  exceptFor :: AnySymbolSet -> Model -> Model
exceptFor (SymbolSet HashSet SomeTypedAnySymbol
s) (Model HashMap SomeTypedAnySymbol ModelValue
m) = HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$ (HashMap SomeTypedAnySymbol ModelValue
 -> SomeTypedAnySymbol -> HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
-> HashSet SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl' ((SomeTypedAnySymbol
 -> HashMap SomeTypedAnySymbol ModelValue
 -> HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
-> SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
forall a b c. (a -> b -> c) -> b -> a -> c
flip SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete) HashMap SomeTypedAnySymbol ModelValue
m HashSet SomeTypedAnySymbol
s
  exceptFor' :: forall t. TypedAnySymbol t -> Model -> Model
exceptFor' TypedAnySymbol t
s (Model HashMap SomeTypedAnySymbol ModelValue
m) = HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$ SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> HashMap k v
M.delete (TypedAnySymbol t -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedAnySymbol t
s) HashMap SomeTypedAnySymbol ModelValue
m
  restrictTo :: AnySymbolSet -> Model -> Model
restrictTo (SymbolSet HashSet SomeTypedAnySymbol
s) (Model HashMap SomeTypedAnySymbol ModelValue
m) =
    HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
      (HashMap SomeTypedAnySymbol ModelValue
 -> SomeTypedAnySymbol -> HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
-> HashSet SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
        ( \HashMap SomeTypedAnySymbol ModelValue
acc SomeTypedAnySymbol
sym -> case SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTypedAnySymbol
sym HashMap SomeTypedAnySymbol ModelValue
m of
            Just ModelValue
v -> SomeTypedAnySymbol
-> ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTypedAnySymbol
sym ModelValue
v HashMap SomeTypedAnySymbol ModelValue
acc
            Maybe ModelValue
Nothing -> HashMap SomeTypedAnySymbol ModelValue
acc
        )
        HashMap SomeTypedAnySymbol ModelValue
forall k v. HashMap k v
M.empty
        HashSet SomeTypedAnySymbol
s
  extendTo :: AnySymbolSet -> Model -> Model
extendTo (SymbolSet HashSet SomeTypedAnySymbol
s) (Model HashMap SomeTypedAnySymbol ModelValue
m) =
    HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
      (HashMap SomeTypedAnySymbol ModelValue
 -> SomeTypedAnySymbol -> HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
-> HashSet SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue
forall a b. (a -> b -> a) -> a -> HashSet b -> a
S.foldl'
        ( \HashMap SomeTypedAnySymbol ModelValue
acc sym :: SomeTypedAnySymbol
sym@(SomeTypedSymbol (TypedSymbol 'AnyKind t
tsym :: TypedAnySymbol t)) -> case SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTypedAnySymbol
sym HashMap SomeTypedAnySymbol ModelValue
acc of
            Just ModelValue
_ -> HashMap SomeTypedAnySymbol ModelValue
acc
            Maybe ModelValue
Nothing -> TypedSymbol 'AnyKind t
-> ((SupportedPrim t, Typeable t) =>
    HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol 'AnyKind t
tsym (((SupportedPrim t, Typeable t) =>
  HashMap SomeTypedAnySymbol ModelValue)
 -> HashMap SomeTypedAnySymbol ModelValue)
-> ((SupportedPrim t, Typeable t) =>
    HashMap SomeTypedAnySymbol ModelValue)
-> HashMap SomeTypedAnySymbol ModelValue
forall a b. (a -> b) -> a -> b
$ SomeTypedAnySymbol
-> ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTypedAnySymbol
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 SomeTypedAnySymbol ModelValue
acc
        )
        HashMap SomeTypedAnySymbol ModelValue
m
        HashSet SomeTypedAnySymbol
s
  insertValue :: forall t. TypedAnySymbol t -> t -> Model -> Model
insertValue TypedAnySymbol t
sym (t
v :: t) (Model HashMap SomeTypedAnySymbol ModelValue
m) =
    TypedAnySymbol t
-> ((SupportedPrim t, Typeable t) => Model) -> Model
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedAnySymbol t
sym (((SupportedPrim t, Typeable t) => Model) -> Model)
-> ((SupportedPrim t, Typeable t) => Model) -> Model
forall a b. (a -> b) -> a -> b
$
      HashMap SomeTypedAnySymbol ModelValue -> Model
Model (HashMap SomeTypedAnySymbol ModelValue -> Model)
-> HashMap SomeTypedAnySymbol ModelValue -> Model
forall a b. (a -> b) -> a -> b
$
        SomeTypedAnySymbol
-> ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
-> HashMap SomeTypedAnySymbol ModelValue
forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert (TypedAnySymbol t -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedAnySymbol t
sym) (t -> ModelValue
forall a. SupportedPrim a => a -> ModelValue
toModelValue t
v) HashMap SomeTypedAnySymbol ModelValue
m

-- | Evaluate a term in the given model.
evalTerm ::
  (SupportedPrim a) =>
  Bool ->
  Model ->
  S.HashSet SomeTypedConstantSymbol ->
  Term a ->
  Term a
evalTerm :: forall a.
SupportedPrim a =>
Bool
-> Model -> HashSet SomeTypedConstantSymbol -> Term a -> Term a
evalTerm Bool
fillDefault (Model HashMap SomeTypedAnySymbol ModelValue
ma) =
  (forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term a -> Term a
forall v.
(forall a. TypedSymbol 'AnyKind a -> Term a)
-> HashSet SomeTypedConstantSymbol -> Term v -> Term v
generalSubstSomeTerm
    ( \(TypedSymbol 'AnyKind a
sym :: TypedSymbol 'AnyKind a) ->
        TypedSymbol 'AnyKind a
-> ((SupportedPrim a, Typeable a) => Term a) -> Term a
forall (knd :: SymbolKind) t a.
TypedSymbol knd t -> ((SupportedPrim t, Typeable t) => a) -> a
withSymbolSupported TypedSymbol 'AnyKind a
sym (((SupportedPrim a, Typeable a) => Term a) -> Term a)
-> ((SupportedPrim a, Typeable a) => Term a) -> Term a
forall a b. (a -> b) -> a -> b
$
          case (SomeTypedAnySymbol
-> HashMap SomeTypedAnySymbol ModelValue -> Maybe ModelValue
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup (TypedSymbol 'AnyKind a -> SomeTypedAnySymbol
forall (knd :: SymbolKind) t.
TypedSymbol knd t -> SomeTypedSymbol knd
someTypedSymbol TypedSymbol 'AnyKind a
sym) HashMap SomeTypedAnySymbol ModelValue
ma) of
            Maybe ModelValue
Nothing ->
              if Bool
fillDefault
                then a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (forall t. SupportedPrim t => t
defaultValue @a)
                else TypedSymbol 'AnyKind a -> Term a
forall (knd :: SymbolKind) t. TypedSymbol knd t -> Term t
symTerm TypedSymbol 'AnyKind a
sym
            Just ModelValue
dy ->
              a -> Term a
forall t. SupportedPrim t => t -> Term t
conTerm (forall a. Typeable a => ModelValue -> a
unsafeFromModelValue @a ModelValue
dy)
    )

-- |
-- 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 = (TypedAnySymbol 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 (TypedAnySymbol t
sym ::= t
val) = TypedAnySymbol t -> t -> Model -> Model
forall t. TypedAnySymbol t -> t -> Model -> Model
forall model symbolSet (typedSymbol :: * -> *) t.
ModelOps model symbolSet typedSymbol =>
typedSymbol t -> t -> model -> model
insertValue TypedAnySymbol 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