module Language.Fixpoint.Names (
Symbol
, Symbolic (..)
, anfPrefix, tempPrefix, vv, isPrefixOfSym, isSuffixOfSym, stripParensSym
, consSym, unconsSym, dropSym, singletonSym, headSym, takeWhileSym, lengthSym
, symChars, isNonSymbol, nonSymbol
, isNontrivialVV
, symbolText, symbolString
, encode, vvCon
, dropModuleNames
, dropModuleUnique
, takeModuleNames
, dummySymbol, intSymbol, tempSymbol, existSymbol
, qualifySymbol
, suffixSymbol
, dummyName
, preludeName
, boolConName
, funConName
, listConName
, tupConName
, propConName
, hpropConName
, strConName
, nilName
, consName
, vvName
, symSepName
, size32Name, size64Name, bitVecName, bvAndName, bvOrName
, prims
) where
import Control.Applicative
import Control.DeepSeq
import Data.Char
import Data.Generics (Data)
import Data.Hashable
import qualified Data.HashSet as S
import Data.Interned
import Data.Interned.Internal.Text
import Data.Interned.Text
import Data.Monoid
import Data.String
import Data.Text (Text)
import qualified Data.Text as T
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import Language.Fixpoint.Misc (errorstar, mapSnd, stripParens)
symChars
= ['a' .. 'z']
++ ['A' .. 'Z']
++ ['0' .. '9']
++ ['_', '%', '.', '#']
deriving instance Data InternedText
deriving instance Typeable InternedText
deriving instance Generic InternedText
newtype Symbol = S InternedText deriving (Eq, Ord, Data, Typeable, Generic, IsString)
instance Monoid Symbol where
mempty = ""
mappend x y = S . intern $ mappend (symbolText x) (symbolText y)
instance Hashable InternedText where
hashWithSalt s (InternedText i t) = hashWithSalt s i
instance NFData InternedText where
rnf (InternedText id t) = rnf id `seq` rnf t `seq` ()
instance Show Symbol where
show (S x) = show x
instance NFData Symbol where
rnf (S x) = rnf x
instance Hashable Symbol where
hashWithSalt i (S s) = hashWithSalt i s
symbolString :: Symbol -> String
symbolString = T.unpack . symbolText
encode :: String -> String
encode s
| isFixKey s = encodeSym s
| isFixSym' s = s
| otherwise = encodeSym s
encodeSym s = fixSymPrefix ++ concatMap encodeChar s
symbolText :: Symbol -> Text
symbolText (S s) = unintern s
indices :: [Integer]
indices = [0..]
okSymChars
= S.fromList
$ ['a' .. 'z']
++ ['A' .. 'Z']
++ ['0' .. '9']
++ ['_', '.' ]
fixSymPrefix = "fix" ++ [symSepName]
isPrefixOfSym (symbolText -> p) (symbolText -> x) = p `T.isPrefixOf` x
isSuffixOfSym (symbolText -> p) (symbolText -> x) = p `T.isSuffixOf` x
takeWhileSym p (symbolText -> t) = symbol $ T.takeWhile p t
headSym (symbolText -> t) = T.head t
consSym c (symbolText -> s) = symbol $ T.cons c s
singletonSym = (`consSym` "")
lengthSym (symbolText -> t) = T.length t
unconsSym :: Symbol -> Maybe (Char, Symbol)
unconsSym (symbolText -> s) = mapSnd symbol <$> T.uncons s
dropSym :: Int -> Symbol -> Symbol
dropSym n (symbolText -> t) = symbol $ T.drop n t
stripParensSym (symbolText -> t) = symbol $ stripParens t
suffixSymbol (S s) suf = symbol $ (unintern s) `mappend` suf
isFixSym' (c:chs) = isAlpha c && all (`S.member` (symSepName `S.insert` okSymChars)) chs
isFixSym' _ = False
isFixKey x = S.member x keywords
keywords = S.fromList ["env", "id", "tag", "qualif", "constant", "cut", "bind", "constraint", "grd", "lhs", "rhs"]
encodeChar c
| c `S.member` okSymChars
= [c]
| otherwise
= [symSepName] ++ (show $ ord c) ++ [symSepName]
decodeStr s
= chr ((read s) :: Int)
qualifySymbol :: Symbol -> Symbol -> Symbol
qualifySymbol m'@(symbolText -> m) x'@(symbolText -> x)
| isQualified x = x'
| isParened x = symbol (wrapParens (m `mappend` "." `mappend` stripParens x))
| otherwise = symbol (m `mappend` "." `mappend` x)
isQualified y = "." `T.isInfixOf` y
wrapParens x = "(" `mappend` x `mappend` ")"
isParened xs = xs /= stripParens xs
vv :: Maybe Integer -> Symbol
vv (Just i) = symbol $ symbolText vvName `T.snoc` symSepName `mappend` T.pack (show i)
vv Nothing = vvName
vvCon = symbol $ symbolText vvName `T.snoc` symSepName `mappend` "F"
isNontrivialVV = not . (vv Nothing ==)
dummySymbol = dummyName
intSymbol :: (Show a) => Symbol -> a -> Symbol
intSymbol x i = x `mappend` symbol (show i)
tempSymbol, existSymbol :: Symbol -> Integer -> Symbol
tempSymbol prefix n = intSymbol (tempPrefix `mappend` prefix) n
existSymbol prefix n = intSymbol (existPrefix `mappend` prefix) n
tempPrefix, anfPrefix, existPrefix :: Symbol
tempPrefix = "lq_tmp_"
anfPrefix = "lq_anf_"
existPrefix = "lq_ext_"
nonSymbol :: Symbol
nonSymbol = ""
isNonSymbol = (== nonSymbol)
class Symbolic a where
symbol :: a -> Symbol
instance Symbolic String where
symbol = symbol . T.pack
instance Symbolic Text where
symbol = S . intern
instance Symbolic InternedText where
symbol = S
instance Symbolic Symbol where
symbol = id
preludeName, dummyName, boolConName, funConName, listConName, tupConName, propConName, strConName, vvName :: Symbol
preludeName = "Prelude"
dummyName = "_LIQUID_dummy"
boolConName = "Bool"
funConName = "->"
listConName = "[]"
tupConName = "()"
propConName = "Prop"
hpropConName = "HProp"
strConName = "Str"
vvName = "VV"
symSepName = '#'
nilName = "nil" :: Symbol
consName = "cons" :: Symbol
size32Name = "Size32" :: Symbol
size64Name = "Size64" :: Symbol
bitVecName = "BitVec" :: Symbol
bvOrName = "bvor" :: Symbol
bvAndName = "bvAnd" :: Symbol
prims :: [Symbol]
prims = [ propConName
, hpropConName
, vvName
, "Pred"
, "List"
, "Set_Set"
, "Set_sng"
, "Set_cup"
, "Set_cap"
, "Set_dif"
, "Set_emp"
, "Set_empty"
, "Set_mem"
, "Set_sub"
, "Map_t"
, "Map_select"
, "Map_store"
, size32Name
, size64Name
, bitVecName
, bvOrName
, bvAndName
, "FAppTy"
, nilName
, consName
]
sepModNames = "."
sepUnique = "#"
dropModuleNames = mungeNames safeLast sepModNames "dropModuleNames: "
takeModuleNames = mungeNames safeInit sepModNames "takeModuleNames: "
dropModuleUnique = mungeNames safeHead sepUnique "dropModuleUnique: "
safeHead :: String -> [T.Text] -> Symbol
safeHead msg [] = errorstar $ "safeHead with empty list" ++ msg
safeHead _ (x:_) = symbol x
safeInit :: String -> [T.Text] -> Symbol
safeInit _ xs@(_:_) = symbol $ T.intercalate "." $ init xs
safeInit msg _ = errorstar $ "safeInit with empty list " ++ msg
safeLast :: String -> [T.Text] -> Symbol
safeLast _ xs@(_:_) = symbol $ last xs
safeLast msg _ = errorstar $ "safeLast with empty list " ++ msg
mungeNames :: (String -> [T.Text] -> Symbol) -> T.Text -> String -> Symbol -> Symbol
mungeNames _ _ _ "" = ""
mungeNames f d msg s'@(symbolText -> s)
| s' == tupConName
= tupConName
| otherwise = f (msg ++ T.unpack s) $ T.splitOn d $ stripParens s