9 |
9 |
10 Isabelle distinguishes between \emph{outer} and \emph{inner} syntax. |
10 Isabelle distinguishes between \emph{outer} and \emph{inner} syntax. |
11 Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so |
11 Theory commands, such as \isacommand{definition}, \isacommand{inductive} and so |
12 on, belong to the outer syntax, whereas items inside double quotation marks, such |
12 on, belong to the outer syntax, whereas items inside double quotation marks, such |
13 as terms, types and so on, belong to the inner syntax. For parsing inner syntax, |
13 as terms, types and so on, belong to the inner syntax. For parsing inner syntax, |
14 Isabelle uses a rather general and sophisticated algorithm due to Earley, 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 tactics with specific arguments. |
346 |
346 |
347 section {* Parsing Theory Syntax *} |
347 section {* Parsing Theory Syntax *} |
348 |
348 |
349 text {* |
349 text {* |
350 Most of the time, however, Isabelle developers have to deal with parsing |
350 Most of the time, however, Isabelle developers have to deal with parsing |
351 tokens, not strings. These token parsers will have the type: |
351 tokens, not strings. These token parsers have the type: |
352 *} |
352 *} |
353 |
353 |
354 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*} |
354 ML{*type 'a parser = OuterLex.token list -> 'a * OuterLex.token list*} |
355 |
355 |
356 text {* |
356 text {* |
599 |
599 |
600 section {* Parsing Specifications\label{sec:parsingspecs} *} |
600 section {* Parsing Specifications\label{sec:parsingspecs} *} |
601 |
601 |
602 text {* |
602 text {* |
603 There are a number of special purpose parsers that help with parsing |
603 There are a number of special purpose parsers that help with parsing |
604 specifications of functions, inductive definitions and so on. In |
604 specifications of function definitions, inductive predicates and so on. In |
605 Capter~\ref{chp:package}, for example, we will need to parse specifications |
605 Capter~\ref{chp:package}, for example, we will need to parse specifications |
606 for inductive predicates of the form: |
606 for inductive predicates of the form: |
607 *} |
607 *} |
608 |
608 |
609 simple_inductive |
609 simple_inductive |
610 even and odd |
610 even and odd |
611 where |
611 where |
612 even0: "even 0" |
612 even0: "even 0" |
613 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
613 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
614 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
614 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
|
615 |
|
616 text {* and *} |
615 |
617 |
616 simple_inductive |
618 simple_inductive |
617 trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
619 trcl\<iota> for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
618 where |
620 where |
619 base: "trcl\<iota> R x x" |
621 base: "trcl\<iota> R x x" |
690 (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), |
692 (bar, SOME \"\\^E\\^Ftoken\\^Enat\\^E\\^F\\^E\", Mixfix (\"BAR\", [], 100)), |
691 (blonk, NONE, NoSyn)],[])"} |
693 (blonk, NONE, NoSyn)],[])"} |
692 *} |
694 *} |
693 |
695 |
694 text {* |
696 text {* |
695 Whenever types are given, they are stored in the @{ML SOME}s. They types are |
697 Whenever types are given, they are stored in the @{ML SOME}s. The types are |
696 not yet given to the variable: this must be done by type inference later |
698 not yet used to type the variables: this must be done by type-inference later |
697 on. Since types are part of the inner syntax they are strings with some |
699 on. Since types are part of the inner syntax they are strings with some |
698 encoded information (see previous section). If a syntax translation is |
700 encoded information (see previous section). If a syntax translation is |
699 present for a variable, then it is stored in the @{ML Mixfix} datastructure; |
701 present for a variable, then it is stored in the @{ML Mixfix} datastructure; |
700 no syntax translation is indicated by @{ML NoSyn}. |
702 no syntax translation is indicated by @{ML NoSyn}. |
701 |
703 |
851 or something similar depending on your Isabelle distribution and architecture. |
853 or something similar depending on your Isabelle distribution and architecture. |
852 One quick way to assign a shell variable to this directory is by typing |
854 One quick way to assign a shell variable to this directory is by typing |
853 |
855 |
854 @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} |
856 @{text [display] "$ ISABELLE_LOGS=\"$(isabelle getenv -b ISABELLE_OUTPUT)\"/log"} |
855 |
857 |
856 on the Unix prompt. If you now also type @{text "ls $ISABELLE_LOGS"}, then the |
858 on the Unix prompt. If you now type @{text "ls $ISABELLE_LOGS"}, then the |
857 directory should include the files: |
859 directory should include the files: |
858 |
860 |
859 @{text [display] |
861 @{text [display] |
860 "Pure.gz |
862 "Pure.gz |
861 HOL.gz |
863 HOL.gz |