-- |
-- Module      :   Grisette.Internal.Unified.Theories
-- Copyright   :   (c) Sirui Lu 2024
-- License     :   BSD-3-Clause (see the LICENSE file)
--
-- Maintainer  :   siruilu@cs.washington.edu
-- Stability   :   Experimental
-- Portability :   GHC only
module Grisette.Internal.Unified.Theories (TheoryToUnify (..), isUFun) where

-- | This data type is used to represent the theories that is unified.
--
-- The 'UFun' constructor is used to represent a specific uninterpreted function
-- type. The type is uncurried.
data TheoryToUnify
  = UBool
  | UIntN
  | UWordN
  | UInteger
  | UAlgReal
  | UFP
  | UFun [TheoryToUnify]
  deriving (TheoryToUnify -> TheoryToUnify -> Bool
(TheoryToUnify -> TheoryToUnify -> Bool)
-> (TheoryToUnify -> TheoryToUnify -> Bool) -> Eq TheoryToUnify
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: TheoryToUnify -> TheoryToUnify -> Bool
== :: TheoryToUnify -> TheoryToUnify -> Bool
$c/= :: TheoryToUnify -> TheoryToUnify -> Bool
/= :: TheoryToUnify -> TheoryToUnify -> Bool
Eq, Int -> TheoryToUnify -> ShowS
[TheoryToUnify] -> ShowS
TheoryToUnify -> String
(Int -> TheoryToUnify -> ShowS)
-> (TheoryToUnify -> String)
-> ([TheoryToUnify] -> ShowS)
-> Show TheoryToUnify
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> TheoryToUnify -> ShowS
showsPrec :: Int -> TheoryToUnify -> ShowS
$cshow :: TheoryToUnify -> String
show :: TheoryToUnify -> String
$cshowList :: [TheoryToUnify] -> ShowS
showList :: [TheoryToUnify] -> ShowS
Show)

-- | Check if the theory is a uninterpreted function.
isUFun :: TheoryToUnify -> Bool
isUFun :: TheoryToUnify -> Bool
isUFun (UFun [TheoryToUnify]
_) = Bool
True
isUFun TheoryToUnify
_ = Bool
False