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
     5 chapter {* System integration *}
     7 section {* Isar toplevel \label{sec:isar-toplevel} *}
     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.
    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.
    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.
    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.
    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 *}
    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}
    66   \begin{description}
    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}).
    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.
    78   \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
    79   toplevel state.
    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.
    85   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
    86   state if available, otherwise raises @{ML Toplevel.UNDEF}.
    88   \item @{ML "Toplevel.debug := true"} makes the toplevel print further
    89   details about internal error conditions, exceptions being raised
    90   etc.
    92   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
    93   information for each Isar command being executed.
    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.
   100   \end{description}
   101 *}
   103 text %mlantiq {*
   104   \begin{matharray}{rcl}
   105   @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
   106   \end{matharray}
   108   \begin{description}
   110   \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
   111   point --- as abstract value.
   113   This only works for diagnostic ML commands, such as @{command
   114   ML_val} or @{command ML_command}.
   116   \end{description}
   117 *}
   120 subsection {* Toplevel transitions \label{sec:toplevel-transition} *}
   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.
   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.
   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 *}
   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}
   163   \begin{description}
   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).
   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.
   173   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   174   function.
   176   \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
   177   transformer.
   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.
   185   \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
   186   proof command, with a singleton result.
   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).
   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.
   196   \end{description}
   197 *}
   200 section {* Theory database \label{sec:theory-database} *}
   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).
   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!
   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.
   222   The basic internal actions of the theory database are @{text
   223   "update"} and @{text "remove"}:
   225   \begin{itemize}
   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;
   231   \item @{text "remove A"} deletes entry @{text "A"} from the theory
   232   database.
   234   \end{itemize}
   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.
   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 *}
   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}
   267   \begin{description}
   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.
   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.
   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.
   285   \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
   286   descendants from the theory database.
   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.
   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.
   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.
   304   \end{description}
   305 *}
   307 end