module Language.Fixpoint.Names (
dummyName
, preludeName
, boolConName
, funConName
, listConName
, tupConName
, propConName
, strConName
, vvName
, symSepName
, dropModuleNames
, takeModuleNames
) where
import Data.List (intercalate)
import Language.Fixpoint.Misc (errorstar, safeLast, stripParens)
preludeName = "Prelude"
dummyName = "_LIQUID_dummy"
boolConName = "Bool"
funConName = "->"
listConName = "[]"
tupConName = "()"
propConName = "Prop"
strConName = "Str"
vvName = "VV"
symSepName = '#'
dropModuleNames = mungeModuleNames safeLast "dropModuleNames: "
takeModuleNames = mungeModuleNames safeInit "takeModuleNames: "
safeInit _ xs@(_:_) = intercalate "." $ init xs
safeInit msg _ = errorstar $ "safeInit with empty list " ++ msg
mungeModuleNames _ _ [] = []
mungeModuleNames f msg s
| s == tupConName = tupConName
| otherwise = f (msg ++ s) $ words $ dotWhite `fmap` stripParens s
where
dotWhite '.' = ' '
dotWhite c = c