content: {-# LANGUAGE CPP                        #-}
  {-# LANGUAGE TupleSections              #-}
  {-# LANGUAGE DeriveDataTypeable         #-}
  {-# LANGUAGE DeriveGeneric              #-}
  {-# LANGUAGE FlexibleContexts           #-}
  {-# LANGUAGE FlexibleInstances          #-}
  {-# LANGUAGE LambdaCase                 #-}
  {-# LANGUAGE NoMonomorphismRestriction  #-}
  {-# LANGUAGE OverloadedStrings          #-}
  {-# LANGUAGE UndecidableInstances       #-}
  {-# LANGUAGE MultiParamTypeClasses      #-}
  {-# LANGUAGE GADTs                      #-}
  {-# LANGUAGE ViewPatterns               #-}
  
  {-# OPTIONS_GHC -Wno-name-shadowing     #-}
  {-# LANGUAGE DeriveAnyClass #-}
  
  -- | This module contains the data types, operations and
  --   serialization functions for representing Fixpoint's
  --   Horn and well-formedness constraints.
  
  module Language.Fixpoint.Types.Sorts (
  
    -- * Fixpoint Types
      Sort (..)
    , Sub (..)
    , FTycon
  
    , sortFTycon
    , intFTyCon
    , boolFTyCon
    , realFTyCon
    , numFTyCon
    , strFTyCon
    , setFTyCon
    , mapFTyCon -- TODO: hide these
    , mapFVar
    , basicSorts, intSort, realSort, boolSort, strSort, funcSort
    -- , bitVec32Sort, bitVec64Sort
    , setSort, bitVecSort, bagSort
    , arraySort
    , sizedBitVecSort
    , mapSort, charSort
    , listFTyCon
    , isListTC
    , sizeBv
    , isFirstOrder
    , mappendFTC
    , fTyconSymbol, symbolFTycon, fTyconSort, symbolNumInfoFTyCon
    , fTyconSelfSort
    , fApp
    , fAppTC
    , fObj
    , unFApp
    , unAbs
    , sortAbs
  
    , mkSortSubst
    , sortSubst
    , SortSubst
    , functionSort
    , mkFFunc
    , bkFFunc
    , bkAbs
    , mkPoly
    , sortSymbols
    , substSort
  
    , isBool, isNumeric, isReal, isString, isSet, isMap, isBag, isArray, isPolyInst
  
    -- * User-defined ADTs
    , DataField (..)
    , DataCtor (..)
    , DataDecl (..)
    , muSort
  
    -- * Embedding Source types as Sorts
    , TCEmb, TCArgs (..)
    , tceLookup
    , tceFromList
    , tceToList
    , tceMember
    , tceInsert
    , tceInsertWith
    , tceMap
  
    -- * Sort coercion for SMT theory encoding
    , coerceMapToArray
    , coerceSetBagToArray
    , coerceDataDecl
    ) where
  
  import qualified Data.Store as S
  import           Data.Generics             (Data)
  import           Data.Typeable             (Typeable)
  import           GHC.Generics              (Generic)
  import           Data.Aeson
  import           Data.Bifunctor (first)
  
  import           Data.Hashable
  import           Data.HashSet (HashSet)
  import qualified Data.HashSet as HashSet
  #if !MIN_VERSION_base(4,20,0)
  import           Data.List                 (foldl')
  #endif
  import           Control.DeepSeq
  import           Data.Maybe                (fromMaybe)
  import           Language.Fixpoint.Types.Config (ElabFlags, elabSetBag)
  import           Language.Fixpoint.Types.Names
  import           Language.Fixpoint.Types.PrettyPrint
  import           Language.Fixpoint.Types.Spans
  import           Language.Fixpoint.Misc
  import           Text.PrettyPrint.HughesPJ.Compat
  import qualified Data.HashMap.Strict       as M
  import qualified Data.List                 as L
  import qualified Data.Binary as B
  import Text.Read (readMaybe)
  
  data FTycon   = TC LocSymbol TCInfo deriving (Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  -- instance Show FTycon where
  --   show (TC s _) = show (val s)
  
  instance Symbolic FTycon where
    symbol (TC s _) = symbol s
  
  instance Eq FTycon where
    (TC s _) == (TC s' _) = val s == val s'
  
  data TCInfo = TCInfo { tc_isNum :: Bool, tc_isReal :: Bool, tc_isString :: Bool }
    deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  mappendFTC :: FTycon -> FTycon -> FTycon
  mappendFTC (TC x i1) (TC _ i2) = TC x (mappend i1 i2)
  
  instance Semigroup TCInfo where
   TCInfo i1 i2 i3 <> TCInfo i1' i2' i3' = TCInfo (i1 || i1') (i2 || i2') (i3 || i3')
  
  instance Monoid TCInfo where
    mempty  = TCInfo defNumInfo defRealInfo defStrInfo
    mappend = (<>)
  
  defTcInfo, numTcInfo, realTcInfo, strTcInfo :: TCInfo
  defTcInfo  = TCInfo defNumInfo defRealInfo defStrInfo
  numTcInfo  = TCInfo True       defRealInfo defStrInfo
  realTcInfo = TCInfo True       True        defStrInfo
  strTcInfo  = TCInfo defNumInfo defRealInfo True
  
  defNumInfo, defRealInfo, defStrInfo :: Bool
  defNumInfo  = False
  defRealInfo = False
  defStrInfo  = False
  
  charFTyCon, intFTyCon, boolFTyCon, realFTyCon, funcFTyCon, numFTyCon :: FTycon
  strFTyCon, listFTyCon, mapFTyCon, bagFTyCon, setFTyCon :: FTycon
  intFTyCon  = TC (dummyLoc "int"       ) numTcInfo
  boolFTyCon = TC (dummyLoc boolLConName) defTcInfo
  realFTyCon = TC (dummyLoc "real"      ) realTcInfo
  numFTyCon  = TC (dummyLoc "num"       ) numTcInfo
  funcFTyCon = TC (dummyLoc "function"  ) defTcInfo
  strFTyCon  = TC (dummyLoc strConName  ) strTcInfo
  listFTyCon = TC (dummyLoc listConName ) defTcInfo
  charFTyCon = TC (dummyLoc charConName ) defTcInfo
  setFTyCon  = TC (dummyLoc setConName  ) defTcInfo
  mapFTyCon  = TC (dummyLoc mapConName  ) defTcInfo
  bagFTyCon  = TC (dummyLoc bagConName  ) defTcInfo
  
  isListConName :: LocSymbol -> Bool
  isListConName x = c == listConName || c == listLConName --"List"
    where
      c           = val x
  
  isListTC :: FTycon -> Bool
  isListTC (TC z _) = isListConName z
  
  isSetConName :: LocSymbol -> Bool
  isSetConName x = c == setConName
    where
      c           = val x
  
  isSetTC :: FTycon -> Bool
  isSetTC (TC z _) = isSetConName z
  
  isMapConName :: LocSymbol -> Bool
  isMapConName x = c == mapConName
    where
      c           = val x
  
  isMapTC :: FTycon -> Bool
  isMapTC (TC z _) = isMapConName z
  
  isBagConName :: LocSymbol -> Bool
  isBagConName x = c == bagConName
    where
      c           = val x
  
  isBagTC :: FTycon -> Bool
  isBagTC (TC z _) = isBagConName z
  
  isArrayConName :: LocSymbol -> Bool
  isArrayConName x = c == arrayConName
    where
      c           = val x
  
  isArrayTC :: FTycon -> Bool
  isArrayTC (TC z _) = isArrayConName z
  
  sizeBv :: FTycon -> Maybe Int
  sizeBv tc = do
    let s = val $ fTyconSymbol tc
    size <- stripPrefix sizeName s
    readMaybe $ symbolString size
  
  fTyconSymbol :: FTycon -> Located Symbol
  fTyconSymbol (TC s _) = s
  
  symbolNumInfoFTyCon :: LocSymbol -> Bool -> Bool -> FTycon
  symbolNumInfoFTyCon c isNum isReal
    | isListConName c
    = TC (fmap (const listConName) c) tcinfo
    | otherwise
    = TC c tcinfo
    where
      tcinfo = defTcInfo { tc_isNum = isNum, tc_isReal = isReal}
  
  
  
  symbolFTycon :: LocSymbol -> FTycon
  symbolFTycon c = symbolNumInfoFTyCon c defNumInfo defRealInfo
  
  fApp :: Sort -> [Sort] -> Sort
  fApp = foldl' FApp
  
  fAppTC :: FTycon -> [Sort] -> Sort
  fAppTC = fApp . fTyconSort
  
  fTyconSelfSort :: FTycon -> Int -> Sort
  fTyconSelfSort c n = fAppTC c [FVar i | i <- [0..(n - 1)]]
  
  -- | fApp' (FApp (FApp "Map" key) val) ===> ["Map", key, val]
  --   That is, `fApp'` is used to split a type application into
  --   the FTyCon and its args.
  
  unFApp :: Sort -> ListNE Sort
  unFApp = go []
    where
      go acc (FApp t1 t2) = go (t2 : acc) t1
      go acc t            = t : acc
  
  unAbs :: Sort -> Sort
  unAbs (FAbs _ s) = unAbs s
  unAbs s          = s
  
  fObj :: LocSymbol -> Sort
  fObj = fTyconSort . (`TC` defTcInfo)
  
  sortFTycon :: Sort -> Maybe FTycon
  sortFTycon FInt    = Just intFTyCon
  sortFTycon FReal   = Just realFTyCon
  sortFTycon FNum    = Just numFTyCon
  sortFTycon (FTC c) = Just c
  sortFTycon _       = Nothing
  
  
  functionSort :: Sort -> Maybe ([Int], [Sort], Sort)
  functionSort s
    | null is && null ss
    = Nothing
    | otherwise
    = Just (is, ss, r)
    where
      (is, ss, r)            = go [] [] s
      go vs ss (FAbs i t)    = go (i:vs) ss t
      go vs ss (FFunc s1 s2) = go vs (s1:ss) s2
      go vs ss t             = (reverse vs, reverse ss, t)
  
  
  sortAbs :: Sort -> Int
  sortAbs (FAbs i s)    = max i (sortAbs s)
  sortAbs (FFunc s1 s2) = max (sortAbs s1) (sortAbs s2)
  sortAbs (FApp  s1 s2) = max (sortAbs s1) (sortAbs s2)
  sortAbs _             = -1
  
  mapFVar :: (Int -> Int) -> Sort -> Sort
  mapFVar f = go
    where go (FVar i)      = FVar (f i)
          go (FAbs i t)    = FAbs (f i) (go t)
          go (FFunc t1 t2) = FFunc (go t1) (go t2)
          go (FApp t1 t2)  = FApp (go t1) (go t2)
          go t@(FObj _)    = t
          go t@(FTC _)     = t
          go t@FInt        = t
          go t@FReal       = t
          go t@FNum        = t
          go t@FFrac       = t
  
  --------------------------------------------------------------------------------
  -- | Sorts ---------------------------------------------------------------------
  --------------------------------------------------------------------------------
  data Sort = FInt
            | FReal
            | FNum                 -- ^ numeric kind for Num tyvars
            | FFrac                -- ^ numeric kind for Fractional tyvars
            | FObj  !Symbol        -- ^ uninterpreted type
            | FVar  !Int           -- ^ fixpoint type variable
            | FFunc !Sort !Sort    -- ^ function
            | FAbs  !Int !Sort     -- ^ type-abstraction
            | FTC   !FTycon
            | FApp  !Sort !Sort    -- ^ constructed type
              deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  instance PPrint Sort where
    pprintTidy _ = toFix
  
  sortSymbols :: Sort -> HashSet Symbol
  sortSymbols = \case
    FObj s -> HashSet.singleton s
    FFunc t0 t1 -> HashSet.union (sortSymbols t0) (sortSymbols t1)
    FAbs _ t -> sortSymbols t
    FApp t0 t1 -> HashSet.union (sortSymbols t0) (sortSymbols t1)
    _ -> HashSet.empty
  
  substSort :: (Symbol -> Sort) -> Sort -> Sort
  substSort f = \case
    FObj s -> f s
    FFunc t0 t1 -> FFunc (substSort f t0) (substSort f t1)
    FApp t0 t1 -> FApp (substSort f t0) (substSort f t1)
    FAbs i t -> FAbs i (substSort f t)
    t -> t
  
  data DataField = DField
    { dfName :: !LocSymbol          -- ^ Field Name
    , dfSort :: !Sort               -- ^ Field Sort
    } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  data DataCtor = DCtor
    { dcName   :: !LocSymbol        -- ^ Ctor Name
    , dcFields :: ![DataField]      -- ^ Ctor Fields
    } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  data DataDecl = DDecl
    { ddTyCon :: !FTycon            -- ^ Name of defined datatype
    , ddVars  :: !Int               -- ^ Number of type variables
    , ddCtors :: [DataCtor]         -- ^ Datatype Ctors. Invariant: type variables bound in ctors are greater than ddVars
    } deriving (Eq, Ord, Show, Data, Typeable, Generic, ToJSON, FromJSON)
  
  instance Loc DataDecl where
      srcSpan (DDecl ty _ _) = srcSpan ty
  
  instance Symbolic DataDecl where
    symbol = symbol . ddTyCon
  
  instance Symbolic DataField where
    symbol = val . dfName
  
  instance Symbolic DataCtor where
    symbol = val . dcName
  
  --------------------------------------------------------------------------------------------------
  muSort  :: [DataDecl] -> [DataDecl]
  muSort dds = mapSortDataDecl tx <$> dds
    where
      selfs = [(fTyconSelfSort c n, fTyconSort c) | DDecl c n _ <- dds]
      tx t  = fromMaybe t $ L.lookup t selfs
  
      mapSortDataDecl f  dd = dd { ddCtors  = mapSortDataCTor f  <$> ddCtors  dd }
      mapSortDataCTor f  ct = ct { dcFields = mapSortDataField f <$> dcFields ct }
      mapSortDataField f df = df { dfSort   = f $ dfSort df }
  
  
  isFirstOrder, isFunction :: Sort -> Bool
  isFirstOrder (FFunc sx s) = not (isFunction sx) && isFirstOrder s
  isFirstOrder (FAbs _ s)   = isFirstOrder s
  isFirstOrder (FApp s1 s2) = not (isFunction s1) && not (isFunction s2)
  isFirstOrder _            = True
  
  isFunction (FAbs _ s)  = isFunction s
  isFunction (FFunc _ _) = True
  isFunction _           = False
  
  isBool :: Sort -> Bool
  isBool (FTC (TC c _)) = val c == boolLConName
  isBool _              = False
  
  isNumeric :: Sort -> Bool
  isNumeric FInt           = True
  isNumeric FReal          = True
  isNumeric (FApp s _)     = isNumeric s
  isNumeric (FTC (TC _ i)) = tc_isNum i
  isNumeric (FAbs _ s)     = isNumeric s
  isNumeric _              = False
  
  isReal :: Sort -> Bool
  isReal FReal          = True
  isReal (FApp s _)     = isReal s
  isReal (FTC (TC _ i)) = tc_isReal i
  isReal (FAbs _ s)     = isReal s
  isReal _              = False
  
  isString :: Sort -> Bool
  isString (FApp l c)     = (isList l && isChar c) || isString l
  isString (FTC (TC c i)) = val c == strConName || tc_isString i
  isString (FAbs _ s)     = isString s
  isString _              = False
  
  isList :: Sort -> Bool
  isList (FTC c) = isListTC c
  isList _       = False
  
  isSet :: Sort -> Bool
  isSet (FTC c) = isSetTC c
  isSet _       = False
  
  isMap :: Sort -> Bool
  isMap (FTC c) = isMapTC c
  isMap _       = False
  
  isBag :: Sort -> Bool
  isBag (FTC c) = isBagTC c
  isBag _       = False
  
  isArray :: Sort -> Bool
  isArray (FTC c) = isArrayTC c
  isArray _       = False
  
  isChar :: Sort -> Bool
  isChar (FTC c) = c == charFTyCon
  isChar _       = False
  
  {-@ FFunc :: Nat -> ListNE Sort -> Sort @-}
  
  mkFFunc :: Int -> [Sort] -> Sort
  mkFFunc i ss     = go [0..i-1] ss
    where
      go [] [s]    = s
      go [] (s:ss) = FFunc s $ go [] ss
      go (i:is) ss = FAbs  i $ go is ss
      go _ _       = error "cannot happen"
  
     -- foldl' (flip FAbs) (foldl1 (flip FFunc) ss) [0..i-1]
  
  bkFFunc :: Sort -> Maybe (Int, [Sort])
  bkFFunc t    = (maximum (0 : as),) <$> bkFun t'
    where
      (as, t') = bkAbs t
  
  bkAbs :: Sort -> ([Int], Sort)
  bkAbs (FAbs i t) = (i:is, t') where (is, t') = bkAbs t
  bkAbs t          = ([], t)
  
  bkFun :: Sort -> Maybe [Sort]
  bkFun z@(FFunc _ _)  = Just (go z)
    where
      go (FFunc t1 t2) = t1 : go t2
      go t             = [t]
  bkFun _              = Nothing
  
  isPolyInst :: Sort -> Sort -> Bool
  isPolyInst s t = isPoly s && not (isPoly t)
  
  isPoly :: Sort -> Bool
  isPoly FAbs {} = True
  isPoly _       = False
  
  mkPoly :: Int -> Sort -> Sort
  mkPoly i s = foldl' (flip FAbs) s [0..i]
  
  
  instance Hashable FTycon where
    hashWithSalt i (TC s _) = hashWithSalt i s
  
  instance Loc FTycon where
    srcSpan (TC c _) = srcSpan c
  
  instance Hashable Sort
  
  newtype Sub = Sub [(Int, Sort)] deriving (Generic)
  
  instance Fixpoint Sort where
    toFix = toFixSort
  
  toFixSort :: Sort -> Doc
  toFixSort (FVar i)     = text "@" <-> parens (toFix i)
  toFixSort FInt         = text "int"
  toFixSort FReal        = text "real"
  toFixSort FFrac        = text "frac"
  toFixSort (FObj x)     = toFix x
  toFixSort FNum         = text "num"
  toFixSort t@(FAbs _ _) = toFixAbsApp t
  toFixSort t@(FFunc _ _)= toFixAbsApp t
  toFixSort (FTC c)      = toFix c
  toFixSort t@(FApp _ _) = toFixFApp (unFApp t)
  
  toFixAbsApp :: Sort -> Doc
  toFixAbsApp (functionSort -> Just (vs, ss, s)) =
    text "func" <-> parens (toFix n <+> text "," <+> toFix ts)
    where
      n                = length vs
      ts               = ss ++ [s]
  toFixAbsApp _ = error "Unexpected nothing function sort"
  
  toFixFApp            :: ListNE Sort -> Doc
  toFixFApp [t]        = toFixSort t
  toFixFApp [FTC c, t]
    | isListTC c       = brackets $ toFixSort t
  toFixFApp ts         = parens $ intersperse (text "") (toFixSort <$> ts)
  
  instance Fixpoint FTycon where
    toFix (TC s _)       = toFix (val s)
  
  instance Fixpoint DataField where
    toFix (DField x t) = toFix x <+> text ":" <+> toFix t
  
  instance Fixpoint DataCtor where
    toFix (DCtor x flds) = toFix x <+> braces (intersperse comma (toFix <$> flds))
  
  instance Fixpoint DataDecl where
    toFix (DDecl tc n ctors) = vcat ([header] ++ body ++ [footer])
      where
        header               = toFix tc <+> toFix n <+> text "= ["
        body                 = [nest 2 (text "|" <+> toFix ct) | ct <- ctors]
        footer               = text "]"
  
  instance PPrint FTycon where
    pprintTidy _ = toFix
  
  instance PPrint DataField where
    pprintTidy _ = toFix
  
  instance PPrint DataCtor where
    pprintTidy _ = toFix
  
  instance PPrint DataDecl where
    pprintTidy _ = toFix
  
  -------------------------------------------------------------------------
  -- | Exported Basic Sorts -----------------------------------------------
  -------------------------------------------------------------------------
  
  boolSort, intSort, realSort, strSort, charSort, funcSort :: Sort
  boolSort = fTyconSort boolFTyCon
  charSort = fTyconSort charFTyCon
  strSort  = fTyconSort strFTyCon
  intSort  = fTyconSort intFTyCon
  realSort = fTyconSort realFTyCon
  funcSort = fTyconSort funcFTyCon
  
  setSort :: Sort -> Sort
  setSort = FApp (FTC setFTyCon)
  
  -- bitVecSort :: Sort -> Sort
  -- bitVecSort = FApp (FTC $ symbolFTycon' bitVecName)
  
  -- bitVec32Sort :: Sort
  -- bitVec32Sort = bitVecSort (FTC (symbolFTycon' size32Name))
  --
  -- bitVec64Sort :: Sort
  -- bitVec64Sort = bitVecSort (FTC (symbolFTycon' size64Name))
  
  bitVecSort :: Int -> Sort
  bitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FVar i)
  
  sizedBitVecSort :: Symbol -> Sort
  sizedBitVecSort i = FApp (FTC $ symbolFTycon' bitVecName) (FTC $ symbolFTycon' i)
  
  bagSort :: Sort -> Sort
  bagSort = FApp (FTC bagFTyCon)
  
  mapSort :: Sort -> Sort -> Sort
  mapSort = FApp . FApp (FTC (symbolFTycon' mapConName))
  
  arraySort :: Sort -> Sort -> Sort
  arraySort = FApp . FApp (FTC (symbolFTycon' arrayConName))
  
  symbolFTycon' :: Symbol -> FTycon
  symbolFTycon' = symbolFTycon . dummyLoc
  
  fTyconSort :: FTycon -> Sort
  fTyconSort c
    | c == intFTyCon  = FInt
    | c == realFTyCon = FReal
    | c == numFTyCon  = FNum
    | otherwise       = FTC c
  
  basicSorts :: [Sort]
  basicSorts = [FInt, boolSort]
  
  type SortSubst = M.HashMap Symbol Sort
  
  mkSortSubst :: [(Symbol, Sort)] -> SortSubst
  mkSortSubst = M.fromList
  
  ------------------------------------------------------------------------
  sortSubst                 :: SortSubst -> Sort -> Sort
  ------------------------------------------------------------------------
  sortSubst θ t@(FObj x)    = fromMaybe t (M.lookup x θ)
  sortSubst θ (FFunc t1 t2) = FFunc (sortSubst θ t1) (sortSubst θ t2)
  sortSubst θ (FApp t1 t2)  = FApp  (sortSubst θ t1) (sortSubst θ t2)
  sortSubst θ (FAbs i t)    = FAbs i (sortSubst θ t)
  sortSubst _  t            = t
  
  -- instance (S.Store a) => S.Store (TCEmb a)
  instance S.Store TCArgs
  instance S.Store FTycon
  instance S.Store TCInfo
  instance S.Store Sort
  instance S.Store DataField
  instance S.Store DataCtor
  instance S.Store DataDecl
  instance S.Store Sub
  
  -- | We need the Binary instances for LH's spec serialization
  instance B.Binary TCInfo
  instance B.Binary FTycon
  instance B.Binary Sort
  instance (Eq a, Hashable a, B.Binary (M.HashMap a (Sort, TCArgs))) => B.Binary (TCEmb a)
  
  instance NFData FTycon where
    rnf (TC x i) = x `seq` i `seq` ()
  
  instance (NFData a) => NFData (TCEmb a)
  instance NFData TCArgs
  instance NFData TCInfo
  instance NFData Sort
  instance NFData DataField
  instance NFData DataCtor
  instance NFData DataDecl
  instance NFData Sub
  
  -------------------------------------------------------------------------------
  -- | Embedding stuff as Sorts
  -------------------------------------------------------------------------------
  newtype TCEmb a = TCE (M.HashMap a (Sort, TCArgs))
    deriving (Eq, Show, Data, Typeable, Generic)
  
  instance Hashable a => Hashable (TCEmb a)
  instance PPrint a => PPrint (TCEmb a) where
    pprintTidy k = pprintTidy k . tceToList
  
  
  data TCArgs = WithArgs | NoArgs
    deriving (Eq, Ord, Show, Data, Typeable, Generic)
  
  instance Hashable TCArgs
  instance B.Binary TCArgs
  
  tceInsertWith :: (Eq a, Hashable a) => (Sort -> Sort -> Sort) -> a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
  tceInsertWith f k t a (TCE m) = TCE (M.insertWith ff k (t, a) m)
    where
      ff (t1, a1) (t2, a2)      = (f t1 t2, a1 <> a2)
  
  instance Semigroup TCArgs where
    NoArgs <> NoArgs = NoArgs
    _      <> _      = WithArgs
  
  instance Monoid TCArgs where
    mempty = NoArgs
    mappend = (<>)
  
  instance PPrint TCArgs where
    pprintTidy _ WithArgs = "*"
    pprintTidy _ NoArgs   = ""
  
  tceInsert :: (Eq a, Hashable a) => a -> Sort -> TCArgs -> TCEmb a -> TCEmb a
  tceInsert k t a (TCE m) = TCE (M.insert k (t, a) m)
  
  tceLookup :: (Eq a, Hashable a) => a -> TCEmb a -> Maybe (Sort, TCArgs)
  tceLookup k (TCE m) = M.lookup k m
  
  instance (Eq a, Hashable a) => Semigroup (TCEmb a) where
    (TCE m1) <> (TCE m2) = TCE (m1 <> m2)
  
  instance (Eq a, Hashable a) => Monoid (TCEmb a) where
    mempty  = TCE mempty
    mappend = (<>)
  
  
  tceMap :: (Eq b, Hashable b) => (a -> b) -> TCEmb a -> TCEmb b
  tceMap f = tceFromList . fmap (first f) . tceToList
  
  tceFromList :: (Eq a, Hashable a) => [(a, (Sort, TCArgs))] -> TCEmb a
  tceFromList = TCE . M.fromList
  
  tceToList :: TCEmb a -> [(a, (Sort, TCArgs))]
  tceToList (TCE m) = M.toList m
  
  tceMember :: (Eq a, Hashable a) => a -> TCEmb a -> Bool
  tceMember k (TCE m) = M.member k m
  
  -------------------------------------------------------------------------------
  -- | Sort coercion for SMT theory encoding
  -------------------------------------------------------------------------------
  
  coerceMapToArray :: Sort -> Sort
  coerceMapToArray (FFunc sf sa) = FFunc (coerceMapToArray sf) (coerceMapToArray sa)
  coerceMapToArray (FAbs i sa)   = FAbs i (coerceMapToArray sa)
  coerceMapToArray (FApp (FApp sf sa) sb)
    | isMap sf = arraySort (coerceMapToArray sa) (coerceMapToArray sb)
    | otherwise = FApp (FApp (coerceMapToArray sf) (coerceMapToArray sa)) (coerceMapToArray sb)
  coerceMapToArray (FApp sf sa) = FApp (coerceMapToArray sf) (coerceMapToArray sa)
  coerceMapToArray s = s
  
  coerceSetBagToArray :: Sort -> Sort
  coerceSetBagToArray (FFunc sf sa) = FFunc (coerceSetBagToArray sf) (coerceSetBagToArray sa)
  coerceSetBagToArray (FAbs i sa)   = FAbs i (coerceSetBagToArray sa)
  coerceSetBagToArray (FApp sf sa)
    | isSet sf = arraySort (coerceSetBagToArray sa) boolSort
    | isBag sf = arraySort (coerceSetBagToArray sa) intSort
    | otherwise = FApp (coerceSetBagToArray sf) (coerceSetBagToArray sa)
  coerceSetBagToArray s = s
  
  coerceDataField :: ElabFlags -> DataField -> DataField
  coerceDataField ef (DField x t)  = DField x (((if elabSetBag ef then coerceSetBagToArray else id) . coerceMapToArray) t)
  
  coerceDataCtor :: ElabFlags -> DataCtor -> DataCtor
  coerceDataCtor ef (DCtor x flds) = DCtor x (coerceDataField ef <$> flds)
  
  coerceDataDecl :: ElabFlags -> DataDecl -> DataDecl
  coerceDataDecl ef (DDecl tc n ctors) = DDecl tc n (coerceDataCtor ef <$> ctors)
  