doc-src/IsarImplementation/Thy/Integration.thy
author wenzelm
Fri Aug 12 22:10:49 2011 +0200 (2011-08-12)
changeset 44163 32e0c150c010
parent 40149 4c35be108990
permissions -rw-r--r--
normalized theory dependencies wrt. file_store;
     1 theory Integration
     2 imports Base
     3 begin
     4 
     5 chapter {* System integration *}
     6 
     7 section {* Isar toplevel \label{sec:isar-toplevel} *}
     8 
     9 text {* The Isar toplevel may be considered the centeral hub of the
    10   Isabelle/Isar system, where all key components and sub-systems are
    11   integrated into a single read-eval-print loop of Isar commands,
    12   which also incorporates the underlying ML compiler.
    13 
    14   Isabelle/Isar departs from the original ``LCF system architecture''
    15   where ML was really The Meta Language for defining theories and
    16   conducting proofs.  Instead, ML now only serves as the
    17   implementation language for the system (and user extensions), while
    18   the specific Isar toplevel supports the concepts of theory and proof
    19   development natively.  This includes the graph structure of theories
    20   and the block structure of proofs, support for unlimited undo,
    21   facilities for tracing, debugging, timing, profiling etc.
    22 
    23   \medskip The toplevel maintains an implicit state, which is
    24   transformed by a sequence of transitions -- either interactively or
    25   in batch-mode.  In interactive mode, Isar state transitions are
    26   encapsulated as safe transactions, such that both failure and undo
    27   are handled conveniently without destroying the underlying draft
    28   theory (cf.~\secref{sec:context-theory}).  In batch mode,
    29   transitions operate in a linear (destructive) fashion, such that
    30   error conditions abort the present attempt to construct a theory or
    31   proof altogether.
    32 
    33   The toplevel state is a disjoint sum of empty @{text toplevel}, or
    34   @{text theory}, or @{text proof}.  On entering the main Isar loop we
    35   start with an empty toplevel.  A theory is commenced by giving a
    36   @{text \<THEORY>} header; within a theory we may issue theory
    37   commands such as @{text \<DEFINITION>}, or state a @{text
    38   \<THEOREM>} to be proven.  Now we are within a proof state, with a
    39   rich collection of Isar proof commands for structured proof
    40   composition, or unstructured proof scripts.  When the proof is
    41   concluded we get back to the theory, which is then updated by
    42   storing the resulting fact.  Further theory declarations or theorem
    43   statements with proofs may follow, until we eventually conclude the
    44   theory development by issuing @{text \<END>}.  The resulting theory
    45   is then stored within the theory database and we are back to the
    46   empty toplevel.
    47 
    48   In addition to these proper state transformations, there are also
    49   some diagnostic commands for peeking at the toplevel state without
    50   modifying it (e.g.\ \isakeyword{thm}, \isakeyword{term},
    51   \isakeyword{print-cases}).
    52 *}
    53 
    54 text %mlref {*
    55   \begin{mldecls}
    56   @{index_ML_type Toplevel.state} \\
    57   @{index_ML Toplevel.UNDEF: "exn"} \\
    58   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
    59   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
    60   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
    61   @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
    62   @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
    63   @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
    64   \end{mldecls}
    65 
    66   \begin{description}
    67 
    68   \item Type @{ML_type Toplevel.state} represents Isar toplevel
    69   states, which are normally manipulated through the concept of
    70   toplevel transitions only (\secref{sec:toplevel-transition}).  Also
    71   note that a raw toplevel state is subject to the same linearity
    72   restrictions as a theory context (cf.~\secref{sec:context-theory}).
    73 
    74   \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
    75   operations.  Many operations work only partially for certain cases,
    76   since @{ML_type Toplevel.state} is a sum type.
    77 
    78   \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
    79   toplevel state.
    80 
    81   \item @{ML Toplevel.theory_of}~@{text "state"} selects the
    82   background theory of @{text "state"}, raises @{ML Toplevel.UNDEF}
    83   for an empty toplevel state.
    84 
    85   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
    86   state if available, otherwise raises @{ML Toplevel.UNDEF}.
    87 
    88   \item @{ML "Toplevel.debug := true"} makes the toplevel print further
    89   details about internal error conditions, exceptions being raised
    90   etc.
    91 
    92   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
    93   information for each Isar command being executed.
    94 
    95   \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls
    96   low-level profiling of the underlying ML runtime system.  For
    97   Poly/ML, @{text "n = 1"} means time and @{text "n = 2"} space
    98   profiling.
    99 
   100   \end{description}
   101 *}
   102 
   103 text %mlantiq {*
   104   \begin{matharray}{rcl}
   105   @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
   106   \end{matharray}
   107 
   108   \begin{description}
   109 
   110   \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
   111   point --- as abstract value.
   112 
   113   This only works for diagnostic ML commands, such as @{command
   114   ML_val} or @{command ML_command}.
   115 
   116   \end{description}
   117 *}
   118 
   119 
   120 subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
   121 
   122 text {*
   123   An Isar toplevel transition consists of a partial function on the
   124   toplevel state, with additional information for diagnostics and
   125   error reporting: there are fields for command name, source position,
   126   optional source text, as well as flags for interactive-only commands
   127   (which issue a warning in batch-mode), printing of result state,
   128   etc.
   129 
   130   The operational part is represented as the sequential union of a
   131   list of partial functions, which are tried in turn until the first
   132   one succeeds.  This acts like an outer case-expression for various
   133   alternative state transitions.  For example, \isakeyword{qed} works
   134   differently for a local proofs vs.\ the global ending of the main
   135   proof.
   136 
   137   Toplevel transitions are composed via transition transformers.
   138   Internally, Isar commands are put together from an empty transition
   139   extended by name and source position.  It is then left to the
   140   individual command parser to turn the given concrete syntax into a
   141   suitable transition transformer that adjoins actual operations on a
   142   theory or proof state etc.
   143 *}
   144 
   145 text %mlref {*
   146   \begin{mldecls}
   147   @{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
   148   @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
   149   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   150   Toplevel.transition -> Toplevel.transition"} \\
   151   @{index_ML Toplevel.theory: "(theory -> theory) ->
   152   Toplevel.transition -> Toplevel.transition"} \\
   153   @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
   154   Toplevel.transition -> Toplevel.transition"} \\
   155   @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
   156   Toplevel.transition -> Toplevel.transition"} \\
   157   @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.seq) ->
   158   Toplevel.transition -> Toplevel.transition"} \\
   159   @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
   160   Toplevel.transition -> Toplevel.transition"} \\
   161   \end{mldecls}
   162 
   163   \begin{description}
   164 
   165   \item @{ML Toplevel.print}~@{text "tr"} sets the print flag, which
   166   causes the toplevel loop to echo the result state (in interactive
   167   mode).
   168 
   169   \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
   170   transition should never show timing information, e.g.\ because it is
   171   a diagnostic command.
   172 
   173   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   174   function.
   175 
   176   \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
   177   transformer.
   178 
   179   \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
   180   goal function, which turns a theory into a proof state.  The theory
   181   may be changed before entering the proof; the generic Isar goal
   182   setup includes an argument that specifies how to apply the proven
   183   result to the theory, when the proof is finished.
   184 
   185   \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
   186   proof command, with a singleton result.
   187 
   188   \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
   189   command, with zero or more result states (represented as a lazy
   190   list).
   191 
   192   \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
   193   proof command, that returns the resulting theory, after storing the
   194   resulting facts in the context etc.
   195 
   196   \end{description}
   197 *}
   198 
   199 
   200 section {* Theory database \label{sec:theory-database} *}
   201 
   202 text {*
   203   The theory database maintains a collection of theories, together
   204   with some administrative information about their original sources,
   205   which are held in an external store (i.e.\ some directory within the
   206   regular file system).
   207 
   208   The theory database is organized as a directed acyclic graph;
   209   entries are referenced by theory name.  Although some additional
   210   interfaces allow to include a directory specification as well, this
   211   is only a hint to the underlying theory loader.  The internal theory
   212   name space is flat!
   213 
   214   Theory @{text A} is associated with the main theory file @{text
   215   A}\verb,.thy,, which needs to be accessible through the theory
   216   loader path.  Any number of additional ML source files may be
   217   associated with each theory, by declaring these dependencies in the
   218   theory header as @{text \<USES>}, and loading them consecutively
   219   within the theory context.  The system keeps track of incoming ML
   220   sources and associates them with the current theory.
   221 
   222   The basic internal actions of the theory database are @{text
   223   "update"} and @{text "remove"}:
   224 
   225   \begin{itemize}
   226 
   227   \item @{text "update A"} introduces a link of @{text "A"} with a
   228   @{text "theory"} value of the same name; it asserts that the theory
   229   sources are now consistent with that value;
   230 
   231   \item @{text "remove A"} deletes entry @{text "A"} from the theory
   232   database.
   233   
   234   \end{itemize}
   235 
   236   These actions are propagated to sub- or super-graphs of a theory
   237   entry as expected, in order to preserve global consistency of the
   238   state of all loaded theories with the sources of the external store.
   239   This implies certain causalities between actions: @{text "update"}
   240   or @{text "remove"} of an entry will @{text "remove"} all
   241   descendants.
   242 
   243   \medskip There are separate user-level interfaces to operate on the
   244   theory database directly or indirectly.  The primitive actions then
   245   just happen automatically while working with the system.  In
   246   particular, processing a theory header @{text "\<THEORY> A
   247   \<IMPORTS> B\<^sub>1 \<dots> B\<^sub>n \<BEGIN>"} ensures that the
   248   sub-graph of the collective imports @{text "B\<^sub>1 \<dots> B\<^sub>n"}
   249   is up-to-date, too.  Earlier theories are reloaded as required, with
   250   @{text update} actions proceeding in topological order according to
   251   theory dependencies.  There may be also a wave of implied @{text
   252   remove} actions for derived theory nodes until a stable situation
   253   is achieved eventually.
   254 *}
   255 
   256 text %mlref {*
   257   \begin{mldecls}
   258   @{index_ML use_thy: "string -> unit"} \\
   259   @{index_ML use_thys: "string list -> unit"} \\
   260   @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   261   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
   262   @{index_ML Thy_Info.register_thy: "theory -> unit"} \\[1ex]
   263   @{ML_text "datatype action = Update | Remove"} \\
   264   @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
   265   \end{mldecls}
   266 
   267   \begin{description}
   268 
   269   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
   270   up-to-date wrt.\ the external file store, reloading outdated
   271   ancestors as required.  In batch mode, the simultaneous @{ML
   272   use_thys} should be used exclusively.
   273 
   274   \item @{ML use_thys} is similar to @{ML use_thy}, but handles
   275   several theories simultaneously.  Thus it acts like processing the
   276   import header of a theory, without performing the merge of the
   277   result.  By loading a whole sub-graph of theories like that, the
   278   intrinsic parallelism can be exploited by the system, to speedup
   279   loading.
   280 
   281   \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
   282   presently associated with name @{text A}.  Note that the result
   283   might be outdated.
   284 
   285   \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
   286   descendants from the theory database.
   287 
   288   \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an
   289   existing theory value with the theory loader database and updates
   290   source version information according to the current file-system
   291   state.
   292 
   293   \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
   294   f} as a hook for theory database actions.  The function will be
   295   invoked with the action and theory name being involved; thus derived
   296   actions may be performed in associated system components, e.g.\
   297   maintaining the state of an editor for the theory sources.
   298 
   299   The kind and order of actions occurring in practice depends both on
   300   user interactions and the internal process of resolving theory
   301   imports.  Hooks should not rely on a particular policy here!  Any
   302   exceptions raised by the hook are ignored.
   303 
   304   \end{description}
   305 *}
   306 
   307 end