--- 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>