equal
deleted
inserted
replaced
14 Isabelle uses a rather general and sophisticated algorithm, which |
14 Isabelle uses a rather general and sophisticated algorithm, which |
15 is driven by priority grammars. Parsers for outer syntax are built up by functional |
15 is driven by priority grammars. Parsers for outer syntax are built up by functional |
16 parsing combinators. These combinators are a well-established technique for parsing, |
16 parsing combinators. These combinators are a well-established technique for parsing, |
17 which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}. |
17 which has, for example, been described in Paulson's classic ML-book \cite{paulson-ml2}. |
18 Isabelle developers are usually concerned with writing these outer syntax parsers, |
18 Isabelle developers are usually concerned with writing these outer syntax parsers, |
19 either for new definitional packages or for calling tactics with specific arguments. |
19 either for new definitional packages or for calling methods with specific arguments. |
20 |
20 |
21 \begin{readmore} |
21 \begin{readmore} |
22 The library |
22 The library |
23 for writing parser combinators is split up, roughly, into two parts. |
23 for writing parser combinators is split up, roughly, into two parts. |
24 The first part consists of a collection of generic parser combinators defined |
24 The first part consists of a collection of generic parser combinators defined |
296 first the parser @{text p} and upon successful completion applies the |
296 first the parser @{text p} and upon successful completion applies the |
297 function @{text f} to the result. For example |
297 function @{text f} to the result. For example |
298 |
298 |
299 @{ML_response [display,gray] |
299 @{ML_response [display,gray] |
300 "let |
300 "let |
301 fun double (x,y) = (x ^ x, y ^ y) |
301 fun double (x, y) = (x ^ x, y ^ y) |
302 in |
302 in |
303 (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\") |
303 (($$ \"h\") -- ($$ \"e\") >> double) (explode \"hello\") |
304 end" |
304 end" |
305 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"} |
305 "((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"} |
306 |
306 |
316 "(\"foo bar foo\",[])"} |
316 "(\"foo bar foo\",[])"} |
317 |
317 |
318 where the single-character strings in the parsed output are transformed |
318 where the single-character strings in the parsed output are transformed |
319 back into one string. |
319 back into one string. |
320 |
320 |
|
321 (FIXME: move to an earlier place) |
|
322 |
321 The function @{ML Scan.ahead} parses some input, but leaves the original |
323 The function @{ML Scan.ahead} parses some input, but leaves the original |
322 input unchanged. For example: |
324 input unchanged. For example: |
323 |
325 |
324 @{ML_response [display,gray] |
326 @{ML_response [display,gray] |
325 "Scan.ahead (Scan.this_string \"foo\") (explode \"foo\")" |
327 "Scan.ahead (Scan.this_string \"foo\") (explode \"foo\")" |
490 ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *} |
492 ML{*fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input *} |
491 |
493 |
492 text {* |
494 text {* |
493 |
495 |
494 The function @{ML "OuterParse.!!!"} can be used to force termination of the |
496 The function @{ML "OuterParse.!!!"} can be used to force termination of the |
495 parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section), |
497 parser in case of a dead end, just like @{ML "Scan.!!"} (see previous section). |
496 except that the error message is fixed to be @{text [quotes] "Outer syntax error"} |
498 Except that the error message of @{ML "OuterParse.!!!"} is fixed to be |
|
499 @{text [quotes] "Outer syntax error"} |
497 with a relatively precise description of the failure. For example: |
500 with a relatively precise description of the failure. For example: |
498 |
501 |
499 @{ML_response_fake [display,gray] |
502 @{ML_response_fake [display,gray] |
500 "let |
503 "let |
501 val input = filtered_input \"in |\" |
504 val input = filtered_input \"in |\" |
550 \begin{readmore} |
553 \begin{readmore} |
551 The functions related to positions are implemented in the file |
554 The functions related to positions are implemented in the file |
552 @{ML_file "Pure/General/position.ML"}. |
555 @{ML_file "Pure/General/position.ML"}. |
553 \end{readmore} |
556 \end{readmore} |
554 |
557 |
|
558 *} |
|
559 |
|
560 section {* Context Parser (TBD) *} |
|
561 |
|
562 text {* |
|
563 Used for example in \isacommand{attribute\_setup} and \isacommand{method\_setup}. |
555 *} |
564 *} |
556 |
565 |
557 section {* Parsing Inner Syntax *} |
566 section {* Parsing Inner Syntax *} |
558 |
567 |
559 text {* |
568 text {* |
707 |
716 |
708 \begin{readmore} |
717 \begin{readmore} |
709 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
718 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
710 and @{ML_file "Pure/Isar/args.ML"}. |
719 and @{ML_file "Pure/Isar/args.ML"}. |
711 \end{readmore} |
720 \end{readmore} |
|
721 *} |
|
722 |
|
723 text_raw {* |
|
724 \begin{exercise} |
|
725 If you look closely how @{ML SpecParse.where_alt_specs} is implemented |
|
726 in file @{ML_file "Pure/Isar/spec_parse.ML"} and compare it to our @{ML "spec_parser"}, |
|
727 you can notice an additional ``tail'' (Lines 8 to 10): |
|
728 \begin{isabelle} |
|
729 *} |
|
730 ML %linenosgray{*val spec_parser' = |
|
731 OuterParse.fixes -- |
|
732 Scan.optional |
|
733 (OuterParse.$$$ "where" |-- |
|
734 OuterParse.!!! |
|
735 (OuterParse.enum1 "|" |
|
736 ((SpecParse.opt_thm_name ":" -- OuterParse.prop) --| |
|
737 Scan.option (Scan.ahead (OuterParse.name || |
|
738 OuterParse.$$$ "[") -- |
|
739 OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} |
|
740 text_raw {* |
|
741 \end{isabelle} |
|
742 What is the purpose of this additional ``tail''? |
|
743 \end{exercise} |
712 *} |
744 *} |
713 |
745 |
714 section {* New Commands and Keyword Files\label{sec:newcommand} *} |
746 section {* New Commands and Keyword Files\label{sec:newcommand} *} |
715 |
747 |
716 text {* |
748 text {* |
966 (FIXME What do @{ML "Toplevel.theory"} |
998 (FIXME What do @{ML "Toplevel.theory"} |
967 @{ML "Toplevel.print"} |
999 @{ML "Toplevel.print"} |
968 @{ML Toplevel.local_theory} do?) |
1000 @{ML Toplevel.local_theory} do?) |
969 |
1001 |
970 (FIXME read a name and show how to store theorems) |
1002 (FIXME read a name and show how to store theorems) |
971 |
|
972 *} |
1003 *} |
973 |
1004 |
974 section {* Methods *} |
1005 section {* Methods *} |
975 |
1006 |
976 text {* |
1007 text {* |
980 *} |
1011 *} |
981 |
1012 |
982 print_methods |
1013 print_methods |
983 |
1014 |
984 text {* |
1015 text {* |
985 An example of a very simple method is the following code. |
1016 An example of a very simple method is: |
986 *} |
1017 *} |
987 |
1018 |
988 method_setup %gray foobar_meth = |
1019 method_setup %gray foobar_meth = |
989 {* Scan.succeed |
1020 {* Scan.succeed |
990 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1021 (K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1))) *} |
1004 |
1035 |
1005 \begin{minipage}{\textwidth} |
1036 \begin{minipage}{\textwidth} |
1006 @{subgoals} |
1037 @{subgoals} |
1007 \end{minipage} *} |
1038 \end{minipage} *} |
1008 (*<*)oops(*>*) |
1039 (*<*)oops(*>*) |
|
1040 |
|
1041 |
|
1042 (* |
|
1043 ML {* SIMPLE_METHOD *} |
|
1044 ML {* METHOD *} |
|
1045 ML {* K (SIMPLE_METHOD ((etac @{thm conjE} THEN' rtac @{thm conjI}) 1)) *} |
|
1046 ML {* Scan.succeed *} |
|
1047 *) |
1009 |
1048 |
1010 text {* |
1049 text {* |
1011 (FIXME: explain a version of rule-tac) |
1050 (FIXME: explain a version of rule-tac) |
1012 *} |
1051 *} |
1013 |
1052 |