module HOL.Name
where
import qualified Data.Char as Char
import qualified Data.List as List
import qualified Data.Maybe as Maybe
import Data.Set (Set)
import qualified Data.Set as Set
newtype Namespace =
Namespace [String]
deriving (Eq,Ord,Show)
data Name =
Name Namespace String
deriving (Eq,Ord,Show)
global :: Namespace
global = Namespace []
mkGlobal :: String -> Name
mkGlobal = Name global
destGlobal :: Name -> Maybe String
destGlobal (Name ns s) = if ns == global then Just s else Nothing
isGlobal :: Name -> Bool
isGlobal = Maybe.isJust . destGlobal
variantAvoiding :: Set Name -> Name -> Name
variantAvoiding avoid n =
if Set.notMember n avoid then n else variant 0
where
Name ns bx = n
b = List.dropWhileEnd isDigitOrPrime bx
isDigitOrPrime :: Char -> Bool
isDigitOrPrime c = Char.isDigit c || c == '\''
variant :: Int -> Name
variant i =
if Set.notMember ni avoid then ni else variant (i + 1)
where
ni = Name ns bi
bi = b ++ show i
boolNamespace :: Namespace
boolNamespace = Namespace ["Data","Bool"]
listNamespace :: Namespace
listNamespace = Namespace ["Data","List"]
pairNamespace :: Namespace
pairNamespace = Namespace ["Data","Pair"]
sumNamespace :: Namespace
sumNamespace = Namespace ["Data","Sum"]
functionNamespace :: Namespace
functionNamespace = Namespace ["Function"]
naturalNamespace :: Namespace
naturalNamespace = Namespace ["Number","Natural"]
realNamespace :: Namespace
realNamespace = Namespace ["Number","Real"]
setNamespace :: Namespace
setNamespace = Namespace ["Set"]