{-# LANGUAGE ScopedTypeVariables #-}

-- |
-- Module      :   Grisette.Backend.SBV.Data.SMT.SymBiMap
-- 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.Backend.SBV.Data.SMT.SymBiMap
  ( SymBiMap (..),
    emptySymBiMap,
    sizeBiMap,
    addBiMap,
    addBiMapIntermediate,
    findStringToSymbol,
    lookupTerm,
  )
where

import Data.Dynamic
import qualified Data.HashMap.Strict as M
import GHC.Stack
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.SomeTerm
import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term

data SymBiMap = SymBiMap
  { SymBiMap -> HashMap SomeTerm Dynamic
biMapToSBV :: M.HashMap SomeTerm Dynamic,
    SymBiMap -> HashMap String SomeTypedSymbol
biMapFromSBV :: M.HashMap String SomeTypedSymbol
  }
  deriving (Int -> SymBiMap -> ShowS
[SymBiMap] -> ShowS
SymBiMap -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SymBiMap] -> ShowS
$cshowList :: [SymBiMap] -> ShowS
show :: SymBiMap -> String
$cshow :: SymBiMap -> String
showsPrec :: Int -> SymBiMap -> ShowS
$cshowsPrec :: Int -> SymBiMap -> ShowS
Show)

emptySymBiMap :: SymBiMap
emptySymBiMap :: SymBiMap
emptySymBiMap = HashMap SomeTerm Dynamic
-> HashMap String SomeTypedSymbol -> SymBiMap
SymBiMap forall k v. HashMap k v
M.empty forall k v. HashMap k v
M.empty

sizeBiMap :: SymBiMap -> Int
sizeBiMap :: SymBiMap -> Int
sizeBiMap = forall k v. HashMap k v -> Int
M.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymBiMap -> HashMap SomeTerm Dynamic
biMapToSBV

addBiMap :: HasCallStack => SomeTerm -> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap :: HasCallStack =>
SomeTerm
-> Dynamic -> String -> SomeTypedSymbol -> SymBiMap -> SymBiMap
addBiMap SomeTerm
s Dynamic
d String
n SomeTypedSymbol
sb (SymBiMap HashMap SomeTerm Dynamic
t HashMap String SomeTypedSymbol
f) = HashMap SomeTerm Dynamic
-> HashMap String SomeTypedSymbol -> SymBiMap
SymBiMap (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTerm
s Dynamic
d HashMap SomeTerm Dynamic
t) (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert String
n SomeTypedSymbol
sb HashMap String SomeTypedSymbol
f)

addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate :: HasCallStack => SomeTerm -> Dynamic -> SymBiMap -> SymBiMap
addBiMapIntermediate SomeTerm
s Dynamic
d (SymBiMap HashMap SomeTerm Dynamic
t HashMap String SomeTypedSymbol
f) = HashMap SomeTerm Dynamic
-> HashMap String SomeTypedSymbol -> SymBiMap
SymBiMap (forall k v.
(Eq k, Hashable k) =>
k -> v -> HashMap k v -> HashMap k v
M.insert SomeTerm
s Dynamic
d HashMap SomeTerm Dynamic
t) HashMap String SomeTypedSymbol
f

findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol
findStringToSymbol :: String -> SymBiMap -> Maybe SomeTypedSymbol
findStringToSymbol String
s (SymBiMap HashMap SomeTerm Dynamic
_ HashMap String SomeTypedSymbol
f) = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup String
s HashMap String SomeTypedSymbol
f

lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm :: HasCallStack => SomeTerm -> SymBiMap -> Maybe Dynamic
lookupTerm SomeTerm
t SymBiMap
m = forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
M.lookup SomeTerm
t (SymBiMap -> HashMap SomeTerm Dynamic
biMapToSBV SymBiMap
m)