ProgTutorial/Parsing.thy
author griff
Wed, 22 Jul 2009 14:02:47 +0200
changeset 285 abe5306cacbe
parent 284 ee139d9d7ab8
child 286 ff0b3d87a551
permissions -rw-r--r--
spell checker
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     1
theory Parsing
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
     2
imports Base "Package/Simple_Inductive_Package"
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
begin
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
chapter {* Parsing *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     6
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
     9
  Isabelle distinguishes between \emph{outer} and \emph{inner} syntax. 
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    10
  Commands, such as \isacommand{definition}, \isacommand{inductive} and so
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    11
  on, belong to the outer syntax, whereas terms, types and so on belong to the 
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    12
  inner syntax. For parsing inner syntax, 
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
    13
  Isabelle uses a rather general and sophisticated algorithm, which 
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    14
  is driven by priority grammars. Parsers for outer syntax are built up by functional
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    15
  parsing combinators. These combinators are a well-established technique for parsing, 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
    16
  which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}.
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    17
  Isabelle developers are usually concerned with writing these outer syntax parsers, 
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
    18
  either for new definitional packages or for calling methods with specific arguments. 
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    19
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    20
  \begin{readmore}
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    21
  The library for writing parser combinators is split up, roughly, into two
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    22
  parts. The first part consists of a collection of generic parser combinators
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    23
  defined in the structure @{ML_struct Scan} in the file @{ML_file
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    24
  "Pure/General/scan.ML"}. The second part of the library consists of
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    25
  combinators for dealing with specific token types, which are defined in the
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    26
  structure @{ML_struct OuterParse} in the file @{ML_file
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    27
  "Pure/Isar/outer_parse.ML"}. Specific parsers for packages are defined
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    28
  in @{ML_file "Pure/Isar/spec_parse.ML"}. Parsers for method arguments
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
    29
  are defined in @{ML_file "Pure/Isar/args.ML"}.
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    30
  \end{readmore}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    31
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    32
*}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    33
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
    34
section {* Building Generic Parsers *}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    35
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    36
text {*
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    37
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    38
  Let us first have a look at parsing strings using generic parsing
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    39
  combinators. The function @{ML [index] "$$"} takes a string as argument and will
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    40
  ``consume'' this string from a given input list of strings. ``Consume'' in
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    41
  this context means that it will return a pair consisting of this string and
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    42
  the rest of the input list. For example:
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    43
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    44
  @{ML_response [display,gray] 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    45
  "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    46
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    47
  @{ML_response [display,gray] 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    48
  "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    49
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    50
  The function @{ML "$$"} will either succeed (as in the two examples above)
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    51
  or raise the exception @{text "FAIL"} if no string can be consumed. For
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    52
  example trying to parse
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    53
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    54
  @{ML_response_fake [display,gray] 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    55
  "($$ \"x\") (Symbol.explode \"world\")" 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    56
  "Exception FAIL raised"}
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    57
  
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    58
  will raise the exception @{text "FAIL"}.  There are three exceptions used in
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    59
  the parsing combinators:
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    60
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    61
  \begin{itemize}
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
    62
  \item @{text "FAIL"} is used to indicate that alternative routes of parsing 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    63
  might be explored. 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
    64
  \item @{text "MORE"} indicates that there is not enough input for the parser. For example 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
    65
  in @{text "($$ \"h\") []"}.
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 59
diff changeset
    66
  \item @{text "ABORT"} is the exception that is raised when a dead end is reached. 
108
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
parents: 105
diff changeset
    67
  It is used for example in the function @{ML "!!"} (see below).
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    68
  \end{itemize}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    69
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    70
  However, note that these exceptions are private to the parser and cannot be accessed
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
    71
  by the programmer (for example to handle them).
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    72
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    73
  \indexdef{explode@ {\tt\slshape{}explode}}{in {\tt\slshape Symbol}}
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    74
  \index{explode@ {\tt\slshape{}explode}}
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    75
  In the examples above we use the function @{ML Symbol.explode}, instead of the 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    76
  more standard library function @{ML explode}, for obtaining an input list for 
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    77
  the parser. The reason is that @{ML Symbol.explode} is aware of character sequences,
261
358f325f4db6 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 258
diff changeset
    78
  for example @{text "\<foo>"}, that have a special meaning in Isabelle. To see
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    79
  the difference consider
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    80
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    81
@{ML_response_fake [display,gray]
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    82
"let 
261
358f325f4db6 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 258
diff changeset
    83
  val input = \"\<foo> bar\"
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    84
in
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    85
  (explode input, Symbol.explode input)
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    86
end"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    87
"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
261
358f325f4db6 updated to new Isabelle
Christian Urban <urbanc@in.tum.de>
parents: 258
diff changeset
    88
 [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
    89
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    90
  Slightly more general than the parser @{ML "$$"} is the function 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    91
  @{ML [index] one in Scan}, in that it takes a predicate as argument and 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
    92
  then parses exactly
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
    93
  one item from the input list satisfying this predicate. For example the
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
    94
  following parser either consumes an @{text [quotes] "h"} or a @{text
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
    95
  [quotes] "w"}:
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    96
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
    97
@{ML_response [display,gray] 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    98
"let 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
    99
  val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   100
  val input1 = Symbol.explode \"hello\"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   101
  val input2 = Symbol.explode \"world\"
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   102
in
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   103
  (hw input1, hw input2)
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   104
end"
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   105
    "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   106
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   107
  Two parsers can be connected in sequence by using the function @{ML [index] "--"}. 
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   108
  For example parsing @{text "h"}, @{text "e"} and @{text "l"} (in this 
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   109
  order) you can achieve by:
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   110
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   111
  @{ML_response [display,gray] 
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   112
  "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   113
  "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   114
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   115
  Note how the result of consumed strings builds up on the left as nested pairs.  
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   116
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   117
  If, as in the previous example, you want to parse a particular string, 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   118
  then you should use the function @{ML [index] this_string in Scan}:
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   119
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   120
  @{ML_response [display,gray] 
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   121
  "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   122
  "(\"hell\", [\"o\"])"}
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   123
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   124
  Parsers that explore alternatives can be constructed using the function 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   125
  @{ML [index] "||"}. The parser @{ML "(p || q)" for p q} returns the
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   126
  result of @{text "p"}, in case it succeeds, otherwise it returns the
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   127
  result of @{text "q"}. For example:
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   128
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   129
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   130
@{ML_response [display,gray] 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   131
"let 
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   132
  val hw = $$ \"h\" || $$ \"w\"
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   133
  val input1 = Symbol.explode \"hello\"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   134
  val input2 = Symbol.explode \"world\"
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   135
in
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   136
  (hw input1, hw input2)
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   137
end"
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   138
  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   139
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   140
  The functions @{ML [index] "|--"} and @{ML [index] "--|"} work like the sequencing function 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   141
  for parsers, except that they discard the item being parsed by the first (respectively second)
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   142
  parser. For example:
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   143
  
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   144
@{ML_response [display,gray]
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   145
"let 
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   146
  val just_e = $$ \"h\" |-- $$ \"e\" 
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   147
  val just_h = $$ \"h\" --| $$ \"e\" 
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   148
  val input = Symbol.explode \"hello\"  
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   149
in 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   150
  (just_e input, just_h input)
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   151
end"
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   152
  "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   153
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   154
  \indexdef{optional@ {\tt\slshape{optional}}}{in {\tt\slshape Scan}}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   155
  The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   156
  @{text "p"}, if it succeeds; otherwise it returns 
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   157
  the default value @{text "x"}. For example:
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   158
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   159
@{ML_response [display,gray]
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   160
"let 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   161
  val p = Scan.optional ($$ \"h\") \"x\"
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   162
  val input1 = Symbol.explode \"hello\"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   163
  val input2 = Symbol.explode \"world\"  
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   164
in 
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   165
  (p input1, p input2)
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   166
end" 
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   167
 "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   168
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   169
  The function @{ML [index] option in Scan} works similarly, except no default value can
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   170
  be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   171
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   172
@{ML_response [display,gray]
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   173
"let 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   174
  val p = Scan.option ($$ \"h\")
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   175
  val input1 = Symbol.explode \"hello\"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   176
  val input2 = Symbol.explode \"world\"  
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   177
in 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   178
  (p input1, p input2)
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   179
end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   180
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   181
  The function @{ML [index] "!!"} helps to produce appropriate error messages
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   182
  for parsing. For example if you want to parse @{text p} immediately 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   183
  followed by @{text q}, or start a completely different parser @{text r},
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   184
  you might write:
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   185
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   186
  @{ML [display,gray] "(p -- q) || r" for p q r}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   187
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   188
  However, this parser is problematic for producing an appropriate error
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   189
  message, if the parsing of @{ML "(p -- q)" for p q} fails. Because in that
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   190
  case you lose the information that @{text p} should be followed by @{text q}.
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   191
  To see this assume that @{text p} is present in the input, but it is not
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   192
  followed by @{text q}. That means @{ML "(p -- q)" for p q} will fail and
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   193
  hence the alternative parser @{text r} will be tried. However, in many
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   194
  circumstances this will be the wrong parser for the input ``@{text "p"}-followed-by-something''
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   195
  and therefore will also fail. The error message is then caused by the failure
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   196
  of @{text r}, not by the absence of @{text q} in the input. This kind of
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   197
  situation can be avoided when using the function @{ML "!!"}.  This function
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   198
  aborts the whole process of parsing in case of a failure and prints an error
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   199
  message. For example if you invoke the parser
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   200
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   201
  
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   202
  @{ML [display,gray] "!! (fn _ => \"foo\") ($$ \"h\")"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   203
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   204
  on @{text [quotes] "hello"}, the parsing succeeds
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   205
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   206
  @{ML_response [display,gray] 
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   207
  "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   208
  "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   209
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   210
  but if you invoke it on @{text [quotes] "world"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   211
  
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   212
  @{ML_response_fake [display,gray] "(!! (fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   213
                               "Exception ABORT raised"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   214
108
8bea3f74889d added to the tactical chapter; polished; added the tabularstar environment (which is just tabular*)
Christian Urban <urbanc@in.tum.de>
parents: 105
diff changeset
   215
  then the parsing aborts and the error message @{text "foo"} is printed. In order to
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 116
diff changeset
   216
  see the error message properly, you need to prefix the parser with the function 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   217
  @{ML [index] error in Scan}. For example:
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   218
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   219
  @{ML_response_fake [display,gray] 
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   220
  "Scan.error (!! (fn _ => \"foo\") ($$ \"h\"))"
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   221
  "Exception Error \"foo\" raised"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   222
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   223
  This ``prefixing'' is usually done by wrappers such as @{ML [index] local_theory in OuterSyntax} 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   224
  (see Section~\ref{sec:newcommand} which explains this function in more detail). 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   225
  
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   226
  Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   227
  r}. If you want to generate the correct error message for 
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   228
  @{text "p"}-followed-by-@{text "q"}, then you have to write:
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   229
*}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   230
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   231
ML{*fun p_followed_by_q p q r =
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   232
let 
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   233
  val err_msg = fn _ => p ^ " is not followed by " ^ q
133
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   234
in
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   235
  ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
3e94ccc0f31e polishing and start of the section about attributes
Christian Urban <urbanc@in.tum.de>
parents: 132
diff changeset
   236
end *}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   237
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   238
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   239
text {*
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   240
  Running this parser with the arguments
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   241
  @{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   242
  the input @{text [quotes] "holle"} 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   243
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   244
  @{ML_response_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   245
                               "Exception ERROR \"h is not followed by e\" raised"} 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   246
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   247
  produces the correct error message. Running it with
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   248
 
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   249
  @{ML_response [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   250
                          "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   251
  
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   252
  yields the expected parsing. 
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   253
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   254
  The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   255
  often as it succeeds. For example:
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   256
  
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   257
  @{ML_response [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")" 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   258
                "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   259
  
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   260
  Note that @{ML [index] repeat in Scan} stores the parsed items in a list. The function
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   261
  @{ML [index] repeat1 in Scan} is similar, but requires that the parser @{text "p"} 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   262
  succeeds at least once.
48
609f9ef73494 fixed FIXME's in fake responses
Christian Urban <urbanc@in.tum.de>
parents: 47
diff changeset
   263
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   264
  Also note that the parser would have aborted with the exception @{text MORE}, if
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   265
  you had run it only on just @{text [quotes] "hhhh"}. This can be avoided by using
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   266
  the wrapper @{ML [index] finite in Scan} and the ``stopper-token'' 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   267
  @{ML [index] stopper in Symbol}. With them you can write:
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   268
  
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   269
  @{ML_response [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")" 
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   270
                "([\"h\", \"h\", \"h\", \"h\"], [])"}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   271
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   272
  @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   273
  other stoppers need to be used when parsing, for example, tokens. However, this kind of 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   274
  manually wrapping is often already done by the surrounding infrastructure. 
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   275
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   276
  The function @{ML [index] repeat in Scan} can be used with @{ML [index] one in Scan} to read any 
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   277
  string as in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   278
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   279
  @{ML_response [display,gray] 
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   280
"let 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   281
   val p = Scan.repeat (Scan.one Symbol.not_eof)
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   282
   val input = Symbol.explode \"foo bar foo\"
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   283
in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   284
   Scan.finite Symbol.stopper p input
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   285
end" 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   286
"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   287
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   288
  where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   289
  end of the input string (i.e.~stopper symbol).
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   290
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   291
  The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can 
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 59
diff changeset
   292
  parse the input, then the whole parser fails; if not, then the second is tried. Therefore
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   293
  
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   294
  @{ML_response_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   295
                               "Exception FAIL raised"}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   296
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   297
  fails, while
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   298
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   299
  @{ML_response [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   300
                          "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   301
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   302
  succeeds. 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   303
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   304
  The functions @{ML [index] repeat in Scan} and @{ML [index] unless in Scan} can 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   305
  be combined to read any input until a certain marker symbol is reached. In the 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   306
  example below the marker symbol is a @{text [quotes] "*"}.
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   307
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   308
  @{ML_response [display,gray]
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   309
"let 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   310
  val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   311
  val input1 = Symbol.explode \"fooooo\"
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   312
  val input2 = Symbol.explode \"foo*ooo\"
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   313
in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   314
  (Scan.finite Symbol.stopper p input1, 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   315
   Scan.finite Symbol.stopper p input2)
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   316
end"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   317
"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   318
 ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   319
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   320
  
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   321
  After parsing is done, you almost always want to apply a function to the parsed 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   322
  items. One way to do this is the function @{ML [index]">>"} where 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   323
  @{ML "(p >> f)" for p f} runs 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   324
  first the parser @{text p} and upon successful completion applies the 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   325
  function @{text f} to the result. For example
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   326
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   327
@{ML_response [display,gray]
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   328
"let 
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   329
  fun double (x, y) = (x ^ x, y ^ y) 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   330
in
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   331
  (($$ \"h\") -- ($$ \"e\") >> double) (Symbol.explode \"hello\")
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   332
end"
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   333
"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   334
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   335
  doubles the two parsed input strings; or
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   336
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   337
  @{ML_response [display,gray] 
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   338
"let 
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   339
   val p = Scan.repeat (Scan.one Symbol.not_eof)
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   340
   val input = Symbol.explode \"foo bar foo\" 
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   341
in
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   342
   Scan.finite Symbol.stopper (p >> implode) input
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   343
end" 
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   344
"(\"foo bar foo\",[])"}
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   345
60
5b9c6010897b doem tuning and made the cookbook work again with recent changes (CookBook/Package/Ind_Interface.thy needs to be looked at to see what the problem with the new parser type is)
Christian Urban <urbanc@in.tum.de>
parents: 59
diff changeset
   346
  where the single-character strings in the parsed output are transformed
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   347
  back into one string.
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   348
 
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   349
  (FIXME:  move to an earlier place)
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   350
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   351
  The function @{ML [index] ahead in Scan} parses some input, but leaves the original
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   352
  input unchanged. For example:
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   353
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   354
  @{ML_response [display,gray]
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   355
  "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")" 
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   356
  "(\"foo\", [\"f\", \"o\", \"o\"])"} 
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   357
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   358
  The function @{ML [index] lift in Scan} takes a parser and a pair as arguments. This function applies
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   359
  the given parser to the second component of the pair and leaves the  first component 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   360
  untouched. For example
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   361
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   362
@{ML_response [display,gray]
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
   363
"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   364
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   365
43
02f76f1b6e7b added positions to anti-quotations; removed old antiquotation_setup; tuned the text a bit
Christian Urban <urbanc@in.tum.de>
parents: 42
diff changeset
   366
  (FIXME: In which situations is this useful? Give examples.) 
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   367
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   368
  \begin{exercise}\label{ex:scancmts}
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   369
  Write a parser that parses an input string so that any comment enclosed
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   370
  within @{text "(*\<dots>*)"} is replaced by the same comment but enclosed within
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   371
  @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   372
  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
236
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   373
  "s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper 
7b6d81ff9d9a some polishing
Christian Urban <urbanc@in.tum.de>
parents: 230
diff changeset
   374
  nesting of comments.
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   375
  \end{exercise}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   376
*}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   377
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   378
section {* Parsing Theory Syntax *}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   379
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   380
text {*
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   381
  Most of the time, however, Isabelle developers have to deal with parsing
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   382
  tokens, not strings.  These token parsers have the type:
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   383
*}
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   384
  
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   385
ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*}
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   386
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   387
text {*
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   388
  The reason for using token parsers is that theory syntax, as well as the
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   389
  parsers for the arguments of proof methods, use the type @{ML_type
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   390
  OuterLex.token}.
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   391
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   392
  \begin{readmore}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   393
  The parser functions for the theory syntax are contained in the structure
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   394
  @{ML_struct OuterParse} defined in the file @{ML_file  "Pure/Isar/outer_parse.ML"}.
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   395
  The definition for tokens is in the file @{ML_file "Pure/Isar/outer_lex.ML"}.
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   396
  \end{readmore}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   397
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   398
  The structure @{ML_struct [index] OuterLex} defines several kinds of tokens (for
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   399
  example @{ML [index] Ident in OuterLex} for identifiers, @{ML Keyword in
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   400
  OuterLex} for keywords and @{ML [index] Command in OuterLex} for commands). Some
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   401
  token parsers take into account the kind of tokens. The first example shows
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   402
  how to generate a token list out of a string using the function 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   403
  @{ML [index] scan in OuterSyntax}. It is given the argument 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   404
  @{ML "Position.none"} since,
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   405
  at the moment, we are not interested in generating precise error
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   406
  messages. The following code\footnote{Note that because of a possible bug in
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   407
  the PolyML runtime system, the result is printed as @{text [quotes] "?"},
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   408
  instead of the tokens.}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   409
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   410
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   411
@{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   412
"[Token (\<dots>,(Ident, \"hello\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   413
 Token (\<dots>,(Space, \" \"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   414
 Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   415
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   416
  produces three tokens where the first and the last are identifiers, since
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   417
  @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   418
  other syntactic category. The second indicates a space.
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   419
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   420
  We can easily change what is recognised as a keyword with 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   421
  @{ML [index] keyword in OuterKeyword}. For example calling this function 
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   422
*}
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   423
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   424
ML{*val _ = OuterKeyword.keyword "hello"*}
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   425
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   426
text {*
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   427
  then lexing @{text [quotes] "hello world"} will produce
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   428
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   429
  @{ML_response_fake [display,gray] "OuterSyntax.scan Position.none \"hello world\"" 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   430
"[Token (\<dots>,(Keyword, \"hello\"),\<dots>), 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   431
 Token (\<dots>,(Space, \" \"),\<dots>), 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   432
 Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   433
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   434
  Many parsing functions later on will require white space, comments and the like
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   435
  to have already been filtered out.  So from now on we are going to use the 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   436
  functions @{ML filter} and @{ML [index] is_proper in OuterLex} to do this. 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   437
  For example:
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   438
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   439
@{ML_response_fake [display,gray]
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   440
"let
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   441
   val input = OuterSyntax.scan Position.none \"hello world\"
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   442
in
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   443
   filter OuterLex.is_proper input
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   444
end" 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   445
"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   446
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   447
  For convenience we define the function:
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   448
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   449
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   450
ML{*fun filtered_input str = 
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
   451
  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) *}
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   452
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   453
text {* 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   454
  If you now parse
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   455
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   456
@{ML_response_fake [display,gray] 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   457
"filtered_input \"inductive | for\"" 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   458
"[Token (\<dots>,(Command, \"inductive\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   459
 Token (\<dots>,(Keyword, \"|\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   460
 Token (\<dots>,(Keyword, \"for\"),\<dots>)]"}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   461
221
a9eb69749c93 corrected some typos
griff
parents: 220
diff changeset
   462
  you obtain a list consisting of only one command and two keyword tokens.
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   463
  If you want to see which keywords and commands are currently known to Isabelle, 
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   464
  type:
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   465
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   466
@{ML_response_fake [display,gray] 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   467
"let 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   468
  val (keywords, commands) = OuterKeyword.get_lexicons ()
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   469
in 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   470
  (Scan.dest_lexicon commands, Scan.dest_lexicon keywords)
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   471
end" 
132
2d9198bcb850 polished
Christian Urban <urbanc@in.tum.de>
parents: 131
diff changeset
   472
"([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   473
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   474
  You might have to adjust the @{ML [index] print_depth} in order to
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   475
  see the complete list.
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   476
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   477
  The parser @{ML [index] "$$$" in OuterParse} parses a single keyword. For example:
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   478
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   479
@{ML_response [display,gray]
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   480
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   481
  val input1 = filtered_input \"where for\"
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   482
  val input2 = filtered_input \"| in\"
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   483
in 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   484
  (OuterParse.$$$ \"where\" input1, OuterParse.$$$ \"|\" input2)
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   485
end"
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   486
"((\"where\",\<dots>), (\"|\",\<dots>))"}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   487
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   488
  Any non-keyword string can be parsed with the function @{ML [index] reserved in OuterParse}.
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   489
  For example:
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   490
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   491
  @{ML_response [display,gray]
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   492
"let 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   493
  val p = OuterParse.reserved \"bar\"
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   494
  val input = filtered_input \"bar\"
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   495
in
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   496
  p input
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   497
end"
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   498
  "(\"bar\",[])"}
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   499
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   500
  Like before, you can sequentially connect parsers with @{ML [index] "--"}. For example: 
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   501
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   502
@{ML_response [display,gray]
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   503
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   504
  val input = filtered_input \"| in\"
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   505
in 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   506
  (OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\") input
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   507
end"
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 181
diff changeset
   508
"((\"|\", \"in\"), [])"}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   509
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   510
  \indexdef{enum@ {\tt\slshape{enum}}}{in {\tt\slshape OuterParse}}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   511
  The parser @{ML "OuterParse.enum s p" for s p} parses a possibly empty 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   512
  list of items recognised by the parser @{text p}, where the items being parsed
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   513
  are separated by the string @{text s}. For example:
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   514
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   515
@{ML_response [display,gray]
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   516
"let 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   517
  val input = filtered_input \"in | in | in foo\"
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   518
in 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   519
  (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   520
end" 
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 181
diff changeset
   521
"([\"in\", \"in\", \"in\"], [\<dots>])"}
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   522
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   523
  @{ML [index] enum1 in OuterParse} works similarly, except that the parsed list must
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   524
  be non-empty. Note that we had to add a string @{text [quotes] "foo"} at the
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   525
  end of the parsed string, otherwise the parser would have consumed all
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   526
  tokens and then failed with the exception @{text "MORE"}. Like in the
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   527
  previous section, we can avoid this exception using the wrapper @{ML
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   528
  Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   529
  OuterLex.stopper}. We can write:
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   530
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   531
@{ML_response [display,gray]
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   532
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   533
  val input = filtered_input \"in | in | in\"
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   534
in 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   535
  Scan.finite OuterLex.stopper 
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   536
         (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   537
end" 
183
8bb4eaa2ec92 a simplification suggested by Stefan and some polishing
Christian Urban <urbanc@in.tum.de>
parents: 181
diff changeset
   538
"([\"in\", \"in\", \"in\"], [])"}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   539
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   540
  The following function will help to run examples.
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   541
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   542
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   543
ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *}
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   544
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   545
text {*
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   546
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   547
  The function @{ML [index] "!!!" in OuterParse} can be used to force termination of the
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   548
  parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   549
  Except that the error message of @{ML "OuterParse.!!!"} is fixed to be 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   550
  @{text [quotes] "Outer syntax error"}
221
a9eb69749c93 corrected some typos
griff
parents: 220
diff changeset
   551
  together with a relatively precise description of the failure. For example:
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   552
72
7b8c4fe235aa added an antiquotation option [gray] for gray boxes around displays
Christian Urban <urbanc@in.tum.de>
parents: 69
diff changeset
   553
@{ML_response_fake [display,gray]
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   554
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   555
  val input = filtered_input \"in |\"
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   556
  val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   557
in 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   558
  parse (OuterParse.!!! parse_bar_then_in) input 
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   559
end"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   560
"Exception ERROR \"Outer syntax error: keyword \"|\" expected, 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   561
but keyword in was found\" raised"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   562
}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   563
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   564
  \begin{exercise} (FIXME)
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   565
  A type-identifier, for example @{typ "'a"}, is a token of 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   566
  kind @{ML [index] Keyword in OuterLex}. It can be parsed using 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   567
  the function @{ML type_ident in OuterParse}.
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   568
  \end{exercise}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   569
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   570
  (FIXME: or give parser for numbers)
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   571
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   572
  Whenever there is a possibility that the processing of user input can fail, 
221
a9eb69749c93 corrected some typos
griff
parents: 220
diff changeset
   573
  it is a good idea to give all available information about where the error 
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   574
  occurred. For this Isabelle can attach positional information to tokens
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   575
  and then thread this information up the processing chain. To see this,
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   576
  modify the function @{ML filtered_input} described earlier to 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   577
*}
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   578
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   579
ML{*fun filtered_input' str = 
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   580
       filter OuterLex.is_proper (OuterSyntax.scan (Position.line 7) str) *}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   581
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   582
text {*
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   583
  where we pretend the parsed string starts on line 7. An example is
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   584
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   585
@{ML_response_fake [display,gray]
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   586
"filtered_input' \"foo \\n bar\""
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   587
"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), \<dots>),
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   588
 Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), \<dots>)]"}
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   589
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   590
  in which the @{text [quotes] "\\n"} causes the second token to be in 
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   591
  line 8.
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   592
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   593
  By using the parser @{ML OuterParse.position} you can access the token position
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   594
  and return it as part of the parser result. For example
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   595
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   596
@{ML_response_fake [display,gray]
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   597
"let
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   598
  val input = filtered_input' \"where\"
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   599
in 
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   600
  parse (OuterParse.position (OuterParse.$$$ \"where\")) input
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   601
end"
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   602
"((\"where\", {line=7, end_line=7}), [])"}
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   603
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   604
  \begin{readmore}
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   605
  The functions related to positions are implemented in the file
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   606
  @{ML_file "Pure/General/position.ML"}.
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   607
  \end{readmore}
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   608
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   609
*}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   610
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   611
text {*
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   612
  (FIXME: there are also handy parsers for ML-expressions and ML-files)
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   613
*}
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   614
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   615
section {* Context Parser (TBD) *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   616
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   617
text {*
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   618
  Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}.
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   619
*}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   620
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   621
section {* Argument and Attribute Parsers (TBD) *}
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   622
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   623
section {* Parsing Inner Syntax *}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   624
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   625
text {*
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   626
  There is usually no need to write your own parser for parsing inner syntax, that is 
285
abe5306cacbe spell checker
griff
parents: 284
diff changeset
   627
  for terms and  types: you can just call the predefined parsers. Terms can 
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   628
  be parsed using the function @{ML OuterParse.term}. For example:
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   629
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   630
@{ML_response [display,gray]
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   631
"let 
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   632
  val input = OuterSyntax.scan Position.none \"foo\"
44
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   633
in 
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   634
  OuterParse.term input
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   635
end"
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   636
"(\"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\", [])"}
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   637
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   638
  The function @{ML OuterParse.prop} is similar, except that it gives a different
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   639
  error message, when parsing fails. As you can see, the parser not just returns 
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   640
  the parsed string, but also some encoded information. You can decode the
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   641
  information with the function @{ML YXML.parse}. For example
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   642
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   643
  @{ML_response [display,gray]
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   644
  "YXML.parse \"\\^E\\^Ftoken\\^Efoo\\^E\\^F\\^E\""
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   645
  "XML.Elem (\"token\", [], [XML.Text \"foo\"])"}
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   646
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   647
  The result of the decoding is an XML-tree. You can see better what is going on if
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   648
  you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   649
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   650
@{ML_response [display,gray]
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   651
"let 
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   652
  val input = OuterSyntax.scan (Position.line 42) \"foo\"
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   653
in 
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   654
  YXML.parse (fst (OuterParse.term input))
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   655
end"
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   656
"XML.Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   657
  
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   658
  The positional information is stored as part of an XML-tree so that code 
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   659
  called later on will be able to give more precise error messages. 
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   660
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   661
  \begin{readmore}
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   662
  The functions to do with input and output of XML and YXML are defined 
127
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   663
  in @{ML_file "Pure/General/xml.ML"} and @{ML_file "Pure/General/yxml.ML"}.
74846cb0fff9 updated and added two tentative recipes
Christian Urban <urbanc@in.tum.de>
parents: 126
diff changeset
   664
  \end{readmore}
160
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations
Christian Urban <urbanc@in.tum.de>
parents: 156
diff changeset
   665
  
125
748d9c1a32fb polished parser section
Christian Urban <urbanc@in.tum.de>
parents: 124
diff changeset
   666
*}
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   667
116
c9ff326e3ce5 more changes to the package chapter
Christian Urban <urbanc@in.tum.de>
parents: 114
diff changeset
   668
section {* Parsing Specifications\label{sec:parsingspecs} *}
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   669
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   670
text {*
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   671
  There are a number of special purpose parsers that help with parsing
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   672
  specifications of function definitions, inductive predicates and so on. In
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
   673
  Chapter~\ref{chp:package}, for example, we will need to parse specifications
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   674
  for inductive predicates of the form:
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   675
*}
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   676
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   677
simple_inductive
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   678
  even and odd
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   679
where
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   680
  even0: "even 0"
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   681
| evenS: "odd n \<Longrightarrow> even (Suc n)"
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   682
| oddS: "even n \<Longrightarrow> odd (Suc n)"
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   683
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   684
text {*
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   685
  For this we are going to use the parser:
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   686
*}
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   687
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   688
ML %linenosgray{*val spec_parser = 
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   689
     OuterParse.fixes -- 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   690
     Scan.optional 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   691
       (OuterParse.$$$ "where" |--
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   692
          OuterParse.!!! 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   693
            (OuterParse.enum1 "|" 
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   694
               (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 116
diff changeset
   695
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   696
text {*
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   697
  Note that the parser must not parse the keyword \simpleinductive, even if it is
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   698
  meant to process definitions as shown above. The parser of the keyword 
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   699
  will be given by the infrastructure that will eventually call @{ML spec_parser}.
126
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   700
  
fcc0e6e54dca polished
Christian Urban <urbanc@in.tum.de>
parents: 125
diff changeset
   701
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   702
  To see what the parser returns, let us parse the string corresponding to the 
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   703
  definition of @{term even} and @{term odd}:
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   704
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   705
@{ML_response [display,gray]
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   706
"let
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   707
  val input = filtered_input
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   708
     (\"even and odd \" ^  
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   709
      \"where \" ^
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   710
      \"  even0[intro]: \\\"even 0\\\" \" ^ 
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   711
      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   712
      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   713
in
120
c39f83d8daeb some polishing; split up the file External Solver into two
Christian Urban <urbanc@in.tum.de>
parents: 116
diff changeset
   714
  parse spec_parser input
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   715
end"
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   716
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   717
     [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   718
      ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   719
      ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   720
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   721
  As you see, the result is a pair consisting of a list of
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   722
  variables with optional type-annotation and syntax-annotation, and a list of
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   723
  rules where every rule has optionally a name and an attribute.
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   724
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   725
  The function @{ML [index] "fixes" in OuterParse} in Line 2 of the parser reads an 
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   726
  \isacommand{and}-separated 
124
0b9fa606a746 added to the first-steps section
Christian Urban <urbanc@in.tum.de>
parents: 122
diff changeset
   727
  list of variables that can include optional type annotations and syntax translations. 
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   728
  For example:\footnote{Note that in the code we need to write 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   729
  @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   730
  in the compound type.}
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   731
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   732
@{ML_response [display,gray]
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   733
"let
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   734
  val input = filtered_input 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   735
        \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   736
in
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   737
  parse OuterParse.fixes input
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   738
end"
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   739
"([(foo, SOME \"\\^E\\^Ftoken\\^Eint \<Rightarrow> bool\\^E\\^F\\^E\", NoSyn), 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   740
  (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   741
  (blonk, NONE, NoSyn)],[])"}  
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   742
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   743
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   744
text {*
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   745
  Whenever types are given, they are stored in the @{ML SOME}s. The types are
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   746
  not yet used to type the variables: this must be done by type-inference later
149
253ea99c1441 polished
Christian Urban <urbanc@in.tum.de>
parents: 133
diff changeset
   747
  on. Since types are part of the inner syntax they are strings with some
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   748
  encoded information (see previous section). If a mixfix-syntax is
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   749
  present for a variable, then it is stored in the @{ML [index] Mixfix} data structure;
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   750
  no syntax translation is indicated by @{ML [index] NoSyn}.
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   751
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   752
  \begin{readmore}
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   753
  The data structure for mixfix annotations is defined in @{ML_file "Pure/Syntax/mixfix.ML"}.
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   754
  \end{readmore}
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   755
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   756
  Lines 3 to 7 in the function @{ML spec_parser} implement the parser for a
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   757
  list of introduction rules, that is propositions with theorem annotations
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   758
  such as rule names and attributes. The introduction rules are propositions
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   759
  parsed by @{ML [index] prop  in OuterParse}. However, they can include an optional
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   760
  theorem name plus some attributes. For example
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   761
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   762
@{ML_response [display,gray] "let 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   763
  val input = filtered_input \"foo_lemma[intro,dest!]:\"
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   764
  val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   765
in 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   766
  (name, map Args.dest_src attrib)
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   767
end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"}
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   768
 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   769
  The function @{ML [index] opt_thm_name in SpecParse} is the ``optional'' variant of
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   770
  @{ML [index] thm_name in SpecParse}. Theorem names can contain attributes. The name 
131
8db9195bb3e9 polished
Christian Urban <urbanc@in.tum.de>
parents: 128
diff changeset
   771
  has to end with @{text [quotes] ":"}---see the argument of 
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
   772
  the function @{ML SpecParse.opt_thm_name} in Line 7.
121
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   773
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   774
  \begin{readmore}
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   775
  Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} 
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   776
  and @{ML_file "Pure/Isar/args.ML"}.
26e5b41faa74 polishing
Christian Urban <urbanc@in.tum.de>
parents: 120
diff changeset
   777
  \end{readmore}
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   778
*}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   779
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   780
text_raw {*
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   781
  \begin{exercise}
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   782
  Have a look at how the parser @{ML SpecParse.where_alt_specs} is implemented
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   783
  in file @{ML_file "Pure/Isar/spec_parse.ML"}. This parser corresponds
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   784
  to the ``where-part'' of the introduction rules given above. Below
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   785
  we paraphrase the code of @{ML [index] where_alt_specs in SpecParse} adapted to our
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   786
  purposes. 
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   787
  \begin{isabelle}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   788
*}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   789
ML %linenosgray{*val spec_parser' = 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   790
     OuterParse.fixes -- 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   791
     Scan.optional
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   792
     (OuterParse.$$$ "where" |-- 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   793
        OuterParse.!!! 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   794
          (OuterParse.enum1 "|" 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   795
             ((SpecParse.opt_thm_name ":" -- OuterParse.prop) --| 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   796
                  Scan.option (Scan.ahead (OuterParse.name || 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   797
                  OuterParse.$$$ "[") -- 
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   798
                  OuterParse.!!! (OuterParse.$$$ "|"))))) [] *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   799
text_raw {*
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   800
  \end{isabelle}
284
ee139d9d7ab8 comment
griff
parents: 261
diff changeset
   801
  Both parsers accept the same input% that's not true:
ee139d9d7ab8 comment
griff
parents: 261
diff changeset
   802
  % spec_parser accepts input that is refuted by spec_parser'
ee139d9d7ab8 comment
griff
parents: 261
diff changeset
   803
  , but if you look closely, you can notice 
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   804
  an additional  ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of 
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   805
  this additional ``tail''?
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   806
  \end{exercise}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   807
*}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
   808
229
abc7f90188af permutation example uses now recent infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 228
diff changeset
   809
text {*
abc7f90188af permutation example uses now recent infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 228
diff changeset
   810
  (FIXME: @{ML OuterParse.type_args}, @{ML OuterParse.typ}, @{ML OuterParse.opt_mixfix})
abc7f90188af permutation example uses now recent infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 228
diff changeset
   811
*}
abc7f90188af permutation example uses now recent infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 228
diff changeset
   812
abc7f90188af permutation example uses now recent infrastructure
Christian Urban <urbanc@in.tum.de>
parents: 228
diff changeset
   813
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   814
section {* New Commands and Keyword Files\label{sec:newcommand} *}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   815
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   816
text {*
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   817
  Often new commands, for example for providing new definitional principles,
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   818
  need to be implemented. While this is not difficult on the ML-level,
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   819
  new commands, in order to be useful, need to be recognised by
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   820
  ProofGeneral. This results in some subtle configuration issues, which we
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   821
  will explain in this section.
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   822
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   823
  To keep things simple, let us start with a ``silly'' command that does nothing 
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   824
  at all. We shall name this command \isacommand{foobar}. On the ML-level it can be 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   825
  defined as:
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   826
*}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   827
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   828
ML{*let
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   829
  val do_nothing = Scan.succeed (LocalTheory.theory I)
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   830
  val kind = OuterKeyword.thy_decl
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   831
in
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   832
  OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   833
end *}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   834
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   835
text {*
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   836
  The crucial function @{ML [index] local_theory in OuterSyntax} expects a name for the command, a
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   837
  short description, a kind indicator (which we will explain later more thoroughly) and a
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   838
  parser producing a local theory transition (its purpose will also explained
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   839
  later). 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   840
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   841
  While this is everything you have to do on the ML-level, you need a keyword
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   842
  file that can be loaded by ProofGeneral. This is to enable ProofGeneral to
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   843
  recognise \isacommand{foobar} as a command. Such a keyword file can be
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   844
  generated with the command-line:
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   845
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   846
  @{text [display] "$ isabelle keywords -k foobar some_log_files"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   847
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   848
  The option @{text "-k foobar"} indicates which postfix the name of the keyword file 
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   849
  will be assigned. In the case above the file will be named @{text
86
fdb9ea86c2a3 polished
Christian Urban <urbanc@in.tum.de>
parents: 85
diff changeset
   850
  "isar-keywords-foobar.el"}. This command requires log files to be
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   851
  present (in order to extract the keywords from them). To generate these log
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   852
  files, you first need to package the code above into a separate theory file named
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   853
  @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   854
  complete code.
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   855
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   856
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   857
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   858
  \begin{figure}[t]
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   859
  \begin{graybox}\small
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   860
  \isacommand{theory}~@{text Command}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   861
  \isacommand{imports}~@{text Main}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   862
  \isacommand{begin}\\
85
b02904872d6b better handling of {* and *}
Christian Urban <urbanc@in.tum.de>
parents: 81
diff changeset
   863
  \isacommand{ML}~@{text "\<verbopen>"}\\
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   864
  @{ML
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   865
"let
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   866
  val do_nothing = Scan.succeed (LocalTheory.theory I)
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   867
  val kind = OuterKeyword.thy_decl
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   868
in
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   869
  OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   870
end"}\\
85
b02904872d6b better handling of {* and *}
Christian Urban <urbanc@in.tum.de>
parents: 81
diff changeset
   871
  @{text "\<verbclose>"}\\
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   872
  \isacommand{end}
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   873
  \end{graybox}
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   874
  \caption{This file can be used to generate a log file. This log file in turn can
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   875
  be used to generate a keyword file containing the command \isacommand{foobar}.
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   876
  \label{fig:commandtheory}}
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   877
  \end{figure}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   878
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   879
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   880
  For our purposes it is sufficient to use the log files of the theories
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   881
  @{text "Pure"}, @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   882
  the log file for the theory @{text "Command.thy"}, which contains the new
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   883
  \isacommand{foobar}-command. If you target other logics besides HOL, such
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   884
  as Nominal or ZF, then you need to adapt the log files appropriately.
104
5dcad9348e4d polished
Christian Urban <urbanc@in.tum.de>
parents: 102
diff changeset
   885
  
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   886
  @{text Pure} and @{text HOL} are usually compiled during the installation of
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   887
  Isabelle. So log files for them should be already available. If not, then
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   888
  they can be conveniently compiled with the help of the build-script from the Isabelle
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   889
  distribution.
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   890
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   891
  @{text [display] 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   892
"$ ./build -m \"Pure\"
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   893
$ ./build -m \"HOL\""}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   894
  
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   895
  The @{text "Pure-ProofGeneral"} theory needs to be compiled with:
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   896
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   897
  @{text [display] "$ ./build -m \"Pure-ProofGeneral\" \"Pure\""}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   898
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   899
  For the theory @{text "Command.thy"}, you first need to create a ``managed'' subdirectory 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   900
  with:
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   901
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   902
  @{text [display] "$ isabelle mkdir FoobarCommand"}
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   903
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   904
  This generates a directory containing the files: 
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   905
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   906
  @{text [display] 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   907
"./IsaMakefile
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   908
./FoobarCommand/ROOT.ML
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   909
./FoobarCommand/document
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   910
./FoobarCommand/document/root.tex"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   911
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   912
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   913
  You need to copy the file @{text "Command.thy"} into the directory @{text "FoobarCommand"}
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   914
  and add the line 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   915
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
   916
  @{text [display] "no_document use_thy \"Command\";"} 
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   917
  
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   918
  to the file @{text "./FoobarCommand/ROOT.ML"}. You can now compile the theory by just typing:
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   919
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   920
  @{text [display] "$ isabelle make"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   921
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   922
  If the compilation succeeds, you have finally created all the necessary log files. 
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   923
  They are stored in the directory 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   924
  
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   925
  @{text [display]  "~/.isabelle/heaps/Isabelle2009/polyml-5.2.1_x86-linux/log"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   926
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   927
  or something similar depending on your Isabelle distribution and architecture.
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   928
  One quick way to assign a shell variable to this directory is by typing
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   929
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   930
  @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   931
 
156
e8f11280c762 polished
Christian Urban <urbanc@in.tum.de>
parents: 149
diff changeset
   932
  on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the 
128
693711a0c702 polished
Christian Urban <urbanc@in.tum.de>
parents: 127
diff changeset
   933
  directory should include the files:
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   934
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   935
  @{text [display] 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   936
"Pure.gz
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   937
HOL.gz
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   938
Pure-ProofGeneral.gz
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   939
HOL-FoobarCommand.gz"} 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   940
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   941
  From them you can create the keyword files. Assuming the name 
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   942
  of the directory is in  @{text "$ISABELLE_LOGS"},
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   943
  then the Unix command for creating the keyword file is:
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   944
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   945
@{text [display]
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   946
"$ isabelle keywords -k foobar 
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   947
   $ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral.gz,HOL-FoobarCommand.gz}"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   948
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   949
  The result is the file @{text "isar-keywords-foobar.el"}. It should contain
86
fdb9ea86c2a3 polished
Christian Urban <urbanc@in.tum.de>
parents: 85
diff changeset
   950
  the string @{text "foobar"} twice.\footnote{To see whether things are fine, check
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   951
  that @{text "grep foobar"} on this file returns something
86
fdb9ea86c2a3 polished
Christian Urban <urbanc@in.tum.de>
parents: 85
diff changeset
   952
  non-empty.}  This keyword file needs to
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
   953
  be copied into the directory @{text "~/.isabelle/etc"}. To make ProofGeneral
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   954
  aware of this keyword file, you have to start Isabelle with the option @{text
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   955
  "-k foobar"}, that is:
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   956
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
   957
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   958
  @{text [display] "$ isabelle emacs -k foobar a_theory_file"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   959
101
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   960
  If you now build a theory on top of @{text "Command.thy"}, 
Christian Urban <urbanc@in.tum.de>
parents: 86
diff changeset
   961
  then the command \isacommand{foobar} can be used. 
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   962
  Similarly with any other new command, and also any new keyword that is 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   963
  introduced with
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   964
*}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   965
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   966
ML{*val _ = OuterKeyword.keyword "blink" *}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   967
230
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   968
text {*
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   969
  At the moment the command \isacommand{foobar} is not very useful. Let us refine 
8def50824320 added material about OuterKeyword.keyword and OuterParse.reserved
Christian Urban <urbanc@in.tum.de>
parents: 229
diff changeset
   970
  it a bit 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   971
  next by letting it take a proposition as argument and printing this proposition 
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   972
  inside the tracing buffer. 
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   973
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   974
  The crucial part of a command is the function that determines the behaviour
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   975
  of the command. In the code above we used a ``do-nothing''-function, which
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
   976
  because of @{ML [index] succeed in Scan} does not parse any argument, but immediately
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   977
  returns the simple function @{ML "LocalTheory.theory I"}. We can
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   978
  replace this code by a function that first parses a proposition (using the
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   979
  parser @{ML OuterParse.prop}), then prints out the tracing
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   980
  information (using a new function @{text trace_prop}) and 
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   981
  finally does nothing. For this you can write:
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   982
*}
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   983
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   984
ML{*let
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   985
  fun trace_prop str = 
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 211
diff changeset
   986
     LocalTheory.theory (fn lthy => (tracing str; lthy))
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
   987
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   988
  val trace_prop_parser = OuterParse.prop >> trace_prop
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   989
  val kind = OuterKeyword.thy_decl
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   990
in
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   991
  OuterSyntax.local_theory "foobar" "traces a proposition" 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
   992
    kind trace_prop_parser
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
   993
end *}
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   994
218
7ff7325e3b4e started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
parents: 211
diff changeset
   995
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   996
text {*
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
   997
  Now you can type
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
   998
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
   999
  \begin{isabelle}
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1000
  \isacommand{foobar}~@{text [quotes] "True \<and> False"}\\
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1001
  @{text "> \"True \<and> False\""}
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1002
  \end{isabelle}
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1003
  
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1004
  and see the proposition in the tracing buffer.  
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1005
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1006
  Note that so far we used @{ML [index] thy_decl in OuterKeyword} as the kind
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1007
  indicator for the command.  This means that the command finishes as soon as
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1008
  the arguments are processed. Examples of this kind of commands are
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1009
  \isacommand{definition} and \isacommand{declare}.  In other cases, commands
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1010
  are expected to parse some arguments, for example a proposition, and then
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1011
  ``open up'' a proof in order to prove the proposition (for example
86
fdb9ea86c2a3 polished
Christian Urban <urbanc@in.tum.de>
parents: 85
diff changeset
  1012
  \isacommand{lemma}) or prove some other properties (for example
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1013
  \isacommand{function}). To achieve this kind of behaviour, you have to use
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1014
  the kind indicator @{ML [index] thy_goal in OuterKeyword} and the function @{ML
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1015
  "local_theory_to_proof" in OuterSyntax} to set up the command.  Note,
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1016
  however, once you change the ``kind'' of a command from @{ML thy_decl in
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1017
  OuterKeyword} to @{ML thy_goal in OuterKeyword} then the keyword file needs
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1018
  to be re-created!
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1019
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1020
  Below we change \isacommand{foobar} so that it takes a proposition as
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1021
  argument and then starts a proof in order to prove it. Therefore in Line 13, 
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1022
  we set the kind indicator to @{ML thy_goal in OuterKeyword}.
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1023
*}
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1024
114
13fd0a83d3c3 properly handled linenumbers in ML-text and Isar-proofs
Christian Urban <urbanc@in.tum.de>
parents: 108
diff changeset
  1025
ML%linenosgray{*let
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1026
  fun prove_prop str lthy =
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1027
    let
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1028
      val prop = Syntax.read_prop lthy str
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1029
    in
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1030
      Proof.theorem_i NONE (K I) [[(prop,[])]] lthy
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1031
    end;
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1032
  
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1033
  val prove_prop_parser = OuterParse.prop >> prove_prop 
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1034
  val kind = OuterKeyword.thy_goal
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1035
in
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1036
  OuterSyntax.local_theory_to_proof "foobar" "proving a proposition" 
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1037
    kind prove_prop_parser
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1038
end *}
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1039
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1040
text {*
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1041
  The function @{text prove_prop} in Lines 2 to 7 takes a string (the proposition to be
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1042
  proved) and a context as argument.  The context is necessary in order to be able to use
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1043
  @{ML [index] read_prop in Syntax}, which converts a string into a proper proposition.
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1044
  In Line 6 the function @{ML [index] theorem_i in Proof} starts the proof for the
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1045
  proposition. Its argument @{ML NONE} stands for a locale (which we chose to
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1046
  omit); the argument @{ML "(K I)"} stands for a function that determines what
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1047
  should be done with the theorem once it is proved (we chose to just forget
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1048
  about it). Line 9 contains the parser for the proposition.
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1049
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1050
  If you now type \isacommand{foobar}~@{text [quotes] "True \<and> True"}, you obtain the following 
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1051
  proof state
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1052
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1053
  \begin{isabelle}
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
  1054
  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
102
5e309df58557 general cleaning up; deleted antiquotation ML_text; adjusted pathnames of various files in the distribution
Christian Urban <urbanc@in.tum.de>
parents: 101
diff changeset
  1055
  @{text "goal (1 subgoal):"}\\
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1056
  @{text "1. True \<and> True"}
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1057
  \end{isabelle}
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1058
219
98d43270024f more work on the simple inductive chapter
Christian Urban <urbanc@in.tum.de>
parents: 218
diff changeset
  1059
  and you can build the following proof
68
e7519207c2b7 added more to the "new command section" and tuning
Christian Urban <urbanc@in.tum.de>
parents: 67
diff changeset
  1060
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1061
  \begin{isabelle}
80
Christian Urban <urbanc@in.tum.de>
parents: 75
diff changeset
  1062
  \isacommand{foobar}~@{text [quotes] "True \<and> True"}\\
74
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1063
  \isacommand{apply}@{text "(rule conjI)"}\\
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1064
  \isacommand{apply}@{text "(rule TrueI)+"}\\
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1065
  \isacommand{done}
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1066
  \end{isabelle}
Christian Urban <urbanc@in.tum.de>
parents: 72
diff changeset
  1067
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1068
  (FIXME: read a name and show how to store theorems; see @{ML [index] note in LocalTheory})
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1069
  
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
  1070
*}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
  1071
211
d5accbc67e1b more work on simple inductive and marked all sections that are still seriously incomplete with TBD
Christian Urban <urbanc@in.tum.de>
parents: 207
diff changeset
  1072
section {* Methods (TBD) *}
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1073
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1074
text {*
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1075
  (FIXME: maybe move to after the tactic section)
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1076
221
a9eb69749c93 corrected some typos
griff
parents: 220
diff changeset
  1077
  Methods are central to Isabelle. They are the ones you use for example
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
  1078
  in \isacommand{apply}. To print out all currently known methods you can use the 
192
2fff636e1fa0 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 189
diff changeset
  1079
  Isabelle command:
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1080
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1081
  \begin{isabelle}
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1082
  \isacommand{print\_methods}\\
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1083
  @{text "> methods:"}\\
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1084
  @{text ">   -:  do nothing (insert current facts only)"}\\
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1085
  @{text ">   HOL.default:  apply some intro/elim rule (potentially classical)"}\\
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1086
  @{text ">   ..."}
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1087
  \end{isabelle}
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1088
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1089
  An example of a very simple method is:
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1090
*}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1091
244
dc95a56b1953 fixed the problem with double definition of even and odd
Christian Urban <urbanc@in.tum.de>
parents: 241
diff changeset
  1092
method_setup %gray foo = 
181
5baaabe1ab92 updated to new method_setup
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
  1093
 {* Scan.succeed
5baaabe1ab92 updated to new method_setup
Christian Urban <urbanc@in.tum.de>
parents: 178
diff changeset
  1094
      (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *}
244
dc95a56b1953 fixed the problem with double definition of even and odd
Christian Urban <urbanc@in.tum.de>
parents: 241
diff changeset
  1095
         "foo method for conjE and conjI"
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1096
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1097
text {*
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1098
  It defines the method @{text foobar}, which takes no arguments (therefore the
207
d3cd633e8240 some polishing
Christian Urban <urbanc@in.tum.de>
parents: 194
diff changeset
  1099
  parser @{ML Scan.succeed}) and only applies a single tactic, namely the tactic which 
256
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1100
  applies @{thm [source] conjE} and then @{thm [source] conjI}. The function 
1fb8d62c88a0 added some first index-information
Christian Urban <urbanc@in.tum.de>
parents: 250
diff changeset
  1101
  @{ML [index] SIMPLE_METHOD}
241
29d4701c5ee1 polished
Christian Urban <urbanc@in.tum.de>
parents: 240
diff changeset
  1102
  turns such a tactic into a method. The method @{text "foobar"} can be used as follows
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1103
*}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1104
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1105
lemma shows "A \<and> B \<Longrightarrow> C \<and> D"
244
dc95a56b1953 fixed the problem with double definition of even and odd
Christian Urban <urbanc@in.tum.de>
parents: 241
diff changeset
  1106
apply(foo)
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1107
txt {*
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1108
  where it results in the goal state
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1109
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1110
  \begin{minipage}{\textwidth}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1111
  @{subgoals}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1112
  \end{minipage} *}
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1113
(*<*)oops(*>*)
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1114
193
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1115
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1116
(*
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1117
ML {* SIMPLE_METHOD *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1118
ML {* METHOD *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1119
ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1120
ML {* Scan.succeed  *}
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1121
*)
ffd93dcc269d polishing to the theorem attributes section
Christian Urban <urbanc@in.tum.de>
parents: 192
diff changeset
  1122
186
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
  1123
text {*
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
  1124
  (FIXME: explain a version of rule-tac)
371e4375c994 made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
parents: 183
diff changeset
  1125
*}
178
fb8f22dd8ad0 adapted to latest Attrib.setup changes and more work on the simple induct chapter
Christian Urban <urbanc@in.tum.de>
parents: 177
diff changeset
  1126
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1127
(*<*)
194
8cd51a25a7ca some polishing
Christian Urban <urbanc@in.tum.de>
parents: 193
diff changeset
  1128
(* THIS IS AN OLD VERSION OF THE PARSING CHAPTER BY JEREMY DAWSON *)
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1129
chapter {* Parsing *}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1130
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1131
text {*
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
  1132
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1133
  Lots of Standard ML code is given in this document, for various reasons,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1134
  including:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1135
  \begin{itemize}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1136
  \item direct quotation of code found in the Isabelle source files,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1137
  or simplified versions of such code
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1138
  \item identifiers found in the Isabelle source code, with their types 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1139
  (or specialisations of their types)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1140
  \item code examples, which can be run by the reader, to help illustrate the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1141
  behaviour of functions found in the Isabelle source code
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1142
  \item ancillary functions, not from the Isabelle source code, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1143
  which enable the reader to run relevant code examples
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1144
  \item type abbreviations, which help explain the uses of certain functions
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1145
  \end{itemize}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1146
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1147
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1148
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1149
section {* Parsing Isar input *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1150
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1151
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1152
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1153
  The typical parsing function has the type
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1154
  \texttt{'src -> 'res * 'src}, with input  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1155
  of type \texttt{'src}, returning a result 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1156
  of type \texttt{'res}, which is (or is derived from) the first part of the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1157
  input, and also returning the remainder of the input.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1158
  (In the common case, when it is clear what the ``remainder of the input''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1159
  means, we will just say that the functions ``returns'' the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1160
  value of type \texttt{'res}). 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1161
  An exception is raised if an appropriate value 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1162
  cannot be produced from the input.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1163
  A range of exceptions can be used to identify different reasons 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1164
  for the failure of a parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1165
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1166
  This contrasts the standard parsing function in Standard ML,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1167
  which is of type 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1168
  \texttt{type ('res, 'src) reader = 'src -> ('res * 'src) option};
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1169
  (for example, \texttt{List.getItem} and \texttt{Substring.getc}).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1170
  However, much of the discussion at 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1171
  FIX file:/home/jeremy/html/ml/SMLBasis/string-cvt.html
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1172
  is relevant.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1173
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1174
  Naturally one may convert between the two different sorts of parsing functions
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1175
  as follows:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1176
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1177
  open StringCvt ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1178
  type ('res, 'src) ex_reader = 'src -> 'res * 'src
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1179
  ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader 
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1180
  fun ex_reader rdr src = Option.valOf (rdr src) ;
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1181
  reader : ('res, 'src) ex_reader -> ('res, 'src) reader 
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1182
  fun reader exrdr src = SOME (exrdr src) handle _ => NONE ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1183
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1184
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1185
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1186
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1187
section{* The \texttt{Scan} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1188
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1189
text {* 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1190
  The source file is \texttt{src/General/scan.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1191
  This structure provides functions for using and combining parsing functions
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1192
  of the type \texttt{'src -> 'res * 'src}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1193
  Three exceptions are used:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1194
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1195
  exception MORE of string option;  (*need more input (prompt)*)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1196
  exception FAIL of string option;  (*try alternatives (reason of failure)*)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1197
  exception ABORT of string;        (*dead end*)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1198
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1199
  Many functions in this structure (generally those with names composed of
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1200
  symbols) are declared as infix.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1201
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1202
  Some functions from that structure are
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1203
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1204
  |-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1205
  'src -> 'res2 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1206
  --| : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1207
  'src -> 'res1 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1208
  -- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1209
  'src -> ('res1 * 'res2) * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1210
  ^^ : ('src -> string * 'src') * ('src' -> string * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1211
  'src -> string * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1212
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1213
  These functions parse a result off the input source twice.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1214
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1215
  \texttt{|--} and \texttt{--|} 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1216
  return the first result and the second result, respectively.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1217
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1218
  \texttt{--} returns both.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1219
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1220
  \verb|^^| returns the result of concatenating the two results
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1221
  (which must be strings).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1222
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1223
  Note how, although the types 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1224
  \texttt{'src}, \texttt{'src'} and \texttt{'src''} will normally be the same,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1225
  the types as shown help suggest the behaviour of the functions.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1226
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1227
  :-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1228
  'src -> ('res1 * 'res2) * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1229
  :|-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1230
  'src -> 'res2 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1231
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1232
  These are similar to \texttt{|--} and \texttt{--|},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1233
  except that the second parsing function can depend on the result of the first.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1234
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1235
  >> : ('src -> 'res1 * 'src') * ('res1 -> 'res2) -> 'src -> 'res2 * 'src'
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1236
  || : ('src -> 'res_src) * ('src -> 'res_src) -> 'src -> 'res_src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1237
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1238
  \texttt{p >> f} applies a function \texttt{f} to the result of a parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1239
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1240
  \texttt{||} tries a second parsing function if the first one
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1241
  fails by raising an exception of the form \texttt{FAIL \_}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1242
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1243
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1244
  succeed : 'res -> ('src -> 'res * 'src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1245
  fail : ('src -> 'res_src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1246
  !! : ('src * string option -> string) -> 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1247
  ('src -> 'res_src) -> ('src -> 'res_src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1248
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1249
  \texttt{succeed r} returns \texttt{r}, with the input unchanged.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1250
  \texttt{fail} always fails, raising exception \texttt{FAIL NONE}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1251
  \texttt{!! f} only affects the failure mode, turning a failure that
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1252
  raises \texttt{FAIL \_} into a failure that raises \texttt{ABORT ...}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1253
  This is used to prevent recovery from the failure ---
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1254
  thus, in \texttt{!! parse1 || parse2}, if \texttt{parse1} fails, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1255
  it won't recover by trying \texttt{parse2}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1256
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1257
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1258
  one : ('si -> bool) -> ('si list -> 'si * 'si list) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1259
  some : ('si -> 'res option) -> ('si list -> 'res * 'si list) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1260
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1261
  These require the input to be a list of items:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1262
  they fail, raising \texttt{MORE NONE} if the list is empty.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1263
  On other failures they raise \texttt{FAIL NONE} 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1264
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1265
  \texttt{one p} takes the first
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1266
  item from the list if it satisfies \texttt{p}, otherwise fails.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1267
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1268
  \texttt{some f} takes the first
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1269
  item from the list and applies \texttt{f} to it, failing if this returns
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1270
  \texttt{NONE}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1271
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1272
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1273
  many : ('si -> bool) -> 'si list -> 'si list * 'si list ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1274
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1275
  \texttt{many p} takes items from the input until it encounters one 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1276
  which does not satisfy \texttt{p}.  If it reaches the end of the input
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1277
  it fails, raising \texttt{MORE NONE}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1278
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1279
  \texttt{many1} (with the same type) fails if the first item 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1280
  does not satisfy \texttt{p}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1281
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1282
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1283
  option : ('src -> 'res * 'src) -> ('src -> 'res option * 'src)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1284
  optional : ('src -> 'res * 'src) -> 'res -> ('src -> 'res * 'src)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1285
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1286
  \texttt{option}: 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1287
  where the parser \texttt{f} succeeds with result \texttt{r} 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1288
  or raises \texttt{FAIL \_},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1289
  \texttt{option f} gives the result \texttt{SOME r} or \texttt{NONE}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1290
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1291
  \texttt{optional}: if parser \texttt{f} fails by raising \texttt{FAIL \_},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1292
  \texttt{optional f default} provides the result \texttt{default}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1293
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1294
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1295
  repeat : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1296
  repeat1 : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1297
  bulk : ('src -> 'res * 'src) -> 'src -> 'res list * 'src 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1298
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1299
  \texttt{repeat f} repeatedly parses an item off the remaining input until 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1300
  \texttt{f} fails with \texttt{FAIL \_}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1301
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1302
  \texttt{repeat1} is as for \texttt{repeat}, but requires at least one
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1303
  successful parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1304
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1305
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1306
  lift : ('src -> 'res * 'src) -> ('ex * 'src -> 'res * ('ex * 'src))
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1307
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1308
  \texttt{lift} changes the source type of a parser by putting in an extra
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1309
  component \texttt{'ex}, which is ignored in the parsing.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1310
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1311
  The \texttt{Scan} structure also provides the type \texttt{lexicon}, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1312
  HOW DO THEY WORK ?? TO BE COMPLETED
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1313
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1314
  dest_lexicon: lexicon -> string list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1315
  make_lexicon: string list list -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1316
  empty_lexicon: lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1317
  extend_lexicon: string list list -> lexicon -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1318
  merge_lexicons: lexicon -> lexicon -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1319
  is_literal: lexicon -> string list -> bool ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1320
  literal: lexicon -> string list -> string list * string list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1321
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1322
  Two lexicons, for the commands and keywords, are stored and can be retrieved
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1323
  by:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1324
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1325
  val (command_lexicon, keyword_lexicon) = OuterSyntax.get_lexicons () ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1326
  val commands = Scan.dest_lexicon command_lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1327
  val keywords = Scan.dest_lexicon keyword_lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1328
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1329
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1330
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1331
section{* The \texttt{OuterLex} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1332
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1333
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1334
  The source file is @{text "src/Pure/Isar/outer_lex.ML"}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1335
  In some other source files its name is abbreviated:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1336
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1337
  structure T = OuterLex;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1338
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1339
  This structure defines the type \texttt{token}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1340
  (The types
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1341
  \texttt{OuterLex.token},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1342
  \texttt{OuterParse.token} and
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1343
  \texttt{SpecParse.token} are all the same).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1344
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1345
  Input text is split up into tokens, and the input source type for many parsing
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1346
  functions is \texttt{token list}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1347
250
ab9e09076462 some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
parents: 244
diff changeset
  1348
  The datatype definition (which is not published in the signature) is
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1349
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1350
  datatype token = Token of Position.T * (token_kind * string);
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1351
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1352
  but here are some runnable examples for viewing tokens: 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1353
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1354
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1355
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1356
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1357
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1358
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1359
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1360
  val toks = OuterSyntax.scan Position.none
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1361
   "theory,imports;begin x.y.z apply ?v1 ?'a 'a -- || 44 simp (* xx *) { * fff * }" ;
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1362
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1363
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1364
ML{*
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1365
  print_depth 20 ;
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1366
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1367
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1368
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1369
  map OuterLex.text_of toks ;
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1370
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1371
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1372
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1373
  val proper_toks = filter OuterLex.is_proper toks ;
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1374
*}  
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1375
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1376
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1377
  map OuterLex.kind_of proper_toks 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1378
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1379
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1380
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1381
  map OuterLex.unparse proper_toks ;
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1382
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1383
69
19106a9975c1 highligted the background of ML-code
Christian Urban <urbanc@in.tum.de>
parents: 68
diff changeset
  1384
ML{*
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
  1385
  OuterLex.stopper
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1386
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1387
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1388
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1389
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1390
  The function \texttt{is\_proper : token -> bool} identifies tokens which are
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1391
  not white space or comments: many parsing functions assume require spaces or
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1392
  comments to have been filtered out.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1393
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1394
  There is a special end-of-file token:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1395
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1396
  val (tok_eof : token, is_eof : token -> bool) = T.stopper ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1397
  (* end of file token *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1398
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1399
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1400
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1401
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1402
section {* The \texttt{OuterParse} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1403
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1404
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1405
  The source file is \texttt{src/Pure/Isar/outer\_parse.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1406
  In some other source files its name is abbreviated:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1407
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1408
  structure P = OuterParse;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1409
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1410
  Here the parsers use \texttt{token list} as the input source type. 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1411
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1412
  Some of the parsers simply select the first token, provided that it is of the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1413
  right kind (as returned by \texttt{T.kind\_of}): these are 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1414
  \texttt{ command, keyword, short\_ident, long\_ident, sym\_ident, term\_var,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1415
  type\_ident, type\_var, number, string, alt\_string, verbatim, sync, eof}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1416
  Others select the first token, provided that it is one of several kinds,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1417
  (eg, \texttt{name, xname, text, typ}).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1418
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1419
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1420
  type 'a tlp = token list -> 'a * token list ; (* token list parser *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1421
  $$$ : string -> string tlp
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1422
  nat : int tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1423
  maybe : 'a tlp -> 'a option tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1424
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1425
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1426
  \texttt{\$\$\$ s} returns the first token,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1427
  if it equals \texttt{s} \emph{and} \texttt{s} is a keyword.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1428
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1429
  \texttt{nat} returns the first token, if it is a number, and evaluates it.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1430
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1431
  \texttt{maybe}: if \texttt{p} returns \texttt{r}, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1432
  then \texttt{maybe p} returns \texttt{SOME r} ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1433
  if the first token is an underscore, it returns \texttt{NONE}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1434
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1435
  A few examples:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1436
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1437
  P.list : 'a tlp -> 'a list tlp ; (* likewise P.list1 *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1438
  P.and_list : 'a tlp -> 'a list tlp ; (* likewise P.and_list1 *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1439
  val toks : token list = OuterSyntax.scan "44 ,_, 66,77" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1440
  val proper_toks = List.filter T.is_proper toks ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1441
  P.list P.nat toks ; (* OK, doesn't recognize white space *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1442
  P.list P.nat proper_toks ; (* fails, doesn't recognize what follows ',' *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1443
  P.list (P.maybe P.nat) proper_toks ; (* fails, end of input *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1444
  P.list (P.maybe P.nat) (proper_toks @ [tok_eof]) ; (* OK *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1445
  val toks : token list = OuterSyntax.scan "44 and 55 and 66 and 77" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1446
  P.and_list P.nat (List.filter T.is_proper toks @ [tok_eof]) ; (* ??? *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1447
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1448
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1449
  The following code helps run examples:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1450
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1451
  fun parse_str tlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1452
  let val toks : token list = OuterSyntax.scan str ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1453
  val proper_toks = List.filter T.is_proper toks @ [tok_eof] ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1454
  val (res, rem_toks) = tlp proper_toks ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1455
  val rem_str = String.concat
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1456
  (Library.separate " " (List.map T.unparse rem_toks)) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1457
  in (res, rem_str) end ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1458
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1459
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1460
  Some examples from \texttt{src/Pure/Isar/outer\_parse.ML}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1461
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1462
  val type_args =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1463
  type_ident >> Library.single ||
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1464
  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1465
  Scan.succeed [];
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1466
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1467
  There are three ways parsing a list of type arguments can succeed.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1468
  The first line reads a single type argument, and turns it into a singleton
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1469
  list.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1470
  The second line reads "(", and then the remainder, ignoring the "(" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1471
  the remainder consists of a list of type identifiers (at least one),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1472
  and then a ")" which is also ignored.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1473
  The \texttt{!!!} ensures that if the parsing proceeds this far and then fails,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1474
  it won't try the third line (see the description of \texttt{Scan.!!}).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1475
  The third line consumes no input and returns the empty list.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1476
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1477
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1478
  fun triple2 (x, (y, z)) = (x, y, z);
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1479
  val arity = xname -- ($$$ "::" |-- !!! (
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1480
  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) []
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1481
  -- sort)) >> triple2;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1482
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1483
  The parser \texttt{arity} reads a typename $t$, then ``\texttt{::}'' (which is
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1484
  ignored), then optionally a list $ss$ of sorts and then another sort $s$.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1485
  The result $(t, (ss, s))$ is transformed by \texttt{triple2} to $(t, ss, s)$.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1486
  The second line reads the optional list of sorts:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1487
  it reads first ``\texttt{(}'' and last ``\texttt{)}'', which are both ignored,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1488
  and between them a comma-separated list of sorts.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1489
  If this list is absent, the default \texttt{[]} provides the list of sorts.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1490
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1491
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1492
  parse_str P.type_args "('a, 'b) ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1493
  parse_str P.type_args "'a ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1494
  parse_str P.type_args "ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1495
  parse_str P.arity "ty :: tycl" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1496
  parse_str P.arity "ty :: (tycl1, tycl2) tycl" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1497
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1498
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1499
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1500
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1501
section {* The \texttt{SpecParse} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1502
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1503
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1504
  The source file is \texttt{src/Pure/Isar/spec\_parse.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1505
  This structure contains token list parsers for more complicated values.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1506
  For example, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1507
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1508
  open SpecParse ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1509
  attrib : Attrib.src tok_rdr ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1510
  attribs : Attrib.src list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1511
  opt_attribs : Attrib.src list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1512
  xthm : (thmref * Attrib.src list) tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1513
  xthms1 : (thmref * Attrib.src list) list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1514
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1515
  parse_str attrib "simp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1516
  parse_str opt_attribs "hello" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1517
  val (ass, "") = parse_str attribs "[standard, xxxx, simp, intro, OF sym]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1518
  map Args.dest_src ass ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1519
  val (asrc, "") = parse_str attrib "THEN trans [THEN sym]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1520
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1521
  parse_str xthm "mythm [attr]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1522
  parse_str xthms1 "thm1 [attr] thms2" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1523
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1524
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1525
  As you can see, attributes are described using types of the \texttt{Args}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1526
  structure, described below.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1527
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1528
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1529
section{* The \texttt{Args} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1530
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1531
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1532
  The source file is \texttt{src/Pure/Isar/args.ML}.
250
ab9e09076462 some polishing; added together with Jasmin more examples to the pretty printing section
Christian Urban <urbanc@in.tum.de>
parents: 244
diff changeset
  1533
  The primary type of this structure is the \texttt{src} datatype;
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1534
  the single constructors not published in the signature, but 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1535
  \texttt{Args.src} and \texttt{Args.dest\_src}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1536
  are in fact the constructor and destructor functions.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1537
  Note that the types \texttt{Attrib.src} and \texttt{Method.src}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1538
  are in fact \texttt{Args.src}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1539
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1540
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1541
  src : (string * Args.T list) * Position.T -> Args.src ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1542
  dest_src : Args.src -> (string * Args.T list) * Position.T ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1543
  Args.pretty_src : Proof.context -> Args.src -> Pretty.T ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1544
  fun pr_src ctxt src = Pretty.string_of (Args.pretty_src ctxt src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1545
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1546
  val thy = ML_Context.the_context () ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1547
  val ctxt = ProofContext.init thy ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1548
  map (pr_src ctxt) ass ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1549
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1550
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1551
  So an \texttt{Args.src} consists of the first word, then a list of further 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1552
  ``arguments'', of type \texttt{Args.T}, with information about position in the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1553
  input.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1554
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1555
  (* how an Args.src is parsed *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1556
  P.position : 'a tlp -> ('a * Position.T) tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1557
  P.arguments : Args.T list tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1558
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1559
  val parse_src : Args.src tlp =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1560
  P.position (P.xname -- P.arguments) >> Args.src ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1561
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1562
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1563
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1564
  val ((first_word, args), pos) = Args.dest_src asrc ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1565
  map Args.string_of args ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1566
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1567
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1568
  The \texttt{Args} structure contains more parsers and parser transformers 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1569
  for which the input source type is \texttt{Args.T list}.  For example,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1570
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1571
  type 'a atlp = Args.T list -> 'a * Args.T list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1572
  open Args ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1573
  nat : int atlp ; (* also Args.int *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1574
  thm_sel : PureThy.interval list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1575
  list : 'a atlp -> 'a list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1576
  attribs : (string -> string) -> Args.src list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1577
  opt_attribs : (string -> string) -> Args.src list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1578
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1579
  (* parse_atl_str : 'a atlp -> (string -> 'a * string) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1580
  given an Args.T list parser, to get a string parser *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1581
  fun parse_atl_str atlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1582
  let val (ats, rem_str) = parse_str P.arguments str ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1583
  val (res, rem_ats) = atlp ats ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1584
  in (res, String.concat (Library.separate " "
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1585
  (List.map Args.string_of rem_ats @ [rem_str]))) end ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1586
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1587
  parse_atl_str Args.int "-1-," ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1588
  parse_atl_str (Scan.option Args.int) "x1-," ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1589
  parse_atl_str Args.thm_sel "(1-,4,13-22)" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1590
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1591
  val (ats as atsrc :: _, "") = parse_atl_str (Args.attribs I)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1592
  "[THEN trans [THEN sym], simp, OF sym]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1593
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1594
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1595
  From here, an attribute is interpreted using \texttt{Attrib.attribute}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1596
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1597
  \texttt{Args} has a large number of functions which parse an \texttt{Args.src}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1598
  and also refer to a generic context.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1599
  Note the use of \texttt{Scan.lift} for this.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1600
  (as does \texttt{Attrib} - RETHINK THIS)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1601
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1602
  (\texttt{Args.syntax} shown below has type specialised)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1603
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1604
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1605
  type ('res, 'src) parse_fn = 'src -> 'res * 'src ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1606
  type 'a cgatlp = ('a, Context.generic * Args.T list) parse_fn ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1607
  Scan.lift : 'a atlp -> 'a cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1608
  term : term cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1609
  typ : typ cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1610
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1611
  Args.syntax : string -> 'res cgatlp -> src -> ('res, Context.generic) parse_fn ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1612
  Attrib.thm : thm cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1613
  Attrib.thms : thm list cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1614
  Attrib.multi_thm : thm list cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1615
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1616
  (* parse_cgatl_str : 'a cgatlp -> (string -> 'a * string) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1617
  given a (Context.generic * Args.T list) parser, to get a string parser *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1618
  fun parse_cgatl_str cgatlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1619
  let 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1620
    (* use the current generic context *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1621
    val generic = Context.Theory thy ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1622
    val (ats, rem_str) = parse_str P.arguments str ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1623
    (* ignore any change to the generic context *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1624
    val (res, (_, rem_ats)) = cgatlp (generic, ats) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1625
  in (res, String.concat (Library.separate " "
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1626
      (List.map Args.string_of rem_ats @ [rem_str]))) end ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1627
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1628
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1629
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1630
section{* Attributes, and the \texttt{Attrib} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1631
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1632
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1633
  The type \texttt{attribute} is declared in \texttt{src/Pure/thm.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1634
  The source file for the \texttt{Attrib} structure is
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1635
  \texttt{src/Pure/Isar/attrib.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1636
  Most attributes use a theorem to change a generic context (for example, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1637
  by declaring that the theorem should be used, by default, in simplification),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1638
  or change a theorem (which most often involves referring to the current
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1639
  theory). 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1640
  The functions \texttt{Thm.rule\_attribute} and
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1641
  \texttt{Thm.declaration\_attribute} create attributes of these kinds.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1642
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1643
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1644
  type attribute = Context.generic * thm -> Context.generic * thm;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1645
  type 'a trf = 'a -> 'a ; (* transformer of a given type *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1646
  Thm.rule_attribute  : (Context.generic -> thm -> thm) -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1647
  Thm.declaration_attribute : (thm -> Context.generic trf) -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1648
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1649
  Attrib.print_attributes : theory -> unit ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1650
  Attrib.pretty_attribs : Proof.context -> src list -> Pretty.T list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1651
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1652
  List.app Pretty.writeln (Attrib.pretty_attribs ctxt ass) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1653
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1654
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1655
  An attribute is stored in a theory as indicated by:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1656
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1657
  Attrib.add_attributes : 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1658
  (bstring * (src -> attribute) * string) list -> theory trf ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1659
  (*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1660
  Attrib.add_attributes [("THEN", THEN_att, "resolution with rule")] ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1661
  *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1662
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1663
  where the first and third arguments are name and description of the attribute,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1664
  and the second is a function which parses the attribute input text 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1665
  (including the attribute name, which has necessarily already been parsed).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1666
  Here, \texttt{THEN\_att} is a function declared in the code for the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1667
  structure \texttt{Attrib}, but not published in its signature.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1668
  The source file \texttt{src/Pure/Isar/attrib.ML} shows the use of 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1669
  \texttt{Attrib.add\_attributes} to add a number of attributes.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1670
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1671
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1672
  FullAttrib.THEN_att : src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1673
  FullAttrib.THEN_att atsrc (generic, ML_Context.thm "sym") ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1674
  FullAttrib.THEN_att atsrc (generic, ML_Context.thm "all_comm") ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1675
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1676
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1677
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1678
  Attrib.syntax : attribute cgatlp -> src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1679
  Attrib.no_args : attribute -> src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1680
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1681
  When this is called as \texttt{syntax scan src (gc, th)}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1682
  the generic context \texttt{gc} is used 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1683
  (and potentially changed to \texttt{gc'})
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1684
  by \texttt{scan} in parsing to obtain an attribute \texttt{attr} which would
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1685
  then be applied to \texttt{(gc', th)}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1686
  The source for parsing the attribute is the arguments part of \texttt{src},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1687
  which must all be consumed by the parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1688
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1689
  For example, for \texttt{Attrib.no\_args attr src}, the attribute parser 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1690
  simply returns \texttt{attr}, requiring that the arguments part of
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1691
  \texttt{src} must be empty.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1692
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1693
  Some examples from \texttt{src/Pure/Isar/attrib.ML}, modified:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1694
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1695
  fun rot_att_n n (gc, th) = (gc, rotate_prems n th) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1696
  rot_att_n : int -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1697
  val rot_arg = Scan.lift (Scan.optional Args.int 1 : int atlp) : int cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1698
  val rotated_att : src -> attribute =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1699
  Attrib.syntax (rot_arg >> rot_att_n : attribute cgatlp) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1700
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1701
  val THEN_arg : int cgatlp = Scan.lift 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1702
  (Scan.optional (Args.bracks Args.nat : int atlp) 1 : int atlp) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1703
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1704
  Attrib.thm : thm cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1705
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1706
  THEN_arg -- Attrib.thm : (int * thm) cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1707
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1708
  fun THEN_att_n (n, tht) (gc, th) = (gc, th RSN (n, tht)) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1709
  THEN_att_n : int * thm -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1710
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1711
  val THEN_att : src -> attribute = Attrib.syntax
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1712
  (THEN_arg -- Attrib.thm >> THEN_att_n : attribute cgatlp);
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1713
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1714
  The functions I've called \texttt{rot\_arg} and \texttt{THEN\_arg}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1715
  read an optional argument, which for \texttt{rotated} is an integer, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1716
  and for \texttt{THEN} is a natural enclosed in square brackets;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1717
  the default, if the argument is absent, is 1 in each case.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1718
  Functions \texttt{rot\_att\_n} and \texttt{THEN\_att\_n} turn these into
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1719
  attributes, where \texttt{THEN\_att\_n} also requires a theorem, which is
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1720
  parsed by \texttt{Attrib.thm}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1721
  Infix operators \texttt{--} and \texttt{>>} are in the structure \texttt{Scan}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1722
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1723
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1724
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1725
section{* Methods, and the \texttt{Method} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1726
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1727
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1728
  The source file is \texttt{src/Pure/Isar/method.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1729
  The type \texttt{method} is defined by the datatype declaration
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1730
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1731
  (* datatype method = Meth of thm list -> cases_tactic; *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1732
  RuleCases.NO_CASES : tactic -> cases_tactic ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1733
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1734
  In fact \texttt{RAW\_METHOD\_CASES} (below) is exactly the constructor
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1735
  \texttt{Meth}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1736
  A \texttt{cases\_tactic} is an elaborated version of a tactic.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1737
  \texttt{NO\_CASES tac} is a \texttt{cases\_tactic} which consists of a
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1738
  \texttt{cases\_tactic} without any further case information.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1739
  For further details see the description of structure \texttt{RuleCases} below.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1740
  The list of theorems to be passed to a method consists of the current
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1741
  \emph{facts} in the proof.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1742
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1743
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1744
  RAW_METHOD : (thm list -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1745
  METHOD : (thm list -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1746
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1747
  SIMPLE_METHOD : tactic -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1748
  SIMPLE_METHOD' : (int -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1749
  SIMPLE_METHOD'' : ((int -> tactic) -> tactic) -> (int -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1750
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1751
  RAW_METHOD_CASES : (thm list -> cases_tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1752
  METHOD_CASES : (thm list -> cases_tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1753
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1754
  A method is, in its simplest form, a tactic; applying the method is to apply
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1755
  the tactic to the current goal state.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1756
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1757
  Applying \texttt{RAW\_METHOD tacf} creates a tactic by applying 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1758
  \texttt{tacf} to the current {facts}, and applying that tactic to the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1759
  goal state.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1760
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1761
  \texttt{METHOD} is similar but also first applies
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1762
  \texttt{Goal.conjunction\_tac} to all subgoals.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1763
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1764
  \texttt{SIMPLE\_METHOD tac} inserts the facts into all subgoals and then
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1765
  applies \texttt{tacf}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1766
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1767
  \texttt{SIMPLE\_METHOD' tacf} inserts the facts and then
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1768
  applies \texttt{tacf} to subgoal 1.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1769
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1770
  \texttt{SIMPLE\_METHOD'' quant tacf} does this for subgoal(s) selected by
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1771
  \texttt{quant}, which may be, for example,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1772
  \texttt{ALLGOALS} (all subgoals),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1773
  \texttt{TRYALL} (try all subgoals, failure is OK),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1774
  \texttt{FIRSTGOAL} (try subgoals until it succeeds once), 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1775
  \texttt{(fn tacf => tacf 4)} (subgoal 4), etc
16
5045dec52d2b polished
Christian Urban <urbanc@in.tum.de>
parents: 4
diff changeset
  1776
  (see the \texttt{Tactical} structure, FIXME) %%\cite[Chapter 4]{ref}).
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1777
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1778
  A method is stored in a theory as indicated by:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1779
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1780
  Method.add_method : 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1781
  (bstring * (src -> Proof.context -> method) * string) -> theory trf ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1782
  ( *
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1783
  * )
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1784
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1785
  where the first and third arguments are name and description of the method,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1786
  and the second is a function which parses the method input text 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1787
  (including the method name, which has necessarily already been parsed).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1788
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1789
  Here, \texttt{xxx} is a function declared in the code for the
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1790
  structure \texttt{Method}, but not published in its signature.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1791
  The source file \texttt{src/Pure/Isar/method.ML} shows the use of 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1792
  \texttt{Method.add\_method} to add a number of methods.
240
d111f5988e49 replaced explode by Symbol.explode
Christian Urban <urbanc@in.tum.de>
parents: 236
diff changeset
  1793
*}
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1794
75
Christian Urban <urbanc@in.tum.de>
parents: 74
diff changeset
  1795
(*>*)
220
fbcb89d84ba6 polishing
griff
parents: 211
diff changeset
  1796
end