# HG changeset patch
# User wenzelm
# Date 1627834352 -7200
# Node ID 0bda15b1b937ff670663634a22e8b9223edce58f
# Parent  5aaccec7c1a109c765f6d93f8ecaacc03c3d30bc
clarified signature;

diff -r 5aaccec7c1a1 -r 0bda15b1b937 src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Sun Aug 01 16:12:08 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Sun Aug 01 18:12:32 2021 +0200
@@ -23,8 +23,8 @@
   Bytes,
   make, unmake, pack, unpack,
   empty, null, length, index, all, any,
-  head, last, take, drop, concat,
-  space, spaces, singleton, char, byte,
+  head, last, take, drop, isPrefixOf, isSuffixOf,
+  concat, space, spaces, singleton, char, byte,
   trim_line, space_explode, split_lines
 )
 where
@@ -84,6 +84,16 @@
 drop :: Int -> Bytes -> Bytes
 drop n = pack . List.drop n . unpack
 
+isPrefixOf :: Bytes -> Bytes -> Bool
+isPrefixOf bs1 bs2 =
+  n1 <= n2 && List.all (\i -> index bs1 i == index bs2 i) [0 .. n1 - 1]
+  where n1 = length bs1; n2 = length bs2
+
+isSuffixOf :: Bytes -> Bytes -> Bool
+isSuffixOf bs1 bs2 =
+  n1 <= n2 && List.all (\i -> index bs1 i == index bs2 (i + k)) [0 .. n1 - 1]
+  where n1 = length bs1; n2 = length bs2; k = n2 - n1
+
 concat :: [Bytes] -> Bytes
 concat = mconcat
 
@@ -233,7 +243,7 @@
   StringLike, STRING (..), TEXT (..), BYTES (..),
 
   proper_string, quote, space_implode, commas, commas_quote, cat_lines,
-  space_explode, split_lines, trim_line, clean_name)
+  space_explode, split_lines, trim_line)
 where
 
 import qualified Data.Text as Text
@@ -366,9 +376,6 @@
       '\n' : rest -> reverse rest
       _ -> line
   else line
-
-clean_name :: String -> String
-clean_name = reverse #> dropWhile (== '_') #> reverse
 \<close>
 
 
@@ -1514,8 +1521,6 @@
     Name, T, names, none, make, markup_element, markup_report, make_report
   ) where
 
-import qualified Data.List as List
-
 import Isabelle.Library
 import qualified Isabelle.Bytes as Bytes
 import Isabelle.Bytes (Bytes)
@@ -1535,10 +1540,17 @@
 none :: T
 none = names 0 [] []
 
+clean_name :: Bytes -> Bytes
+clean_name bs =
+  if not (Bytes.null bs) && Bytes.last bs == u then
+    Bytes.unpack bs |> reverse |> dropWhile (== u) |> reverse |> Bytes.pack
+  else bs
+  where u = Bytes.byte '_'
+
 make :: Int -> (Bytes, Properties.T) -> ((Bytes -> Bool) -> [Name]) -> T
 make limit (name, props) make_names =
   if name /= "" && name /= "_" then
-    names limit props (make_names (List.isPrefixOf (clean_name (make_string name)) . make_string))
+    names limit props (make_names (Bytes.isPrefixOf (clean_name name)))
   else none
 
 markup_element :: T -> (Markup.T, XML.Body)