{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- |
-- Module      :   Grisette.IR.SymPrim.Data.Prim.ModelValue
-- 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.ModelValue
  ( ModelValue (..),
    toModelValue,
    unsafeFromModelValue,
  )
where

import Data.Hashable
import Type.Reflection

data ModelValue where
  ModelValue :: forall v. (Show v, Eq v, Hashable v) => TypeRep v -> v -> ModelValue

instance Show ModelValue where
  show :: ModelValue -> String
show (ModelValue TypeRep v
t v
v) = v -> String
forall a. Show a => a -> String
show v
v String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" :: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep v -> String
forall a. Show a => a -> String
show TypeRep v
t

instance Eq ModelValue where
  (ModelValue TypeRep v
t1 v
v1) == :: ModelValue -> ModelValue -> Bool
== (ModelValue TypeRep v
t2 v
v2) =
    case TypeRep v -> TypeRep v -> Maybe (v :~~: v)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep v
t1 TypeRep v
t2 of
      Just v :~~: v
HRefl -> v
v1 v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
v
v2
      Maybe (v :~~: v)
_ -> Bool
False

instance Hashable ModelValue where
  Int
s hashWithSalt :: Int -> ModelValue -> Int
`hashWithSalt` (ModelValue TypeRep v
t v
v) = Int
s Int -> TypeRep v -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` TypeRep v
t Int -> v -> Int
forall a. Hashable a => Int -> a -> Int
`hashWithSalt` v
v

unsafeFromModelValue :: forall a. (Typeable a) => ModelValue -> a
unsafeFromModelValue :: forall a. Typeable a => ModelValue -> a
unsafeFromModelValue (ModelValue TypeRep v
t v
v) = case TypeRep v -> TypeRep a -> Maybe (v :~~: a)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep TypeRep v
t (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) of
  Just v :~~: a
HRefl -> a
v
v
  Maybe (v :~~: a)
_ -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"Bad model value type, expected type: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", but got: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ TypeRep v -> String
forall a. Show a => a -> String
show TypeRep v
t

toModelValue :: forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue :: forall a. (Show a, Eq a, Hashable a, Typeable a) => a -> ModelValue
toModelValue = TypeRep a -> a -> ModelValue
forall v.
(Show v, Eq v, Hashable v) =>
TypeRep v -> v -> ModelValue
ModelValue (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)