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

{-# OPTIONS_GHC -Wno-orphans            #-}

-- | 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
  , isFixKey

  -- * Destructors
  , prefixOfSym
  , suffixOfSym
  , stripPrefix
  , stripSuffix
  , consSym
  , unconsSym
  , dropSym
  , dropPrefixOfSym
  , headSym
  , lengthSym

  -- * Transforms
  , nonSymbol
  , vvCon
  , tidySymbol

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

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

  -- * Wrapping Symbols
  , litSymbol
  , bindSymbol
  , 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, tyCastName
  , 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)
import           Data.Generics               (Data)
import           Data.Hashable               (Hashable (..))
import qualified Data.HashSet                as S hiding (size)
import           Data.Interned
import           Data.Interned.Internal.Text
import           Data.String                 (IsString(..))
import qualified Data.Text                   as T
import qualified Data.Store                  as S
import           Data.Typeable               (Typeable)
import qualified GHC.Arr                     as Arr
import           GHC.Generics                (Generic)
import           Text.PrettyPrint.HughesPJ   (text)
import           Language.Fixpoint.Types.PrettyPrint
import           Language.Fixpoint.Types.Spans
import           Language.Fixpoint.Utils.Builder as Builder (Builder, fromText)
import Data.Functor.Contravariant (Contravariant(contramap))
import qualified Data.Binary as B

---------------------------------------------------------------
-- | 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
Symbol -> DataType
Symbol -> Constr
(forall b. Data b => b -> b) -> Symbol -> 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)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
MonadPlus m =>
(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 (m :: * -> *).
Monad m =>
(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 :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Symbol -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> Symbol -> [u]
gmapQr :: forall r r'.
(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 :: forall r r'.
(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 (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(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 (t :: * -> *) (c :: * -> *).
Typeable t =>
(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 (c :: * -> *).
(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 (c :: * -> *).
(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
Data, Typeable, 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 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 = 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
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
DT
  identify :: Int -> Uninterned Symbol -> Symbol
identify Int
i Uninterned Symbol
t = Int -> Text -> Text -> Symbol
S Int
i Uninterned Symbol
t (Text -> Text
encode 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
t

instance Hashable (Description Symbol) where
  hashWithSalt :: Int -> Description Symbol -> Int
hashWithSalt Int
s (DT Text
t) = {-# SCC "hashWithSalt-Description-Symbol" #-} 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
_) = forall a. Hashable a => Int -> a -> Int
hashWithSalt Int
s Text
t

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

instance S.Store Symbol where
  poke :: Symbol -> Poke ()
poke = forall a. Store a => a -> Poke ()
S.poke forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText
  peek :: Peek Symbol
peek = Text -> Symbol
textSymbol forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Store a => Peek a
S.peek
  size :: Size Symbol
size = forall (f :: * -> *) a' a.
Contravariant f =>
(a' -> a) -> f a -> f a'
contramap Symbol -> Text
symbolText forall a. Store a => Size a
S.size

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

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

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

instance Show Symbol where
  show :: Symbol -> String
show = forall a. Show a => a -> String
show 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 forall a b. (a -> b) -> a -> b
$ 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 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 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 = forall a. Fixpoint a => a -> Doc
toFix 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  = (forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
`S.member` HashSet Char
alphaChars)
    okChr :: Char -> Bool
okChr = (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 :: forall a. Symbolic a => a -> Bool
isDummy a
a = Symbol -> Symbol -> Bool
isPrefixOfSym (forall a. Symbolic a => a -> Symbol
symbol Symbol
dummyName) (forall a. Symbolic a => a -> Symbol
symbol a
a)

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

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

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

{-# SCC symbolString #-}
symbolString :: Symbol -> String
symbolString :: Symbol -> String
symbolString = Text -> String
T.unpack 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolSafeText

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

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

{-# SCC textSymbol #-}
textSymbol :: T.Text -> Symbol
textSymbol :: Text -> Symbol
textSymbol = 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 = forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Text
x HashSet Text
keywords

{-# SCC encodeUnsafe #-}
encodeUnsafe :: T.Text -> T.Text
encodeUnsafe :: Text -> Text
encodeUnsafe Text
t = String -> Text
T.pack forall a b. (a -> b) -> a -> b
$ ShowS
pad forall a b. (a -> b) -> a -> b
$ ShowS
go forall a b. (a -> b) -> a -> b
$ Text -> String
T.unpack (Text -> Text
prefixAlpha Text
t)
  where
    pad :: ShowS
pad cs :: String
cs@(Char
'$':String
_) = Char
'z' forall a. a -> [a] -> [a]
: Char
'$' forall a. a -> [a] -> [a]
: String
cs
    pad String
cs = String
cs
    go :: ShowS
go [] = []
    go (Char
c:String
cs) =
      if Char -> Bool
isUnsafeChar Char
c then
        Char
'$' forall a. a -> [a] -> [a]
: forall a. Show a => a -> ShowS
shows (Char -> Int
ord Char
c) (Char
'$' forall a. a -> [a] -> [a]
: ShowS
go String
cs)
      else
        Char
c forall a. a -> [a] -> [a]
: ShowS
go String
cs

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
_) -> forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member Char
c HashSet Char
alphaChars
               Maybe (Char, Text)
Nothing     -> Bool
False

isUnsafeChar :: Char -> Bool
isUnsafeChar :: Char -> Bool
isUnsafeChar Char
c =
  let ic :: Int
ic = Char -> Int
ord Char
c
   in Int
ic forall a. Ord a => a -> a -> Bool
>= forall i e. Array i e -> Int
Arr.numElements Array Int Bool
okSymChars Bool -> Bool -> Bool
|| Bool -> Bool
not (Array Int Bool
okSymChars forall i e. Ix i => Array i e -> i -> e
Arr.! Int
ic)

keywords :: S.HashSet T.Text
keywords :: HashSet Text
keywords   = 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 = forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList forall a b. (a -> b) -> a -> b
$ [Char
'a' .. Char
'z'] forall a. [a] -> [a] -> [a]
++ [Char
'A' .. Char
'Z']

numChars :: S.HashSet Char
numChars :: HashSet Char
numChars = 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 forall a. Monoid a => a -> a -> a
`mappend`
            HashSet Char
numChars   forall a. Monoid a => a -> a -> a
`mappend`
            forall a. (Eq a, Hashable a) => [a] -> HashSet a
S.fromList [Char
'_', Char
'.']

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

okSymChars :: Arr.Array Int Bool
okSymChars :: Array Int Bool
okSymChars =
    forall i e. Ix i => (i, i) -> [e] -> Array i e
Arr.listArray (Int
0, Int
maxChar) [ forall a. (Eq a, Hashable a) => a -> HashSet a -> Bool
S.member (forall a. Enum a => Int -> a
toEnum Int
i) HashSet Char
safeChars | Int
i <- [Int
0..Int
maxChar]]
  where
    cs :: String
cs = forall a. HashSet a -> [a]
S.toList HashSet Char
safeChars
    maxChar :: Int
maxChar = Char -> Int
ord (forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum String
cs)

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) = forall a. Symbolic a => a -> Symbol
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) = forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a. Symbolic a => a -> Symbol
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) = forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
T.drop Int
n Text
t

dropPrefixOfSym :: Symbol -> Symbol
dropPrefixOfSym :: Symbol -> Symbol
dropPrefixOfSym =
  forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Int -> Text -> Text
T.drop (Text -> Int
T.length forall a. IsString a => a
symSepName) forall b c a. (b -> c) -> (a -> b) -> a -> c
.  forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Text -> Text -> (Text, Text)
T.breakOn forall a. IsString a => a
symSepName forall b c a. (b -> c) -> (a -> b) -> a -> c
.  Symbol -> Text
symbolText

prefixOfSym :: Symbol -> Symbol
prefixOfSym :: Symbol -> Symbol
prefixOfSym = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> (Text, Text)
T.breakOn forall a. IsString a => a
symSepName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

suffixOfSym :: Symbol -> Symbol
suffixOfSym :: Symbol -> Symbol
suffixOfSym = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> (Text, Text)
T.breakOnEnd forall a. IsString a => a
symSepName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText

stripPrefix :: Symbol -> Symbol -> Maybe Symbol
stripPrefix :: Symbol -> Symbol -> Maybe Symbol
stripPrefix Symbol
p Symbol
x = forall a. Symbolic a => a -> Symbol
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 = forall a. Symbolic a => a -> Symbol
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 = forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ Text -> Text -> Text
suffixSymbolText (Symbol -> Text
symbolText Symbol
x) (Symbol -> Text
symbolText Symbol
y)

suffixSymbolText :: T.Text -> T.Text -> T.Text
suffixSymbolText :: Text -> Text -> Text
suffixSymbolText  Text
x Text
y = Text
x forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => a
symSepName forall a. Semigroup a => a -> a -> a
<> Text
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)         = 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      = (Maybe Integer -> Symbol
vv forall a. Maybe a
Nothing 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 :: forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
x a
i = forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ Symbol -> Text
symbolText Symbol
x Text -> Text -> Text
`suffixSymbolText` String -> Text
T.pack (forall a. Show a => a -> String
show a
i)

appendSymbolText :: Symbol -> T.Text -> T.Text
appendSymbolText :: Symbol -> Text -> Text
appendSymbolText Symbol
s Text
t = Text -> Text
encode (Symbol -> Text
symbolText Symbol
s forall a. Semigroup a => a -> a -> a
<> forall a. IsString a => a
symSepName forall a. Semigroup a => a -> a -> a
<> Text
t)

tempSymbol :: Symbol -> Integer -> Symbol
tempSymbol :: Symbol -> Integer -> Symbol
tempSymbol Symbol
prefix = 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 = 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 = forall a. Show a => Symbol -> a -> Symbol
intSymbol (Symbol
existPrefix Symbol -> Symbol -> Symbol
`mappendSym` Symbol
prefix)

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

-- | Used to define functions corresponding to binding predicates
--
-- The integer is the BindId.
bindSymbol :: Integer -> Symbol
bindSymbol :: Integer -> Symbol
bindSymbol = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
bindPrefix

tempPrefix, anfPrefix, renamePrefix, litPrefix, gradPrefix, bindPrefix :: 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$"
bindPrefix :: Symbol
bindPrefix   = Symbol
"b$"

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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
unSuffixSymbol 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 = 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)
  = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Symbol
s forall a. Symbolic a => a -> Symbol
symbol forall a b. (a -> b) -> a -> b
$ Text -> Text -> Maybe Text
T.stripSuffix forall a. IsString a => a
symSepName forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Text -> Text -> (Text, Text)
T.breakOnEnd 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 = (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 :: forall a. Symbolic a => a -> String
symbolicString = Symbol -> String
symbolString forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a. Symbolic a => a -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Text
T.pack

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

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

{-# INLINE buildMany #-}
buildMany :: [Builder.Builder] -> Builder.Builder
buildMany :: [Builder] -> Builder
buildMany []     = forall a. Monoid a => a
mempty
buildMany [Builder
b]    = Builder
b
buildMany (Builder
b:[Builder]
bs) = Builder
b forall a. Semigroup a => a -> a -> a
<> forall a. Monoid a => [a] -> a
mconcat [ 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 = 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, tyCastName :: 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"
tyCastName :: Symbol
tyCastName      = Symbol
"cast_as"

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

setApplyName, bitVecApplyName, mapApplyName, boolApplyName, realApplyName, intApplyName :: Int -> Symbol
setApplyName :: Int -> Symbol
setApplyName    = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"set_apply_"
bitVecApplyName :: Int -> Symbol
bitVecApplyName = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"bitvec_apply"
mapApplyName :: Int -> Symbol
mapApplyName    = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"map_apply_"
boolApplyName :: Int -> Symbol
boolApplyName   = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"bool_apply_"
realApplyName :: Int -> Symbol
realApplyName   = forall a. Show a => Symbol -> a -> Symbol
intSymbol Symbol
"real_apply_"
intApplyName :: Int -> Symbol
intApplyName    = 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 :: forall a. IsString a => a
strConName   = a
"Str"
charConName :: forall a. IsString a => a
charConName  = a
"Char"
-- symSepName   :: Char
-- symSepName   = '#' -- DO NOT EVER CHANGE THIS

symSepName   :: (IsString a) => a
symSepName :: forall a. IsString a => 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 = 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 = 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
  , 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

-}