-- | This module provides a way to generate infinitely many distinct
-- concrete variable names from a list of name suggestions.
--
-- Since bound atoms must sometimes be renamed, we need a way to
-- generate suitable concrete names.  This should be configurable on a
-- per-atom basis, with a fallback default behavior for each atom
-- type.
--
-- A name suggestion is a list of possible names. The first useable
-- name from the list is chosen. If the list is finite and contains no
-- useable names, then we will generate more names by appending
-- numerical subscripts. A client can override this default behavior
-- by specifying an infinite list of name suggestions.
--
-- An empty list of name suggestions counts as no suggestion, in which
-- case a default will be used.
--
-- When merging two atoms (see 'Nominal.merge'), we concatenate their
-- name suggestions. In particular, if one name has a user-specified
-- suggestion and the other one does not, we always use the
-- user-specified one.
--
-- This module exposes implementation details of the Nominal library,
-- and should not normally be imported. Users of the library should
-- only import the top-level module "Nominal".

module Nominal.ConcreteNames where

import Data.Char
import Data.List
import Data.Set (Set)
import qualified Data.Set as Set

-- | A name suggestion is a list of possible names. When an atom must
-- be renamed, the first useable name from the list is chosen. If the
-- list is finite and contains no useable names, then additional names
-- will be generated by appending numerical subscripts. To override
-- this behavior, redefine 'Nominal.expand_names' for the given
-- 'AtomKind' instance, or specify an infinite list of names.
type NameSuggestion = [String]

-- | The names to use if nothing else was specified.
default_names :: NameSuggestion
default_names :: NameSuggestion
default_names = [String
"x", String
"y", String
"z", String
"u", String
"v", String
"w", String
"r", String
"s", String
"t", String
"p", String
"q"]

-- | Convert a digit to a subscript.
to_subscript :: Char -> Char
to_subscript :: Char -> Char
to_subscript Char
'0' = Char
'₀'
to_subscript Char
'1' = Char
'₁'
to_subscript Char
'2' = Char
'₂'
to_subscript Char
'3' = Char
'₃'
to_subscript Char
'4' = Char
'₄'
to_subscript Char
'5' = Char
'₅'
to_subscript Char
'6' = Char
'₆'
to_subscript Char
'7' = Char
'₇'
to_subscript Char
'8' = Char
'₈'
to_subscript Char
'9' = Char
'₉'
to_subscript Char
c = Char
c

-- | Check if a character is a letter or underscore.
isAlphaOrWild :: Char -> Bool
isAlphaOrWild :: Char -> Bool
isAlphaOrWild Char
c = Char -> Bool
isAlpha Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_'

-- | Generate an infinite list of possible names from a (possibly
-- finite) list of suggestions.
expand_default :: NameSuggestion -> [String]
expand_default :: NameSuggestion -> NameSuggestion
expand_default NameSuggestion
xs0 = NameSuggestion
xs1 NameSuggestion -> NameSuggestion -> NameSuggestion
forall a. [a] -> [a] -> [a]
++ NameSuggestion
xs3 NameSuggestion -> NameSuggestion -> NameSuggestion
forall a. [a] -> [a] -> [a]
++ [ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Char -> Char) -> String -> String
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
to_subscript (Integer -> String
forall a. Show a => a -> String
show Integer
n) | Integer
n <- [Integer
1..] :: [Integer], String
x <- NameSuggestion
xs3 ]
  where
    xs1 :: NameSuggestion
xs1 = [ String
x | String
x <- NameSuggestion
xs0, String
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"" ]
    xs2 :: NameSuggestion
xs2 = [ String
y | String
x <- NameSuggestion
xs0, let y :: String
y = (Char -> Bool) -> String -> String
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAlphaOrWild String
x, String
y String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"" ]
    xs3 :: NameSuggestion
xs3 = if NameSuggestion -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null NameSuggestion
xs2 then NameSuggestion
default_names else NameSuggestion
xs2

-- | A name generator consists of a (possibly finite) list of name
-- suggestions and an /expander/, which is a function for generating
-- more names.
data NameGen = NameGen NameSuggestion (NameSuggestion -> [String])

-- | The default name generator.
default_namegen :: NameGen
default_namegen :: NameGen
default_namegen = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen NameSuggestion
default_names NameSuggestion -> NameSuggestion
expand_default

-- | Compute a string that is not in the given set, and whose name is
-- based on the supplied suggestions.
rename_fresh :: Set String -> NameGen -> String
rename_fresh :: Set String -> NameGen -> String
rename_fresh Set String
as (NameGen NameSuggestion
ns NameSuggestion -> NameSuggestion
expander) = String
n'
  where
    n' :: String
n' = NameSuggestion -> String
forall a. HasCallStack => [a] -> a
head [ String
x | String
x <- NameSuggestion -> NameSuggestion
expand_default (NameSuggestion
ns' NameSuggestion -> NameSuggestion -> NameSuggestion
forall a. [a] -> [a] -> [a]
++ NameSuggestion -> NameSuggestion
expander NameSuggestion
ns'), Bool -> Bool
not (String -> Bool
used String
x) ]
    ns' :: NameSuggestion
ns' = if NameSuggestion -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null NameSuggestion
ns then NameSuggestion
default_names else NameSuggestion
ns
    used :: String -> Bool
used String
x = String
x String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set String
as

-- | Merge two name suggestions. Essentially this appends them, but we
-- try to avoid duplication. We use the left expander.
combine_names :: NameGen -> NameGen -> NameGen
combine_names :: NameGen -> NameGen -> NameGen
combine_names (NameGen NameSuggestion
xs NameSuggestion -> NameSuggestion
ex1) (NameGen NameSuggestion
ys NameSuggestion -> NameSuggestion
ex2) = NameSuggestion -> (NameSuggestion -> NameSuggestion) -> NameGen
NameGen (NameSuggestion
xs NameSuggestion -> NameSuggestion -> NameSuggestion
forall a. [a] -> [a] -> [a]
++ (NameSuggestion
ys NameSuggestion -> NameSuggestion -> NameSuggestion
forall a. Eq a => [a] -> [a] -> [a]
\\ NameSuggestion
xs)) NameSuggestion -> NameSuggestion
ex1