{- |
module: $Header$
description: Names in a hierarchical namespace
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

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

-------------------------------------------------------------------------------
-- Namespaces
-------------------------------------------------------------------------------

newtype Namespace =
    Namespace [String]
  deriving (Namespace -> Namespace -> Bool
(Namespace -> Namespace -> Bool)
-> (Namespace -> Namespace -> Bool) -> Eq Namespace
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Namespace -> Namespace -> Bool
$c/= :: Namespace -> Namespace -> Bool
== :: Namespace -> Namespace -> Bool
$c== :: Namespace -> Namespace -> Bool
Eq,Eq Namespace
Eq Namespace
-> (Namespace -> Namespace -> Ordering)
-> (Namespace -> Namespace -> Bool)
-> (Namespace -> Namespace -> Bool)
-> (Namespace -> Namespace -> Bool)
-> (Namespace -> Namespace -> Bool)
-> (Namespace -> Namespace -> Namespace)
-> (Namespace -> Namespace -> Namespace)
-> Ord Namespace
Namespace -> Namespace -> Bool
Namespace -> Namespace -> Ordering
Namespace -> Namespace -> Namespace
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Namespace -> Namespace -> Namespace
$cmin :: Namespace -> Namespace -> Namespace
max :: Namespace -> Namespace -> Namespace
$cmax :: Namespace -> Namespace -> Namespace
>= :: Namespace -> Namespace -> Bool
$c>= :: Namespace -> Namespace -> Bool
> :: Namespace -> Namespace -> Bool
$c> :: Namespace -> Namespace -> Bool
<= :: Namespace -> Namespace -> Bool
$c<= :: Namespace -> Namespace -> Bool
< :: Namespace -> Namespace -> Bool
$c< :: Namespace -> Namespace -> Bool
compare :: Namespace -> Namespace -> Ordering
$ccompare :: Namespace -> Namespace -> Ordering
$cp1Ord :: Eq Namespace
Ord,Int -> Namespace -> ShowS
[Namespace] -> ShowS
Namespace -> String
(Int -> Namespace -> ShowS)
-> (Namespace -> String)
-> ([Namespace] -> ShowS)
-> Show Namespace
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Namespace] -> ShowS
$cshowList :: [Namespace] -> ShowS
show :: Namespace -> String
$cshow :: Namespace -> String
showsPrec :: Int -> Namespace -> ShowS
$cshowsPrec :: Int -> Namespace -> ShowS
Show)

-------------------------------------------------------------------------------
-- Names
-------------------------------------------------------------------------------

data Name =
    Name Namespace String
  deriving (Name -> Name -> Bool
(Name -> Name -> Bool) -> (Name -> Name -> Bool) -> Eq Name
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Name -> Name -> Bool
$c/= :: Name -> Name -> Bool
== :: Name -> Name -> Bool
$c== :: Name -> Name -> Bool
Eq,Eq Name
Eq Name
-> (Name -> Name -> Ordering)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Bool)
-> (Name -> Name -> Name)
-> (Name -> Name -> Name)
-> Ord Name
Name -> Name -> Bool
Name -> Name -> Ordering
Name -> Name -> Name
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Name -> Name -> Name
$cmin :: Name -> Name -> Name
max :: Name -> Name -> Name
$cmax :: Name -> Name -> Name
>= :: Name -> Name -> Bool
$c>= :: Name -> Name -> Bool
> :: Name -> Name -> Bool
$c> :: Name -> Name -> Bool
<= :: Name -> Name -> Bool
$c<= :: Name -> Name -> Bool
< :: Name -> Name -> Bool
$c< :: Name -> Name -> Bool
compare :: Name -> Name -> Ordering
$ccompare :: Name -> Name -> Ordering
$cp1Ord :: Eq Name
Ord,Int -> Name -> ShowS
[Name] -> ShowS
Name -> String
(Int -> Name -> ShowS)
-> (Name -> String) -> ([Name] -> ShowS) -> Show Name
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Name] -> ShowS
$cshowList :: [Name] -> ShowS
show :: Name -> String
$cshow :: Name -> String
showsPrec :: Int -> Name -> ShowS
$cshowsPrec :: Int -> Name -> ShowS
Show)

-------------------------------------------------------------------------------
-- The global namespace (contains all type and term variable names)
-------------------------------------------------------------------------------

global :: Namespace
global :: Namespace
global = [String] -> Namespace
Namespace []

mkGlobal :: String -> Name
mkGlobal :: String -> Name
mkGlobal = Namespace -> String -> Name
Name Namespace
global

destGlobal :: Name -> Maybe String
destGlobal :: Name -> Maybe String
destGlobal (Name Namespace
ns String
s) = if Namespace
ns Namespace -> Namespace -> Bool
forall a. Eq a => a -> a -> Bool
== Namespace
global then String -> Maybe String
forall a. a -> Maybe a
Just String
s else Maybe String
forall a. Maybe a
Nothing

isGlobal :: Name -> Bool
isGlobal :: Name -> Bool
isGlobal = Maybe String -> Bool
forall a. Maybe a -> Bool
Maybe.isJust (Maybe String -> Bool) -> (Name -> Maybe String) -> Name -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Maybe String
destGlobal

-------------------------------------------------------------------------------
-- Fresh names
-------------------------------------------------------------------------------

variantAvoiding :: Set Name -> Name -> Name
variantAvoiding :: Set Name -> Name -> Name
variantAvoiding Set Name
avoid Name
n =
    if Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Name
n Set Name
avoid then Name
n else Int -> Name
variant Int
0
  where
    Name Namespace
ns String
bx = Name
n
    b :: String
b = (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
List.dropWhileEnd Char -> Bool
isDigitOrPrime String
bx

    isDigitOrPrime :: Char -> Bool
    isDigitOrPrime :: Char -> Bool
isDigitOrPrime Char
c = Char -> Bool
Char.isDigit Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\''

    variant :: Int -> Name
    variant :: Int -> Name
variant Int
i =
        if Name -> Set Name -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Name
ni Set Name
avoid then Name
ni else Int -> Name
variant (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      where
        ni :: Name
ni = Namespace -> String -> Name
Name Namespace
ns String
bi
        bi :: String
bi = String
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i

freshSupply :: [Name]
freshSupply :: [Name]
freshSupply = (String -> Name) -> [String] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map String -> Name
mkGlobal ([String]
stem [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [[String]] -> [String]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Int -> [String]) -> [Int] -> [[String]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [String]
forall a. Show a => a -> [String]
add [(Int
0 :: Int) ..]))
  where
    add :: a -> [String]
add a
n = ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n) [String]
stem
    stem :: [String]
stem = (Char -> String) -> String -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Char -> ShowS
forall a. a -> [a] -> [a]
: []) String
"abcdefghijklmnpqrstuvwxyz"

-------------------------------------------------------------------------------
-- Standard namespaces
-------------------------------------------------------------------------------

-- Booleans

boolNamespace :: Namespace
boolNamespace :: Namespace
boolNamespace = [String] -> Namespace
Namespace [String
"Data",String
"Bool"]

-- Lists

listNamespace :: Namespace
listNamespace :: Namespace
listNamespace = [String] -> Namespace
Namespace [String
"Data",String
"List"]

-- Products

pairNamespace :: Namespace
pairNamespace :: Namespace
pairNamespace = [String] -> Namespace
Namespace [String
"Data",String
"Pair"]

-- Sums

sumNamespace :: Namespace
sumNamespace :: Namespace
sumNamespace = [String] -> Namespace
Namespace [String
"Data",String
"Sum"]

-- Functions

functionNamespace :: Namespace
functionNamespace :: Namespace
functionNamespace = [String] -> Namespace
Namespace [String
"Function"]

-- Natural numbers

naturalNamespace :: Namespace
naturalNamespace :: Namespace
naturalNamespace = [String] -> Namespace
Namespace [String
"Number",String
"Natural"]

-- Real numbers

realNamespace :: Namespace
realNamespace :: Namespace
realNamespace = [String] -> Namespace
Namespace [String
"Number",String
"Real"]

-- Sets

setNamespace :: Namespace
setNamespace :: Namespace
setNamespace = [String] -> Namespace
Namespace [String
"Set"]