{- generated by Isabelle -}

   Title :       Isabelle / Name.hs 
     Author :      Makarius 

 Names of basic logical entities ( variables etc . ) . 

 See " $ ISABELLE_HOME / src / Pure / name . ML " . 

    Author:     Makarius

Names of basic logical entities (variables etc.).

See "$ISABELLE_HOME/src/Pure/name.ML".
-}

{-# LANGUAGE OverloadedStrings #-}

module Isabelle.Name (
  Name,
  uu, uu_, aT,
  clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
  Context, declare, declare_renaming, is_declared, declared, context, make_context,
  variant, variant_list
)
where

import Data.Maybe (fromMaybe)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Word (Word8)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Symbol as Symbol
import Isabelle.Library


type Name = Bytes


{- common defaults -}

uu, uu_, aT :: Name
uu = "uu"
uu_ = "uu_"
aT = "'a"


{- internal names -- NB: internal subsumes skolem -}

underscore :: Word8
underscore = Bytes.byte '_'

internal, skolem :: Name -> Name
internal x = x <> "_"
skolem x = x <> "__"

is_internal, is_skolem :: Name -> Bool
is_internal = Bytes.isSuffixOf "_"
is_skolem = Bytes.isSuffixOf "__"

dest_internal, dest_skolem :: Name -> Maybe Name
dest_internal = Bytes.try_unsuffix "_"
dest_skolem = Bytes.try_unsuffix "__"

clean_index :: (Name, Int) -> (Name, Int)
clean_index (x, i) =
  case dest_internal x of
    Nothing -> (x, i)
    Just x' -> clean_index (x', i + 1)

clean :: Name -> Name
clean x = fst (clean_index (x, 0))


{- context for used names -}

newtype Context = Context (Map Name (Maybe Name))  {-declared names with latest renaming-}

declare :: Name -> Context -> Context
declare x (Context names) =
  Context (
    let a = clean x
    in if Map.member a names then names else Map.insert a Nothing names)

declare_renaming :: (Name, Name) -> Context -> Context
declare_renaming (x, x') (Context names) =
  Context (Map.insert (clean x) (Just (clean x')) names)

is_declared :: Context -> Name -> Bool
is_declared (Context names) x = Map.member x names

declared :: Context -> Name -> Maybe (Maybe Name)
declared (Context names) a = Map.lookup a names

context :: Context
context = Context Map.empty |> fold declare ["", "'"]

make_context :: [Name] -> Context
make_context used = fold declare used context


{- generating fresh names -}

bump_init :: Name -> Name
bump_init str = str <> "a"

bump_string :: Name -> Name
bump_string str =
  let
    a = Bytes.byte 'a'
    z = Bytes.byte 'z'
    bump (b : bs) | b == z = a : bump bs
    bump (b : bs) | a <= b && b < z = b + 1 : bs
    bump bs = a : bs

    rev = reverse (Bytes.unpack str)
    part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev)
    part1 = reverse (bump (drop (length part2) rev))
  in Bytes.pack (part1 <> part2)

variant :: Name -> Context -> (Name, Context)
variant name ctxt =
  let
    vary x =
      case declared ctxt x of
        Nothing -> x
        Just x' -> vary (bump_string (fromMaybe x x'))

    (x, n) = clean_index (name, 0)
    (x', ctxt') =
      if not (is_declared ctxt x) then (x, declare x ctxt)
      else
        let
          x0 = bump_init x
          x' = vary x0
          ctxt' = ctxt
            |> (if x0 /= x' then declare_renaming (x0, x') else id)
            |> declare x'
        in (x', ctxt')
  in (x' <> Bytes.pack (replicate n underscore), ctxt')

variant_list :: [Name] -> [Name] -> [Name]
variant_list used names = fst (make_context used |> fold_map variant names)

 generated by Isabelle 
# LANGUAGE OverloadedStrings #
 common defaults 
 internal names -- NB: internal subsumes skolem 
 context for used names 
declared names with latest renaming
 generating fresh names 

   Title :       Isabelle / Name.hs 
     Author :      Makarius 

 Names of basic logical entities ( variables etc . ) . 

 See " $ ISABELLE_HOME / src / Pure / name . ML " . 

    Author:     Makarius

Names of basic logical entities (variables etc.).

See "$ISABELLE_HOME/src/Pure/name.ML".
-}


module Isabelle.Name (
  Name,
  uu, uu_, aT,
  clean_index, clean, internal, skolem, is_internal, is_skolem, dest_internal, dest_skolem,
  Context, declare, declare_renaming, is_declared, declared, context, make_context,
  variant, variant_list
)
where

import Data.Maybe (fromMaybe)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Word (Word8)
import qualified Isabelle.Bytes as Bytes
import Isabelle.Bytes (Bytes)
import qualified Isabelle.Symbol as Symbol
import Isabelle.Library


type Name = Bytes



uu, uu_, aT :: Name
uu = "uu"
uu_ = "uu_"
aT = "'a"



underscore :: Word8
underscore = Bytes.byte '_'

internal, skolem :: Name -> Name
internal x = x <> "_"
skolem x = x <> "__"

is_internal, is_skolem :: Name -> Bool
is_internal = Bytes.isSuffixOf "_"
is_skolem = Bytes.isSuffixOf "__"

dest_internal, dest_skolem :: Name -> Maybe Name
dest_internal = Bytes.try_unsuffix "_"
dest_skolem = Bytes.try_unsuffix "__"

clean_index :: (Name, Int) -> (Name, Int)
clean_index (x, i) =
  case dest_internal x of
    Nothing -> (x, i)
    Just x' -> clean_index (x', i + 1)

clean :: Name -> Name
clean x = fst (clean_index (x, 0))




declare :: Name -> Context -> Context
declare x (Context names) =
  Context (
    let a = clean x
    in if Map.member a names then names else Map.insert a Nothing names)

declare_renaming :: (Name, Name) -> Context -> Context
declare_renaming (x, x') (Context names) =
  Context (Map.insert (clean x) (Just (clean x')) names)

is_declared :: Context -> Name -> Bool
is_declared (Context names) x = Map.member x names

declared :: Context -> Name -> Maybe (Maybe Name)
declared (Context names) a = Map.lookup a names

context :: Context
context = Context Map.empty |> fold declare ["", "'"]

make_context :: [Name] -> Context
make_context used = fold declare used context



bump_init :: Name -> Name
bump_init str = str <> "a"

bump_string :: Name -> Name
bump_string str =
  let
    a = Bytes.byte 'a'
    z = Bytes.byte 'z'
    bump (b : bs) | b == z = a : bump bs
    bump (b : bs) | a <= b && b < z = b + 1 : bs
    bump bs = a : bs

    rev = reverse (Bytes.unpack str)
    part2 = reverse (takeWhile (Symbol.is_ascii_quasi . Bytes.char) rev)
    part1 = reverse (bump (drop (length part2) rev))
  in Bytes.pack (part1 <> part2)

variant :: Name -> Context -> (Name, Context)
variant name ctxt =
  let
    vary x =
      case declared ctxt x of
        Nothing -> x
        Just x' -> vary (bump_string (fromMaybe x x'))

    (x, n) = clean_index (name, 0)
    (x', ctxt') =
      if not (is_declared ctxt x) then (x, declare x ctxt)
      else
        let
          x0 = bump_init x
          x' = vary x0
          ctxt' = ctxt
            |> (if x0 /= x' then declare_renaming (x0, x') else id)
            |> declare x'
        in (x', ctxt')
  in (x' <> Bytes.pack (replicate n underscore), ctxt')

variant_list :: [Name] -> [Name] -> [Name]
variant_list used names = fst (make_context used |> fold_map variant names)
