5 (*<*)

     5 section{* The Interface \label{sec:ind-interface} *}

     6 ML {*

     6 

     7 structure SIP = SimpleInductivePackage

     7 text {*

     8 *}

     8 

     9 (*>*)

     9   In order to add a new inductive predicate to a theory with the help of our

    10 

    10   package, the user must \emph{invoke} it. For every package, there are

    11 section{* The interface *}

    11   essentially two different ways of invoking it, which we will refer to as

    12 

    12   \emph{external} and \emph{internal}. By external invocation we mean that the

    13 text {*

    13   package is called from within a theory document. In this case, the type of

    14 \label{sec:ind-interface}

    14   the inductive predicate, as well as its introduction rules, are given as

    15 In order to add a new inductive predicate to a theory with the help of our package, the user

    15   strings by the user. Before the package can actually make the definition,

    16 must \emph{invoke} it. For every package, there are essentially two different ways of invoking

    16   the type and introduction rules have to be parsed. In contrast, internal

    17 it, which we will refer to as \emph{external} and \emph{internal}. By external

    17   invocation means that the package is called by some other package. For

    18 invocation we mean that the package is called from within a theory document. In this case,

    18   example, the function definition package \cite{Krauss-IJCAR06} calls the

    19 the type of the inductive predicate, as well as its introduction rules, are given as strings

    19   inductive definition package to define the graph of the function. However,

    20 by the user. Before the package can actually make the definition, the type and introduction

    20   it is not a good idea for the function definition package to pass the

    21 rules have to be parsed. In contrast, internal invocation means that the package is called

    21   introduction rules for the function graph to the inductive definition

    22 by some other package. For example, the function definition package \cite{Krauss-IJCAR06}

    22   package as strings. In this case, it is better to directly pass the rules to

    23 calls the inductive definition package to define the graph of the function. However, it is

    23   the package as a list of terms, which is more robust than handling strings

    24 not a good idea for the function definition package to pass the introduction rules for the

    24   that are lacking the additional structure of terms. These two ways of

    25 function graph to the inductive definition package as strings. In this case, it is better

    25   invoking the package are reflected in its ML programming interface, which

    26 to directly pass the rules to the package as a list of terms, which is more robust than

    26   consists of two functions:

    27 handling strings that are lacking the additional structure of terms. These two ways of

    27 

    28 invoking the package are reflected in its ML programming interface, which consists of two

    28   @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}

    29 functions:

    29 *}

    30 

    30 

    31 @{ML_chunk [display] SIMPLE_INDUCTIVE_PACKAGE}

    31 text {*

    32 *}

    32   The function for external invocation of the package is called @{ML

    33 

    33   add_inductive in SimpleInductivePackage}, whereas the one for internal

    34 text {*

    34   invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both

    35 The function for external invocation of the package is called @{ML add_inductive in SIP},

    35   of these functions take as arguments the names and types of the inductive

    36 whereas the one for internal invocation is called @{ML add_inductive_i in SIP}. Both

    36   predicates, the names and types of their parameters, the actual introduction

    37 of these functions take as arguments the names and types of the inductive predicates, the

    37   rules and a \emph{local theory}.  They return a local theory containing the

    38 names and types of their parameters, the actual introduction rules and a \emph{local theory}.

    38   definition, together with a tuple containing the introduction and induction

    39 They return a local theory containing the definition, together with a tuple containing

    39   rules, which are stored in the local theory, too.  In contrast to an

    40 the introduction and induction rules, which are stored in the local theory, too.

    40   ordinary theory, which simply consists of a type signature, as well as

    41 In contrast to an ordinary theory, which simply consists of a type signature, as

    41   tables for constants, axioms and theorems, a local theory also contains

    42 well as tables for constants, axioms and theorems, a local theory also contains

    42   additional context information, such as locally fixed variables and local

    43 additional context information, such as locally fixed variables and local assumptions

    43   assumptions that may be used by the package. The type @{ML_type

    44 that may be used by the package. The type @{ML_type local_theory} is identical to the

    44   local_theory} is identical to the type of \emph{proof contexts} @{ML_type

    45 type of \emph{proof contexts} @{ML_type "Proof.context"}, although not every proof context

    45   "Proof.context"}, although not every proof context constitutes a valid local

    46 constitutes a valid local theory.

    46   theory.  Note that @{ML add_inductive_i in SimpleInductivePackage} expects

    47 Note that @{ML add_inductive_i in SIP} expects the types

    47   the types of the predicates and parameters to be specified using the

    48 of the predicates and parameters to be specified using the datatype @{ML_type typ} of Isabelle's

    48   datatype @{ML_type typ} of Isabelle's logical framework, whereas @{ML

    49 logical framework, whereas @{ML add_inductive in SIP}

    49   add_inductive in SimpleInductivePackage} expects them to be given as

    50 expects them to be given as optional strings. If no string is

    50   optional strings. If no string is given for a particular predicate or

    51 given for a particular predicate or parameter, this means that the type should be

    51   parameter, this means that the type should be inferred by the

    52 inferred by the package. Additional \emph{mixfix syntax} may be associated with

    52   package. Additional \emph{mixfix syntax} may be associated with the

    53 the predicates and parameters as well. Note that @{ML add_inductive_i in SIP} does not

    53   predicates and parameters as well. Note that @{ML add_inductive_i in

    54 allow mixfix syntax to be associated with parameters, since it can only be used

    54   SimpleInductivePackage} does not allow mixfix syntax to be associated with

    55 for parsing. The names of the predicates, parameters and rules are represented by the

    55   parameters, since it can only be used for parsing. The names of the

    56 type @{ML_type Binding.binding}. Strings can be turned into elements of the type

    56   predicates, parameters and rules are represented by the type @{ML_type

    57 @{ML_type Binding.binding} using the function

    57   Binding.binding}. Strings can be turned into elements of the type @{ML_type

    58 @{ML [display] "Binding.name : string -> Binding.binding"}

    58   Binding.binding} using the function @{ML [display] "Binding.name : string ->

    59 Each introduction rule is given as a tuple containing its name, a list of \emph{attributes}

    59   Binding.binding"} Each introduction rule is given as a tuple containing its

    60 and a logical formula. Note that the type @{ML_type Attrib.binding} used in the list of

    60   name, a list of \emph{attributes} and a logical formula. Note that the type

    61 introduction rules is just a shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}.

    61   @{ML_type Attrib.binding} used in the list of introduction rules is just a

    62 The function @{ML add_inductive_i in SIP} expects the formula to be specified using the datatype

    62   shorthand for the type @{ML_type "Binding.binding * Attrib.src list"}.  The

    63 @{ML_type term}, whereas @{ML add_inductive in SIP} expects it to be given as a string.

    63   function @{ML add_inductive_i in SimpleInductivePackage} expects the formula

    64 An attribute specifies additional actions and transformations that should be applied to

    64   to be specified using the datatype @{ML_type term}, whereas @{ML

    65 a theorem, such as storing it in the rule databases used by automatic tactics

    65   add_inductive in SimpleInductivePackage} expects it to be given as a string.

    66 like the simplifier. The code of the package, which will be described in the following

    66   An attribute specifies additional actions and transformations that should be

    67 section, will mostly treat attributes as a black box and just forward them to other

    67   applied to a theorem, such as storing it in the rule databases used by

    68 functions for storing theorems in local theories.

    68   automatic tactics like the simplifier. The code of the package, which will

    69 The implementation of the function @{ML add_inductive in SIP} for external invocation

    69   be described in the following section, will mostly treat attributes as a

    70 of the package is quite simple. Essentially, it just parses the introduction rules

    70   black box and just forward them to other functions for storing theorems in

    71 and then passes them on to @{ML add_inductive_i in SIP}:

    71   local theories.  The implementation of the function @{ML add_inductive in

    72 @{ML_chunk [display] add_inductive}

    72   SimpleInductivePackage} for external invocation of the package is quite

    73 For parsing and type checking the introduction rules, we use the function

    73   simple. Essentially, it just parses the introduction rules and then passes

    74 @{ML [display] "Specification.read_specification:

    74   them on to @{ML add_inductive_i in SimpleInductivePackage}:

    75 

    76   @{ML_chunk [display] add_inductive}

    77 

    78   For parsing and type checking the introduction rules, we use the function

    79   

    80   @{ML [display] "Specification.read_specification:

    84 During parsing, both predicates and parameters are treated as variables, so

    90   During parsing, both predicates and parameters are treated as variables, so

    85 the lists \verb!preds_syn! and \verb!params_syn! are just appended

    91   the lists \verb!preds_syn! and \verb!params_syn! are just appended

    86 before being passed to @{ML read_specification in Specification}. Note that the format

    92   before being passed to @{ML read_specification in Specification}. Note that the format

    87 for rules supported by @{ML read_specification in Specification} is more general than

    93   for rules supported by @{ML read_specification in Specification} is more general than

    88 what is required for our package. It allows several rules to be associated

    94   what is required for our package. It allows several rules to be associated

    89 with one name, and the list of rules can be partitioned into several

    95   with one name, and the list of rules can be partitioned into several

    90 sublists. In order for the list \verb!intro_srcs! of introduction rules

    96   sublists. In order for the list \verb!intro_srcs! of introduction rules

    91 to be acceptable as an input for @{ML read_specification in Specification}, we first

    97   to be acceptable as an input for @{ML read_specification in Specification}, we first

    92 have to turn it into a list of singleton lists. This transformation

    98   have to turn it into a list of singleton lists. This transformation

    93 has to be reversed later on by applying the function

    99   has to be reversed later on by applying the function

    94 @{ML [display] "the_single: 'a list -> 'a"}

   100   @{ML [display] "the_single: 'a list -> 'a"}

    95 to the list \verb!specs! containing the parsed introduction rules.

   101   to the list \verb!specs! containing the parsed introduction rules.

    96 The function @{ML read_specification in Specification} also returns the list \verb!vars!

   102   The function @{ML read_specification in Specification} also returns the list \verb!vars!

    97 of predicates and parameters that contains the inferred types as well.

   103   of predicates and parameters that contains the inferred types as well.

    98 This list has to be chopped into the two lists \verb!preds_syn'! and

   104   This list has to be chopped into the two lists \verb!preds_syn'! and

    99 \verb!params_syn'! for predicates and parameters, respectively.

   105   \verb!params_syn'! for predicates and parameters, respectively.

   100 All variables occurring in a rule but not in the list of variables passed to

   106   All variables occurring in a rule but not in the list of variables passed to

   101 @{ML read_specification in Specification} will be bound by a meta-level universal

   107   @{ML read_specification in Specification} will be bound by a meta-level universal

   102 quantifier.

   108   quantifier.

   103 *}

   109 *}

   104 

   110 

   105 text {*

   111 text {*

   106 Finally, @{ML read_specification in Specification} also returns another local theory,

   112   Finally, @{ML read_specification in Specification} also returns another local theory,

   107 but we can safely discard it. As an example, let us look at how we can use this

   113   but we can safely discard it. As an example, let us look at how we can use this

   108 function to parse the introduction rules of the @{text trcl} predicate:

   114   function to parse the introduction rules of the @{text trcl} predicate:

   109 @{ML_response [display]

   115 

   116   @{ML_response [display]

   132 In the list of variables passed to @{ML read_specification in Specification}, we have

   139 

   133 used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any

   140   In the list of variables passed to @{ML read_specification in Specification}, we have

   134 mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r},

   141   used the mixfix annotation @{ML NoSyn} to indicate that we do not want to associate any

   135 whereas the type of \texttt{trcl} is computed using type inference.

   142   mixfix syntax with the variable. Moreover, we have only specified the type of \texttt{r},

   136 The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules

   143   whereas the type of \texttt{trcl} is computed using type inference.

   137 are turned into bound variables with the de Bruijn indices,

   144   The local variables \texttt{x}, \texttt{y} and \texttt{z} of the introduction rules

   138 whereas \texttt{trcl} and \texttt{r} remain free variables.

   145   are turned into bound variables with the de Bruijn indices,

   139 *}

   146   whereas \texttt{trcl} and \texttt{r} remain free variables.

   140 

   147 

   141 text {*

   148 *}

   142 \paragraph{Parsers for theory syntax}

   149 

   143 

   150 text {*

   144 Although the function @{ML add_inductive in SIP} parses terms and types, it still

   151 

   145 cannot be used to invoke the package directly from within a theory document.

   152   \paragraph{Parsers for theory syntax}

   146 In order to do this, we have to write another parser. Before we describe

   153 

   147 the process of writing parsers for theory syntax in more detail, we first

   154   Although the function @{ML add_inductive in SimpleInductivePackage} parses terms and types, it still

   148 show some examples of how we would like to use the inductive definition

   155   cannot be used to invoke the package directly from within a theory document.

   149 package.

   156   In order to do this, we have to write another parser. Before we describe

   150 

   157   the process of writing parsers for theory syntax in more detail, we first

   151 \noindent

   158   show some examples of how we would like to use the inductive definition

   152 The definition of the transitive closure should look as follows:

   159   package.

   160 

   161 

   162   The definition of the transitive closure should look as follows:

   191 text {*

   201 text {* Even and odd numbers can be defined by *}

   192 \noindent

   193 Even and odd numbers can be defined by

   194 *}

   211 text {*

   218 text {* The accessible part of a relation can be introduced as follows: *}

   212 \noindent

   213 The accessible part of a relation can be introduced as follows:

   214 *}

   227 \noindent

   231   Moreover, it should also be possible to define the accessible part

   228 Moreover, it should also be possible to define the accessible part

   232   inside a locale fixing the relation @{text r}:

   229 inside a locale fixing the relation @{text r}:

   250 ML {*

   253 ML{*val (result, lthy) = SimpleInductivePackage.add_inductive

   251 val (result, lthy) = SimpleInductivePackage.add_inductive

   259 \noindent

   261 

   260 In this context, it is important to note that Isabelle distinguishes

   262   In this context, it is important to note that Isabelle distinguishes

   261 between \emph{outer} and \emph{inner} syntax. Theory commands such as

   263   between \emph{outer} and \emph{inner} syntax. Theory commands such as

   262 \isa{\isacommand{simple{\isacharunderscore}inductive} $\ldots$ \isacommand{for} $\ldots$ \isacommand{where} $\ldots$}

   264   \isa{\isacommand{simple{\isacharunderscore}inductive} $\ldots$ \isacommand{for} $\ldots$ \isacommand{where} $\ldots$}

   263 belong to the outer syntax, whereas items in quotation marks, in particular

   265   belong to the outer syntax, whereas items in quotation marks, in particular

   264 terms such as @{text [source] "trcl r x x"} and types such as

   266   terms such as @{text [source] "trcl r x x"} and types such as

   265 @{text [source] "'a \<Rightarrow> 'a \<Rightarrow> bool"} belong to the inner syntax.

   267   @{text [source] "'a \<Rightarrow> 'a \<Rightarrow> bool"} belong to the inner syntax.

   266 Separating the two layers of outer and inner syntax greatly simplifies

   268   Separating the two layers of outer and inner syntax greatly simplifies

   267 matters, because the parser for terms and types does not have to know

   269   matters, because the parser for terms and types does not have to know

   268 anything about the possible syntax of theory commands, and the parser

   270   anything about the possible syntax of theory commands, and the parser

   269 for theory commands need not be concerned about the syntactic structure

   271   for theory commands need not be concerned about the syntactic structure

   270 of terms and types.

   272   of terms and types.

   271 

   273 

   272 \medskip

   274   \medskip

   273 \noindent

   275   \noindent

   274 The syntax of the \isa{\isacommand{simple{\isacharunderscore}inductive}} command

   276   The syntax of the \isa{\isacommand{simple{\isacharunderscore}inductive}} command

   275 can be described by the following railroad diagram:

   277   can be described by the following railroad diagram:

   276 \begin{rail}

   278   \begin{rail}

   280 \end{rail}

   282   \end{rail}

   281 

   283 

   282 \paragraph{Functional parsers}

   284   \paragraph{Functional parsers}

   283 

   285 

   284 For parsing terms and types, Isabelle uses a rather general and sophisticated

   286   For parsing terms and types, Isabelle uses a rather general and sophisticated

   285 algorithm due to Earley, which is driven by \emph{priority grammars}.

   287   algorithm due to Earley, which is driven by \emph{priority grammars}.

   286 In contrast, parsers for theory syntax are built up using a set of combinators.

   288   In contrast, parsers for theory syntax are built up using a set of combinators.

   287 Functional parsing using combinators is a well-established technique, which

   289   Functional parsing using combinators is a well-established technique, which

   288 has been described by many authors, including Paulson \cite{paulson-ML-91}

   290   has been described by many authors, including Paulson \cite{paulson-ML-91}

   289 and Wadler \cite{Wadler-AFP95}. 

   291   and Wadler \cite{Wadler-AFP95}. 

   290 The central idea is that a parser is a function of type @{ML_type "'a list -> 'b * 'a list"},

   292   The central idea is that a parser is a function of type @{ML_type "'a list -> 'b * 'a list"},

   291 where @{ML_type "'a"} is a type of \emph{tokens}, and @{ML_type "'b"} is a type for

   293   where @{ML_type "'a"} is a type of \emph{tokens}, and @{ML_type "'b"} is a type for

   292 encoding items that the parser has recognized. When a parser is applied to a

   294   encoding items that the parser has recognized. When a parser is applied to a

   293 list of tokens whose prefix it can recognize, it returns an encoding of the

   295   list of tokens whose prefix it can recognize, it returns an encoding of the

   294 prefix as an element of type @{ML_type "'b"}, together with the suffix of the list

   296   prefix as an element of type @{ML_type "'b"}, together with the suffix of the list

   295 containing the remaining tokens. Otherwise, the parser raises an exception

   297   containing the remaining tokens. Otherwise, the parser raises an exception

   296 indicating a syntax error. The library for writing functional parsers in

   298   indicating a syntax error. The library for writing functional parsers in

   297 Isabelle can roughly be split up into two parts. The first part consists of a

   299   Isabelle can roughly be split up into two parts. The first part consists of a

   298 collection of generic parser combinators that are contained in the structure

   300   collection of generic parser combinators that are contained in the structure

   299 @{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle

   301   @{ML_struct Scan} defined in the file @{ML_file "Pure/General/scan.ML"} in the Isabelle

   300 sources. While these combinators do not make any assumptions about the concrete

   302   sources. While these combinators do not make any assumptions about the concrete

   301 structure of the tokens used, the second part of the library consists of combinators

   303   structure of the tokens used, the second part of the library consists of combinators

   302 for dealing with specific token types.

   304   for dealing with specific token types.

   303 The following is an excerpt from the signature of @{ML_struct Scan}:

   305   The following is an excerpt from the signature of @{ML_struct Scan}:

   304 

   306 

   305 \begin{table}

   307   \begin{table}

   306 @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\

   308   @{ML "|| : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b"} \\

   307 @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\

   309   @{ML "-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e"} \\

   308 @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\

   310   @{ML "|-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e"} \\

   309 @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\

   311   @{ML "--| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e"} \\

   310 @{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\

   312   @{ML "optional: ('a -> 'b * 'a) -> 'b -> 'a -> 'b * 'a" in Scan} \\

   311 @{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

   313   @{ML "repeat: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

   312 @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

   314   @{ML "repeat1: ('a -> 'b * 'a) -> 'a -> 'b list * 'a" in Scan} \\

   313 @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\

   315   @{ML ">> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c"} \\

   314 @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}

   316   @{ML "!! : ('a * string option -> string) -> ('a -> 'b) -> 'a -> 'b"}

   315 \end{table}

   317   \end{table}

   316 Interestingly, the functions shown above are so generic that they do not

   318 

   317 even rely on the input and output of the parser being a list of tokens.

   319   Interestingly, the functions shown above are so generic that they do not

   318 If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser

   320   even rely on the input and output of the parser being a list of tokens.

   319 @{ML "p || q" for p q} returns the result of \texttt{p}, otherwise it returns

   321   If \texttt{p} succeeds, i.e.\ does not raise an exception, the parser

   320 the result of \texttt{q}. The parser @{ML "p -- q" for p q} first parses an

   322   @{ML "p || q" for p q} returns the result of \texttt{p}, otherwise it returns

   321 item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens

   323   the result of \texttt{q}. The parser @{ML "p -- q" for p q} first parses an

   322 of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}

   324   item of type @{ML_type "'b"} using \texttt{p}, then passes the remaining tokens

   323 and returns the remaining tokens of type @{ML_type "'e"}, which are finally

   325   of type @{ML_type "'c"} to \texttt{q}, which parses an item of type @{ML_type "'d"}

   324 returned together with a pair of type @{ML_type "'b * 'd"} containing the two

   326   and returns the remaining tokens of type @{ML_type "'e"}, which are finally

   325 parsed items. The parsers @{ML "p |-- q" for p q} and @{ML "p --| q" for p q}

   327   returned together with a pair of type @{ML_type "'b * 'd"} containing the two

   326 work in a similar way as the previous one, with the difference that they

   328   parsed items. The parsers @{ML "p |-- q" for p q} and @{ML "p --| q" for p q}

   327 discard the item parsed by the first and the second parser, respectively.

   329   work in a similar way as the previous one, with the difference that they

   328 If \texttt{p} succeeds, the parser @{ML "optional p x" for p x in Scan} returns the result

   330   discard the item parsed by the first and the second parser, respectively.

   329 of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser

   331   If \texttt{p} succeeds, the parser @{ML "optional p x" for p x in Scan} returns the result

   330 @{ML "repeat p" for p in Scan} applies \texttt{p} as often as it can, returning a possibly

   332   of \texttt{p}, otherwise it returns the default value \texttt{x}. The parser

   331 empty list of parsed items. The parser @{ML "repeat1 p" for p in Scan} is similar,

   333   @{ML "repeat p" for p in Scan} applies \texttt{p} as often as it can, returning a possibly

   332 but requires \texttt{p} to succeed at least once. The parser

   334   empty list of parsed items. The parser @{ML "repeat1 p" for p in Scan} is similar,

   333 @{ML "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which

   335   but requires \texttt{p} to succeed at least once. The parser

   334 it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which

   336   @{ML "p >> f" for p f} uses \texttt{p} to parse an item of type @{ML_type "'b"}, to which

   335 is returned together with the remaining tokens of type @{ML_type "'c"}.

   337   it applies the function \texttt{f} yielding a value of type @{ML_type "'d"}, which

   336 Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.

   338   is returned together with the remaining tokens of type @{ML_type "'c"}.

   337 If \texttt{p} raises an exception indicating that it cannot parse a given input,

   339   Finally, @{ML "!!"} is used for transforming exceptions produced by parsers.

   338 then an enclosing parser such as

   340   If \texttt{p} raises an exception indicating that it cannot parse a given input,

   339 @{ML [display] "q -- p || r" for p q r}

   341   then an enclosing parser such as

   340 will try the alternative parser \texttt{r}. By writing

   342   @{ML [display] "q -- p || r" for p q r}

   341 @{ML [display] "q -- !! err p || r" for err p q r}

   343   will try the alternative parser \texttt{r}. By writing

   342 instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.

   344   @{ML [display] "q -- !! err p || r" for err p q r}

   343 The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents

   345   instead, one can achieve that a failure of \texttt{p} causes the whole parser to abort.

   344 the interpreter from backtracking. The \texttt{err} function supplied as an argument

   346   The @{ML "!!"} operator is similar to the \emph{cut} operator in Prolog, which prevents

   345 to @{ML "!!"} can be used to produce an error message depending on the current

   347   the interpreter from backtracking. The \texttt{err} function supplied as an argument

   346 state of the parser, as well as the optional error message returned by \texttt{p}.

   348   to @{ML "!!"} can be used to produce an error message depending on the current

   347 

   349   state of the parser, as well as the optional error message returned by \texttt{p}.

   348 So far, we have only looked at combinators that construct more complex parsers

   350   

   349 from simpler parsers. In order for these combinators to be useful, we also need

   351   So far, we have only looked at combinators that construct more complex parsers

   350 some basic parsers. As an example, we consider the following two parsers

   352   from simpler parsers. In order for these combinators to be useful, we also need

   351 defined in @{ML_struct Scan}:

   353   some basic parsers. As an example, we consider the following two parsers

   352 

   354   defined in @{ML_struct Scan}:

   353 \begin{table}

   355   

   354 @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\

   356   \begin{table}

   355 @{ML "$$ : string -> string list -> string * string list"}

   357   @{ML "one: ('a -> bool) -> 'a list -> 'a * 'a list" in Scan} \\

   356 \end{table}

   358   @{ML "$$ : string -> string list -> string * string list"}

   357 

   359   \end{table}

   358 The parser @{ML "one pred" for pred in Scan} parses exactly one token that

   360   

   359 satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only

   361   The parser @{ML "one pred" for pred in Scan} parses exactly one token that

   360 accepts a token that equals the string \texttt{s}. Note that we can easily

   362   satisfies the predicate \texttt{pred}, whereas @{ML "$$ s" for s} only

   361 express @{ML "$$ s" for s} using @{ML "one" in Scan}:

   363   accepts a token that equals the string \texttt{s}. Note that we can easily

   362 @{ML [display] "one (fn s' => s' = s)" for s in Scan}

   364   express @{ML "$$ s" for s} using @{ML "one" in Scan}:

   363 As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse

   365   @{ML [display] "one (fn s' => s' = s)" for s in Scan}

   364 the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':

   366   As an example, let us look at how we can use @{ML "$$"} and @{ML "--"} to parse

   365 @{ML_response [display]

   367   the prefix ``\texttt{hello}'' of the character list ``\texttt{hello world}'':

   366 "($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\")

   368   

   367 [\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]"

   369   @{ML_response [display]

   368 "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"])

   370   "($$ \"h\" -- $$ \"e\" -- $$ \"l\" -- $$ \"l\" -- $$ \"o\")

   369 : ((((string * string) * string) * string) * string) * string list"}

   371   [\"h\", \"e\", \"l\", \"l\", \"o\", \" \", \"w\", \"o\", \"r\", \"l\", \"d\"]"

   370 Most of the time, however, we will have to deal with tokens that are not just strings.

   372   "(((((\"h\", \"e\"), \"l\"), \"l\"), \"o\"), [\" \", \"w\", \"o\", \"r\", \"l\", \"d\"])

   371 The parsers for the theory syntax, as well as the parsers for the argument syntax

   373   : ((((string * string) * string) * string) * string) * string list"}

   372 of proof methods and attributes use the token type @{ML_type OuterParse.token},

   374 

   373 which is identical to @{ML_type OuterLex.token}.

   375   Most of the time, however, we will have to deal with tokens that are not just strings.

   374 The parser functions for the theory syntax are contained in the structure

   376   The parsers for the theory syntax, as well as the parsers for the argument syntax

   375 @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.

   377   of proof methods and attributes use the token type @{ML_type OuterParse.token},

   376 In our parser, we will use the following functions:

   378   which is identical to @{ML_type OuterLex.token}.

   377 

   379   The parser functions for the theory syntax are contained in the structure

   378 \begin{table}

   380   @{ML_struct OuterParse} defined in the file @{ML_file "Pure/Isar/outer_parse.ML"}.

   379 @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\

   381   In our parser, we will use the following functions:

   380 @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->

   382   

   383   \begin{table}

   384   @{ML "$$$ : string -> token list -> string * token list" in OuterParse} \\

   385   @{ML "enum1: string -> (token list -> 'a * token list) -> token list ->

   382 @{ML "prop: token list -> string * token list" in OuterParse} \\

   387   @{ML "prop: token list -> string * token list" in OuterParse} \\

   383 @{ML "opt_target: token list -> string option * token list" in OuterParse} \\

   388   @{ML "opt_target: token list -> string option * token list" in OuterParse} \\

   384 @{ML "fixes: token list ->

   389   @{ML "fixes: token list ->

   386 @{ML "for_fixes: token list ->

   391   @{ML "for_fixes: token list ->

   388 @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}

   393   @{ML "!!! : (token list -> 'a) -> token list -> 'a" in OuterParse}

   389 \end{table}

   394   \end{table}

   390 

   395 

   391 The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are

   396   The parsers @{ML "$$$" in OuterParse} and @{ML "!!!" in OuterParse} are

   392 defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from

   397   defined using the parsers @{ML "one" in Scan} and @{ML "!!"} from

   393 @{ML_struct Scan}.

   398   @{ML_struct Scan}.

   394 The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items

   399   The parser @{ML "enum1 s p" for s p in OuterParse} parses a non-emtpy list of items

   395 recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.

   400   recognized by the parser \texttt{p}, where the items are separated by \texttt{s}.

   396 A proposition can be parsed using the function @{ML prop in OuterParse}.

   401   A proposition can be parsed using the function @{ML prop in OuterParse}.

   397 Essentially, a proposition is just a string or an identifier, but using the

   402   Essentially, a proposition is just a string or an identifier, but using the

   398 specific parser function @{ML prop in OuterParse} leads to more instructive

   403   specific parser function @{ML prop in OuterParse} leads to more instructive

   399 error messages, since the parser will complain that a proposition was expected

   404   error messages, since the parser will complain that a proposition was expected

   400 when something else than a string or identifier is found.

   405   when something else than a string or identifier is found.

   401 An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)}

   406   An optional locale target specification of the form \isa{(\isacommand{in}\ $\ldots$)}

   402 can be parsed using @{ML opt_target in OuterParse}.

   407   can be parsed using @{ML opt_target in OuterParse}.

   403 The lists of names of the predicates and parameters, together with optional

   408   The lists of names of the predicates and parameters, together with optional

   404 types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}

   409   types and syntax, are parsed using the functions @{ML "fixes" in OuterParse}

   405 and @{ML for_fixes in OuterParse}, respectively.

   410   and @{ML for_fixes in OuterParse}, respectively.

   406 In addition, the following function from @{ML_struct SpecParse} for parsing

   411   In addition, the following function from @{ML_struct SpecParse} for parsing

   407 an optional theorem name and attribute, followed by a delimiter, will be useful:

   412   an optional theorem name and attribute, followed by a delimiter, will be useful:

   408 

   413   

   409 \begin{table}

   414   \begin{table}

   410 @{ML "opt_thm_name:

   415   @{ML "opt_thm_name:

   412 \end{table}

   417   \end{table}

   413 

   418 

   414 We now have all the necessary tools to write the parser for our

   419   We now have all the necessary tools to write the parser for our

   415 \isa{\isacommand{simple{\isacharunderscore}inductive}} command:

   420   \isa{\isacommand{simple{\isacharunderscore}inductive}} command:

   416 @{ML_chunk [display] syntax}

   421   

   417 The definition of the parser \verb!ind_decl! closely follows the railroad

   422   @{ML_chunk [display] syntax}

   418 diagram shown above. In order to make the code more readable, the structures

   423 

   419 @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by

   424   The definition of the parser \verb!ind_decl! closely follows the railroad

   420 \texttt{P} and \texttt{K}, respectively. Note how the parser combinator

   425   diagram shown above. In order to make the code more readable, the structures

   421 @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}

   426   @{ML_struct OuterParse} and @{ML_struct OuterKeyword} are abbreviated by

   422 has been parsed, a non-empty list of introduction rules must follow.

   427   \texttt{P} and \texttt{K}, respectively. Note how the parser combinator

   423 Had we not used the combinator @{ML "!!!" in OuterParse}, a

   428   @{ML "!!!" in OuterParse} is used: once the keyword \texttt{where}

   424 \texttt{where} not followed by a list of rules would have caused the parser

   429   has been parsed, a non-empty list of introduction rules must follow.

   425 to respond with the somewhat misleading error message

   430   Had we not used the combinator @{ML "!!!" in OuterParse}, a

   426 \begin{verbatim}

   431   \texttt{where} not followed by a list of rules would have caused the parser

   432   to respond with the somewhat misleading error message

   433 

   434   \begin{verbatim}

   428 \end{verbatim}

   436   \end{verbatim}

   429 rather than with the more instructive message

   437 

   430 \begin{verbatim}

   438   rather than with the more instructive message

   439 

   440   \begin{verbatim}

   432 \end{verbatim}

   442   \end{verbatim}

   433 Once all arguments of the command have been parsed, we apply the function

   443 

   434 @{ML add_inductive in SimpleInductivePackage}, which yields a local theory

   444   Once all arguments of the command have been parsed, we apply the function

   435 transformer of type @{ML_type "local_theory -> local_theory"}. Commands in

   445   @{ML add_inductive in SimpleInductivePackage}, which yields a local theory

   436 Isabelle/Isar are realized by transition transformers of type

   446   transformer of type @{ML_type "local_theory -> local_theory"}. Commands in

   437 @{ML_type [display] "Toplevel.transition -> Toplevel.transition"}

   447   Isabelle/Isar are realized by transition transformers of type

   438 We can turn a local theory transformer into a transition transformer by using

   448   @{ML_type [display] "Toplevel.transition -> Toplevel.transition"}

   439 the function

   449   We can turn a local theory transformer into a transition transformer by using

   440 @{ML [display] "Toplevel.local_theory : string option ->

   450   the function

   451 

   452   @{ML [display] "Toplevel.local_theory : string option ->

   443 which, apart from the local theory transformer, takes an optional name of a locale

   455  

   444 to be used as a basis for the local theory. 

   456   which, apart from the local theory transformer, takes an optional name of a locale

   445 

   457   to be used as a basis for the local theory. 

   446 (FIXME : needs to be adjusted to new parser type)

   458 

   447 

   459   (FIXME : needs to be adjusted to new parser type)

   448 {\it

   460 

   449 The whole parser for our command has type

   461   {\it

   450 @{ML_text [display] "OuterLex.token list ->

   462   The whole parser for our command has type

   463   @{ML_text [display] "OuterLex.token list ->

   452 which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added

   465   which is abbreviated by @{ML_text OuterSyntax.parser_fn}. The new command can be added

   453 to the system via the function

   466   to the system via the function

   454 @{ML_text [display] "OuterSyntax.command :

   467   @{ML_text [display] "OuterSyntax.command :

   456 which imperatively updates the parser table behind the scenes. }

   469   which imperatively updates the parser table behind the scenes. }

   457 

   470 

   458 In addition to the parser, this

   471   In addition to the parser, this

   459 function takes two strings representing the name of the command and a short description,

   472   function takes two strings representing the name of the command and a short description,

   460 as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of

   473   as well as an element of type @{ML_type OuterKeyword.T} describing which \emph{kind} of

   461 command we intend to add. Since we want to add a command for declaring new concepts,

   474   command we intend to add. Since we want to add a command for declaring new concepts,

   462 we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include

   475   we choose the kind @{ML "OuterKeyword.thy_decl"}. Other kinds include

   463 @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword},

   476   @{ML "OuterKeyword.thy_goal"}, which is similar to @{ML thy_decl in OuterKeyword},

   464 but requires the user to prove a goal before making the declaration, or

   477   but requires the user to prove a goal before making the declaration, or

   465 @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does

   478   @{ML "OuterKeyword.diag"}, which corresponds to a purely diagnostic command that does

   466 not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used

   479   not change the context. For example, the @{ML thy_goal in OuterKeyword} kind is used

   467 by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user

   480   by the \isa{\isacommand{function}} command \cite{Krauss-IJCAR06}, which requires the user

   468 to prove that a given set of equations is non-overlapping and covers all cases. The kind

   481   to prove that a given set of equations is non-overlapping and covers all cases. The kind

   469 of the command should be chosen with care, since selecting the wrong one can cause strange

   482   of the command should be chosen with care, since selecting the wrong one can cause strange

   470 behaviour of the user interface, such as failure of the undo mechanism.

   483   behaviour of the user interface, such as failure of the undo mechanism.