48 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and |
48 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and |
49 @{term "fresh"}.\label{fig:specs}} |
49 @{term "fresh"}.\label{fig:specs}} |
50 \end{figure} |
50 \end{figure} |
51 *} |
51 *} |
52 |
52 |
53 text {* |
53 text {* |
54 \begin{figure}[p] |
54 To be able to write down the specifications of inductive predicates, we have |
55 \begin{boxedminipage}{\textwidth} |
55 to introduce a new command (see Section~\ref{sec:newcommand}). As the |
56 \begin{isabelle} |
56 keyword for the new command we chose \simpleinductive{}. Examples of |
57 \railnontermfont{\rmfamily\itshape} |
57 specifications from the previous section are shown in |
58 \railterm{simpleinductive,where,for} |
58 Figure~\ref{fig:specs}. The syntax used in these examples more or |
59 \railalias{simpleinductive}{\simpleinductive{}} |
59 less translates directly into the parser: |
60 \railalias{where}{\isacommand{where}} |
|
61 \railalias{for}{\isacommand{for}} |
|
62 \begin{rail} |
|
63 simpleinductive target?\\ fixes |
|
64 (where (thmdecl? prop + '|'))? |
|
65 ; |
|
66 \end{rail} |
|
67 \end{isabelle} |
|
68 \end{boxedminipage} |
|
69 \caption{A railroad diagram describing the syntax of \simpleinductive{}. |
|
70 The \emph{target} indicates an optional locale; the \emph{fixes} are an |
|
71 \isacommand{and}-separated list of names for the inductive predicates (they |
|
72 can also contain typing- and syntax annotations); \emph{prop} stands for a |
|
73 introduction rule with an optional theorem declaration (\emph{thmdecl}). |
|
74 \label{fig:railroad}} |
|
75 \end{figure} |
|
76 *} |
|
77 |
60 |
78 text {* |
|
79 To be able to write down the specifications or inductive predicates, we have |
|
80 to introduce |
|
81 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
|
82 new command we chose \simpleinductive{}. Examples of specifications we expect |
|
83 the user gives for the inductive predicates from the previous section are |
|
84 shown in Figure~\ref{fig:specs}. The general syntax we will parse is specified |
|
85 in the railroad diagram shown in Figure~\ref{fig:railroad}. This diagram more |
|
86 or less translates directly into the parser: |
|
87 *} |
61 *} |
88 |
62 |
89 ML{*val spec_parser = |
63 ML{*val spec_parser = |
90 OuterParse.fixes -- |
64 OuterParse.fixes -- |
91 Scan.optional |
65 Scan.optional |
93 OuterParse.!!! |
67 OuterParse.!!! |
94 (OuterParse.enum1 "|" |
68 (OuterParse.enum1 "|" |
95 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
69 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
96 |
70 |
97 text {* |
71 text {* |
98 which we explained in Section~\ref{sec:parsingspecs}. However, if you look |
72 which we explained in Section~\ref{sec:parsingspecs}. There is no code included |
99 closely, there is no code for parsing the target given optionally after the |
73 for parsing the keyword and what is called a \emph{target}. The latter can be given |
100 keyword. This is an ``advanced'' feature which we will inherit for ``free'' |
74 optionally after the keyword. The target is an ``advanced'' feature which we will |
101 from the infrastructure on which we shall build the package. The target |
75 inherit for ``free'' from the infrastructure on which we shall build the package. |
102 stands for a locale and allows us to specify |
76 The target stands for a locale and allows us to specify |
103 *} |
77 *} |
104 |
78 |
105 locale rel = |
79 locale rel = |
106 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
80 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
107 |
81 |
137 val input = filtered_input |
111 val input = filtered_input |
138 (\"even and odd \" ^ |
112 (\"even and odd \" ^ |
139 \"where \" ^ |
113 \"where \" ^ |
140 \" even0[intro]: \\\"even 0\\\" \" ^ |
114 \" even0[intro]: \\\"even 0\\\" \" ^ |
141 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
115 \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ |
142 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\"\") |
116 \"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\" \") |
143 in |
117 in |
144 parse spec_parser input |
118 parse spec_parser input |
145 end" |
119 end" |
146 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
120 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
147 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
121 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
149 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
123 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
150 |
124 |
151 then we get back the specifications of the predicates (with type and syntax annotations), |
125 then we get back the specifications of the predicates (with type and syntax annotations), |
152 and specifications of the introduction rules. This is all the information we |
126 and specifications of the introduction rules. This is all the information we |
153 need for calling the package and setting up the keyword. The latter is |
127 need for calling the package and setting up the keyword. The latter is |
154 done in Lines 5 to 7 in the code below.\footnote{FIXME: Is there a way to state |
128 done in Lines 5 to 7 in the code below. |
155 here @{text "simple_inductive"}?} |
|
156 *} |
129 *} |
157 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
130 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy |
158 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
131 fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) |
159 ML_val %linenosgray{*val specification = |
132 ML_val %linenosgray{*val specification = |
160 spec_parser >> |
133 spec_parser >> |