{-# 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
  , sizeName
  , bitVecName
  -- , bvAndName, bvOrName, bvSubName, bvAddName
  , intbv32Name, intbv64Name, bv32intName, bv64intName
  , 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.ByteString.Builder     (Builder)
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 (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
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 :: Symbol
-- nilName      = "nil"
-- consName     = "cons"
-- size32Name   = "Size32"
-- size64Name   = "Size64"
-- bitVecName   = "BitVec"

-- bvOrName, bvAndName, bvSubName, bvAddName,
intbv32Name, intbv64Name, bv32intName, bv64intName :: Symbol
-- bvOrName    = "bvor"
-- bvAndName   = "bvand"
-- bvSubName   = "bvsub"
-- bvAddName   = "bvadd"
intbv32Name :: Symbol
intbv32Name = Symbol
"int_to_bv32"
intbv64Name :: Symbol
intbv64Name = Symbol
"int_to_bv64"
bv32intName :: Symbol
bv32intName = Symbol
"bv32_to_int"
bv64intName :: Symbol
bv64intName = Symbol
"bv64_to_int"

nilName, consName, sizeName, bitVecName :: Symbol
nilName :: Symbol
nilName       = Symbol
"nil"
consName :: Symbol
consName      = Symbol
"cons"
sizeName :: Symbol
sizeName      = Symbol
"Size"
bitVecName :: Symbol
bitVecName    = Symbol
"BitVec"


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"
  -- Currently we parse X in "SizeX" to get the bitvec size
  -- so there is no finite set of names to add here...
  -- , size32Name
  -- , size64Name
  , Symbol
bitVecName
  -- , bvOrName
  -- , 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

-}