*Subject*: [isabelle] Code generation from abstract types*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Wed, 26 Dec 2012 14:22:51 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Sender*: jmaransay at gmail.com

Dear all, we were trying to carry out an experiment in code generation over the Multivariate Analysis Library in Isabelle. Our idea was to generate code from operations on vectors and matrices, as defined in that library; in the library, there exists a "vec" type which is defined as the set of functions from an underlying finite type to any type. The Abs and Rep operations between that type and the function type a are called, respectively, vec_lambda (given a function it returns a "vec") and vec_nth (it returns a function from a "vec"). Matrices are then defined as a "vec of a vec". When we try to generate code from definitions about vectors (the zero vector, addition, multiplication), things work perfectly, making use of the "code abstype" and "code abstract" labels: theory execution imports Main "~~/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space" begin lemma [code abstype]: "vec_lambda (vec_nth g) = g" by (metis vec_nth_inverse) lemma [code abstract]: "vec_nth 0 = (%x. 0)" by (metis zero_index) lemma [code abstract]: "vec_nth (a + b) = (%i. a$i + b$i)" by (metis vector_add_component) export_code "(0:: ('a::{zero,plus},'b::finite) vec)" "op + :: ('a::{zero,plus},'b::finite) vec => ('a,'b) vec => ('a,'b) vec" When we try to generate code for operations over matrices which return a matrix (for instance, matrix multiplication), we do not know how to define the "code abstract" lemma for such operation, since it involves a "vec_nth of a vec_lambda of a vec_nth", for which the code generator produces a "violation abstraction error": lemma mat_mult [code abstract]: "vec_nth (m ** m') = (%f. vec_lambda (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set)))" unfolding matrix_matrix_mult_def using vec_lambda_beta by auto Is there a way to express the previous lemma and that code generation for matrix multiplication is still possible? Is anybody aware of any possible workaround? Thanks a lot for any hint, sorry for not being capable of translating the example to a generic setting, Jesus On Sat, Dec 22, 2012 at 6:44 PM, Alfio Martini <alfio.martini at acm.org> wrote: > Well...I see two ways to do it with my little knowledge of Isabelle: > > 1) I have just to write a recursive function from D into D' and this is > the morphism I wanted (similar to what is done with boolean datatypes > in the LNCS Tutorial). > > 2)just to include D as a type (prefixed by a dummy constructor) > in the definition of D'. This seems to be the easiest way, if the D is a > proper subset of D', > and the one I decided to use. > > Best! > > On Sat, Dec 22, 2012 at 2:40 PM, Alfio Martini <alfio.martini at acm.org>wrote: > >> Dear Isabelle Users, >> >> This is a very simple question: >> >> Assume a language L specifiied by a datatype D, where L = Lang(D). If L is >> a subset of L', how >> can I write in Isabelle a datatype D', that extends D such that Lang(D')= >> L'? >> >> More generally, how can I model datatype morphisms in Isabelle, so that >> the case above >> is just a simple inclusion arrow. >> >> Many thanks! >> -- >> Alfio Ricardo Martini >> PhD in Computer Science (TU Berlin) >> Associate Professor at Faculty of Informatics (PUCRS) >> Coordenador do Curso de Ciência da Computação >> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática >> 90619-900 -Porto Alegre - RS - Brasil >> > > > > -- > Alfio Ricardo Martini > PhD in Computer Science (TU Berlin) > Associate Professor at Faculty of Informatics (PUCRS) > Coordenador do Curso de Ciência da Computação > Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática > 90619-900 -Porto Alegre - RS - Brasil -- Jesús María Aransay Azofra Universidad de La Rioja Dpto. de Matemáticas y Computación tlf.: (+34) 941299438 fax: (+34) 941299460 mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

**Follow-Ups**:**Re: [isabelle] Code generation from abstract types***From:*Florian Haftmann

- Previous by Date: [isabelle] ESSS 2013 -- submission deadline extended
- Next by Date: [isabelle] Code generation and partiality
- Previous by Thread: [isabelle] ESSS 2013 -- submission deadline extended
- Next by Thread: Re: [isabelle] Code generation from abstract types
- Cl-isabelle-users December 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list