more Isabelle/Haskell operations;
authorwenzelm
Wed, 25 Aug 2021 17:46:53 +0200
changeset 74196 6dc7ff326906
parent 74195 30e2e44baa57
child 74197 1f78a40e4399
more Isabelle/Haskell operations;
src/Tools/Haskell/Haskell.thy
--- 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)