diff -r ab3f32f86847 -r 2681f9e34390 doc-src/IsarImplementation/Thy/document/integration.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Mon Jan 02 20:16:52 2006 +0100
@@ -0,0 +1,536 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{integration}%
+%
+\isadelimtheory
+\isanewline
+\isanewline
+\isanewline
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{theory}\isamarkupfalse%
+\ integration\ \isakeyword{imports}\ base\ \isakeyword{begin}%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isamarkupchapter{System integration%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Isar toplevel%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The Isar toplevel may be considered the centeral hub of the
+  Isabelle/Isar system, where all key components and sub-systems are
+  integrated into a single read-eval-print loop of Isar commands.
+  Here we even incorporate the existing {\ML} toplevel of the compiler
+  and run-time system (cf.\ \secref{sec:ML-toplevel}).
+
+  Isabelle/Isar departs from original ``LCF system architecture''
+  where {\ML} was really The Meta Language for defining theories and
+  conducting proofs.  Instead, {\ML} merely serves as the
+  implementation language for the system (and user extensions), while
+  our specific Isar toplevel supports particular notions of
+  incremental theory and proof development more directly.  This
+  includes the graph structure of theories and the block structure of
+  proofs, support for unlimited undo, facilities for tracing,
+  debugging, timing, profiling.
+
+  \medskip The toplevel maintains an implicit state, which is
+  transformed by a sequence of transitions -- either interactively or
+  in batch-mode.  In interactive mode, Isar state transitions are
+  encapsulated as safe transactions, such that both failure and undo
+  are handled conveniently without destroying the underlying draft
+  theory (cf.~\secref{sec:context-theory}).  In batch mode,
+  transitions operate in a strictly linear (destructive) fashion, such
+  that error conditions abort the present attempt to construct a
+  theory altogether.
+
+  The toplevel state is a disjoint sum of empty \isa{toplevel}, or
+  \isa{theory}, or \isa{proof}.  On entering the main Isar loop we
+  start with an empty toplevel.  A theory is commenced by giving a
+  \isa{{\isasymTHEORY}} header; within a theory we may issue theory
+  commands such as \isa{{\isasymCONSTS}} or \isa{{\isasymDEFS}}, or state a
+  \isa{{\isasymTHEOREM}} to be proven.  Now we are within a proof state,
+  with a rich collection of Isar proof commands for structured proof
+  composition, or unstructured proof scripts.  When the proof is
+  concluded we get back to the theory, which is then updated by
+  storing the resulting fact.  Further theory declarations or theorem
+  statements with proofs may follow, until we eventually conclude the
+  theory development by issuing \isa{{\isasymEND}}.  The resulting theory
+  is then stored within the theory database and we are back to the
+  empty toplevel.
+
+  In addition to these proper state transformations, there are also
+  some diagnostic commands for peeking at the toplevel state without
+  modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
+  \isakeyword{print-cases}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexmltype{Toplevel.state}\verb|type Toplevel.state| \\
+  \indexml{Toplevel.UNDEF}\verb|Toplevel.UNDEF: exn| \\
+  \indexml{Toplevel.is-toplevel}\verb|Toplevel.is_toplevel: Toplevel.state -> bool| \\
+  \indexml{Toplevel.theory-of}\verb|Toplevel.theory_of: Toplevel.state -> theory| \\
+  \indexml{Toplevel.proof-of}\verb|Toplevel.proof_of: Toplevel.state -> Proof.state| \\
+  \indexml{Toplevel.debug}\verb|Toplevel.debug: bool ref| \\
+  \indexml{Toplevel.timing}\verb|Toplevel.timing: bool ref| \\
+  \indexml{Toplevel.profiling}\verb|Toplevel.profiling: int ref| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|Toplevel.state| represents Isar toplevel states,
+  which are normally only manipulated through the toplevel transition
+  concept (\secref{sec:toplevel-transition}).  Also note that a
+  toplevel state is subject to the same linerarity restrictions as a
+  theory context (cf.~\secref{sec:context-theory}).
+
+  \item \verb|Toplevel.UNDEF| is raised for undefined toplevel
+  operations: \verb|Toplevel.state| is a sum type, many operations
+  work only partially for certain cases.
+
+  \item \verb|Toplevel.is_toplevel| checks for an empty toplevel state.
+
+  \item \verb|Toplevel.theory_of| gets the theory of a theory or proof
+  (!), otherwise raises \verb|Toplevel.UNDEF|.
+
+  \item \verb|Toplevel.proof_of| gets the Isar proof state if
+  available, otherwise raises \verb|Toplevel.UNDEF|.
+
+  \item \verb|set Toplevel.debug| makes the toplevel print further
+  details about internal error conditions, exceptions being raised
+  etc.
+
+  \item \verb|set Toplevel.timing| makes the toplevel print timing
+  information for each Isar command being executed.
+
+  \item \verb|Toplevel.profiling| controls low-level profiling of the
+  underlying {\ML} runtime system.\footnote{For Poly/ML, 1 means time
+  and 2 space profiling.}
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Toplevel transitions%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+An Isar toplevel transition consists of a partial
+  function on the toplevel state, with additional information for
+  diagnostics and error reporting: there are fields for command name,
+  source position, optional source text, as well as flags for
+  interactive-only commands (which issue a warning in batch-mode),
+  printing of result state, etc.
+
+  The operational part is represented as a sequential union of a list
+  of partial functions, which are tried in turn until the first one
+  succeeds (i.e.\ does not raise \verb|Toplevel.UNDEF|).  For example,
+  a single Isar command like \isacommand{qed} consists of the union of
+  some function \verb|Proof.state -> Proof.state| for proofs
+  within proofs, plus \verb|Proof.state -> theory| for proofs at
+  the outer theory level.
+
+  Toplevel transitions are composed via transition transformers.
+  Internally, Isar commands are put together from an empty transition
+  extended by name and source position (and optional source text).  It
+  is then left to the individual command parser to turn the given
+  syntax body into a suitable transition transformer that adjoin
+  actual operations on a theory or proof state etc.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{Toplevel.print}\verb|Toplevel.print: Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.no-timing}\verb|Toplevel.no_timing: Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.keep}\verb|Toplevel.keep: (Toplevel.state -> unit) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.theory}\verb|Toplevel.theory: (theory -> theory) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.theory-to-proof}\verb|Toplevel.theory_to_proof: (theory -> Proof.state) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.proof}\verb|Toplevel.proof: (Proof.state -> Proof.state) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.proofs}\verb|Toplevel.proofs: (Proof.state -> Proof.state Seq.seq) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \indexml{Toplevel.proof-to-theory}\verb|Toplevel.proof_to_theory: (Proof.state -> theory) ->|\isasep\isanewline%
+\verb|  Toplevel.transition -> Toplevel.transition| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|Toplevel.print| sets the print flag, which causes the
+  resulting state of the transition to be echoed in interactive mode.
+
+  \item \verb|Toplevel.no_timing| indicates that the transition should
+  never show timing information, e.g.\ because it is merely a
+  diagnostic command.
+
+  \item \verb|Toplevel.keep| adjoins a diagnostic function.
+
+  \item \verb|Toplevel.theory| adjoins a theory transformer.
+
+  \item \verb|Toplevel.theory_to_proof| adjoins a global goal function,
+  which turns a theory into a proof state.  The theory must not be
+  changed here!  The generic Isar goal setup includes an argument that
+  specifies how to apply the proven result to the theory, when the
+  proof is finished.
+
+  \item \verb|Toplevel.proof| adjoins a deterministic proof command,
+  with a singleton result state.
+
+  \item \verb|Toplevel.proofs| adjoins a general proof command, with
+  zero or more result states (represented as a lazy list).
+
+  \item \verb|Toplevel.proof_to_theory| adjoins a concluding proof
+  command, that returns the resulting theory, after storing the
+  resulting facts etc.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsubsection{Toplevel control%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Apart from regular toplevel transactions there are a few
+  special control commands that modify the behavior the toplevel
+  itself, and only make sense in interactive mode.  Under normal
+  circumstances, the user encounters these only implicitly as part of
+  the protocol between the Isabelle/Isar system and a user-interface
+  such as ProofGeneral.
+
+  \begin{description}
+
+  \item \isacommand{undo} follows the three-level hierarchy of empty
+  toplevel vs.\ theory vs.\ proof: undo within a proof reverts to the
+  previous proof context, undo after a proof reverts to the theory
+  before the initial goal statement, undo of a theory command reverts
+  to the previous theory value, undo of a theory header discontinues
+  the current theory development and removes it from the theory
+  database (\secref{sec:theory-database}).
+
+  \item \isacommand{kill} aborts the current level of development:
+  kill in a proof context reverts to the theory before the initial
+  goal statement, kill in a theory context aborts the current theory
+  development, removing it from the database.
+
+  \item \isacommand{exit} drops out of the Isar toplevel into the
+  underlying {\ML} toplevel (\secref{sec:ML-toplevel}).  The Isar
+  toplevel state is preserved and may be continued later.
+
+  \item \isacommand{quit} terminates the Isabelle/Isar process without
+  saving.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{ML toplevel \label{sec:ML-toplevel}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The {\ML} toplevel provides a read-compile-eval-print loop for
+  {\ML} values, types, structures, and functors.  {\ML} declarations
+  operate on the global system state, which consists of the compiler
+  environment plus the values of {\ML} reference variables.  There is
+  no clean way to undo {\ML} declarations, except for reverting to a
+  previously saved state of the whole Isabelle process.  {\ML} input
+  is either read interactively from a TTY, or from a string (usually
+  within a theory text), or from a source file (usually associated
+  with a theory).
+
+  Whenever the {\ML} toplevel is active, the current Isabelle theory
+  context is passed as an internal reference variable.  Thus {\ML}
+  code may access the theory context during compilation, it may even
+  change the value of a theory being under construction --- following
+  the usual linearity restrictions (cf.~\secref{sec:context-theory}).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{context}\verb|context: theory -> unit| \\
+  \indexml{the-context}\verb|the_context: unit -> theory| \\
+  \indexml{Context.$>$$>$ }\verb|Context.>> : (theory -> theory) -> unit| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|context|~\isa{thy} sets the {\ML} theory context to
+  \isa{thy}.  This is usually performed automatically by the system,
+  when dropping out of the interactive Isar toplevel into {\ML}, or
+  when Isar invokes {\ML} to process code from a string or a file.
+
+  \item \verb|the_context ()| refers to the theory context of the
+  {\ML} toplevel --- at compile time!  {\ML} code needs to take care
+  to refer to \verb|the_context ()| correctly, recall that evaluation
+  of a function body is delayed until actual runtime.  Moreover,
+  persistent {\ML} toplevel bindings to an unfinished theory should be
+  avoided: code should either project out the desired information
+  immediately, or produce an explicit \verb|theory_ref| (cf.\
+  \secref{sec:context-theory}).
+
+  \item \verb|Context.>>|~\isa{f} applies theory transformation
+  \isa{f} to the current theory of the {\ML} toplevel.  In order to
+  work as expected, the theory should be still under construction, and
+  the Isar language element that invoked the {\ML} compiler in the
+  first place shoule be ready to accept the changed theory value
+  (e.g.\ \isakeyword{ML-setup}, but not plain \isakeyword{ML}).
+  Otherwise the theory may get destroyed!
+
+  \end{description}
+
+  It is very important to note that the above functions are really
+  restricted to the compile time, even though the {\ML} compiler is
+  invoked at runtime!  The majority of {\ML} code uses explicit
+  functional arguments of a theory or proof context, as required.
+  Thus it may get run in an arbitrary context later on.
+
+  \bigskip
+
+  \begin{mldecls}
+  \indexml{Isar.main}\verb|Isar.main: unit -> unit| \\
+  \indexml{Isar.loop}\verb|Isar.loop: unit -> unit| \\
+  \indexml{Isar.state}\verb|Isar.state: unit -> Toplevel.state| \\
+  \indexml{Isar.exn}\verb|Isar.exn: unit -> (exn * string) option| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|Isar.main ()| invokes the Isar toplevel from {\ML},
+  initializing the state to empty toplevel state.
+
+  \item \verb|Isar.loop ()| continues the Isar toplevel with the
+  current state, after dropping out of the Isar toplevel loop.
+
+  \item \verb|Isar.state ()| and \verb|Isar.exn ()| get current
+  toplevel state and optional error condition, respectively.  This
+  only works after dropping out of the Isar toplevel loop.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isamarkupsection{Theory database%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The theory database maintains a collection of theories,
+  together with some administrative information about the original
+  sources, which are held in an external store (i.e.\ a collection of
+  directories within the regular file system of the underlying
+  platform).
+
+  The theory database is organized as a directed acyclic graph, with
+  entries referenced by theory name.  Although some external
+  interfaces allow to include a directory specification, this is only
+  a hint to the underlying theory loader mechanism: the internal
+  theory name space is flat.
+
+  Theory \isa{A} is associated with the main theory file \isa{A}\verb,.thy,, which needs to be accessible through the theory
+  loader path.  A number of optional {\ML} source files may be
+  associated with each theory, by declaring these dependencies in the
+  theory header as \isa{{\isasymUSES}}, and loading them consecutively
+  within the theory context.  The system keeps track of incoming {\ML}
+  sources and associates them with the current theory.  The special
+  theory {\ML} file \isa{A}\verb,.ML, is loaded after a theory has
+  been concluded, in order to support legacy proof {\ML} proof
+  scripts.
+
+  The basic internal actions of the theory database are \isa{update}\indexbold{\isa{update} theory}, \isa{outdate}\indexbold{\isa{outdate} theory}, and \isa{remove}\indexbold{\isa{remove} theory}:
+
+  \begin{itemize}
+
+  \item \isa{update\ A} introduces a link of \isa{A} with a
+  \isa{theory} value of the same name; it asserts that the theory
+  sources are consistent with that value.
+
+  \item \isa{outdate\ A} invalidates the link of a theory database
+  entry to its sources, but retains the present theory value.
+
+  \item \isa{remove\ A} removes entry \isa{A} from the theory
+  database.
+  
+  \end{itemize}
+
+  These actions are propagated to sub- or super-graphs of a theory
+  entry in the usual way, in order to preserve global consistency of
+  the state of all loaded theories with the sources of the external
+  store.  This implies causal dependencies of certain actions: \isa{update} or \isa{outdate} of an entry will \isa{outdate}
+  all descendants; \isa{remove} will \isa{remove} all
+  descendants.
+
+  \medskip There are separate user-level interfaces to operate on the
+  theory database directly or indirectly.  The primitive actions then
+  just happen automatically while working with the system.  In
+  particular, processing a theory header \isa{{\isasymTHEORY}\ A\ {\isasymIMPORTS}\ B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n\ {\isasymBEGIN}} ensure that the
+  sub-graph of the collective imports \isa{B\isactrlsub {\isadigit{1}}\ {\isasymdots}\ B\isactrlsub n}
+  is up-to-date.  Earlier theories are reloaded as required, with
+  \isa{update} actions proceeding in topological order according to
+  theory dependencies.  There may be also a wave of implied \isa{outdate} actions for derived theory nodes until a stable situation
+  is achieved eventually.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isatagmlref
+%
+\begin{isamarkuptext}%
+\begin{mldecls}
+  \indexml{theory}\verb|theory: string -> theory| \\
+  \indexml{use-thy}\verb|use_thy: string -> unit| \\
+  \indexml{update-thy}\verb|update_thy: string -> unit| \\
+  \indexml{use-thy-only}\verb|use_thy_only: string -> unit| \\
+  \indexml{update-thy-only}\verb|update_thy_only: string -> unit| \\
+  \indexml{touch-thy}\verb|touch_thy: string -> unit| \\
+  \indexml{remove-thy}\verb|remove_thy: string -> unit| \\[1ex]
+  \indexml{ThyInfo.begin-theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
+  \indexml{ThyInfo.end-theory}\verb|ThyInfo.end_theory: theory -> theory| \\
+  \indexml{ThyInfo.register-theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
+  \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
+  \indexml{ThyInfo.add-hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item \verb|theory|~\isa{A} retrieves the theory value presently
+  associated with \isa{A}.  The result is not necessarily
+  up-to-date!
+
+  \item \verb|use_thy|~\isa{A} loads theory \isa{A} if it is absent
+  or out-of-date.  It ensures that all parent theories are available
+  as well, but does not reload them if older versions are already
+  present.
+
+  \item \verb|update_thy| is similar to \verb|use_thy|, but ensures that
+  the \isa{A} and all of its ancestors are fully up-to-date.
+
+  \item \verb|use_thy_only|~\isa{A} is like \verb|use_thy|~\isa{A},
+  but refrains from loading the attached \isa{A}\verb,.ML, file.
+  This is occasionally useful in replaying legacy {\ML} proof scripts
+  by hand.
+  
+  \item \verb|update_thy_only| is analogous to \verb|use_thy_only|, but
+  proceeds like \verb|update_thy| for ancestors.
+
+  \item \verb|touch_thy|~\isa{A} performs \isa{outdate} action on
+  theory \isa{A} and all of its descendants.
+
+  \item \verb|remove_thy|~\isa{A} removes \isa{A} and all of its
+  descendants from the theory database.
+
+  \item \verb|ThyInfo.begin_theory| is the basic operation behind a
+  \isa{{\isasymTHEORY}} header declaration.  The boolean argument
+  indicates the strictness of treating ancestors: for \verb|true| (as
+  in interactive mode) like \verb|update_thy|, and for \verb|false| (as
+  in batch mode) like \verb|use_thy|.  This is {\ML} functions is
+  normally not invoked directly.
+
+  \item \verb|ThyInfo.end_theory| concludes the loading of a theory
+  proper; an attached theory {\ML} file may be still loaded later on.
+  This is {\ML} functions is normally not invoked directly.
+
+  \item \verb|ThyInfo.register_theory|~{text thy} registers an existing
+  theory value with the theory loader database.  There is no
+  management of associated sources; this is mainly for bootstrapping.
+
+  \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
+  invoked with the action and theory name being involved; thus derived
+  actions may be performed in associated system components, e.g.\
+  maintaining the state of an editor for theory sources.
+
+  The kind and order of actions occurring in practice depends both on
+  user interactions and the internal process of resolving theory
+  imports.  Hooks should not rely on a particular policy here!  Any
+  exceptions raised by the hook are ignored by the theory database.
+
+  \end{description}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagmlref
+{\isafoldmlref}%
+%
+\isadelimmlref
+%
+\endisadelimmlref
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+\isacommand{end}\isamarkupfalse%
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isanewline
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: