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