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