526 |
526 |
527 section {* Parsing Specifications\label{sec:parsingspecs} *} |
527 section {* Parsing Specifications\label{sec:parsingspecs} *} |
528 |
528 |
529 text {* |
529 text {* |
530 There are a number of special purpose parsers that help with parsing |
530 There are a number of special purpose parsers that help with parsing |
531 specifications for functions, inductive definitions and so on. In |
531 specifications of functions, inductive definitions and so on. In |
532 Capter~\ref{chp:package}, for example, we will need to parse specifications |
532 Capter~\ref{chp:package}, for example, we will need to parse specifications |
533 for inductive predicates of the form: |
533 for inductive predicates of the form: |
534 *} |
534 *} |
535 |
535 |
536 simple_inductive |
536 simple_inductive |
553 ML %linenosgray{*val spec_parser = |
553 ML %linenosgray{*val spec_parser = |
554 OuterParse.opt_target -- |
554 OuterParse.opt_target -- |
555 OuterParse.fixes -- |
555 OuterParse.fixes -- |
556 OuterParse.for_fixes -- |
556 OuterParse.for_fixes -- |
557 Scan.optional |
557 Scan.optional |
558 (OuterParse.$$$ "where" |-- |
558 (OuterParse.$$$ "where" |-- |
559 OuterParse.!!! |
559 OuterParse.!!! |
560 (OuterParse.enum1 "|" |
560 (OuterParse.enum1 "|" |
561 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
561 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
562 |
562 |
563 text {* |
563 text {* |
564 To see what it returns, let us parse the string corresponding to the |
564 Note that the parser does not parse the ketword \simpleinductive. This |
|
565 will be done by the infrastructure that will eventually call this parser. |
|
566 To see what the parser returns, let us parse the string corresponding to the |
565 definition of @{term even} and @{term odd}: |
567 definition of @{term even} and @{term odd}: |
566 |
568 |
567 @{ML_response [display,gray] |
569 @{ML_response [display,gray] |
568 "let |
570 "let |
569 val input = filtered_input |
571 val input = filtered_input |
579 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
581 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
580 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
582 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
581 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
583 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
582 |
584 |
583 As can be seen, the result is a ``nested'' four-tuple consisting of an |
585 As can be seen, the result is a ``nested'' four-tuple consisting of an |
584 optional locale; a list of variables with optional type-annotation and optional |
586 optional locale; a list of variables with optional type-annotation and |
585 syntax-annotation; a list of for-fixes (fixed variables); and a list of rules |
587 syntax-annotation; a list of for-fixes (fixed variables); and a list of rules |
586 where each rule has optionally a name and an attribute. |
588 where each rule has optionally a name and an attribute. |
587 |
589 |
588 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target |
590 In Line 2 of the parser, the function @{ML OuterParse.opt_target} reads a target |
589 in order to indicate a locale in which the specification is made. For example |
591 in order to indicate a locale in which the specification is made. For example |
590 |
592 |
591 @{ML_response [display,gray] |
593 @{ML_response [display,gray] |
592 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"} |
594 "parse OuterParse.opt_target (filtered_input \"(in test)\")" "(SOME \"test\",[])"} |
593 |
595 |
594 The function @{ML OuterParse.opt_target} returns @{ML NONE}, if no target is given. |
596 returns the locale @{text [quotes] "test"}; if no target is given' like in the |
|
597 casde of @{text "even"} and @{text "odd"}, the function returns @{ML NONE}. |
595 |
598 |
596 The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated |
599 The function @{ML OuterParse.fixes} in Line 3 reads an \isacommand{and}-separated |
597 list of variables that can include type annotations and syntax translations. |
600 list of variables that can include optional type annotations and syntax translations. |
598 For example:\footnote{Note that in the code we need to write |
601 For example:\footnote{Note that in the code we need to write |
599 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes |
602 @{text "\\\"int \<Rightarrow> bool\\\""} in order to properly escape the double quotes |
600 in the compound type.} |
603 in the compound type.} |
601 |
604 |
602 @{ML_response [display,gray] |
605 @{ML_response [display,gray] |
611 (blonk, NONE, NoSyn)],[])"} |
614 (blonk, NONE, NoSyn)],[])"} |
612 *} |
615 *} |
613 |
616 |
614 text {* |
617 text {* |
615 Whenever types are given, they are stored in the @{ML SOME}s. Since types |
618 Whenever types are given, they are stored in the @{ML SOME}s. Since types |
616 are part of the inner syntax they are strings with some printing directives. |
619 are part of the inner syntax they are strings with some printing directives |
|
620 (see previous section). |
617 If a syntax translation is present for a variable, then it is |
621 If a syntax translation is present for a variable, then it is |
618 stored in the @{ML Mixfix} datastructure; no syntax translation is |
622 stored in the @{ML Mixfix} datastructure; no syntax translation is |
619 indicated by @{ML NoSyn}. |
623 indicated by @{ML NoSyn}. |
620 |
624 |
621 \begin{readmore} |
625 \begin{readmore} |
625 Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the |
629 Similarly, the function @{ML OuterParse.for_fixes} in Line 4: it reads the |
626 same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, |
630 same \isacommand{and}-separated list of variables as @{ML "fixes" in OuterParse}, |
627 but requires that this list is prefixed by the keyword \isacommand{for}. |
631 but requires that this list is prefixed by the keyword \isacommand{for}. |
628 |
632 |
629 @{ML_response [display,gray] |
633 @{ML_response [display,gray] |
630 "parse OuterParse.for_fixes (filtered_input \"for foo and bar\")" |
634 "parse OuterParse.for_fixes (filtered_input \"for foo and bar and blink\")" |
631 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn)],[])"} |
635 "([(foo, NONE, NoSyn), (bar, NONE, NoSyn), (blink, NONE, NoSyn)],[])"} |
632 |
636 |
633 Lines 5 to 9 include the parser for a list of introduction rules, that is propositions |
637 Lines 5 to 9 implement the parser for a list of introduction rules, that is propositions |
634 with theorem annotations. The introduction rules are propositions parsed |
638 with theorem annotations. The introduction rules are propositions parsed |
635 by @{ML OuterParse.prop}. However, they can include an optional theorem name plus |
639 by @{ML OuterParse.prop}. However, they can include an optional theorem name plus |
636 some attributes. For example |
640 some attributes. For example |
637 |
641 |
638 @{ML_response [display,gray] "let |
642 @{ML_response [display,gray] "let |
640 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input |
644 val ((name, attrib), _) = parse (SpecParse.thm_name \":\") input |
641 in |
645 in |
642 (name, map Args.dest_src attrib) |
646 (name, map Args.dest_src attrib) |
643 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
647 end" "(foo_lemma, [((\"intro\", []), \<dots>), ((\"dest\", [\<dots>]), \<dots>)])"} |
644 |
648 |
|
649 A name of a theorem can be quite complicated, as it can include attrinutes. |
645 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
650 The function @{ML opt_thm_name in SpecParse} is the ``optional'' variant of |
646 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some |
651 @{ML thm_name in SpecParse}. As can be seen each theorem name can contain some |
647 attributes. If you want to print out all currently known attributes a theorem |
652 attributes. If you want to print out all currently known attributes a theorem |
648 can have, you can use the function: |
653 can have, you can use the function: |
649 *} |
654 |
650 |
655 @{ML_response_fake [display,gray] "Attrib.print_attributes @{theory}" |
651 ML{*Attrib.print_attributes @{theory}*} |
656 "COMP: direct composition with rules (no lifting) |
652 |
657 HOL.dest: declaration of Classical destruction rule |
653 text {* |
658 HOL.elim: declaration of Classical elimination rule |
654 For the inductive definitions described above only the attibutes @{text "[intro]"} and |
659 \<dots>"} |
|
660 |
|
661 |
|
662 For the inductive definitions described above only, the attibutes @{text "[intro]"} and |
655 @{text "[simp]"} make sense. |
663 @{text "[simp]"} make sense. |
656 |
664 |
657 \begin{readmore} |
665 \begin{readmore} |
658 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
666 Attributes and arguments are implemented in the files @{ML_file "Pure/Isar/attrib.ML"} |
659 and @{ML_file "Pure/Isar/args.ML"}. |
667 and @{ML_file "Pure/Isar/args.ML"}. |