CookBook/Parsing.thy
author Christian Urban <urbanc@in.tum.de>
Mon, 12 Jan 2009 16:03:05 +0000
changeset 66 d563f8ff6aa0
parent 65 c8e9a4f97916
child 67 5fbeeac2901b
permissions -rw-r--r--
tuned
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
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
     2
imports Base
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     3
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     4
begin
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     5
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
     6
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     7
chapter {* Parsing *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     8
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
     9
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
    10
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    11
  Isabelle distinguishes between \emph{outer} and \emph{inner} syntax. 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    12
  Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    13
  on, belong to the outer syntax, whereas items inside double quotation marks, such 
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    14
  as terms, types and so on, belong to the inner syntax. For parsing inner syntax, 
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    15
  Isabelle uses a rather general and sophisticated algorithm due to Earley, which 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    16
  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
    17
  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
    18
  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
    19
  Isabelle developers are usually concerned with writing these outer syntax parsers, 
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    20
  either for new definitional packages or for calling tactics with specific arguments. 
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    21
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    22
  \begin{readmore}
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    23
  The library 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    24
  for writing parser combinators is split up, roughly, into two parts. 
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    25
  The first part consists of a collection of generic parser combinators defined
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    26
  in the structure @{ML_struct Scan} in the file 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    27
  @{ML_file "Pure/General/scan.ML"}. The second part of the library consists of 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    28
  combinators for dealing with specific token types, which are defined in the 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    29
  structure @{ML_struct OuterParse} in the file 
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    30
  @{ML_file "Pure/Isar/outer_parse.ML"}.
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
    31
  \end{readmore}
38
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
*}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    34
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
    35
section {* Building Generic Parsers *}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    36
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    37
text {*
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    38
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    39
  Let us first have a look at parsing strings using generic parsing combinators. 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
    40
  The function @{ML "(op $$)"} 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
    41
  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
    42
  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
    43
  For example:
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    44
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    45
  @{ML_response [display] "($$ \"h\") (explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    46
  @{ML_response [display] "($$ \"w\") (explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    47
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
    48
  This function 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
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    51
  @{ML_response_fake [display] "($$ \"x\") (explode \"world\")" 
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. 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    63
  It is used for example in the function @{ML "(op !!)"} (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
  
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
    69
  Slightly more general than the parser @{ML "(op $$)"} is the function @{ML
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
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    76
@{ML_response [display] 
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\")
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    79
  val input1 = (explode \"hello\")
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    80
  val input2 = (explode \"world\")
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    81
in
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    82
    (hw input1, hw input2)
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
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
    86
  Two parser can be connected in sequence by using the function @{ML "(op --)"}. 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
    87
  For example parsing @{text "h"}, @{text "e"} and @{text "l"} in this 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
    88
  sequence can be achieved by
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
    89
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    90
  @{ML_response [display] "(($$ \"h\") -- ($$ \"e\") -- ($$ \"l\")) (explode \"hello\")"
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    91
                          "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    92
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
    93
  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
    94
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
    95
  If, as in the previous example, one wants to parse a particular string, 
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
    96
  then one 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
    97
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
    98
  @{ML_response [display] "Scan.this_string \"hell\" (explode \"hello\")"
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
    99
                          "(\"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
   100
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   101
  Parsers that explore alternatives can be constructed using the function @{ML
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   102
  "(op ||)"}. For example, the parser @{ML "(p || q)" for p q} returns the
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   103
  result of @{text "p"}, in case it succeeds, otherwise it returns the
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   104
  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
   105
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   106
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   107
@{ML_response [display] 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   108
"let 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   109
  val hw = ($$ \"h\") || ($$ \"w\")
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   110
  val input1 = (explode \"hello\")
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   111
  val input2 = (explode \"world\")
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   112
in
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   113
  (hw input1, hw input2)
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   114
end"
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   115
  "((\"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
   116
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
   117
  The functions @{ML "(op |--)"} and @{ML "(op --|)"} work like the sequencing function 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   118
  for parsers, except that they discard the item being parsed by the first (respectively second)
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   119
  parser. For example
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   120
  
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   121
@{ML_response [display]
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   122
"let 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   123
  val just_e = ($$ \"h\") |-- ($$ \"e\") 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   124
  val just_h = ($$ \"h\") --| ($$ \"e\") 
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   125
  val input = (explode \"hello\")  
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   126
in 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   127
  (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
   128
end"
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   129
  "((\"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
   130
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   131
  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
   132
  @{text "p"}, if it succeeds; otherwise it returns 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   133
  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
   134
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   135
@{ML_response [display]
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   136
"let 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   137
  val p = Scan.optional ($$ \"h\") \"x\"
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   138
  val input1 = (explode \"hello\")
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   139
  val input2 = (explode \"world\")  
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   140
in 
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   141
  (p input1, p input2)
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   142
end" 
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   143
 "((\"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
   144
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   145
  The function @{ML Scan.option} works similarly, except no default value can
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   146
  be given. Instead, the result is wrapped as an @{text "option"}-type. For example:
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   147
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   148
@{ML_response [display]
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   149
"let 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   150
  val p = Scan.option ($$ \"h\")
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   151
  val input1 = (explode \"hello\")
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   152
  val input2 = (explode \"world\")  
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   153
in 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   154
  (p input1, p input2)
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   155
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
   156
39
631d12c25bde substantial changes to the antiquotations (preliminary version)
Christian Urban <urbanc@in.tum.de>
parents: 38
diff changeset
   157
  The function @{ML "(op !!)"} helps to produce appropriate error messages
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   158
  during parsing. For example if one wants to parse that @{text p} is immediately 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   159
  followed by @{text q}, or start a completely different parser @{text r},
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   160
  one might write
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   161
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   162
  @{ML [display] "(p -- q) || r" for p q r}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   163
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   164
  However, this parser is problematic for producing an appropriate error message, in case
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   165
  the parsing of @{ML "(p -- q)" for p q} fails. Because in that case one loses the information 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   166
  that @{text p} should be followed by @{text q}. To see this consider the case in
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   167
  which @{text p} 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   168
  is present in the input, but not @{text q}. That means @{ML "(p -- q)" for p q} will fail 
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   169
  and the 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   170
  alternative parser @{text r} will be tried. However in many circumstance this will be the wrong
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
   171
  parser for the input ``p-followed-by-q'' and therefore will also fail. The error message is then 
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
   172
  caused by the
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   173
  failure of @{text r}, not by the absence of @{text q} in the input. This kind of situation
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   174
  can be avoided when using the function @{ML "(op !!)"}. This function aborts the whole process of
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   175
  parsing in case of a failure and prints an error message. For example if we invoke the parser
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   176
  
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   177
  @{ML [display] "(!! (fn _ => \"foo\") ($$ \"h\"))"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   178
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   179
  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
   180
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   181
  @{ML_response [display] 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   182
                "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"hello\")" 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   183
                "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   184
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   185
  but if we invoke it on @{text [quotes] "world"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   186
  
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   187
  @{ML_response_fake [display] "(!! (fn _ => \"foo\") ($$ \"h\")) (explode \"world\")"
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   188
                               "Exception ABORT raised"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   189
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   190
  then the parsing aborts and the error message @{text "foo"} is printed out. In order to
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   191
  see the error message properly, we need to prefix the parser with the function 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   192
  @{ML "Scan.error"}. For example
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   193
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   194
  @{ML_response_fake [display] "Scan.error ((!! (fn _ => \"foo\") ($$ \"h\")))"
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   195
                               "Exception Error \"foo\" raised"}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   196
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   197
  This ``prefixing'' is usually done by wrappers such as @{ML "OuterSyntax.command"} 
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   198
  (FIXME: give reference to later place). 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   199
  
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   200
  Let us now return to our example of parsing @{ML "(p -- q) || r" for p q r}. If we want
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   201
  to generate the correct error message for p-followed-by-q, then
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   202
  we have to write:
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   203
*}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   204
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   205
ML {* 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   206
fun p_followed_by_q p q r =
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   207
  let 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   208
     val err_msg = (fn _ => p ^ " is not followed by " ^ q)
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   209
  in
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   210
    ($$ p -- (!! err_msg ($$ q))) || ($$ r -- $$ r)
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   211
  end
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   212
*}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   213
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   214
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   215
text {*
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   216
  Running this parser with the @{text [quotes] "h"} and @{text [quotes] "e"}, and 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   217
  the input @{text [quotes] "holle"} 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   218
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   219
  @{ML_response_fake [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"holle\")"
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   220
                               "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
   221
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   222
  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
   223
 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   224
  @{ML_response [display] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (explode \"wworld\")"
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   225
                          "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   226
  
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   227
  yields the expected parsing. 
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   228
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   229
  The function @{ML "Scan.repeat p" for p} will apply a parser @{text p} as 
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   230
  often as it succeeds. For example
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   231
  
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   232
  @{ML_response [display] "Scan.repeat ($$ \"h\") (explode \"hhhhello\")" 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   233
                "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   234
  
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   235
  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
   236
  @{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
   237
  succeeds at least once.
48
609f9ef73494 fixed FIXME's in fake responses
Christian Urban <urbanc@in.tum.de>
parents: 47
diff changeset
   238
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   239
  Also note that the parser would have aborted with the exception @{text MORE}, if
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   240
  we 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
   241
  the wrapper @{ML Scan.finite} and the ``stopper-token'' @{ML Symbol.stopper}. With
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   242
  them we can write
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   243
  
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   244
  @{ML_response [display] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (explode \"hhhh\")" 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   245
                "([\"h\", \"h\", \"h\", \"h\"], [])"}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   246
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   247
  @{ML Symbol.stopper} is the ``end-of-input'' indicator for parsing strings;
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   248
  other stoppers need to be used when parsing token, for example. However, this kind of 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   249
  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
   250
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   251
  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
   252
  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
   253
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   254
  @{ML_response [display] 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   255
"let 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   256
   val p = Scan.repeat (Scan.one Symbol.not_eof)
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   257
   val input = (explode \"foo bar foo\") 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   258
in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   259
   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
   260
end" 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   261
"([\"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
   262
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   263
  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
   264
  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
   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
  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
   267
  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
   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
  @{ML_response_fake_both [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"hello\")"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   270
                               "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
   271
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   272
  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
   273
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   274
  @{ML_response [display] "Scan.unless ($$ \"h\") ($$ \"w\") (explode \"world\")"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   275
                          "(\"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
   276
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   277
  succeeds. 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   278
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   279
  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
   280
  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
   281
  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
   282
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   283
  @{ML_response [display]
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   284
"let 
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   285
  val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   286
  val input1 = (explode \"fooooo\")
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   287
  val input2 = (explode \"foo*ooo\")
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   288
in
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   289
  (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
   290
   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
   291
end"
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   292
"(([\"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
   293
 ([\"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
   294
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   295
  After parsing is done, one nearly always wants to apply a function on the parsed 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   296
  items. To do this the function @{ML "(p >> f)" for p f} can be employed, which runs 
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   297
  first the parser @{text p} and upon successful completion applies the 
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   298
  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
   299
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   300
@{ML_response [display]
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   301
"let 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   302
  fun double (x,y) = (x^x,y^y) 
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   303
in
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   304
  (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\")
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   305
end"
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   306
"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   307
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   308
  doubles the two parsed input strings. Or
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   309
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   310
  @{ML_response [display] 
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   311
"let 
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   312
   val p = Scan.repeat (Scan.one Symbol.not_eof) >> implode
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   313
   val input = (explode \"foo bar foo\") 
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   314
in
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   315
   Scan.finite Symbol.stopper p input
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   316
end" 
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   317
"(\"foo bar foo\",[])"}
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   318
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
   319
  where the single-character strings in the parsed output are transformed
59
Christian Urban <urbanc@in.tum.de>
parents: 58
diff changeset
   320
  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
   321
 
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   322
  \begin{exercise}\label{ex:scancmts}
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   323
  Write a parser that parses an input string so that any comment enclosed
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   324
  inside @{text "(*\<dots>*)"} is replaced by a the same comment but enclosed inside
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   325
  @{text "(**\<dots>**)"} in the output string. To enclose a string, you can use the
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   326
  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   327
  "s1^s^s2" for s1 s2 s}.
56
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   328
  \end{exercise}
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   329
126646f2aa88 added a para on Scan.unless and an exercise about scanning comments
Christian Urban <urbanc@in.tum.de>
parents: 54
diff changeset
   330
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   331
  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
   332
  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
   333
  untouched. For example
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   334
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   335
@{ML_response [display]
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   336
"Scan.lift (($$ \"h\") -- ($$ \"e\")) (1,(explode \"hello\"))"
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   337
"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   338
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
   339
  (FIXME: In which situations is this useful? Give examples.) 
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   340
*}
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   341
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   342
section {* Parsing Theory Syntax *}
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   343
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   344
text {*
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   345
  Most of the time, however, Isabelle developers have to deal with parsing tokens, not strings.
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   346
  This is because the parsers for the theory syntax, as well as the parsers for the 
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
   347
  argument syntax of proof methods and attributes use the type 
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
   348
  @{ML_type OuterLex.token} (which is identical to the type @{ML_type OuterParse.token}).
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   349
  There are also parsers for ML-expressions and ML-files.
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   350
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   351
  \begin{readmore}
40
35e1dff0d9bb more on the parsing section
Christian Urban <urbanc@in.tum.de>
parents: 39
diff changeset
   352
  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
   353
  @{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
   354
  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
   355
  \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
   356
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
   357
  The structure @{ML_struct OuterLex} defines several kinds of token (for example 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   358
  @{ML "Ident" in OuterLex} for identifiers, @{ML "Keyword" in OuterLex} for keywords and
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   359
  @{ML "Command" in OuterLex} for commands). Some token parsers take into account the 
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   360
  kind of token.
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   361
*}  
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   362
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   363
text {*
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   364
  For the examples below, we can generate a token list out of a string using
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   365
  the function @{ML "OuterSyntax.scan"}, which we give below @{ML
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   366
  "Position.none"} as argument since, at the moment, we are not interested in
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   367
  generating precise error messages. The following
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   368
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
   369
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   370
@{ML_response_fake [display] "OuterSyntax.scan Position.none \"hello world\"" 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   371
"[Token (\<dots>,(Ident, \"hello\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   372
 Token (\<dots>,(Space, \" \"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   373
 Token (\<dots>,(Ident, \"world\"),\<dots>)]"}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   374
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   375
  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
   376
  @{text [quotes] "hello"} and @{text [quotes] "world"} do not match any
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   377
  other syntactic category.\footnote{Note that because of a possible a bug in
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   378
  the PolyML runtime system the result is printed as @{text "?"}, instead of
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   379
  the token.} The second indicates a space.
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   380
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   381
  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
   382
  to have already been filtered out.  So from now on we are going to use the 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   383
  functions @{ML filter} and @{ML OuterLex.is_proper} do this. For example
Christian Urban <urbanc@in.tum.de>
parents: 49
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
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   386
@{ML_response_fake [display]
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   387
"let
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   388
   val input = OuterSyntax.scan Position.none \"hello world\"
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   389
in
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   390
   filter OuterLex.is_proper input
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   391
end" 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   392
"[Token (\<dots>,(Ident, \"hello\"), \<dots>), Token (\<dots>,(Ident, \"world\"), \<dots>)]"}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   393
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   394
  For convenience we define the function
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   395
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   396
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   397
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   398
ML {* 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   399
fun filtered_input str = 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   400
       filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   401
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   402
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   403
text {*
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   404
48
609f9ef73494 fixed FIXME's in fake responses
Christian Urban <urbanc@in.tum.de>
parents: 47
diff changeset
   405
  If we 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
   406
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   407
@{ML_response_fake [display] 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   408
"filtered_input \"inductive | for\"" 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   409
"[Token (\<dots>,(Command, \"inductive\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   410
 Token (\<dots>,(Keyword, \"|\"),\<dots>), 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   411
 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
   412
52
Christian Urban <urbanc@in.tum.de>
parents: 50
diff changeset
   413
  we obtain a list consisting of only a command and two keyword tokens.
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   414
  If you want to see which keywords and commands are currently known, type in
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   415
  the following (you might have to adjust the @{ML print_depth} in order to
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   416
  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
   417
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   418
@{ML_response_fake [display] 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   419
"let 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   420
  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
   421
in 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   422
  (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
   423
end" 
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   424
"([\"}\",\"{\",\<dots>],[\"\<rightleftharpoons>\",\"\<leftharpoondown>\",\<dots>])"}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   425
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
   426
  Now the parser @{ML "OuterParse.$$$"} parses a single keyword. For example
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   427
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
   428
@{ML_response [display]
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
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   430
  val input1 = filtered_input \"where for\"
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   431
  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
   432
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
   433
  (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
   434
end"
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
"((\"where\",\<dots>),(\"|\",\<dots>))"}
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
   436
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
   437
  Like before, we can sequentially connect parsers with @{ML "(op --)"}. For example 
dee4b3e66dfe added a readme chapter for prospective authors; added commands for referring to the Isar Reference Manual
Christian Urban <urbanc@in.tum.de>
parents: 43
diff changeset
   438
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
   439
@{ML_response [display]
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
   440
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   441
  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
   442
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
   443
  (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
   444
end"
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
   445
"((\"|\",\"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
   446
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   447
  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
   448
  list of items recognised by the parser @{text p}, where the items being parsed
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   449
  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
   450
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
   451
@{ML_response [display]
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 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   453
  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
   454
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
   455
  (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
   456
end" 
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
"([\"in\",\"in\",\"in\"],[\<dots>])"}
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
   458
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   459
  @{ML "OuterParse.enum1"} works similarly, except that the parsed list must
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   460
  be non-empty. Note that we had to add an @{text [quotes] "foo"} at the end
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   461
  of the parsed string, otherwise the parser would have consumed all tokens
58
f3794c231898 fixed typos
Christian Urban <urbanc@in.tum.de>
parents: 56
diff changeset
   462
  and then failed with the exception @{text "MORE"}. Like in the previous
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   463
  section, we can avoid this exception using the wrapper @{ML
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   464
  Scan.finite}. This time, however, we have to use the ``stopper-token'' @{ML
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   465
  OuterLex.stopper}. We can write
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   466
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   467
@{ML_response [display]
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   468
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   469
  val input = filtered_input \"in | in | in\"
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   470
in 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   471
  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
   472
         (OuterParse.enum \"|\" (OuterParse.$$$ \"in\")) input
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   473
end" 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   474
"([\"in\",\"in\",\"in\"],[])"}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   475
54
1783211b3494 tuned; added document antiquotation ML_response_fake_both
Christian Urban <urbanc@in.tum.de>
parents: 53
diff changeset
   476
  The following function will help us later 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
   477
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   478
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   479
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   480
ML {*
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   481
fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   482
*}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   483
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   484
text {*
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   485
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   486
  The function @{ML "OuterParse.!!!"} can be used to force termination of the
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   487
  parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   488
  except that the error message is fixed to be @{text [quotes] "Outer syntax error"}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   489
  with a relatively precise description of the failure. For example:
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   490
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   491
@{ML_response_fake [display]
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   492
"let 
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   493
  val input = filtered_input \"in |\"
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   494
  val parse_bar_then_in = OuterParse.$$$ \"|\" -- OuterParse.$$$ \"in\"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   495
in 
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   496
  parse (OuterParse.!!! parse_bar_then_in) input 
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   497
end"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   498
"Exception ERROR \"Outer syntax error: keyword \"|\" expected, 
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   499
but keyword in was found\" raised"
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   500
}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   501
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   502
  \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
   503
  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
   504
  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
   505
  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
   506
  \end{exercise}
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   507
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   508
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   509
*}
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   510
53
0c3580c831a4 removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
parents: 52
diff changeset
   511
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   512
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   513
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   514
49
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   515
section {* Positional Information *}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   516
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   517
text {*
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   518
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   519
  @{ML OuterParse.position}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   520
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   521
*}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   522
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   523
ML {*
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   524
  OuterParse.position
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   525
*}
a0edabf14457 added more material
Christian Urban <urbanc@in.tum.de>
parents: 48
diff changeset
   526
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
   527
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
   528
section {* Parsing Inner Syntax *}
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   529
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
   530
ML {*
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
   531
let 
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
   532
  val input = OuterSyntax.scan Position.none "0"
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
   533
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
   534
  OuterParse.prop 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
   535
end 
42
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   536
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   537
*}
cd612b489504 tuned mostly antiquotation and text
Christian Urban <urbanc@in.tum.de>
parents: 41
diff changeset
   538
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   539
ML {*
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   540
  OuterParse.opt_target
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   541
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   542
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   543
text {* (FIXME funny output for a proposition) *}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   544
50
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   545
ML {*
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   546
  OuterParse.opt_target --
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   547
  OuterParse.fixes -- 
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   548
  OuterParse.for_fixes --
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   549
  Scan.optional (OuterParse.$$$ "where" |--
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   550
    OuterParse.!!! (OuterParse.enum1 "|" (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   551
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   552
*}
Christian Urban <urbanc@in.tum.de>
parents: 49
diff changeset
   553
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   554
ML {* OuterSyntax.command *}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   555
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   556
section {* New Commands and Creating Keyword Files *}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   557
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   558
text {*
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   559
  Often new commands, for example for providing a new definitional principle,
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   560
  need to be programmed. While this is not difficult to do on the ML-level,
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   561
  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
   562
  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
   563
  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
   564
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   565
  Let us start with a ``silly'' command, below named \isacommand{foo}, which does nothing at all. 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   566
  On the ML-level it can be defined as
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   567
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   568
@{ML [display]
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   569
"let
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   570
  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   571
  val flag = OuterKeyword.thy_decl
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   572
in
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   573
  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   574
end"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   575
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   576
  The function @{ML OuterSyntax.command} expects a name for the command, a
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   577
  short description, a flag (which we will explain it later on more thoroughly) and a
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   578
  parser for a top-level transition function (its purpose will also explained
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   579
  later). 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   580
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   581
  While this is everything we have to do on the ML-level, we need 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   582
  now a keyword file that can be loaded by ProofGeneral. This is to enable ProofGeneral 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   583
  to recognise  \isacommand{foo} as a command. Such a keyword file can be generated with 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   584
  the command-line
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   585
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   586
  @{text [display] "$ isabelle keywords -k foo <some-log-files>"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   587
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   588
  The option @{text "-k foo"} indicates which postfix the keyword file will obtain. In
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   589
  the case above the generated file will be named @{text "isar-keywords-foo.el"}. This command
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   590
  requires log files to be present (in order to extract the keywords from them). 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   591
  To generate these log files, we first package the code above into a separate theory file 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   592
  named @{text "Command.thy"}, say---see Figure~\ref{fig:commandtheory} for the complete code. 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   593
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   594
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   595
  \begin{figure}[t]
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   596
  \begin{boxedminipage}{\textwidth}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   597
  \isacommand{theory}~@{text Command}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   598
  \isacommand{imports}~@{text Main}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   599
  \isacommand{begin}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   600
  \isacommand{ML}~\isa{\isacharverbatimopen}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   601
  @{ML
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   602
"let
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   603
  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   604
  val flag = OuterKeyword.thy_decl
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   605
in
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   606
  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   607
end"}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   608
  \isa{\isacharverbatimclose}\\
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   609
  \isacommand{end}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   610
  \end{boxedminipage}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   611
  \caption{The file @{text "Command.thy"} is necessary for generating a log 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   612
  file. This log file enables Isabelle to generate a keyword file containing 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   613
  the command \isacommand{foo}.\label{fig:commandtheory}}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   614
  \end{figure}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   615
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   616
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   617
  For 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   618
  our purposes it is sufficient to use the log files for the theories @{text "Pure"},
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   619
  @{text "HOL"} and @{text "Pure-ProofGeneral"}, as well as the theory @{text "Command.thy"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   620
  containing the new command. @{text Pure} and @{text HOL} are usually compiled during the 
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   621
  installation of Isabelle. So log files for them are already available. If not, then they 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   622
  can be conveniently compiled using build-script from the distribution
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   623
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   624
  @{text [display] 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   625
"$ ./build -m \"Pure\"
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   626
$ ./build -m \"HOL\""}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   627
  
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   628
  The @{text "Pure-ProofGeneral"} theory needs to be compiled with
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   629
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   630
  @{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
   631
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   632
  For the theory @{text "Command.thy"}, we first create a ``managed'' subdirectory 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   633
  with
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   634
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   635
  @{text [display] "$ isabelle mkdir FooCommand"}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   636
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   637
  This creates a directory containing the files 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   638
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   639
  @{text [display] 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   640
"./IsaMakefile
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   641
./FooCommand/ROOT.ML
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   642
./FooCommand/document
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   643
./FooCommand/document/root.tex"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   644
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   645
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   646
  We need to copy the file @{text "Command.thy"} into the directory @{text "FooCommand"}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   647
  and add the line 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   648
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   649
  @{text [display] "use_thy \"Command\";"} 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   650
  
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   651
  to the file @{text "./FooCommand/ROOT.ML"}. Now we can 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
   652
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   653
  @{text [display] "$ isabelle make"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   654
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   655
  We created now the necessary log files. They are typically stored 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   656
  in the directory 
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   657
  
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   658
  @{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
   659
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   660
  or something similar depending on your Isabelle distribution and architecture. 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   661
  Let us assume the name of this directory is stored in the shell variable 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   662
  @{text "ISABELLE_LOGS"}. One way to assign this shell variable is by typing
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   663
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   664
  @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"}
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   665
 
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   666
  In this directory are the files
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   667
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   668
  @{text [display] 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   669
"Pure.gz
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   670
HOL.gz
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   671
Pure-ProofGeneral.gz
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   672
HOL-FooCommand.gz"} 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   673
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   674
  We can now create the keyword file with
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   675
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   676
@{text [display]
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   677
"$ isabelle keywords -k foo 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   678
       `$ISABELLE_LOGS/{Pure.gz,HOL.gz,Pure-ProofGeneral,HOL-FooCommand.gz}`"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   679
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   680
  The result is the file @{text "isar-keywords-foo.el"}, which needs to be 
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   681
  copied to the directory @{text "~/.isabelle/etc"}. To make Isabelle use
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   682
  this keyword file, we need to start it with the option @{text "-k foo"}, i.e.
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   683
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   684
  @{text [display] "isabelle -k foo <a-theory-file>"}
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   685
66
Christian Urban <urbanc@in.tum.de>
parents: 65
diff changeset
   686
  If we now run the original code
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   687
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   688
  @{ML [display]
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   689
"let
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   690
  val do_nothing = Scan.succeed (Toplevel.theory (fn x => x))
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   691
  val flag = OuterKeyword.thy_decl
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   692
in
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   693
  OuterSyntax.command \"foo\" \"description of foo\" flag do_nothing
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   694
end"}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   695
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   696
  then we can finally make use of \isacommand{foo}! Similarly
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   697
  with any other command you want to implement. 
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   698
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   699
  In the example above, we built the theories on top of the HOL-logic. If you
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   700
  target other logics, such as Nominal or ZF, then you need to change the
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   701
  log files appropriately.
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   702
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   703
  (FIXME Explain @{text "OuterKeyword.thy_decl"} and parser)
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   704
  
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   705
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   706
*}
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
   707
41
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   708
b11653b11bd3 further progress on the parsing section and tuning on the antiqu's
Christian Urban <urbanc@in.tum.de>
parents: 40
diff changeset
   709
38
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   710
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   711
chapter {* Parsing *}
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   712
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   713
text {*
e21b2f888fa2 added a preliminary section about parsing
Christian Urban <urbanc@in.tum.de>
parents: 16
diff changeset
   714
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   715
  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
   716
  including:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   717
  \begin{itemize}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   718
  \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
   719
  or simplified versions of such code
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   720
  \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
   721
  (or specialisations of their types)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   722
  \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
   723
  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
   724
  \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
   725
  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
   726
  \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
   727
  \end{itemize}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   728
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   729
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   730
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   731
section {* Parsing Isar input *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   732
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   733
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   734
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   735
  The typical parsing function has the type
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   736
  \texttt{'src -> 'res * 'src}, with input  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   737
  of type \texttt{'src}, returning a result 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   738
  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
   739
  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
   740
  (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
   741
  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
   742
  value of type \texttt{'res}). 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   743
  An exception is raised if an appropriate value 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   744
  cannot be produced from the input.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   745
  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
   746
  for the failure of a parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   747
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   748
  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
   749
  which is of type 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   750
  \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
   751
  (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
   752
  However, much of the discussion at 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   753
  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
   754
  is relevant.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   755
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   756
  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
   757
  as follows:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   758
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   759
  open StringCvt ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   760
  type ('res, 'src) ex_reader = 'src -> 'res * 'src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   761
  (* ex_reader : ('res, 'src) reader -> ('res, 'src) ex_reader *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   762
  fun ex_reader rdr src = Option.valOf (rdr src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   763
  (* reader : ('res, 'src) ex_reader -> ('res, 'src) reader *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   764
  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
   765
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   766
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   767
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   768
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   769
section{* The \texttt{Scan} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   770
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   771
text {* 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   772
  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
   773
  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
   774
  of the type \texttt{'src -> 'res * 'src}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   775
  Three exceptions are used:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   776
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   777
  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
   778
  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
   779
  exception ABORT of string;        (*dead end*)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   780
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   781
  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
   782
  symbols) are declared as infix.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   783
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   784
  Some functions from that structure are
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   785
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   786
  |-- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   787
  'src -> 'res2 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   788
  --| : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   789
  'src -> 'res1 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   790
  -- : ('src -> 'res1 * 'src') * ('src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   791
  'src -> ('res1 * 'res2) * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   792
  ^^ : ('src -> string * 'src') * ('src' -> string * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   793
  'src -> string * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   794
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   795
  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
   796
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   797
  \texttt{|--} and \texttt{--|} 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   798
  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
   799
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   800
  \texttt{--} returns both.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   801
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   802
  \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
   803
  (which must be strings).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   804
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   805
  Note how, although the types 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   806
  \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
   807
  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
   808
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   809
  :-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   810
  'src -> ('res1 * 'res2) * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   811
  :|-- : ('src -> 'res1 * 'src') * ('res1 -> 'src' -> 'res2 * 'src'') ->
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   812
  'src -> 'res2 * 'src''
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   813
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   814
  These are similar to \texttt{|--} and \texttt{--|},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   815
  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
   816
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   817
  >> : ('src -> 'res1 * 'src') * ('res1 -> 'res2) -> 'src -> 'res2 * 'src'
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   818
  || : ('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
   819
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   820
  \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
   821
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   822
  \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
   823
  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
   824
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   825
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   826
  succeed : 'res -> ('src -> 'res * 'src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   827
  fail : ('src -> 'res_src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   828
  !! : ('src * string option -> string) -> 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   829
  ('src -> 'res_src) -> ('src -> 'res_src) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   830
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   831
  \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
   832
  \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
   833
  \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
   834
  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
   835
  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
   836
  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
   837
  it won't recover by trying \texttt{parse2}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   838
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   839
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   840
  one : ('si -> bool) -> ('si list -> 'si * 'si list) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   841
  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
   842
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   843
  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
   844
  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
   845
  On other failures they raise \texttt{FAIL NONE} 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   846
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   847
  \texttt{one p} takes the first
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   848
  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
   849
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   850
  \texttt{some f} takes the first
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   851
  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
   852
  \texttt{NONE}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   853
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   854
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   855
  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
   856
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   857
  \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
   858
  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
   859
  it fails, raising \texttt{MORE NONE}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   860
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   861
  \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
   862
  does not satisfy \texttt{p}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   863
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   864
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   865
  option : ('src -> 'res * 'src) -> ('src -> 'res option * 'src)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   866
  optional : ('src -> 'res * 'src) -> 'res -> ('src -> 'res * 'src)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   867
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   868
  \texttt{option}: 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   869
  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
   870
  or raises \texttt{FAIL \_},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   871
  \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
   872
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   873
  \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
   874
  \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
   875
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   876
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   877
  repeat : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   878
  repeat1 : ('src -> 'res * 'src) -> 'src -> 'res list * 'src
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   879
  bulk : ('src -> 'res * 'src) -> 'src -> 'res list * 'src 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   880
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   881
  \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
   882
  \texttt{f} fails with \texttt{FAIL \_}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   883
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   884
  \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
   885
  successful parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   886
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   887
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   888
  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
   889
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   890
  \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
   891
  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
   892
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   893
  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
   894
  HOW DO THEY WORK ?? TO BE COMPLETED
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   895
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   896
  dest_lexicon: lexicon -> string list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   897
  make_lexicon: string list list -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   898
  empty_lexicon: lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   899
  extend_lexicon: string list list -> lexicon -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   900
  merge_lexicons: lexicon -> lexicon -> lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   901
  is_literal: lexicon -> string list -> bool ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   902
  literal: lexicon -> string list -> string list * string list ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   903
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   904
  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
   905
  by:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   906
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   907
  val (command_lexicon, keyword_lexicon) = OuterSyntax.get_lexicons () ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   908
  val commands = Scan.dest_lexicon command_lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   909
  val keywords = Scan.dest_lexicon keyword_lexicon ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   910
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   911
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   912
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   913
section{* The \texttt{OuterLex} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   914
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   915
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   916
  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
   917
  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
   918
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   919
  structure T = OuterLex;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   920
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   921
  This structure defines the type \texttt{token}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   922
  (The types
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   923
  \texttt{OuterLex.token},
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   924
  \texttt{OuterParse.token} and
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   925
  \texttt{SpecParse.token} are all the same).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   926
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   927
  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
   928
  functions is \texttt{token list}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   929
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   930
  The datatype definition (which is not published in the signature) is
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   931
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   932
  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
   933
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   934
  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
   935
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   936
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   937
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   938
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   939
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   940
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   941
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   942
  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
   943
   "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
   944
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   945
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   946
ML {*
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   947
  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
   948
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   949
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   950
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   951
  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
   952
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   953
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   954
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   955
  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
   956
*}  
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   957
47
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   958
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   959
  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
   960
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   961
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   962
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   963
  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
   964
*}
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   965
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   966
ML {*
4daf913fdbe1 hakked latex so that it does not display ML {* *}; general tuning
Christian Urban <urbanc@in.tum.de>
parents: 44
diff changeset
   967
  OuterLex.stopper
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   968
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   969
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   970
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   971
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   972
  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
   973
  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
   974
  comments to have been filtered out.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   975
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   976
  There is a special end-of-file token:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   977
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   978
  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
   979
  (* end of file token *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   980
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   981
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   982
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   983
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   984
section {* The \texttt{OuterParse} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   985
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   986
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   987
  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
   988
  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
   989
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   990
  structure P = OuterParse;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   991
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   992
  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
   993
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
   994
  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
   995
  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
   996
  \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
   997
  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
   998
  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
   999
  (eg, \texttt{name, xname, text, typ}).
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1000
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1001
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1002
  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
  1003
  $$$ : string -> string tlp
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1004
  nat : int tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1005
  maybe : 'a tlp -> 'a option tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1006
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1007
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1008
  \texttt{\$\$\$ s} returns the first token,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1009
  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
  1010
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1011
  \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
  1012
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1013
  \texttt{maybe}: if \texttt{p} returns \texttt{r}, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1014
  then \texttt{maybe p} returns \texttt{SOME r} ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1015
  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
  1016
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1017
  A few examples:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1018
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1019
  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
  1020
  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
  1021
  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
  1022
  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
  1023
  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
  1024
  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
  1025
  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
  1026
  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
  1027
  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
  1028
  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
  1029
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1030
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1031
  The following code helps run examples:
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1032
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1033
  fun parse_str tlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1034
  let val toks : token list = OuterSyntax.scan str ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1035
  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
  1036
  val (res, rem_toks) = tlp proper_toks ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1037
  val rem_str = String.concat
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1038
  (Library.separate " " (List.map T.unparse rem_toks)) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1039
  in (res, rem_str) end ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1040
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1041
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1042
  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
  1043
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1044
  val type_args =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1045
  type_ident >> Library.single ||
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1046
  $$$ "(" |-- !!! (list1 type_ident --| $$$ ")") ||
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1047
  Scan.succeed [];
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1048
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1049
  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
  1050
  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
  1051
  list.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1052
  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
  1053
  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
  1054
  and then a ")" which is also ignored.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1055
  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
  1056
  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
  1057
  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
  1058
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1059
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1060
  fun triple2 (x, (y, z)) = (x, y, z);
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1061
  val arity = xname -- ($$$ "::" |-- !!! (
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1062
  Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) []
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1063
  -- sort)) >> triple2;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1064
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1065
  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
  1066
  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
  1067
  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
  1068
  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
  1069
  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
  1070
  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
  1071
  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
  1072
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1073
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1074
  parse_str P.type_args "('a, 'b) ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1075
  parse_str P.type_args "'a ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1076
  parse_str P.type_args "ntyp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1077
  parse_str P.arity "ty :: tycl" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1078
  parse_str P.arity "ty :: (tycl1, tycl2) tycl" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1079
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1080
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1081
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1082
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1083
section {* The \texttt{SpecParse} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1084
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1085
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1086
  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
  1087
  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
  1088
  For example, 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1089
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1090
  open SpecParse ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1091
  attrib : Attrib.src tok_rdr ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1092
  attribs : Attrib.src list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1093
  opt_attribs : Attrib.src list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1094
  xthm : (thmref * Attrib.src list) tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1095
  xthms1 : (thmref * Attrib.src list) list tok_rdr ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1096
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1097
  parse_str attrib "simp" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1098
  parse_str opt_attribs "hello" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1099
  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
  1100
  map Args.dest_src ass ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1101
  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
  1102
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1103
  parse_str xthm "mythm [attr]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1104
  parse_str xthms1 "thm1 [attr] thms2" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1105
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1106
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1107
  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
  1108
  structure, described below.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1109
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1110
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1111
section{* The \texttt{Args} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1112
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1113
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1114
  The source file is \texttt{src/Pure/Isar/args.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1115
  The primary type of this structure is the \texttt{src} datatype;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1116
  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
  1117
  \texttt{Args.src} and \texttt{Args.dest\_src}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1118
  are in fact the constructor and destructor functions.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1119
  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
  1120
  are in fact \texttt{Args.src}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1121
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1122
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1123
  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
  1124
  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
  1125
  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
  1126
  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
  1127
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1128
  val thy = ML_Context.the_context () ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1129
  val ctxt = ProofContext.init thy ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1130
  map (pr_src ctxt) ass ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1131
  \end{verbatim}
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
  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
  1134
  ``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
  1135
  input.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1136
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1137
  (* how an Args.src is parsed *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1138
  P.position : 'a tlp -> ('a * Position.T) tlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1139
  P.arguments : Args.T list tlp ;
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
  val parse_src : Args.src tlp =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1142
  P.position (P.xname -- P.arguments) >> Args.src ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1143
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1144
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1145
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1146
  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
  1147
  map Args.string_of args ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1148
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1149
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1150
  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
  1151
  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
  1152
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1153
  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
  1154
  open Args ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1155
  nat : int atlp ; (* also Args.int *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1156
  thm_sel : PureThy.interval list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1157
  list : 'a atlp -> 'a list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1158
  attribs : (string -> string) -> Args.src list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1159
  opt_attribs : (string -> string) -> Args.src list atlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1160
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1161
  (* parse_atl_str : 'a atlp -> (string -> 'a * string) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1162
  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
  1163
  fun parse_atl_str atlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1164
  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
  1165
  val (res, rem_ats) = atlp ats ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1166
  in (res, String.concat (Library.separate " "
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1167
  (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
  1168
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1169
  parse_atl_str Args.int "-1-," ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1170
  parse_atl_str (Scan.option Args.int) "x1-," ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1171
  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
  1172
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1173
  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
  1174
  "[THEN trans [THEN sym], simp, OF sym]" ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1175
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1176
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1177
  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
  1178
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1179
  \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
  1180
  and also refer to a generic context.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1181
  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
  1182
  (as does \texttt{Attrib} - RETHINK THIS)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1183
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1184
  (\texttt{Args.syntax} shown below has type specialised)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1185
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1186
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1187
  type ('res, 'src) parse_fn = 'src -> 'res * 'src ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1188
  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
  1189
  Scan.lift : 'a atlp -> 'a cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1190
  term : term cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1191
  typ : typ cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1192
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1193
  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
  1194
  Attrib.thm : thm cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1195
  Attrib.thms : thm list cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1196
  Attrib.multi_thm : thm list cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1197
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1198
  (* parse_cgatl_str : 'a cgatlp -> (string -> 'a * string) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1199
  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
  1200
  fun parse_cgatl_str cgatlp str = 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1201
  let 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1202
    (* use the current generic context *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1203
    val generic = Context.Theory thy ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1204
    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
  1205
    (* ignore any change to the generic context *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1206
    val (res, (_, rem_ats)) = cgatlp (generic, ats) ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1207
  in (res, String.concat (Library.separate " "
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1208
      (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
  1209
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1210
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1211
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1212
section{* Attributes, and the \texttt{Attrib} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1213
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1214
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1215
  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
  1216
  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
  1217
  \texttt{src/Pure/Isar/attrib.ML}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1218
  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
  1219
  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
  1220
  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
  1221
  theory). 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1222
  The functions \texttt{Thm.rule\_attribute} and
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1223
  \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
  1224
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1225
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1226
  type attribute = Context.generic * thm -> Context.generic * thm;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1227
  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
  1228
  Thm.rule_attribute  : (Context.generic -> thm -> thm) -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1229
  Thm.declaration_attribute : (thm -> Context.generic trf) -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1230
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1231
  Attrib.print_attributes : theory -> unit ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1232
  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
  1233
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1234
  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
  1235
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1236
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1237
  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
  1238
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1239
  Attrib.add_attributes : 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1240
  (bstring * (src -> attribute) * string) list -> theory trf ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1241
  (*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1242
  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
  1243
  *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1244
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1245
  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
  1246
  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
  1247
  (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
  1248
  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
  1249
  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
  1250
  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
  1251
  \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
  1252
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1253
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1254
  FullAttrib.THEN_att : src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1255
  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
  1256
  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
  1257
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1258
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1259
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1260
  Attrib.syntax : attribute cgatlp -> src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1261
  Attrib.no_args : attribute -> src -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1262
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1263
  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
  1264
  the generic context \texttt{gc} is used 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1265
  (and potentially changed to \texttt{gc'})
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1266
  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
  1267
  then be applied to \texttt{(gc', th)}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1268
  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
  1269
  which must all be consumed by the parse.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1270
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1271
  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
  1272
  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
  1273
  \texttt{src} must be empty.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1274
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1275
  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
  1276
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1277
  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
  1278
  rot_att_n : int -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1279
  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
  1280
  val rotated_att : src -> attribute =
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1281
  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
  1282
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1283
  val THEN_arg : int cgatlp = Scan.lift 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1284
  (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
  1285
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1286
  Attrib.thm : thm cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1287
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1288
  THEN_arg -- Attrib.thm : (int * thm) cgatlp ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1289
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1290
  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
  1291
  THEN_att_n : int * thm -> attribute ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1292
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1293
  val THEN_att : src -> attribute = Attrib.syntax
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1294
  (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
  1295
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1296
  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
  1297
  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
  1298
  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
  1299
  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
  1300
  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
  1301
  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
  1302
  parsed by \texttt{Attrib.thm}.  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1303
  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
  1304
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1305
*}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1306
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1307
section{* Methods, and the \texttt{Method} structure *}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1308
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1309
text {*
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1310
  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
  1311
  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
  1312
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1313
  (* datatype method = Meth of thm list -> cases_tactic; *)
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1314
  RuleCases.NO_CASES : tactic -> cases_tactic ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1315
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1316
  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
  1317
  \texttt{Meth}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1318
  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
  1319
  \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
  1320
  \texttt{cases\_tactic} without any further case information.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1321
  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
  1322
  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
  1323
  \emph{facts} in the proof.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1324
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1325
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1326
  RAW_METHOD : (thm list -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1327
  METHOD : (thm list -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1328
  
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1329
  SIMPLE_METHOD : tactic -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1330
  SIMPLE_METHOD' : (int -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1331
  SIMPLE_METHOD'' : ((int -> tactic) -> tactic) -> (int -> tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1332
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1333
  RAW_METHOD_CASES : (thm list -> cases_tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1334
  METHOD_CASES : (thm list -> cases_tactic) -> method ;
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1335
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1336
  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
  1337
  the tactic to the current goal state.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1338
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1339
  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
  1340
  \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
  1341
  goal state.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1342
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1343
  \texttt{METHOD} is similar but also first applies
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1344
  \texttt{Goal.conjunction\_tac} to all subgoals.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1345
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1346
  \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
  1347
  applies \texttt{tacf}.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1348
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1349
  \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
  1350
  applies \texttt{tacf} to subgoal 1.
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1351
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1352
  \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
  1353
  \texttt{quant}, which may be, for example,
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1354
  \texttt{ALLGOALS} (all subgoals),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1355
  \texttt{TRYALL} (try all subgoals, failure is OK),
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1356
  \texttt{FIRSTGOAL} (try subgoals until it succeeds once), 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1357
  \texttt{(fn tacf => tacf 4)} (subgoal 4), etc
16
5045dec52d2b polished
Christian Urban <urbanc@in.tum.de>
parents: 4
diff changeset
  1358
  (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
  1359
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1360
  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
  1361
  \begin{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1362
  Method.add_method : 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1363
  (bstring * (src -> Proof.context -> method) * string) -> theory trf ; 
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1364
  ( *
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1365
  * )
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1366
  \end{verbatim}
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1367
  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
  1368
  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
  1369
  (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
  1370
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1371
  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
  1372
  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
  1373
  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
  1374
  \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
  1375
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1376
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1377
*}
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
65
c8e9a4f97916 tuned and added a section about creating keyword files
Christian Urban <urbanc@in.tum.de>
parents: 60
diff changeset
  1380
4
2a69b119cdee added verbatim the notes by Jeremy
Christian Urban <urbanc@in.tum.de>
parents:
diff changeset
  1381
end