--- a/src/Tools/Haskell/Haskell.thy Wed Aug 25 17:27:40 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy Wed Aug 25 17:46:53 2021 +0200
@@ -2116,7 +2116,7 @@
module Isabelle.Name (
Name,
uu, uu_, aT,
- clean_index, clean,
+ clean_index, clean, internal, skolem, is_internal, is_skolem,
Context, declare, is_declared, context, make_context, variant
)
where
@@ -2141,11 +2141,19 @@
aT = "'a"
-{- suffix for internal names -}
+{- 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 "__"
+
clean_index :: Name -> (Name, Int)
clean_index x =
if Bytes.null x || Bytes.last x /= underscore then (x, 0)