155 \frametitle{Introduction of Isabelle Contexts} |
155 \frametitle{Introduction of Isabelle Contexts} |
156 \begin{itemize} |
156 \begin{itemize} |
157 \item theories too general |
157 \item theories too general |
158 \item not capable of type inference |
158 \item not capable of type inference |
159 \item replace function \texttt{parseNEW} |
159 \item replace function \texttt{parseNEW} |
160 \end{itemize} |
160 \item assumptions \& environment $\rightarrow$ context |
161 \end{frame} |
161 \end{itemize} |
162 |
162 \end{frame} |
163 \begin{frame} |
163 |
164 \frametitle{Introduction of Isabelle Contexts} |
164 \begin{frame} |
|
165 \frametitle{Code Snippets: \texttt{parse}} |
165 \texttt{\tiny{ |
166 \texttt{\tiny{ |
166 \begin{tabbing} |
167 \begin{tabbing} |
167 xx\=xx\=xx\=xx\=\kill |
168 xx\=xx\=xx\=xx\=\kill |
168 fun parse thy str =\\ |
169 fun parse thy str =\\ |
169 \>(let val t = (typ\_a2real o numbers\_to\_string)\\ |
170 \>(let val t = (typ\_a2real o numbers\_to\_string)\\ |
171 \>\>in SOME (cterm\_of thy t) end)\\ |
172 \>\>in SOME (cterm\_of thy t) end)\\ |
172 \>\>\>handle \_ => NONE; |
173 \>\>\>handle \_ => NONE; |
173 \\~\\~\\ |
174 \\~\\~\\ |
174 fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\ |
175 fun parseNEW ctxt str = SOME (Syntax.read\_term ctxt str |> numbers\_to\_string)\\ |
175 \>\>\>handle \_ => NONE; |
176 \>\>\>handle \_ => NONE; |
176 \\~\\~\\ |
177 \end{tabbing} |
|
178 }} |
|
179 \end{frame} |
|
180 |
|
181 |
|
182 \begin{frame} |
|
183 \frametitle{Code Snippets: context data} |
|
184 \texttt{\tiny{ |
|
185 \begin{tabbing} |
|
186 xx\=xx\=xx\=xx\=\kill |
|
187 datatype Isac\_Ctxt =\\ |
|
188 \>\>Env of term * term\\ |
|
189 \>| Asm of term;\\ |
|
190 \\ |
|
191 structure ContextData = Proof\_Data\\ |
|
192 \>~(type T = Isac\_Ctxt list\\ |
|
193 \>\>fun init \_ = []);\\ |
|
194 \\ |
177 local\\ |
195 local\\ |
178 \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\ |
196 \>fun insert\_ctxt data = ContextData.map (fn xs => distinct (data@xs));\\ |
179 in\\ |
197 in\\ |
180 \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\ |
198 \>fun insert\_assumptions asms = map (fn t => Asm t) asms |> insert\_ctxt;\\ |
181 \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\ |
199 \>fun insert\_environments envs = map (fn t => Env t) envs |> insert\_ctxt;\\ |
|
200 end\\ |
|
201 \\ |
|
202 local\\ |
|
203 \>fun unpack\_asms (Asm t::ts) = t::(unpack\_asms ts)\\ |
|
204 \>\>| unpack\_asms (Env \_::ts) = unpack\_asms ts\\ |
|
205 \>\>| unpack\_asms [] = [];\\ |
|
206 \>fun unpack\_envs (Env t::ts) = t::(unpack\_envs ts)\\ |
|
207 \>\>| unpack\_envs (Asm \_::ts) = unpack\_envs ts\\ |
|
208 \>\>| unpack\_envs [] = [];\\ |
|
209 in\\ |
|
210 \>fun get\_assumptions ctxt = ContextData.get ctxt |> unpack\_asms;\\ |
|
211 \>fun get\_environments ctxt = ContextData.get ctxt |> unpack\_envs;\\ |
182 end |
212 end |
183 \end{tabbing} |
213 \end{tabbing} |
184 }} |
214 }} |
185 \end{frame} |
215 \end{frame} |
186 |
216 |
187 \subsection[Redesign]{Redesign of Type Inference in \isac} |
217 \subsection[Redesign]{Redesign of Type Inference in \isac} |
188 \begin{frame} |
218 \begin{frame} |
189 \frametitle{Redesign of type inference in \isac} |
219 \frametitle{Redesign of Type Inference in \isac} |
190 \begin{itemize} |
220 \begin{itemize} |
191 \item use context type inference |
221 \item use context type inference |
192 \item parsing input (specification \& user input) |
222 \item parsing input (specification \& user input) |
193 \item specification with polymorphic types |
223 \item specification with polymorphic types |
194 \item etc. |
224 \item etc. |
195 \end{itemize} |
225 \end{itemize} |
|
226 \end{frame} |
|
227 |
|
228 \begin{frame} |
|
229 \frametitle{Lines of Code} |
|
230 \begin{tabular}{lr} |
|
231 src/ & 1700 k \\ |
|
232 src/Pure/ & 70 k \\ |
|
233 src/Provers/ & 8 k \\ |
|
234 src/Tools/ & 800 k \\ |
|
235 src/isac/ & 37 k \\ |
|
236 src/isac/Knowledge & 16 k \\ |
|
237 \end{tabular} |
196 \end{frame} |
238 \end{frame} |
197 |
239 |
198 \subsection[Code Improvement]{Improvement of functional code} |
240 \subsection[Code Improvement]{Improvement of functional code} |
199 \begin{frame} |
241 \begin{frame} |
200 \frametitle{Improvement of functional code} |
242 \frametitle{Improvement of functional code} |
263 \item \isac programming language more compact\\ |
305 \item \isac programming language more compact\\ |
264 $\rightarrow$ context built automatically |
306 $\rightarrow$ context built automatically |
265 \end{itemize} |
307 \end{itemize} |
266 \end{frame} |
308 \end{frame} |
267 |
309 |
|
310 \begin{frame} |
|
311 \frametitle{jedit demonstration} |
|
312 DEMO |
|
313 \end{frame} |
|
314 |
268 \section[Problems]{Problems encountered in the project} |
315 \section[Problems]{Problems encountered in the project} |
269 \begin{frame} |
316 \begin{frame} |
270 \frametitle{Problems encountered in the project} |
317 \frametitle{Problems encountered in the project} |
271 \begin{itemize} |
318 \begin{itemize} |
272 \item publication of new Isabelle release |
319 \item publication of new Isabelle release |
273 \item amount of code in Isabelle and \isac |
320 \item amount of code in Isabelle and \isac |
274 \item changes scattered throughout the code |
321 \item changes scattered throughout the code ($\rightarrow$ grep) |
275 \end{itemize} |
322 \end{itemize} |
276 \end{frame} |
323 \end{frame} |
277 |
324 |
278 \section{Summary} |
325 \section{Summary} |
279 \begin{frame} |
326 \begin{frame} |