{-# LANGUAGE TypeOperators, GeneralizedNewtypeDeriving, FlexibleInstances, CPP #-}
module Jukebox.Name where

import Control.Monad
import Control.Monad.Trans.State.Strict
import Data.Ord
import Data.Int
import Data.Symbol
import Data.Char
import Data.Ratio
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative
#endif

data Name =
    Fixed !FixedName (Maybe String)
  | Unique {-# UNPACK #-} !Int64 {-# UNPACK #-} !Symbol (Maybe String) Renamer
  | Variant !Name ![Name] Renamer

data FixedName =
    Basic {-# UNPACK #-} !Symbol
  | Overloaded {-# UNPACK #-} !Symbol {-# UNPACK #-} !Symbol
  | Integer !Integer
  | Rational !Rational
  | Real !Rational
  deriving (FixedName -> FixedName -> Bool
(FixedName -> FixedName -> Bool)
-> (FixedName -> FixedName -> Bool) -> Eq FixedName
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FixedName -> FixedName -> Bool
$c/= :: FixedName -> FixedName -> Bool
== :: FixedName -> FixedName -> Bool
$c== :: FixedName -> FixedName -> Bool
Eq, Eq FixedName
Eq FixedName
-> (FixedName -> FixedName -> Ordering)
-> (FixedName -> FixedName -> Bool)
-> (FixedName -> FixedName -> Bool)
-> (FixedName -> FixedName -> Bool)
-> (FixedName -> FixedName -> Bool)
-> (FixedName -> FixedName -> FixedName)
-> (FixedName -> FixedName -> FixedName)
-> Ord FixedName
FixedName -> FixedName -> Bool
FixedName -> FixedName -> Ordering
FixedName -> FixedName -> FixedName
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 :: FixedName -> FixedName -> FixedName
$cmin :: FixedName -> FixedName -> FixedName
max :: FixedName -> FixedName -> FixedName
$cmax :: FixedName -> FixedName -> FixedName
>= :: FixedName -> FixedName -> Bool
$c>= :: FixedName -> FixedName -> Bool
> :: FixedName -> FixedName -> Bool
$c> :: FixedName -> FixedName -> Bool
<= :: FixedName -> FixedName -> Bool
$c<= :: FixedName -> FixedName -> Bool
< :: FixedName -> FixedName -> Bool
$c< :: FixedName -> FixedName -> Bool
compare :: FixedName -> FixedName -> Ordering
$ccompare :: FixedName -> FixedName -> Ordering
$cp1Ord :: Eq FixedName
Ord)

type Renamer = String -> Int -> Renaming
data Renaming = Renaming [String] String

base :: Named a => a -> String
base :: a -> String
base a
x =
  case a -> Name
forall a. Named a => a -> Name
name a
x of
    Fixed FixedName
x Maybe String
_ -> FixedName -> String
forall a. Show a => a -> String
show FixedName
x
    Unique Int64
_ Symbol
xs Maybe String
_ Renamer
_ -> Symbol -> String
unintern Symbol
xs
    Variant Name
x [Name]
_ Renamer
_ -> Name -> String
forall a. Named a => a -> String
base Name
x

label :: Named a => a -> Maybe String
label :: a -> Maybe String
label a
x =
  case a -> Name
forall a. Named a => a -> Name
name a
x of
    Fixed FixedName
_ Maybe String
x -> Maybe String
x
    Unique Int64
_ Symbol
_ Maybe String
x Renamer
_ -> Maybe String
x
    Variant Name
x [Name]
_ Renamer
_ -> Name -> Maybe String
forall a. Named a => a -> Maybe String
label Name
x

hasLabel :: Named a => String -> a -> Bool
hasLabel :: String -> a -> Bool
hasLabel String
l a
x = a -> Maybe String
forall a. Named a => a -> Maybe String
label a
x Maybe String -> Maybe String -> Bool
forall a. Eq a => a -> a -> Bool
== String -> Maybe String
forall a. a -> Maybe a
Just String
l

withMaybeLabel :: Maybe String -> Name -> Name
withMaybeLabel :: Maybe String -> Name -> Name
withMaybeLabel Maybe String
l (Fixed FixedName
x Maybe String
_) = FixedName -> Maybe String -> Name
Fixed FixedName
x Maybe String
l
withMaybeLabel Maybe String
l (Unique Int64
x Symbol
xs Maybe String
_ Renamer
f) = Int64 -> Symbol -> Maybe String -> Renamer -> Name
Unique Int64
x Symbol
xs Maybe String
l Renamer
f
withMaybeLabel Maybe String
l (Variant Name
x [Name]
xs Renamer
r) = Name -> [Name] -> Renamer -> Name
Variant (Maybe String -> Name -> Name
withMaybeLabel Maybe String
l Name
x) [Name]
xs Renamer
r

withLabel :: String -> Name -> Name
withLabel :: String -> Name -> Name
withLabel String
l Name
x = Maybe String -> Name -> Name
withMaybeLabel (String -> Maybe String
forall a. a -> Maybe a
Just String
l) Name
x

instance Show FixedName where
  show :: FixedName -> String
show (Basic Symbol
xs) = Symbol -> String
unintern Symbol
xs
  show (Overloaded Symbol
xs Symbol
_) = Symbol -> String
unintern Symbol
xs
  show (Integer Integer
n) = Integer -> String
forall a. Show a => a -> String
show Integer
n
  show (Rational Rational
x) = Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x)
  show (Real Rational
x) = String
"$to_real(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
numerator Rational
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"/" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show (Rational -> Integer
forall a. Ratio a -> a
denominator Rational
x) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

renamer :: Named a => a -> Renamer
renamer :: a -> Renamer
renamer a
x =
  case a -> Name
forall a. Named a => a -> Name
name a
x of
    Fixed FixedName
_ Maybe String
_ -> Renamer
defaultRenamer
    Unique Int64
_ Symbol
_ Maybe String
_ Renamer
f -> Renamer
f
    Variant Name
_ [Name]
_ Renamer
f -> Renamer
f

defaultRenamer :: Renamer
defaultRenamer :: Renamer
defaultRenamer String
xs Int
0 = [String] -> String -> Renaming
Renaming [] String
xs
defaultRenamer String
xs Int
n = [String] -> String -> Renaming
Renaming [] (String -> Renaming) -> String -> Renaming
forall a b. (a -> b) -> a -> b
$ String
xs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
sep String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1)
  where
    sep :: String
sep
      | Bool -> Bool
not (String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
xs) Bool -> Bool -> Bool
&& Char -> Bool
isDigit (String -> Char
forall a. [a] -> a
last String
xs) = String
"_"
      | Bool
otherwise = String
""

withRenamer :: Name -> Renamer -> Name
Fixed FixedName
x Maybe String
l withRenamer :: Name -> Renamer -> Name
`withRenamer` Renamer
_ = FixedName -> Maybe String -> Name
Fixed FixedName
x Maybe String
l
Unique Int64
n Symbol
xs Maybe String
l Renamer
_ `withRenamer` Renamer
f = Int64 -> Symbol -> Maybe String -> Renamer -> Name
Unique Int64
n Symbol
xs Maybe String
l Renamer
f
Variant Name
x [Name]
xs Renamer
_ `withRenamer` Renamer
f = Name -> [Name] -> Renamer -> Name
Variant Name
x [Name]
xs Renamer
f

instance Eq Name where
  Name
x == :: Name -> Name -> Bool
== Name
y = Name -> Either FixedName (Either Int64 (Name, [Name]))
compareName Name
x Either FixedName (Either Int64 (Name, [Name]))
-> Either FixedName (Either Int64 (Name, [Name])) -> Bool
forall a. Eq a => a -> a -> Bool
== Name -> Either FixedName (Either Int64 (Name, [Name]))
compareName Name
y

instance Ord Name where
  compare :: Name -> Name -> Ordering
compare = (Name -> Either FixedName (Either Int64 (Name, [Name])))
-> Name -> Name -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing Name -> Either FixedName (Either Int64 (Name, [Name]))
compareName

-- It's important that FixedNames come first so that they get added
-- first to the used names list in Jukebox.TPTP.Print.prettyRename.
compareName :: Name -> Either FixedName (Either Int64 (Name, [Name]))
compareName :: Name -> Either FixedName (Either Int64 (Name, [Name]))
compareName (Fixed FixedName
xs Maybe String
_) = FixedName -> Either FixedName (Either Int64 (Name, [Name]))
forall a b. a -> Either a b
Left FixedName
xs
compareName (Unique Int64
n Symbol
_ Maybe String
_ Renamer
_) = Either Int64 (Name, [Name])
-> Either FixedName (Either Int64 (Name, [Name]))
forall a b. b -> Either a b
Right (Int64 -> Either Int64 (Name, [Name])
forall a b. a -> Either a b
Left Int64
n)
compareName (Variant Name
x [Name]
xs Renamer
_) = Either Int64 (Name, [Name])
-> Either FixedName (Either Int64 (Name, [Name]))
forall a b. b -> Either a b
Right ((Name, [Name]) -> Either Int64 (Name, [Name])
forall a b. b -> Either a b
Right (Name
x, [Name]
xs))

instance Show Name where
  show :: Name -> String
show (Fixed FixedName
x Maybe String
_) = FixedName -> String
forall a. Show a => a -> String
show FixedName
x
  show (Unique Int64
n Symbol
xs Maybe String
ml Renamer
f) =
    String
ys String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"@" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int64 -> String
forall a. Show a => a -> String
show Int64
n String -> ShowS
forall a. [a] -> [a] -> [a]
++
    case Maybe String
ml of
      Maybe String
Nothing -> String
""
      Just String
l -> String
"[" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
l String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"]"
    where
      Renaming [String]
_ String
ys = Renamer
f (Symbol -> String
unintern Symbol
xs) Int
0
  show (Variant Name
x [Name]
xs Renamer
_) =
    String
"variant(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x String -> ShowS
forall a. [a] -> [a] -> [a]
++
      [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Show a => a -> String
show Name
x | Name
x <- [Name]
xs] String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

class Named a where
  name :: a -> Name

instance Named [Char] where
  name :: String -> Name
name String
x = Symbol -> Name
forall a. Named a => a -> Name
name (String -> Symbol
intern String
x)

instance Named Symbol where
  name :: Symbol -> Name
name Symbol
x = FixedName -> Maybe String -> Name
Fixed (Symbol -> FixedName
Basic Symbol
x) Maybe String
forall a. Maybe a
Nothing

instance Named Integer where
  name :: Integer -> Name
name Integer
n = String -> Name
forall a. Named a => a -> Name
name (String
"n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n)

instance Named Int where
  name :: Int -> Name
name = Integer -> Name
forall a. Named a => a -> Name
name (Integer -> Name) -> (Int -> Integer) -> Int -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Integer
forall a. Integral a => a -> Integer
toInteger

instance Named Name where
  name :: Name -> Name
name = Name -> Name
forall a. a -> a
id

-- Get all names, including those only used as part of a variant.
allNames :: Named a => a -> [Name]
allNames :: a -> [Name]
allNames a
x = [Name] -> [Name] -> [Name]
gather [a -> Name
forall a. Named a => a -> Name
name a
x] []
  where
    gather :: [Name] -> [Name] -> [Name]
gather [] [Name]
xs = [Name]
xs
    gather (Name
x:[Name]
xs) [Name]
ys =
      Name -> [Name] -> [Name]
sub Name
x (Name
xName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name] -> [Name] -> [Name]
gather [Name]
xs [Name]
ys)
    sub :: Name -> [Name] -> [Name]
sub (Variant Name
x [Name]
xs Renamer
_) [Name]
ys =
      [Name] -> [Name] -> [Name]
gather (Name
xName -> [Name] -> [Name]
forall a. a -> [a] -> [a]
:[Name]
xs) [Name]
ys
    sub Name
_ [Name]
ys = [Name]
ys

variant :: (Named a, Named b) => a -> [b] -> Name
variant :: a -> [b] -> Name
variant a
x [b]
xs =
  Name -> [Name] -> Renamer -> Name
Variant (a -> Name
forall a. Named a => a -> Name
name a
x) ((b -> Name) -> [b] -> [Name]
forall a b. (a -> b) -> [a] -> [b]
map b -> Name
forall a. Named a => a -> Name
name [b]
xs) Renamer
defaultRenamer

unvariant :: Name -> Maybe (Name, [Name])
unvariant :: Name -> Maybe (Name, [Name])
unvariant (Variant Name
x [Name]
xs Renamer
_) = (Name, [Name]) -> Maybe (Name, [Name])
forall a. a -> Maybe a
Just (Name
x, [Name]
xs)
unvariant Name
_ = Maybe (Name, [Name])
forall a. Maybe a
Nothing

data a ::: b = a ::: b deriving Int -> (a ::: b) -> ShowS
[a ::: b] -> ShowS
(a ::: b) -> String
(Int -> (a ::: b) -> ShowS)
-> ((a ::: b) -> String) -> ([a ::: b] -> ShowS) -> Show (a ::: b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> (a ::: b) -> ShowS
forall a b. (Show a, Show b) => [a ::: b] -> ShowS
forall a b. (Show a, Show b) => (a ::: b) -> String
showList :: [a ::: b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [a ::: b] -> ShowS
show :: (a ::: b) -> String
$cshow :: forall a b. (Show a, Show b) => (a ::: b) -> String
showsPrec :: Int -> (a ::: b) -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> (a ::: b) -> ShowS
Show

lhs :: (a ::: b) -> a
lhs :: (a ::: b) -> a
lhs (a
x ::: b
_) = a
x

rhs :: (a ::: b) -> b
rhs :: (a ::: b) -> b
rhs (a
_ ::: b
y) = b
y

instance Named a => Eq (a ::: b) where a ::: b
s == :: (a ::: b) -> (a ::: b) -> Bool
== a ::: b
t = (a ::: b) -> Name
forall a. Named a => a -> Name
name a ::: b
s Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== (a ::: b) -> Name
forall a. Named a => a -> Name
name a ::: b
t
instance Named a => Ord (a ::: b) where compare :: (a ::: b) -> (a ::: b) -> Ordering
compare = ((a ::: b) -> Name) -> (a ::: b) -> (a ::: b) -> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing (a ::: b) -> Name
forall a. Named a => a -> Name
name

instance Named a => Named (a ::: b) where
  name :: (a ::: b) -> Name
name (a
a ::: b
_) = a -> Name
forall a. Named a => a -> Name
name a
a

newtype NameM a =
  NameM { NameM a -> State Int64 a
unNameM :: State Int64 a }
    deriving (a -> NameM b -> NameM a
(a -> b) -> NameM a -> NameM b
(forall a b. (a -> b) -> NameM a -> NameM b)
-> (forall a b. a -> NameM b -> NameM a) -> Functor NameM
forall a b. a -> NameM b -> NameM a
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> NameM b -> NameM a
$c<$ :: forall a b. a -> NameM b -> NameM a
fmap :: (a -> b) -> NameM a -> NameM b
$cfmap :: forall a b. (a -> b) -> NameM a -> NameM b
Functor, Functor NameM
a -> NameM a
Functor NameM
-> (forall a. a -> NameM a)
-> (forall a b. NameM (a -> b) -> NameM a -> NameM b)
-> (forall a b c. (a -> b -> c) -> NameM a -> NameM b -> NameM c)
-> (forall a b. NameM a -> NameM b -> NameM b)
-> (forall a b. NameM a -> NameM b -> NameM a)
-> Applicative NameM
NameM a -> NameM b -> NameM b
NameM a -> NameM b -> NameM a
NameM (a -> b) -> NameM a -> NameM b
(a -> b -> c) -> NameM a -> NameM b -> NameM c
forall a. a -> NameM a
forall a b. NameM a -> NameM b -> NameM a
forall a b. NameM a -> NameM b -> NameM b
forall a b. NameM (a -> b) -> NameM a -> NameM b
forall a b c. (a -> b -> c) -> NameM a -> NameM b -> NameM c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: NameM a -> NameM b -> NameM a
$c<* :: forall a b. NameM a -> NameM b -> NameM a
*> :: NameM a -> NameM b -> NameM b
$c*> :: forall a b. NameM a -> NameM b -> NameM b
liftA2 :: (a -> b -> c) -> NameM a -> NameM b -> NameM c
$cliftA2 :: forall a b c. (a -> b -> c) -> NameM a -> NameM b -> NameM c
<*> :: NameM (a -> b) -> NameM a -> NameM b
$c<*> :: forall a b. NameM (a -> b) -> NameM a -> NameM b
pure :: a -> NameM a
$cpure :: forall a. a -> NameM a
$cp1Applicative :: Functor NameM
Applicative, Applicative NameM
a -> NameM a
Applicative NameM
-> (forall a b. NameM a -> (a -> NameM b) -> NameM b)
-> (forall a b. NameM a -> NameM b -> NameM b)
-> (forall a. a -> NameM a)
-> Monad NameM
NameM a -> (a -> NameM b) -> NameM b
NameM a -> NameM b -> NameM b
forall a. a -> NameM a
forall a b. NameM a -> NameM b -> NameM b
forall a b. NameM a -> (a -> NameM b) -> NameM b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> NameM a
$creturn :: forall a. a -> NameM a
>> :: NameM a -> NameM b -> NameM b
$c>> :: forall a b. NameM a -> NameM b -> NameM b
>>= :: NameM a -> (a -> NameM b) -> NameM b
$c>>= :: forall a b. NameM a -> (a -> NameM b) -> NameM b
$cp1Monad :: Applicative NameM
Monad)

runNameM :: [Name] -> NameM a -> a
runNameM :: [Name] -> NameM a -> a
runNameM [Name]
xs NameM a
m =
  State Int64 a -> Int64 -> a
forall s a. State s a -> s -> a
evalState (NameM a -> State Int64 a
forall a. NameM a -> State Int64 a
unNameM NameM a
m) ([Int64] -> Int64
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum (Int64
0Int64 -> [Int64] -> [Int64]
forall a. a -> [a] -> [a]
:[ Int64 -> Int64
forall a. Enum a => a -> a
succ Int64
n | Unique Int64
n Symbol
_ Maybe String
_ Renamer
_ <- [Name]
xs ]))

newName :: Named a => a -> NameM Name
newName :: a -> NameM Name
newName a
x = State Int64 Name -> NameM Name
forall a. State Int64 a -> NameM a
NameM (State Int64 Name -> NameM Name) -> State Int64 Name -> NameM Name
forall a b. (a -> b) -> a -> b
$ do
  Int64
idx <- StateT Int64 Identity Int64
forall (m :: * -> *) s. Monad m => StateT s m s
get
  let idx' :: Int64
idx' = Int64
idxInt64 -> Int64 -> Int64
forall a. Num a => a -> a -> a
+Int64
1
  Bool -> StateT Int64 Identity () -> StateT Int64 Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int64
idx' Int64 -> Int64 -> Bool
forall a. Ord a => a -> a -> Bool
< Int64
0) (StateT Int64 Identity () -> StateT Int64 Identity ())
-> StateT Int64 Identity () -> StateT Int64 Identity ()
forall a b. (a -> b) -> a -> b
$ String -> StateT Int64 Identity ()
forall a. HasCallStack => String -> a
error String
"Name.newName: too many names"
  Int64 -> StateT Int64 Identity ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int64 -> StateT Int64 Identity ())
-> Int64 -> StateT Int64 Identity ()
forall a b. (a -> b) -> a -> b
$! Int64
idx'
  Name -> State Int64 Name
forall (m :: * -> *) a. Monad m => a -> m a
return (Name -> State Int64 Name) -> Name -> State Int64 Name
forall a b. (a -> b) -> a -> b
$! Int64 -> Symbol -> Maybe String -> Renamer -> Name
Unique Int64
idx' (String -> Symbol
intern (a -> String
forall a. Named a => a -> String
base a
x)) (a -> Maybe String
forall a. Named a => a -> Maybe String
label a
x) (a -> Renamer
forall a. Named a => a -> Renamer
renamer a
x)