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