{-# LANGUAGE CPP                        #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeSynonymInstances       #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE ViewPatterns               #-}
{-# LANGUAGE BangPatterns               #-}
{-# LANGUAGE PatternGuards              #-}


-- | This module contains Haskell variables representing globally visible names.
--   Rather than have strings floating around the system, all constant names
--   should be defined here, and the (exported) variables should be used and
--   manipulated elsewhere.

module Language.Fixpoint.Types.Names (

  -- * Symbols
    Symbol
  , Symbolic (..)
  , LocSymbol
  , LocText
  , symbolicString

  -- * Conversion to/from Text
  , symbolSafeText
  , symbolSafeString
  , symbolText
  , symbolString
  , symbolBuilder
  , buildMany

  -- Predicates
  , isPrefixOfSym
  , isSuffixOfSym
  , isNonSymbol
  , isLitSymbol
  , isTestSymbol
  -- , isCtorSymbol
  , isNontrivialVV
  , isDummy

  -- * Destructors
  , stripPrefix
  , stripSuffix 
  , consSym
  , unconsSym
  , dropSym
  , headSym
  , lengthSym

  -- * Transforms
  , nonSymbol
  , vvCon
  , tidySymbol

  -- * Widely used prefixes
  , anfPrefix
  , tempPrefix
  , vv
  , symChars

  -- * Creating Symbols
  , dummySymbol
  , intSymbol
  , tempSymbol
  , gradIntSymbol

  -- * Wrapping Symbols
  , litSymbol
  , testSymbol
  , renameSymbol
  , kArgSymbol
  , existSymbol
  , suffixSymbol
  , mappendSym 

  -- * Unwrapping Symbols
  , unLitSymbol

  -- * Hardwired global names
  , dummyName
  , preludeName
  , boolConName
  , funConName
  , listConName
  , listLConName
  , tupConName
  , setConName
  , mapConName
  , strConName
  , charConName
  , nilName
  , consName
  , vvName
  , size32Name
  , size64Name
  , bitVecName
  , bvAndName
  , bvOrName
  , propConName
  -- HKT , tyAppName
  , isPrim
  , prims
  , mulFuncName
  , divFuncName

  -- * Casting function names
  , setToIntName, bitVecToIntName, mapToIntName, boolToIntName, realToIntName, toIntName
  , setApplyName, bitVecApplyName, mapApplyName, boolApplyName, realApplyName, intApplyName
  , applyName
  , coerceName

  , lambdaName
  , lamArgSymbol
  , isLamArgSymbol

) where

import           Control.DeepSeq             (NFData (..))
import           Control.Arrow               (second)
import           Data.Char                   (ord)
import           Data.Maybe                  (fromMaybe)
#if !MIN_VERSION_base(4,14,0)
import           Data.Monoid                 ((<>))
#endif
import           Data.Generics               (Data)
import           Data.Hashable               (Hashable (..))
import qualified Data.HashSet                as S
import           Data.Interned
import           Data.Interned.Internal.Text
import           Data.String                 (IsString(..))
import qualified Data.Text                   as T
import qualified Data.Text.Lazy.Builder      as Builder
import           Data.Binary                 (Binary (..))
import           Data.Typeable               (Typeable)
import           GHC.Generics                (Generic)
import           Text.PrettyPrint.HughesPJ   (text)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans

---------------------------------------------------------------
-- | Symbols --------------------------------------------------
---------------------------------------------------------------

deriving instance Data     InternedText
deriving instance Typeable InternedText
deriving instance Generic  InternedText

{- type SafeText = {v: T.Text | IsSafe v} @-}
type SafeText = T.Text

-- | Invariant: a `SafeText` is made up of:
--
--     ['0'..'9'] ++ ['a'...'z'] ++ ['A'..'Z'] ++ '$'
--
--   If the original text has ANY other chars, it is represented as:
--
--     lq$i
--
--   where i is a unique integer (for each text)

data Symbol
  = S { Symbol -> Int
_symbolId      :: !Id
      , Symbol -> Text
symbolRaw     :: !T.Text
      , Symbol -> Text
symbolEncoded :: !T.Text
      } deriving (Typeable Symbol
DataType
Constr
Typeable Symbol
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> Symbol -> c Symbol)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c Symbol)
-> (Symbol -> Constr)
-> (Symbol -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c Symbol))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol))
-> ((forall b. Data b => b -> b) -> Symbol -> Symbol)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> Symbol -> r)
-> (forall u. (forall d. Data d => d -> u) -> Symbol -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Symbol -> m Symbol)
-> Data Symbol
Symbol -> DataType
Symbol -> Constr
(forall b. Data b => b -> b) -> Symbol -> Symbol
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall a.
Typeable a
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cS :: Constr
$tSymbol :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapMp :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapM :: (forall d. Data d => d -> m d) -> Symbol -> m Symbol
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Symbol -> m Symbol
gmapQi :: Int -> (forall d. Data d => d -> u) -> Symbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
gmapQ :: (forall d. Data d => d -> u) -> Symbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Symbol -> r
gmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
$cgmapT :: (forall b. Data b => b -> b) -> Symbol -> Symbol
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Symbol)
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c Symbol)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c Symbol)
dataTypeOf :: Symbol -> DataType
$cdataTypeOf :: Symbol -> DataType
toConstr :: Symbol -> Constr
$ctoConstr :: Symbol -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c Symbol
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Symbol -> c Symbol
$cp1Data :: Typeable Symbol
Data, Typeable, (forall x. Symbol -> Rep Symbol x)
-> (forall x. Rep Symbol x -> Symbol) -> Generic Symbol
forall x. Rep Symbol x -> Symbol
forall x. Symbol -> Rep Symbol x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Symbol x -> Symbol
$cfrom :: forall x. Symbol -> Rep Symbol x
Generic)

instance Eq Symbol where
  S Int
i Text
_ Text
_ == :: Symbol -> Symbol -> Bool
== S Int
j Text
_ Text
_ = Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
j

instance Ord Symbol where
  -- compare (S i _ _) (S j _ _) = compare i j
  -- compare s1 s2 = compare (symbolString s1) (symbolString s2)
  compare :: Symbol -> Symbol -> Ordering
compare Symbol
s1 Symbol
s2 = Text -> Text -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Symbol -> Text
symbolText Symbol
s1) (Symbol -> Text
symbolText Symbol
s2)

instance Interned Symbol where
  type Uninterned Symbol = T.Text
  newtype Description Symbol = DT T.Text deriving (Description Symbol -> Description Symbol -> Bool
(Description Symbol -> Description Symbol -> Bool)
-> (Description Symbol -> Description Symbol -> Bool)
-> Eq (Description Symbol)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Description Symbol -> Description Symbol -> Bool
$c/= :: Description Symbol -> Description Symbol -> Bool
== :: Description Symbol -> Description Symbol -> Bool
$c== :: Description Symbol -> Description Symbol -> Bool
Eq)
  describe :: Uninterned Symbol -> Description Symbol
describe     = Text -> Description Symbol
Uninterned Symbol -> Description Symbol
DT
  identify :: Int -> Uninterned Symbol -> Symbol
identify Int
i Uninterned Symbol
t = Int -> Text -> Text -> Symbol
S Int
i Text
Uninterned Symbol
t (Text -> Text
encode Text
Uninterned Symbol
t)
  cache :: Cache Symbol
cache        = Cache Symbol
sCache

instance Uninternable Symbol where
  unintern :: Symbol -> Uninterned Symbol
unintern (S Int
_ Text
t Text
_) = Text
Uninterned Symbol
t

instance Hashable (Description Symbol) where
  hashWithSalt :: Int -> Description Symbol -> Int
hashWithSalt Int
s (DT t) = Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Text
t

instance Hashable Symbol where
  -- NOTE: hash based on original text rather than id
  hashWithSalt :: Int -> Symbol -> Int
hashWithSalt Int
s (S Int
_ Text
t Text
_) = Int -> Text -> Int
forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Text
t

instance NFData Symbol where
  rnf :: Symbol -> ()
rnf (S {}) = ()

instance Binary Symbol where
  get :: Get Symbol
get = Text -> Symbol
textSymbol (Text -> Symbol) -> Get Text -> Get Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Text
forall t. Binary t => Get t
get
  put :: Symbol -> Put
put = Text -> Put
forall t. Binary t => t -> Put
put (Text -> Put) -> (Symbol -> Text) -> Symbol -> Put
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

sCache :: Cache Symbol
sCache :: Cache Symbol
sCache = Cache Symbol
forall t. Interned t => Cache t
mkCache
{-# NOINLINE sCache #-}

instance IsString Symbol where
  fromString :: String -> Symbol
fromString = Text -> Symbol
textSymbol (Text -> Symbol) -> (String -> Text) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

instance Show Symbol where
  show :: Symbol -> String
show = Text -> String
forall a. Show a => a -> String
show (Text -> String) -> (Symbol -> Text) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolRaw

mappendSym :: Symbol -> Symbol -> Symbol
mappendSym :: Symbol -> Symbol -> Symbol
mappendSym Symbol
s1 Symbol
s2 = Text -> Symbol
textSymbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
forall a. Monoid a => a -> a -> a
mappend Text
s1' Text
s2'
    where
      s1' :: Text
s1'        = Symbol -> Text
symbolText Symbol
s1
      s2' :: Text
s2'        = Symbol -> Text
symbolText Symbol
s2

instance PPrint Symbol where
  pprintTidy :: Tidy -> Symbol -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (Symbol -> String) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> String
symbolString

instance Fixpoint T.Text where
  toFix :: Text -> Doc
toFix = String -> Doc
text (String -> Doc) -> (Text -> String) -> Text -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
T.unpack

{- | [NOTE: SymbolText]
	Use `symbolSafeText` if you want it to machine-readable,
        but `symbolText`     if you want it to be human-readable.
 -}

instance Fixpoint Symbol where
  toFix :: Symbol -> Doc
toFix = Text -> Doc
forall a. Fixpoint a => a -> Doc
toFix (Text -> Doc) -> (Symbol -> Text) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
checkedText -- symbolSafeText

checkedText :: Symbol -> T.Text
checkedText :: Symbol -> Text
checkedText Symbol
x
  | Just (Char
c, Text
t') <- Text -> Maybe (Char, Text)
T.uncons Text
t
  , Char -> Bool
okHd Char
c Bool -> Bool -> Bool
&& (Char -> Bool) -> Text -> Bool
T.all Char -> Bool
okChr Text
t'   = Text
t
  | Bool
otherwise                  = Symbol -> Text
symbolSafeText Symbol
x
  where
    t :: Text
t     = Symbol -> Text
symbolText Symbol
x
    okHd :: Char -> Bool
okHd  = (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
alphaChars)
    okChr :: Char -> Bool
okChr = (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
symChars)

---------------------------------------------------------------------------
-- | Located Symbols -----------------------------------------------------
---------------------------------------------------------------------------

type LocSymbol = Located Symbol
type LocText   = Located T.Text

isDummy :: (Symbolic a) => a -> Bool
isDummy :: a -> Bool
isDummy a
a = Symbol -> Symbol -> Bool
isPrefixOfSym (Symbol -> Symbol
forall a. Symbolic a => a -> Symbol
symbol Symbol
dummyName) (a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol a
a)

instance Symbolic a => Symbolic (Located a) where
  symbol :: Located a -> Symbol
symbol = a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (a -> Symbol) -> (Located a -> a) -> Located a -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Located a -> a
forall a. Located a -> a
val

---------------------------------------------------------------------------
-- | Decoding Symbols -----------------------------------------------------
---------------------------------------------------------------------------

symbolText :: Symbol -> T.Text
symbolText :: Symbol -> Text
symbolText = Symbol -> Text
symbolRaw

symbolString :: Symbol -> String
symbolString :: Symbol -> String
symbolString = Text -> String
T.unpack (Text -> String) -> (Symbol -> Text) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

symbolSafeText :: Symbol -> SafeText
symbolSafeText :: Symbol -> Text
symbolSafeText = Symbol -> Text
symbolEncoded

symbolSafeString :: Symbol -> String
symbolSafeString :: Symbol -> String
symbolSafeString = Text -> String
T.unpack (Text -> String) -> (Symbol -> Text) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolSafeText

---------------------------------------------------------------------------
-- | Encoding Symbols -----------------------------------------------------
---------------------------------------------------------------------------

-- INVARIANT: All strings *must* be built from here

textSymbol :: T.Text -> Symbol
textSymbol :: Text -> Symbol
textSymbol = Text -> Symbol
forall t. Interned t => Uninterned t -> t
intern

encode :: T.Text -> SafeText
encode :: Text -> Text
encode Text
t
  | Text -> Bool
isFixKey Text
t     = Text -> Text -> Text
T.append Text
"key$" Text
t
  | Bool
otherwise      = Text -> Text
encodeUnsafe Text
t

isFixKey :: T.Text -> Bool
isFixKey :: Text -> Bool
isFixKey Text
x = Text -> HashSet Text -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Text
x HashSet Text
keywords

encodeUnsafe :: T.Text -> T.Text
encodeUnsafe :: Text -> Text
encodeUnsafe = (Text, [(Char, Text)]) -> Text
joinChunks ((Text, [(Char, Text)]) -> Text)
-> (Text -> (Text, [(Char, Text)])) -> Text -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> (Text, [(Char, Text)])
splitChunks (Text -> (Text, [(Char, Text)]))
-> (Text -> Text) -> Text -> (Text, [(Char, Text)])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text
prefixAlpha

prefixAlpha :: T.Text -> T.Text
prefixAlpha :: Text -> Text
prefixAlpha Text
t
  | Text -> Bool
isAlpha0 Text
t = Text
t
  | Bool
otherwise  = Text -> Text -> Text
T.append Text
"fix$" Text
t

isAlpha0 :: T.Text -> Bool
isAlpha0 :: Text -> Bool
isAlpha0 Text
t = case Text -> Maybe (Char, Text)
T.uncons Text
t of
               Just (Char
c, Text
_) -> Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Char
c HashSet Char
alphaChars
               Maybe (Char, Text)
Nothing     -> Bool
False

joinChunks :: (T.Text, [(Char, SafeText)]) -> SafeText
joinChunks :: (Text, [(Char, Text)]) -> Text
joinChunks (Text
t, [] ) = Text
t
joinChunks (Text
t, [(Char, Text)]
cts) = [Text] -> Text
T.concat ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text
padNull Text
t Text -> [Text] -> [Text]
forall a. a -> [a] -> [a]
: ((Char, Text) -> Text
tx ((Char, Text) -> Text) -> [(Char, Text)] -> [Text]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Char, Text)]
cts)
  where
    tx :: (Char, Text) -> Text
tx (Char
c, Text
ct)      = [Text] -> Text
forall a. Monoid a => [a] -> a
mconcat [Text
"$", Char -> Text
c2t Char
c, Text
"$", Text
ct]
    c2t :: Char -> Text
c2t             = String -> Text
T.pack (String -> Text) -> (Char -> String) -> Char -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show (Int -> String) -> (Char -> Int) -> Char -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Int
ord

padNull :: T.Text -> T.Text
padNull :: Text -> Text
padNull Text
t
  | Text -> Bool
T.null Text
t  = Text
"z$"
  | Bool
otherwise = Text
t

splitChunks :: T.Text -> (T.Text, [(Char, SafeText)])
splitChunks :: Text -> (Text, [(Char, Text)])
splitChunks Text
t = (Text
h, Text -> [(Char, Text)]
go Text
tl)
  where
    (Text
h, Text
tl)   = (Char -> Bool) -> Text -> (Text, Text)
T.break Char -> Bool
isUnsafeChar Text
t
    go :: Text -> [(Char, Text)]
go !Text
ut    = case Text -> Maybe (Char, Text)
T.uncons Text
ut of
                  Maybe (Char, Text)
Nothing       -> []
                  Just (Char
c, Text
ut') -> let (Text
ct, Text
utl) = (Char -> Bool) -> Text -> (Text, Text)
T.break Char -> Bool
isUnsafeChar Text
ut'
                                   in (Char
c, Text
ct) (Char, Text) -> [(Char, Text)] -> [(Char, Text)]
forall a. a -> [a] -> [a]
: Text -> [(Char, Text)]
go Text
utl

isUnsafeChar :: Char -> Bool
isUnsafeChar :: Char -> Bool
isUnsafeChar = Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> HashSet Char -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
okSymChars)


keywords :: S.HashSet T.Text
keywords :: HashSet Text
keywords   = [Text] -> HashSet Text
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [ Text
"env"
                        , Text
"id"
                        , Text
"tag"
                        , Text
"qualif"
                        , Text
"constant"
                        , Text
"cut"
                        , Text
"bind"
                        , Text
"constraint"
                        , Text
"lhs"
                        , Text
"rhs"
                        , Text
"NaN"
                        , Text
"min"
                        , Text
"map"
                        ]

-- | RJ: We allow the extra 'unsafeChars' to allow parsing encoded symbols.
--   e.g. the raw string "This#is%$inval!d" may get encoded as "enc%12"
--   and serialized as such in the fq/bfq file. We want to allow the parser
--   to then be able to read the above back in.

alphaChars :: S.HashSet Char
alphaChars :: HashSet Char
alphaChars = String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList (String -> HashSet Char) -> String -> HashSet Char
forall a b. (a -> b) -> a -> b
$ [Char
'a' .. Char
'z'] String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char
'A' .. Char
'Z']

numChars :: S.HashSet Char
numChars :: HashSet Char
numChars = String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Char
'0' .. Char
'9']

safeChars :: S.HashSet Char
safeChars :: HashSet Char
safeChars = HashSet Char
alphaChars HashSet Char -> HashSet Char -> HashSet Char
forall a. Monoid a => a -> a -> a
`mappend`
            HashSet Char
numChars   HashSet Char -> HashSet Char -> HashSet Char
forall a. Monoid a => a -> a -> a
`mappend`
            String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Char
'_', Char
'.']

symChars :: S.HashSet Char
symChars :: HashSet Char
symChars =  HashSet Char
safeChars HashSet Char -> HashSet Char -> HashSet Char
forall a. Monoid a => a -> a -> a
`mappend`
            String -> HashSet Char
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Char
'%', Char
'#', Char
'$', Char
'\'']

okSymChars :: S.HashSet Char
okSymChars :: HashSet Char
okSymChars = HashSet Char
safeChars

isPrefixOfSym :: Symbol -> Symbol -> Bool
isPrefixOfSym :: Symbol -> Symbol -> Bool
isPrefixOfSym (Symbol -> Text
symbolText -> Text
p) (Symbol -> Text
symbolText -> Text
x) = Text
p Text -> Text -> Bool
`T.isPrefixOf` Text
x

isSuffixOfSym :: Symbol -> Symbol -> Bool
isSuffixOfSym :: Symbol -> Symbol -> Bool
isSuffixOfSym (Symbol -> Text
symbolText -> Text
p) (Symbol -> Text
symbolText -> Text
x) = Text
p Text -> Text -> Bool
`T.isSuffixOf` Text
x


headSym :: Symbol -> Char
headSym :: Symbol -> Char
headSym (Symbol -> Text
symbolText -> Text
t) = Text -> Char
T.head Text
t

consSym :: Char -> Symbol -> Symbol
consSym :: Char -> Symbol -> Symbol
consSym Char
c (Symbol -> Text
symbolText -> Text
s) = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Char -> Text -> Text
T.cons Char
c Text
s

unconsSym :: Symbol -> Maybe (Char, Symbol)
unconsSym :: Symbol -> Maybe (Char, Symbol)
unconsSym (Symbol -> Text
symbolText -> Text
s) = (Text -> Symbol) -> (Char, Text) -> (Char, Symbol)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol ((Char, Text) -> (Char, Symbol))
-> Maybe (Char, Text) -> Maybe (Char, Symbol)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Maybe (Char, Text)
T.uncons Text
s

-- singletonSym :: Char -> Symbol -- Yuck
-- singletonSym = (`consSym` "")

lengthSym :: Symbol -> Int
lengthSym :: Symbol -> Int
lengthSym (Symbol -> Text
symbolText -> Text
t) = Text -> Int
T.length Text
t

dropSym :: Int -> Symbol -> Symbol
dropSym :: Int -> Symbol -> Symbol
dropSym Int
n (Symbol -> Text
symbolText -> Text
t) = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
T.drop Int
n Text
t

stripPrefix :: Symbol -> Symbol -> Maybe Symbol
stripPrefix :: Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
p Symbol
x = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Maybe Text -> Maybe Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Text -> Maybe Text
T.stripPrefix (Symbol -> Text
symbolText Symbol
p) (Symbol -> Text
symbolText Symbol
x)

stripSuffix :: Symbol -> Symbol -> Maybe Symbol
stripSuffix :: Symbol -> Symbol -> Maybe Symbol
stripSuffix Symbol
p Symbol
x = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Maybe Text -> Maybe Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Text -> Text -> Maybe Text
T.stripSuffix (Symbol -> Text
symbolText Symbol
p) (Symbol -> Text
symbolText Symbol
x)


--------------------------------------------------------------------------------
-- | Use this **EXCLUSIVELY** when you want to add stuff in front of a Symbol
--------------------------------------------------------------------------------
suffixSymbol :: Symbol -> Symbol -> Symbol
suffixSymbol :: Symbol -> Symbol -> Symbol
suffixSymbol  Symbol
x Symbol
y = Symbol
x Symbol -> Symbol -> Symbol
`mappendSym` Symbol
forall a. IsString a => a
symSepName Symbol -> Symbol -> Symbol
`mappendSym` Symbol
y

vv                  :: Maybe Integer -> Symbol
-- vv (Just i)         = symbol $ symbolSafeText vvName `T.snoc` symSepName `mappend` T.pack (show i)
vv :: Maybe Integer -> Symbol
vv (Just Integer
i)         = Symbol -> Integer -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
vvName Integer
i
vv Maybe Integer
Nothing          = Symbol
vvName

isNontrivialVV      :: Symbol -> Bool
isNontrivialVV :: Symbol -> Bool
isNontrivialVV      = Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Integer -> Symbol
vv Maybe Integer
forall a. Maybe a
Nothing Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
==)

vvCon, dummySymbol :: Symbol
vvCon :: Symbol
vvCon       = Symbol
vvName Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol
"F"
dummySymbol :: Symbol
dummySymbol = Symbol
dummyName

-- ctorSymbol :: Symbol -> Symbol
-- ctorSymbol s = ctorPrefix `mappendSym` s

-- isCtorSymbol :: Symbol -> Bool
-- isCtorSymbol = isPrefixOfSym ctorPrefix

-- | 'testSymbol c' creates the `is-c` symbol for the adt-constructor named 'c'.
testSymbol :: Symbol -> Symbol
testSymbol :: Symbol -> Symbol
testSymbol Symbol
s = Symbol
testPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
s

isTestSymbol :: Symbol -> Bool
isTestSymbol :: Symbol -> Bool
isTestSymbol = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
testPrefix

litSymbol :: Symbol -> Symbol
litSymbol :: Symbol -> Symbol
litSymbol Symbol
s = Symbol
litPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
s

isLitSymbol :: Symbol -> Bool
isLitSymbol :: Symbol -> Bool
isLitSymbol = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
litPrefix

unLitSymbol :: Symbol -> Maybe Symbol
unLitSymbol :: Symbol -> Maybe Symbol
unLitSymbol = Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
litPrefix

intSymbol :: (Show a) => Symbol -> a -> Symbol
intSymbol :: Symbol -> a -> Symbol
intSymbol Symbol
x a
i = Symbol
x Symbol -> Symbol -> Symbol
`suffixSymbol` String -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (a -> String
forall a. Show a => a -> String
show a
i)

tempSymbol :: Symbol -> Integer -> Symbol
tempSymbol :: Symbol -> Integer -> Symbol
tempSymbol Symbol
prefix = Symbol -> Integer -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (Symbol
tempPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
prefix)

renameSymbol :: Symbol -> Int -> Symbol
renameSymbol :: Symbol -> Int -> Symbol
renameSymbol Symbol
prefix = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (Symbol
renamePrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
prefix)

kArgSymbol :: Symbol -> Symbol -> Symbol
kArgSymbol :: Symbol -> Symbol -> Symbol
kArgSymbol Symbol
x Symbol
k = (Symbol
kArgPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
x) Symbol -> Symbol -> Symbol
`suffixSymbol` Symbol
k

existSymbol :: Symbol -> Integer -> Symbol
existSymbol :: Symbol -> Integer -> Symbol
existSymbol Symbol
prefix = Symbol -> Integer -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol (Symbol
existPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
prefix)

gradIntSymbol :: Integer -> Symbol
gradIntSymbol :: Integer -> Symbol
gradIntSymbol = Symbol -> Integer -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
gradPrefix

tempPrefix, anfPrefix, renamePrefix, litPrefix, gradPrefix :: Symbol
tempPrefix :: Symbol
tempPrefix   = Symbol
"lq_tmp$"
anfPrefix :: Symbol
anfPrefix    = Symbol
"lq_anf$"
renamePrefix :: Symbol
renamePrefix = Symbol
"lq_rnm$"
litPrefix :: Symbol
litPrefix    = Symbol
"lit$"
gradPrefix :: Symbol
gradPrefix   = Symbol
"grad$"

testPrefix  :: Symbol
testPrefix :: Symbol
testPrefix   = Symbol
"is$"

-- ctorPrefix  :: Symbol
-- ctorPrefix   = "mk$"

kArgPrefix, existPrefix :: Symbol
kArgPrefix :: Symbol
kArgPrefix   = Symbol
"lq_karg$"
existPrefix :: Symbol
existPrefix  = Symbol
"lq_ext$"

-------------------------------------------------------------------------
tidySymbol :: Symbol -> Symbol
-------------------------------------------------------------------------
tidySymbol :: Symbol -> Symbol
tidySymbol = Symbol -> Symbol
unSuffixSymbol (Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
unSuffixSymbol (Symbol -> Symbol) -> (Symbol -> Symbol) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol -> Symbol
unPrefixSymbol Symbol
kArgPrefix

unPrefixSymbol :: Symbol -> Symbol -> Symbol
unPrefixSymbol :: Symbol -> Symbol -> Symbol
unPrefixSymbol Symbol
p Symbol
s = Symbol -> Maybe Symbol -> Symbol
forall a. a -> Maybe a -> a
fromMaybe Symbol
s (Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
p Symbol
s)

unSuffixSymbol :: Symbol -> Symbol
unSuffixSymbol :: Symbol -> Symbol
unSuffixSymbol s :: Symbol
s@(Symbol -> Text
symbolText -> Text
t)
  = Symbol -> (Text -> Symbol) -> Maybe Text -> Symbol
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Symbol
s Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Maybe Text -> Symbol) -> Maybe Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Text -> Text -> Maybe Text
T.stripSuffix Text
forall a. IsString a => a
symSepName (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$ (Text, Text) -> Text
forall a b. (a, b) -> a
fst ((Text, Text) -> Text) -> (Text, Text) -> Text
forall a b. (a -> b) -> a -> b
$ Text -> Text -> (Text, Text)
T.breakOnEnd Text
forall a. IsString a => a
symSepName Text
t

-- takeWhileSym :: (Char -> Bool) -> Symbol -> Symbol
-- takeWhileSym p (symbolText -> t) = symbol $ T.takeWhile p t


nonSymbol :: Symbol
nonSymbol :: Symbol
nonSymbol = Symbol
""

isNonSymbol :: Symbol -> Bool
isNonSymbol :: Symbol -> Bool
isNonSymbol = (Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
nonSymbol)

------------------------------------------------------------------------------
-- | Values that can be viewed as Symbols
------------------------------------------------------------------------------

class Symbolic a where
  symbol :: a -> Symbol

symbolicString :: (Symbolic a) => a -> String
symbolicString :: a -> String
symbolicString = Symbol -> String
symbolString (Symbol -> String) -> (a -> Symbol) -> a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol

instance Symbolic T.Text where
  symbol :: Text -> Symbol
symbol = Text -> Symbol
textSymbol

instance Symbolic String where
  symbol :: String -> Symbol
symbol = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> (String -> Text) -> String -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

instance Symbolic Symbol where
  symbol :: Symbol -> Symbol
symbol = Symbol -> Symbol
forall a. a -> a
id

symbolBuilder :: (Symbolic a) => a -> Builder.Builder
symbolBuilder :: a -> Builder
symbolBuilder = Text -> Builder
Builder.fromText (Text -> Builder) -> (a -> Text) -> a -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolSafeText (Symbol -> Text) -> (a -> Symbol) -> a -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Symbol
forall a. Symbolic a => a -> Symbol
symbol

{-# INLINE buildMany #-}
buildMany :: [Builder.Builder] -> Builder.Builder
buildMany :: [Builder] -> Builder
buildMany []     = Builder
forall a. Monoid a => a
mempty
buildMany [Builder
b]    = Builder
b
buildMany (Builder
b:[Builder]
bs) = Builder
b Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> [Builder] -> Builder
forall a. Monoid a => [a] -> a
mconcat [ Builder
" " Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> Builder
b | Builder
b <- [Builder]
bs ]

----------------------------------------------------------------------------
--------------- Global Name Definitions ------------------------------------
----------------------------------------------------------------------------

lambdaName :: Symbol
lambdaName :: Symbol
lambdaName = Symbol
"smt_lambda"

lamArgPrefix :: Symbol
lamArgPrefix :: Symbol
lamArgPrefix = Symbol
"lam_arg"

lamArgSymbol :: Int -> Symbol
lamArgSymbol :: Int -> Symbol
lamArgSymbol = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
lamArgPrefix

isLamArgSymbol :: Symbol -> Bool
isLamArgSymbol :: Symbol -> Bool
isLamArgSymbol = Symbol -> Symbol -> Bool
isPrefixOfSym Symbol
lamArgPrefix

setToIntName, bitVecToIntName, mapToIntName, realToIntName, toIntName :: Symbol
setToIntName :: Symbol
setToIntName    = Symbol
"set_to_int"
bitVecToIntName :: Symbol
bitVecToIntName = Symbol
"bitvec_to_int"
mapToIntName :: Symbol
mapToIntName    = Symbol
"map_to_int"
realToIntName :: Symbol
realToIntName   = Symbol
"real_to_int"
toIntName :: Symbol
toIntName       = Symbol
"cast_as_int"

boolToIntName :: (IsString a) => a
boolToIntName :: a
boolToIntName   = a
"bool_to_int"

setApplyName, bitVecApplyName, mapApplyName, boolApplyName, realApplyName, intApplyName :: Int -> Symbol
setApplyName :: Int -> Symbol
setApplyName    = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"set_apply_"
bitVecApplyName :: Int -> Symbol
bitVecApplyName = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"bitvec_apply"
mapApplyName :: Int -> Symbol
mapApplyName    = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"map_apply_"
boolApplyName :: Int -> Symbol
boolApplyName   = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"bool_apply_"
realApplyName :: Int -> Symbol
realApplyName   = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"real_apply_"
intApplyName :: Int -> Symbol
intApplyName    = Symbol -> Int -> Symbol
forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"int_apply_"

applyName :: Symbol
applyName :: Symbol
applyName = Symbol
"apply"

coerceName :: Symbol
coerceName :: Symbol
coerceName = Symbol
"coerce"

preludeName, dummyName, boolConName, funConName :: Symbol
preludeName :: Symbol
preludeName  = Symbol
"Prelude"
dummyName :: Symbol
dummyName    = Symbol
"LIQUID$dummy"
boolConName :: Symbol
boolConName  = Symbol
"Bool"
funConName :: Symbol
funConName   = Symbol
"->"


listConName, listLConName, tupConName, propConName, _hpropConName, vvName, setConName, mapConName :: Symbol
listConName :: Symbol
listConName  = Symbol
"[]"
listLConName :: Symbol
listLConName = Symbol
"List"
tupConName :: Symbol
tupConName   = Symbol
"Tuple"
setConName :: Symbol
setConName   = Symbol
"Set_Set"
mapConName :: Symbol
mapConName   = Symbol
"Map_t"
vvName :: Symbol
vvName       = Symbol
"VV"
propConName :: Symbol
propConName  = Symbol
"Prop"
_hpropConName :: Symbol
_hpropConName = Symbol
"HProp"

strConName, charConName :: (IsString a) => a
strConName :: a
strConName   = a
"Str"
charConName :: a
charConName  = a
"Char"
-- symSepName   :: Char
-- symSepName   = '#' -- DO NOT EVER CHANGE THIS

symSepName   :: (IsString a) => a
symSepName :: a
symSepName   = a
"##"

nilName, consName, size32Name, size64Name, bitVecName, bvOrName, bvAndName :: Symbol
nilName :: Symbol
nilName      = Symbol
"nil"
consName :: Symbol
consName     = Symbol
"cons"
size32Name :: Symbol
size32Name   = Symbol
"Size32"
size64Name :: Symbol
size64Name   = Symbol
"Size64"
bitVecName :: Symbol
bitVecName   = Symbol
"BitVec"
bvOrName :: Symbol
bvOrName     = Symbol
"bvor"
bvAndName :: Symbol
bvAndName    = Symbol
"bvand"

-- HKT tyAppName :: Symbol
-- HKT tyAppName    = "LF-App"

mulFuncName, divFuncName :: Symbol
mulFuncName :: Symbol
mulFuncName  = Symbol
"Z3_OP_MUL"
divFuncName :: Symbol
divFuncName  = Symbol
"Z3_OP_DIV"

isPrim :: Symbol -> Bool 
isPrim :: Symbol -> Bool
isPrim Symbol
x = Symbol -> HashSet Symbol -> Bool
forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Symbol
x HashSet Symbol
prims 

prims :: S.HashSet Symbol
prims :: HashSet Symbol
prims = [Symbol] -> HashSet Symbol
forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList 
  [ Symbol
propConName
  , Symbol
_hpropConName
  , Symbol
vvName
  , Symbol
"Pred"
  , Symbol
"List"
  , Symbol
"[]"
  , Symbol
"bool"
  -- , "int"
  -- , "real"
  , Symbol
setConName
  , Symbol
forall a. IsString a => a
charConName
  , Symbol
"Set_sng"
  , Symbol
"Set_cup"
  , Symbol
"Set_cap"
  , Symbol
"Set_dif"
  , Symbol
"Set_emp"
  , Symbol
"Set_empty"
  , Symbol
"Set_mem"
  , Symbol
"Set_sub"
  , Symbol
mapConName
  , Symbol
"Map_select"
  , Symbol
"Map_store"
  , Symbol
"Map_union"
  , Symbol
"Map_default"
  , Symbol
size32Name
  , Symbol
size64Name
  , Symbol
bitVecName
  , Symbol
bvOrName
  , Symbol
bvAndName
  , Symbol
"FAppTy"
  , Symbol
nilName
  , Symbol
consName
  ]

{-
-------------------------------------------------------------------------------
-- | Memoized Decoding
-------------------------------------------------------------------------------

{-# NOINLINE symbolMemo #-}
symbolMemo :: IORef (M.HashMap Int T.Text)
symbolMemo = unsafePerformIO (newIORef M.empty)

{-# NOINLINE memoEncode #-}
memoEncode :: T.Text -> Int
memoEncode t = unsafePerformIO $
                 atomicModifyIORef symbolMemo $ \m ->
                    (M.insert i t m, i)
  where
    i        = internedTextId $ intern t

{-# NOINLINE memoDecode #-}
memoDecode :: Int -> T.Text
memoDecode i = unsafePerformIO $
                 safeLookup msg i <$> readIORef symbolMemo
               where
                 msg = "Symbol Decode Error: " ++ show i

-}