{-# 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
  , 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)
#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 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
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) = {-# SCC "hashWithSalt-Description-Symbol" #-} 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 S.Store Symbol where
  poke :: Symbol -> Poke ()
poke = Text -> Poke ()
forall a. Store a => a -> Poke ()
S.poke (Text -> Poke ()) -> (Symbol -> Text) -> Symbol -> Poke ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Text
symbolText
  peek :: Peek Symbol
peek = Text -> Symbol
textSymbol (Text -> Symbol) -> Peek Text -> Peek Symbol
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Peek Text
forall a. Store a => Peek a
S.peek
  size :: Size Symbol
size = (Symbol -> Text) -> Size Text -> Size Symbol
forall (f :: * -> *) a b. Contravariant f => (a -> b) -> f b -> f a
contramap Symbol -> Text
symbolText Size Text
forall a. Store a => Size a
S.size

instance B.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
B.get
   put :: Symbol -> Put
put = Text -> Put
forall t. Binary t => t -> Put
B.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

{-# SCC symbolString #-}
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

{-# SCC textSymbol #-}
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

{-# SCC encodeUnsafe #-}
encodeUnsafe :: T.Text -> T.Text
encodeUnsafe :: Text -> Text
encodeUnsafe Text
t = String -> Text
T.pack (String -> Text) -> String -> Text
forall a b. (a -> b) -> a -> b
$ ShowS
pad ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ ShowS
go ShowS -> ShowS
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' Char -> ShowS
forall a. a -> [a] -> [a]
: Char
'$' Char -> ShowS
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
'$' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> ShowS
forall a. Show a => a -> ShowS
shows (Char -> Int
ord Char
c) (Char
'$' Char -> ShowS
forall a. a -> [a] -> [a]
: ShowS
go String
cs)
      else
        Char
c Char -> ShowS
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
_) -> 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

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

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

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

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

suffixOfSym :: Symbol -> Symbol
suffixOfSym :: Symbol -> Symbol
suffixOfSym = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> (Symbol -> Text) -> Symbol -> Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Text, Text) -> Text
forall a b. (a, b) -> b
snd ((Text, Text) -> Text)
-> (Symbol -> (Text, Text)) -> Symbol -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Text -> (Text, Text)
T.breakOnEnd Text
forall a. IsString a => a
symSepName (Text -> (Text, Text))
-> (Symbol -> Text) -> Symbol -> (Text, Text)
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 = 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 = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Text -> 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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
forall a. IsString a => a
symSepName Text -> Text -> Text
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)         = 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 = Text -> Symbol
forall a. Symbolic a => a -> Symbol
symbol (Text -> Symbol) -> Text -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> Text
symbolText Symbol
x Text -> Text -> Text
`suffixSymbolText` String -> Text
T.pack (a -> String
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 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
forall a. IsString a => a
symSepName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t)

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

-- | Used to define functions corresponding to binding predicates
--
-- The integer is the BindId.
bindSymbol :: Integer -> Symbol
bindSymbol :: Integer -> Symbol
bindSymbol = Symbol -> Integer -> Symbol
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 (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
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, 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 :: 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

-}