# HG changeset patch
# User wenzelm
# Date 1632144420 -7200
# Node ID 9dca3df78b6af1512228165217dd863ba9335e5a
# Parent  b8a191ce08aabb6f0bb652aff4bd084e7897cac9
more operations from Isabelle/ML;

diff -r b8a191ce08aa -r 9dca3df78b6a src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Sep 20 15:11:13 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Mon Sep 20 15:27:00 2021 +0200
@@ -238,7 +238,8 @@
 module Isabelle.Library (
   (|>), (|->), (#>), (#->),
 
-  fold, fold_rev, single, the_single, singletonM, map_index, get_index, separate,
+  fold, fold_rev, fold_map, single, the_single, singletonM,
+  map_index, get_index, separate,
 
   StringLike, STRING (..), TEXT (..), BYTES (..),
   show_bytes, show_text,
@@ -287,6 +288,14 @@
 fold_rev _ [] y = y
 fold_rev f (x : xs) y = f x (fold_rev f xs y)
 
+fold_map :: (a -> b -> (c, b)) -> [a] -> b -> ([c], b)
+fold_map _ [] y = ([], y)
+fold_map f (x : xs) y =
+  let
+    (x', y') = f x y
+    (xs', y'') = fold_map f xs y'
+  in (x' : xs', y'')
+
 single :: a -> [a]
 single x = [x]
 
@@ -2169,7 +2178,8 @@
   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
+  Context, declare, declare_renaming, is_declared, declared, context, make_context,
+  variant, variant_list
 )
 where
 
@@ -2287,6 +2297,9 @@
             |> 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)
 \<close>
 
 generate_file "Isabelle/Term.hs" = \<open>