# HG changeset patch
# User wenzelm
# Date 1627987169 -7200
# Node ID 4984fad0e91d556d2956eec48d20481cd30e9bf2
# Parent  d3d6e01a6b002929ae2bf6e7771d8ee2f32bc84c
more operations, notably free and bound variables as in Isabelle/Pure;

diff -r d3d6e01a6b00 -r 4984fad0e91d src/Tools/Haskell/Haskell.thy
--- a/src/Tools/Haskell/Haskell.thy	Mon Aug 02 17:20:16 2021 +0200
+++ b/src/Tools/Haskell/Haskell.thy	Tue Aug 03 12:39:29 2021 +0200
@@ -1521,9 +1521,9 @@
     Name, T, names, none, make, markup_element, markup_report, make_report
   ) where
 
-import Isabelle.Library
 import qualified Isabelle.Bytes as Bytes
-import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Name as Name
+import Isabelle.Name (Name)
 import qualified Isabelle.Properties as Properties
 import qualified Isabelle.Markup as Markup
 import qualified Isabelle.XML.Encode as Encode
@@ -1531,26 +1531,19 @@
 import qualified Isabelle.YXML as YXML
 
 
-type Name = (Bytes, (Bytes, Bytes))  -- external name, kind, internal name
-data T = Completion Properties.T Int [Name]  -- position, total length, names
-
-names :: Int -> Properties.T -> [Name] -> T
+type Names = [(Name, (Name, Name))]  -- external name, kind, internal name
+data T = Completion Properties.T Int Names  -- position, total length, names
+
+names :: Int -> Properties.T -> Names -> T
 names limit props names = Completion props (length names) (take limit names)
 
 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 :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> T
 make limit (name, props) make_names =
   if name /= "" && name /= "_" then
-    names limit props (make_names (Bytes.isPrefixOf (clean_name name)))
+    names limit props (make_names (Bytes.isPrefixOf (Name.clean name)))
   else none
 
 markup_element :: T -> (Markup.T, XML.Body)
@@ -1565,12 +1558,12 @@
     in (markup, body)
   else (Markup.empty, [])
 
-markup_report :: [T] -> Bytes
+markup_report :: [T] -> Name
 markup_report [] = Bytes.empty
 markup_report elems =
   YXML.string_of $ XML.Elem (Markup.report, map (XML.Elem . markup_element) elems)
 
-make_report :: Int -> (Bytes, Properties.T) -> ((Bytes -> Bool) -> [Name]) -> Bytes
+make_report :: Int -> (Name, Properties.T) -> ((Name -> Bool) -> Names) -> Name
 make_report limit name_props make_names =
   markup_report [make limit name_props make_names]
 \<close>
@@ -1760,6 +1753,100 @@
 big_list name prts = block (fbreaks (str name : prts))
 \<close>
 
+generate_file "Isabelle/Name.hs" = \<open>
+{-  Title:      Isabelle/Name.hs
+    Author:     Makarius
+
+Names of basic logical entities (variables etc.).
+
+See also \<^file>\<open>$ISABELLE_HOME/src/Pure/name.ML\<close>.
+-}
+
+{-# LANGUAGE OverloadedStrings #-}
+
+module Isabelle.Name (
+  Name, clean_index, clean,
+  Context, declare, is_declared, context, make_context, variant
+)
+where
+
+import Data.Word (Word8)
+import qualified Data.Set as Set
+import Data.Set (Set)
+import qualified Isabelle.Bytes as Bytes
+import Isabelle.Bytes (Bytes)
+import qualified Isabelle.Symbol as Symbol
+import Isabelle.Library
+
+
+type Name = Bytes
+
+
+{- suffix for internal names -}
+
+underscore :: Word8
+underscore = Bytes.byte '_'
+
+clean_index :: Name -> (Name, Int)
+clean_index x =
+  if Bytes.null x || Bytes.last x /= underscore then (x, 0)
+  else
+    let
+      rev = reverse (Bytes.unpack x)
+      n = length (takeWhile (== underscore) rev)
+      y = Bytes.pack (reverse (drop n rev))
+    in (y, n)
+
+clean :: Name -> Name
+clean = fst . clean_index
+
+
+{- context for used names -}
+
+data Context = Context (Set Name)
+
+declare :: Name -> Context -> Context
+declare x (Context names) = Context (Set.insert x names)
+
+is_declared :: Context -> Name -> Bool
+is_declared (Context names) x = Set.member x names
+
+context :: Context
+context = Context (Set.fromList ["", "'"])
+
+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 names =
+  let
+    vary bump x = if is_declared names x then bump x |> vary bump_string else x
+    (x, n) = clean_index name
+    x' = x |> vary bump_init
+    names' = declare x' names;
+  in (x' <> Bytes.pack (replicate n underscore), names')
+\<close>
+
 generate_file "Isabelle/Term.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius
@@ -1773,14 +1860,17 @@
 {-# LANGUAGE OverloadedStrings #-}
 
 module Isabelle.Term (
-  Name, Indexname, Sort, Typ(..), Term(..), Free,
+  Indexname, Sort, Typ(..), Term(..),
+  Free, lambda, declare_frees, incr_boundvars, subst_bound, dest_abs,
   type_op0, type_op1, op0, op1, op2, typed_op2, binder,
   dummyS, dummyT, is_dummyT, propT, is_propT, (-->), dest_funT, (--->),
-  aconv, list_comb, strip_comb, head_of, lambda
+  aconv, list_comb, strip_comb, head_of
 )
 where
 
-import Isabelle.Bytes (Bytes)
+import Isabelle.Library
+import qualified Isabelle.Name as Name
+import Isabelle.Name (Name)
 
 infixr 5 -->
 infixr --->
@@ -1788,8 +1878,6 @@
 
 {- types and terms -}
 
-type Name = Bytes
-
 type Indexname = (Name, Int)
 
 type Sort = [Name]
@@ -1809,8 +1897,52 @@
   | App (Term, Term)
   deriving (Show, Eq, Ord)
 
+
+{- free and bound variables -}
+
 type Free = (Name, Typ)
 
+lambda :: Free -> Term -> Term
+lambda (name, typ) body = Abs (name, typ, abstract 0 body)
+  where
+    abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
+    abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
+    abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
+    abstract _ t = t
+
+declare_frees :: Term -> Name.Context -> Name.Context
+declare_frees (Free (x, _)) = Name.declare x
+declare_frees (Abs (_, _, b)) = declare_frees b
+declare_frees (App (t, u)) = declare_frees t #> declare_frees u
+declare_frees _ = id
+
+incr_boundvars :: Int -> Term -> Term
+incr_boundvars inc = if inc == 0 then id else incr 0
+  where
+    incr lev (Bound i) = if i >= lev then Bound (i + inc) else Bound i
+    incr lev (Abs (a, ty, b)) = Abs (a, ty, incr (lev + 1) b)
+    incr lev (App (t, u)) = App (incr lev t, incr lev u)
+    incr _ t = t
+
+subst_bound :: Term -> Term -> Term
+subst_bound arg = subst 0
+  where
+    subst lev (Bound i) =
+      if i < lev then Bound i
+      else if i == lev then incr_boundvars lev arg
+      else Bound (i - 1)
+    subst lev (Abs (a, ty, b)) = Abs (a, ty, subst (lev + 1) b)
+    subst lev (App (t, u)) = App (subst lev t, subst lev u)
+    subst _ t = t
+
+dest_abs :: Name.Context -> Term -> Maybe (Free, Term)
+dest_abs names (Abs (x, ty, b)) =
+  let
+    (x', _) = Name.variant x (declare_frees b names)
+    v = (x', ty)
+  in Just (v, subst_bound (Free v) b)
+dest_abs _ _ = Nothing
+
 
 {- type and term operators -}
 
@@ -1906,14 +2038,6 @@
 head_of :: Term -> Term
 head_of (App (f, _)) = head_of f
 head_of u = u
-
-lambda :: Free -> Term -> Term
-lambda (name, typ) body = Abs (name, typ, abstract 0 body)
-  where
-    abstract lev (Free (x, ty)) | name == x && typ == ty = Bound lev
-    abstract lev (Abs (a, ty, t)) = Abs (a, ty, abstract (lev + 1) t)
-    abstract lev (App (t, u)) = App (abstract lev t, abstract lev u)
-    abstract _ t = t
 \<close>
 
 generate_file "Isabelle/Pure.hs" = \<open>