src/Doc/Implementation/Integration.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 59090 a0a05a4edb36
child 60094 96a4765ba7d1
permissions -rw-r--r--
tuned signature;
     1 (*:wrap=hard:maxLineLen=78:*)
     2 
     3 theory Integration
     4 imports Base
     5 begin
     6 
     7 chapter \<open>System integration\<close>
     8 
     9 section \<open>Isar toplevel \label{sec:isar-toplevel}\<close>
    10 
    11 text \<open>
    12   The Isar \emph{toplevel state} represents the outermost configuration that
    13   is transformed by a sequence of transitions (commands) within a theory body.
    14   This is a pure value with pure functions acting on it in a timeless and
    15   stateless manner. Historically, the sequence of transitions was wrapped up
    16   as sequential command loop, such that commands are applied one-by-one. In
    17   contemporary Isabelle/Isar, processing toplevel commands usually works in
    18   parallel in multi-threaded Isabelle/ML @{cite "Wenzel:2009" and
    19   "Wenzel:2013:ITP"}.
    20 \<close>
    21 
    22 
    23 subsection \<open>Toplevel state\<close>
    24 
    25 text \<open>
    26   The toplevel state is a disjoint sum of empty @{text toplevel}, or @{text
    27   theory}, or @{text proof}. The initial toplevel is empty; a theory is
    28   commenced by a @{command theory} header; within a theory we may use theory
    29   commands such as @{command definition}, or state a @{command theorem} to be
    30   proven. A proof state accepts a rich collection of Isar proof commands for
    31   structured proof composition, or unstructured proof scripts. When the proof
    32   is concluded we get back to the (local) theory, which is then updated by
    33   defining the resulting fact. Further theory declarations or theorem
    34   statements with proofs may follow, until we eventually conclude the theory
    35   development by issuing @{command end} to get back to the empty toplevel.
    36 \<close>
    37 
    38 text %mlref \<open>
    39   \begin{mldecls}
    40   @{index_ML_type Toplevel.state} \\
    41   @{index_ML_exception Toplevel.UNDEF} \\
    42   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
    43   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
    44   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
    45   \end{mldecls}
    46 
    47   \begin{description}
    48 
    49   \item Type @{ML_type Toplevel.state} represents Isar toplevel
    50   states, which are normally manipulated through the concept of
    51   toplevel transitions only (\secref{sec:toplevel-transition}).
    52 
    53   \item @{ML Toplevel.UNDEF} is raised for undefined toplevel
    54   operations.  Many operations work only partially for certain cases,
    55   since @{ML_type Toplevel.state} is a sum type.
    56 
    57   \item @{ML Toplevel.is_toplevel}~@{text "state"} checks for an empty
    58   toplevel state.
    59 
    60   \item @{ML Toplevel.theory_of}~@{text "state"} selects the
    61   background theory of @{text "state"}, it raises @{ML Toplevel.UNDEF}
    62   for an empty toplevel state.
    63 
    64   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
    65   state if available, otherwise it raises @{ML Toplevel.UNDEF}.
    66 
    67   \end{description}
    68 \<close>
    69 
    70 text %mlantiq \<open>
    71   \begin{matharray}{rcl}
    72   @{ML_antiquotation_def "Isar.state"} & : & @{text ML_antiquotation} \\
    73   \end{matharray}
    74 
    75   \begin{description}
    76 
    77   \item @{text "@{Isar.state}"} refers to Isar toplevel state at that
    78   point --- as abstract value.
    79 
    80   This only works for diagnostic ML commands, such as @{command
    81   ML_val} or @{command ML_command}.
    82 
    83   \end{description}
    84 \<close>
    85 
    86 
    87 subsection \<open>Toplevel transitions \label{sec:toplevel-transition}\<close>
    88 
    89 text \<open>
    90   An Isar toplevel transition consists of a partial function on the toplevel
    91   state, with additional information for diagnostics and error reporting:
    92   there are fields for command name, source position, and other meta-data.
    93 
    94   The operational part is represented as the sequential union of a
    95   list of partial functions, which are tried in turn until the first
    96   one succeeds.  This acts like an outer case-expression for various
    97   alternative state transitions.  For example, \isakeyword{qed} works
    98   differently for a local proofs vs.\ the global ending of an outermost
    99   proof.
   100 
   101   Transitions are composed via transition transformers. Internally, Isar
   102   commands are put together from an empty transition extended by name and
   103   source position. It is then left to the individual command parser to turn
   104   the given concrete syntax into a suitable transition transformer that
   105   adjoins actual operations on a theory or proof state.
   106 \<close>
   107 
   108 text %mlref \<open>
   109   \begin{mldecls}
   110   @{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
   111   Toplevel.transition -> Toplevel.transition"} \\
   112   @{index_ML Toplevel.theory: "(theory -> theory) ->
   113   Toplevel.transition -> Toplevel.transition"} \\
   114   @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) ->
   115   Toplevel.transition -> Toplevel.transition"} \\
   116   @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) ->
   117   Toplevel.transition -> Toplevel.transition"} \\
   118   @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) ->
   119   Toplevel.transition -> Toplevel.transition"} \\
   120   @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) ->
   121   Toplevel.transition -> Toplevel.transition"} \\
   122   \end{mldecls}
   123 
   124   \begin{description}
   125 
   126   \item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
   127   function.
   128 
   129   \item @{ML Toplevel.theory}~@{text "tr"} adjoins a theory
   130   transformer.
   131 
   132   \item @{ML Toplevel.theory_to_proof}~@{text "tr"} adjoins a global
   133   goal function, which turns a theory into a proof state.  The theory
   134   may be changed before entering the proof; the generic Isar goal
   135   setup includes an @{verbatim after_qed} argument that specifies how to
   136   apply the proven result to the enclosing context, when the proof
   137   is finished.
   138 
   139   \item @{ML Toplevel.proof}~@{text "tr"} adjoins a deterministic
   140   proof command, with a singleton result.
   141 
   142   \item @{ML Toplevel.proofs}~@{text "tr"} adjoins a general proof
   143   command, with zero or more result states (represented as a lazy
   144   list).
   145 
   146   \item @{ML Toplevel.end_proof}~@{text "tr"} adjoins a concluding
   147   proof command, that returns the resulting theory, after applying the
   148   resulting facts to the target context.
   149 
   150   \end{description}
   151 \<close>
   152 
   153 text %mlex \<open>The file @{"file" "~~/src/HOL/ex/Commands.thy"} shows some example
   154 Isar command definitions, with the all-important theory header declarations
   155 for outer syntax keywords.\<close>
   156 
   157 
   158 section \<open>Theory loader database\<close>
   159 
   160 text \<open>
   161   In batch mode and within dumped logic images, the theory database maintains
   162   a collection of theories as a directed acyclic graph. A theory may refer to
   163   other theories as @{keyword "imports"}, or to auxiliary files via special
   164   \emph{load commands} (e.g.\ @{command ML_file}). For each theory, the base
   165   directory of its own theory file is called \emph{master directory}: this is
   166   used as the relative location to refer to other files from that theory.
   167 \<close>
   168 
   169 text %mlref \<open>
   170   \begin{mldecls}
   171   @{index_ML use_thy: "string -> unit"} \\
   172   @{index_ML use_thys: "string list -> unit"} \\[0.5ex]
   173   @{index_ML Thy_Info.get_theory: "string -> theory"} \\
   174   @{index_ML Thy_Info.remove_thy: "string -> unit"} \\
   175   @{index_ML Thy_Info.register_thy: "theory -> unit"} \\
   176   \end{mldecls}
   177 
   178   \begin{description}
   179 
   180   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
   181   up-to-date wrt.\ the external file store; outdated ancestors are reloaded on
   182   demand.
   183 
   184   \item @{ML use_thys} is similar to @{ML use_thy}, but handles several
   185   theories simultaneously. Thus it acts like processing the import header of a
   186   theory, without performing the merge of the result. By loading a whole
   187   sub-graph of theories, the intrinsic parallelism can be exploited by the
   188   system to speedup loading.
   189 
   190   This variant is used by default in @{tool build} @{cite "isabelle-sys"}.
   191 
   192   \item @{ML Thy_Info.get_theory}~@{text A} retrieves the theory value
   193   presently associated with name @{text A}. Note that the result might be
   194   outdated wrt.\ the file-system content.
   195 
   196   \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
   197   descendants from the theory database.
   198 
   199   \item @{ML Thy_Info.register_thy}~@{text "text thy"} registers an existing
   200   theory value with the theory loader database and updates source version
   201   information according to the file store.
   202 
   203   \end{description}
   204 \<close>
   205 
   206 end