{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternGuards #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Language.Fixpoint.Types.Names (
Symbol
, Symbolic (..)
, LocSymbol
, LocText
, symbolicString
, symbolSafeText
, symbolSafeString
, symbolText
, symbolString
, symbolBuilder
, buildMany
, isPrefixOfSym
, isSuffixOfSym
, isNonSymbol
, isLitSymbol
, isTestSymbol
, isNontrivialVV
, isDummy
, isFixKey
, prefixOfSym
, suffixOfSym
, stripPrefix
, stripSuffix
, consSym
, unconsSym
, dropSym
, dropPrefixOfSym
, headSym
, lengthSym
, nonSymbol
, vvCon
, tidySymbol
, anfPrefix
, tempPrefix
, vv
, symChars
, dummySymbol
, intSymbol
, tempSymbol
, gradIntSymbol
, appendSymbolText
, litSymbol
, bindSymbol
, testSymbol
, renameSymbol
, kArgSymbol
, existSymbol
, suffixSymbol
, mappendSym
, unLitSymbol
, dummyName
, preludeName
, boolConName
, funConName
, listConName
, listLConName
, tupConName
, setConName
, mapConName
, strConName
, charConName
, nilName
, consName
, vvName
, size32Name
, size64Name
, bitVecName
, bvAndName
, bvOrName
, propConName
, isPrim
, prims
, mulFuncName
, divFuncName
, 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
deriving instance Data InternedText
deriving instance Typeable InternedText
deriving instance Generic InternedText
type SafeText = T.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 :: 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
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
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
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)
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
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
{-# 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"
]
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
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)
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 :: 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
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
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$"
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
nonSymbol :: Symbol
nonSymbol :: Symbol
nonSymbol = Symbol
""
isNonSymbol :: Symbol -> Bool
isNonSymbol :: Symbol -> Bool
isNonSymbol = (forall a. Eq a => a -> a -> Bool
== Symbol
nonSymbol)
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 ]
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 :: (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"
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"
, 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
]