# HG changeset patch
# User wenzelm
# Date 1265060772 -3600
# Node ID c4c02ac736a6684d634b402e8d482352166e15cd
# Parent  19294b07e445d2e4919d0f79ee54a6aec83bd00f
more details on long names, binding/naming, name space;
tuned;

diff -r 19294b07e445 -r c4c02ac736a6 doc-src/IsarImplementation/Thy/Local_Theory.thy
--- a/doc-src/IsarImplementation/Thy/Local_Theory.thy	Sun Jan 31 22:08:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Local_Theory.thy	Mon Feb 01 22:46:12 2010 +0100
@@ -2,7 +2,7 @@
 imports Base
 begin
 
-chapter {* Local theory specifications *}
+chapter {* Local theory specifications \label{ch:local-theory} *}
 
 text {*
   A \emph{local theory} combines aspects of both theory and proof
diff -r 19294b07e445 -r c4c02ac736a6 doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sun Jan 31 22:08:25 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Mon Feb 01 22:46:12 2010 +0100
@@ -492,10 +492,28 @@
 
 text {* In principle, a name is just a string, but there are various
   conventions for representing additional structure.  For example,
-  ``@{text "Foo.bar.baz"}'' is considered as a qualified name
-  consisting of three basic name components.  The individual
-  constituents of a name may have further substructure, e.g.\ the
-  string ``\verb,\,\verb,<alpha>,'' encodes as a single symbol.
+  ``@{text "Foo.bar.baz"}'' is considered as a long name consisting of
+  qualifier @{text "Foo.bar"} and base name @{text "baz"}.  The
+  individual constituents of a name may have further substructure,
+  e.g.\ the string ``\verb,\,\verb,<alpha>,'' encodes as a single
+  symbol.
+
+  \medskip Subsequently, we shall introduce specific categories of
+  names.  Roughly speaking these correspond to logical entities as
+  follows:
+  \begin{itemize}
+
+  \item Basic names (\secref{sec:basic-name}): free and bound
+  variables.
+
+  \item Indexed names (\secref{sec:indexname}): schematic variables.
+
+  \item Long names (\secref{sec:long-name}): constants of any kind
+  (type constructors, term constants, other concepts defined in user
+  space).  Such entities are typically managed via name spaces
+  (\secref{sec:name-space}).
+
+  \end{itemize}
 *}
 
 
@@ -606,15 +624,15 @@
   primitive ML type @{ML_type char} did not exists, and the basic @{ML
   "explode: string -> string list"} operation would produce a list of
   singleton strings as in Isabelle/ML today.  When SML97 came out,
-  Isabelle ignored its slightly anachronistic 8-bit characters, but
-  the idea of exploding a string into a list of small strings was
+  Isabelle did not adopt its slightly anachronistic 8-bit characters,
+  but the idea of exploding a string into a list of small strings was
   extended to ``symbols'' as explained above.  Thus Isabelle sources
   can refer to an infinite store of user-defined symbols, without
   having to worry about the multitude of Unicode encodings.
 *}
 
 
-subsection {* Basic names \label{sec:basic-names} *}
+subsection {* Basic names \label{sec:basic-name} *}
 
 text {*
   A \emph{basic name} essentially consists of a single Isabelle
@@ -699,7 +717,7 @@
 *}
 
 
-subsection {* Indexed names *}
+subsection {* Indexed names \label{sec:indexname} *}
 
 text {*
   An \emph{indexed name} (or @{text "indexname"}) is a pair of a basic
@@ -711,9 +729,9 @@
   @{text "maxidx + 1"}; the maximum index of an empty collection is
   @{text "-1"}.
 
-  Occasionally, basic names and indexed names are injected into the
-  same pair type: the (improper) indexname @{text "(x, -1)"} is used
-  to encode the basic name @{text "x"}.
+  Occasionally, basic names are injected into the same pair type of
+  indexed names: then @{text "(x, -1)"} is used to encode the basic
+  name @{text "x"}.
 
   \medskip Isabelle syntax observes the following rules for
   representing an indexname @{text "(x, i)"} as a packed string:
@@ -728,11 +746,12 @@
 
   \end{itemize}
 
-  Indexnames may acquire large index numbers over time.  Results are
-  normalized towards @{text "0"} at certain checkpoints, notably at
-  the end of a proof.  This works by producing variants of the
-  corresponding basic name components.  For example, the collection
-  @{text "?x1, ?x7, ?x42"} becomes @{text "?x, ?xa, ?xb"}.
+  Indexnames may acquire large index numbers after several maxidx
+  shifts have been applied.  Results are usually normalized towards
+  @{text "0"} at certain checkpoints, notably at the end of a proof.
+  This works by producing variants of the corresponding basic name
+  components.  For example, the collection @{text "?x1, ?x7, ?x42"}
+  becomes @{text "?x, ?xa, ?xb"}.
 *}
 
 text %mlref {*
@@ -752,59 +771,28 @@
 *}
 
 
-subsection {* Qualified names and name spaces *}
+subsection {* Long names \label{sec:long-name} *}
 
-text {*
-  A \emph{qualified name} consists of a non-empty sequence of basic
-  name components.  The packed representation uses a dot as separator,
-  as in ``@{text "A.b.c"}''.  The last component is called \emph{base}
-  name, the remaining prefix \emph{qualifier} (which may be empty).
-  The idea of qualified names is to encode nested structures by
-  recording the access paths as qualifiers.  For example, an item
-  named ``@{text "A.b.c"}'' may be understood as a local entity @{text
-  "c"}, within a local structure @{text "b"}, within a global
-  structure @{text "A"}.  Typically, name space hierarchies consist of
-  1--2 levels of qualification, but this need not be always so.
+text {* A \emph{long name} consists of a sequence of non-empty name
+  components.  The packed representation uses a dot as separator, as
+  in ``@{text "A.b.c"}''.  The last component is called \emph{base
+  name}, the remaining prefix is called \emph{qualifier} (which may be
+  empty).  The qualifier can be understood as the access path to the
+  named entity while passing through some nested block-structure,
+  although our free-form long names do not really enforce any strict
+  discipline.
+
+  For example, an item named ``@{text "A.b.c"}'' may be understood as
+  a local entity @{text "c"}, within a local structure @{text "b"},
+  within a global structure @{text "A"}.  In practice, long names
+  usually represent 1--3 levels of qualification.  User ML code should
+  not make any assumptions about the particular structure of long
+  names!
 
   The empty name is commonly used as an indication of unnamed
-  entities, whenever this makes any sense.  The basic operations on
-  qualified names are smart enough to pass through such improper names
-  unchanged.
-
-  \medskip A @{text "naming"} policy tells how to turn a name
-  specification into a fully qualified internal name (by the @{text
-  "full"} operation), and how fully qualified names may be accessed
-  externally.  For example, the default naming policy is to prefix an
-  implicit path: @{text "full x"} produces @{text "path.x"}, and the
-  standard accesses for @{text "path.x"} include both @{text "x"} and
-  @{text "path.x"}.  Normally, the naming is implicit in the theory or
-  proof context; there are separate versions of the corresponding.
-
-  \medskip A @{text "name space"} manages a collection of fully
-  internalized names, together with a mapping between external names
-  and internal names (in both directions).  The corresponding @{text
-  "intern"} and @{text "extern"} operations are mostly used for
-  parsing and printing only!  The @{text "declare"} operation augments
-  a name space according to the accesses determined by the naming
-  policy.
-
-  \medskip As a general principle, there is a separate name space for
-  each kind of formal entity, e.g.\ logical constant, type
-  constructor, type class, theorem.  It is usually clear from the
-  occurrence in concrete syntax (or from the scope) which kind of
-  entity a name refers to.  For example, the very same name @{text
-  "c"} may be used uniformly for a constant, type constructor, and
-  type class.
-
-  There are common schemes to name theorems systematically, according
-  to the name of the main logical entity involved, e.g.\ @{text
-  "c.intro"} for a canonical theorem related to constant @{text "c"}.
-  This technique of mapping names from one space into another requires
-  some care in order to avoid conflicts.  In particular, theorem names
-  derived from a type constructor or type class are better suffixed in
-  addition to the usual qualification, e.g.\ @{text "c_type.intro"}
-  and @{text "c_class.intro"} for theorems related to type @{text "c"}
-  and class @{text "c"}, respectively.
+  entities, or entities that are not entered into the corresponding
+  name space, whenever this makes any sense.  The basic operations on
+  long names map empty names again to empty names.
 *}
 
 text %mlref {*
@@ -815,6 +803,85 @@
   @{index_ML Long_Name.implode: "string list -> string"} \\
   @{index_ML Long_Name.explode: "string -> string list"} \\
   \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML Long_Name.base_name}~@{text "name"} returns the base name
+  of a long name.
+
+  \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
+  of a long name.
+
+  \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"} appends two long
+  names.
+
+  \item @{ML Long_Name.implode}~@{text "names"} and @{ML
+  Long_Name.explode}~@{text "name"} convert between the packed string
+  representation and the explicit list form of long names.
+
+  \end{description}
+*}
+
+
+subsection {* Name spaces \label{sec:name-space} *}
+
+text {* A @{text "name space"} manages a collection of long names,
+  together with a mapping between partially qualified external names
+  and fully qualified internal names (in both directions).  Note that
+  the corresponding @{text "intern"} and @{text "extern"} operations
+  are mostly used for parsing and printing only!  The @{text
+  "declare"} operation augments a name space according to the accesses
+  determined by a given binding, and a naming policy from the context.
+
+  \medskip A @{text "binding"} specifies details about the prospective
+  long name of a newly introduced formal entity.  It consists of a
+  base name, prefixes for qualification (separate ones for system
+  infrastructure and user-space mechanisms), a slot for the original
+  source position, and some additional flags.
+
+  \medskip A @{text "naming"} provides some additional details for
+  producing a long name from a binding.  Normally, the naming is
+  implicit in the theory or proof context.  The @{text "full"}
+  operation (and its variants for different context types) produces a
+  fully qualified internal name to be entered into a name space.  The
+  main equation of this ``chemical reaction'' when binding new
+  entities in a context is as follows:
+
+  \smallskip
+  \begin{tabular}{l}
+  @{text "binding + naming \<longrightarrow> long name + name space accesses"}
+  \end{tabular}
+  \smallskip
+
+  \medskip As a general principle, there is a separate name space for
+  each kind of formal entity, e.g.\ fact, logical constant, type
+  constructor, type class.  It is usually clear from the occurrence in
+  concrete syntax (or from the scope) which kind of entity a name
+  refers to.  For example, the very same name @{text "c"} may be used
+  uniformly for a constant, type constructor, and type class.
+
+  There are common schemes to name derived entities systematically
+  according to the name of the main logical entity involved, e.g.\
+  fact @{text "c.intro"} for a canonical introduction rule related to
+  constant @{text "c"}.  This technique of mapping names from one
+  space into another requires some care in order to avoid conflicts.
+  In particular, theorem names derived from a type constructor or type
+  class are better suffixed in addition to the usual qualification,
+  e.g.\ @{text "c_type.intro"} and @{text "c_class.intro"} for
+  theorems related to type @{text "c"} and class @{text "c"},
+  respectively.
+*}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML_type binding} \\
+  @{index_ML Binding.empty: binding} \\
+  @{index_ML Binding.name: "string -> binding"} \\
+  @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
+  @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
+  @{index_ML Binding.conceal: "binding -> binding"} \\
+  @{index_ML Binding.str_of: "binding -> string"} \\
+  \end{mldecls}
   \begin{mldecls}
   @{index_ML_type Name_Space.naming} \\
   @{index_ML Name_Space.default_naming: Name_Space.naming} \\
@@ -829,22 +896,41 @@
   string * Name_Space.T"} \\
   @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
   @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\
+  @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
   \end{mldecls}
 
   \begin{description}
 
-  \item @{ML Long_Name.base_name}~@{text "name"} returns the base name of a
-  qualified name.
+  \item @{ML_type binding} represents the abstract concept of name
+  bindings.
+
+  \item @{ML Binding.empty} is the empty binding.
 
-  \item @{ML Long_Name.qualifier}~@{text "name"} returns the qualifier
-  of a qualified name.
+  \item @{ML Binding.name}~@{text "name"} produces a binding with base
+  name @{text "name"}.
+
+  \item @{ML Binding.qualify}~@{text "mandatory name binding"}
+  prefixes qualifier @{text "name"} to @{text "binding"}.  The @{text
+  "mandatory"} flag tells if this name component always needs to be
+  given in name space accesses --- this is mostly @{text "false"} in
+  practice.  Note that this part of qualification is typically used in
+  derived specification mechanisms.
 
-  \item @{ML Long_Name.append}~@{text "name\<^isub>1 name\<^isub>2"}
-  appends two qualified names.
+  \item @{ML Binding.prefix} is similar to @{ML Binding.qualify}, but
+  affects the system prefix.  This part of extra qualification is
+  typically used in the infrastructure for modular specifications,
+  notably ``local theory targets'' (see also \chref{ch:local-theory}).
 
-  \item @{ML Long_Name.implode}~@{text "names"} and @{ML
-  Long_Name.explode}~@{text "name"} convert between the packed string
-  representation and the explicit list form of qualified names.
+  \item @{ML Binding.conceal}~@{text "binding"} indicates that the
+  binding shall refer to an entity that serves foundational purposes
+  only.  This flag helps to mark implementation details of
+  specification mechanism etc.  Other tools should not depend on the
+  particulars of concealed entities (cf.\ @{ML
+  Name_Space.is_concealed}).
+
+  \item @{ML Binding.str_of}~@{text "binding"} produces a string
+  representation for human-readable output, together with some formal
+  markup that might get used in GUI front-ends, for example.
 
   \item @{ML_type Name_Space.naming} represents the abstract concept of
   a naming policy.
@@ -888,6 +974,10 @@
   This operation is mostly for printing!  User code should not rely on
   the precise result too much.
 
+  \item @{ML Name_Space.is_concealed}~@{text "space name"} indicates
+  whether @{text "name"} refers to a strictly private entity that
+  other tools are supposed to ignore!
+
   \end{description}
 *}