src/Tools/Haskell/Haskell.thy

 
 module Isabelle.Completion (
     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
 import qualified Isabelle.XML as XML
 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)
 markup_element (Completion props total names) =
   if not (null names) then

           (Encode.list (Encode.pair Encode.string (Encode.pair Encode.string Encode.string)))
           (total, names)
     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>
 
 generate_file "Isabelle/File.hs" = \<open>

 
 big_list :: BYTES a => a -> [T] -> T
 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
     LICENSE:    BSD 3-clause (Isabelle)
 

 -}
 
 {-# 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 --->
 
 
 {- types and terms -}
-
-type Name = Bytes
 
 type Indexname = (Name, Int)
 
 type Sort = [Name]
 

   | Bound Int
   | Abs (Name, Typ, Term)
   | App (Term, Term)
   deriving (Show, Eq, Ord)
 
+
+{- free and bound variables -}
+
 type Free = (Name, Typ)
-
-
-{- type and term operators -}
-
-type_op0 :: Name -> (Typ, Typ -> Bool)
-type_op0 name = (mk, is)
-  where
-    mk = Type (name, [])
-    is (Type (name, _)) = True
-    is _ = False
-
-type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ)
-type_op1 name = (mk, dest)
-  where
-    mk ty = Type (name, [ty])
-    dest (Type (name, [ty])) = Just ty
-    dest _ = Nothing
-
-type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ))
-type_op2 name = (mk, dest)
-  where
-    mk ty1 ty2 = Type (name, [ty1, ty2])
-    dest (Type (name, [ty1, ty2])) = Just (ty1, ty2)
-    dest _ = Nothing
-
-op0 :: Name -> (Term, Term -> Bool)
-op0 name = (mk, is)
-  where
-    mk = Const (name, [])
-    is (Const (c, _)) = c == name
-    is _ = False
-
-op1 :: Name -> (Term -> Term, Term -> Maybe Term)
-op1 name = (mk, dest)
-  where
-    mk t = App (Const (name, []), t)
-    dest (App (Const (c, _), t)) | c == name = Just t
-    dest _ = Nothing
-
-op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term))
-op2 name = (mk, dest)
-  where
-    mk t u = App (App (Const (name, []), t), u)
-    dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
-    dest _ = Nothing
-
-typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
-typed_op2 name = (mk, dest)
-  where
-    mk ty t u = App (App (Const (name, [ty]), t), u)
-    dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u)
-    dest _ = Nothing
-
-binder :: Name -> Free -> Term -> Term
-binder c (a, ty) b = App (Const (c, [ty]), lambda (a, ty) b)
-
-
-{- type operations -}
-
-dummyS :: Sort
-dummyS = [""]
-
-dummyT :: Typ; is_dummyT :: Typ -> Bool
-(dummyT, is_dummyT) = type_op0 \<open>\<^type_name>\<open>dummy\<close>\<close>
-
-propT :: Typ; is_propT :: Typ -> Bool
-(propT, is_propT) = type_op0 \<open>\<^type_name>\<open>prop\<close>\<close>
-
-(-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ)
-((-->), dest_funT) = type_op2 \<open>\<^type_name>\<open>fun\<close>\<close>
-
-(--->) :: [Typ] -> Typ -> Typ
-[] ---> b = b
-(a : as) ---> b = a --> (as ---> b)
-
-
-{- term operations -}
-
-aconv :: Term -> Term -> Bool
-aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2
-aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2
-aconv a1 a2 = a1 == a2
-
-list_comb :: Term -> [Term] -> Term
-list_comb f [] = f
-list_comb f (t : ts) = list_comb (App (f, t)) ts
-
-strip_comb :: Term -> (Term, [Term])
-strip_comb tm = strip (tm, [])
-  where
-    strip (App (f, t), ts) = strip (f, t : ts)
-    strip x = x
-
-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
+
+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 -}
+
+type_op0 :: Name -> (Typ, Typ -> Bool)
+type_op0 name = (mk, is)
+  where
+    mk = Type (name, [])
+    is (Type (name, _)) = True
+    is _ = False
+
+type_op1 :: Name -> (Typ -> Typ, Typ -> Maybe Typ)
+type_op1 name = (mk, dest)
+  where
+    mk ty = Type (name, [ty])
+    dest (Type (name, [ty])) = Just ty
+    dest _ = Nothing
+
+type_op2 :: Name -> (Typ -> Typ -> Typ, Typ -> Maybe (Typ, Typ))
+type_op2 name = (mk, dest)
+  where
+    mk ty1 ty2 = Type (name, [ty1, ty2])
+    dest (Type (name, [ty1, ty2])) = Just (ty1, ty2)
+    dest _ = Nothing
+
+op0 :: Name -> (Term, Term -> Bool)
+op0 name = (mk, is)
+  where
+    mk = Const (name, [])
+    is (Const (c, _)) = c == name
+    is _ = False
+
+op1 :: Name -> (Term -> Term, Term -> Maybe Term)
+op1 name = (mk, dest)
+  where
+    mk t = App (Const (name, []), t)
+    dest (App (Const (c, _), t)) | c == name = Just t
+    dest _ = Nothing
+
+op2 :: Name -> (Term -> Term -> Term, Term -> Maybe (Term, Term))
+op2 name = (mk, dest)
+  where
+    mk t u = App (App (Const (name, []), t), u)
+    dest (App (App (Const (c, _), t), u)) | c == name = Just (t, u)
+    dest _ = Nothing
+
+typed_op2 :: Name -> (Typ -> Term -> Term -> Term, Term -> Maybe (Typ, Term, Term))
+typed_op2 name = (mk, dest)
+  where
+    mk ty t u = App (App (Const (name, [ty]), t), u)
+    dest (App (App (Const (c, [ty]), t), u)) | c == name = Just (ty, t, u)
+    dest _ = Nothing
+
+binder :: Name -> Free -> Term -> Term
+binder c (a, ty) b = App (Const (c, [ty]), lambda (a, ty) b)
+
+
+{- type operations -}
+
+dummyS :: Sort
+dummyS = [""]
+
+dummyT :: Typ; is_dummyT :: Typ -> Bool
+(dummyT, is_dummyT) = type_op0 \<open>\<^type_name>\<open>dummy\<close>\<close>
+
+propT :: Typ; is_propT :: Typ -> Bool
+(propT, is_propT) = type_op0 \<open>\<^type_name>\<open>prop\<close>\<close>
+
+(-->) :: Typ -> Typ -> Typ; dest_funT :: Typ -> Maybe (Typ, Typ)
+((-->), dest_funT) = type_op2 \<open>\<^type_name>\<open>fun\<close>\<close>
+
+(--->) :: [Typ] -> Typ -> Typ
+[] ---> b = b
+(a : as) ---> b = a --> (as ---> b)
+
+
+{- term operations -}
+
+aconv :: Term -> Term -> Bool
+aconv (App (t1, u1)) (App (t2, u2)) = aconv t1 t2 && aconv u1 u2
+aconv (Abs (_, ty1, t1)) (Abs (_, ty2, t2)) = aconv t1 t2 && ty1 == ty2
+aconv a1 a2 = a1 == a2
+
+list_comb :: Term -> [Term] -> Term
+list_comb f [] = f
+list_comb f (t : ts) = list_comb (App (f, t)) ts
+
+strip_comb :: Term -> (Term, [Term])
+strip_comb tm = strip (tm, [])
+  where
+    strip (App (f, t), ts) = strip (f, t : ts)
+    strip x = x
+
+head_of :: Term -> Term
+head_of (App (f, _)) = head_of f
+head_of u = u
 \<close>
 
 generate_file "Isabelle/Pure.hs" = \<open>
 {-  Title:      Isabelle/Term.hs
     Author:     Makarius