*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Code generation from abstract types*From*: andreas.lochbihler at kit.edu*Date*: Fri, 04 Jan 2013 12:59:19 +0100*Cc*: Jesus Aransay <jesus-maria.aransay at unirioja.es>, isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <50DC1228.2060907@informatik.tu-muenchen.de>*References*: <CAL0S8BddPG-=6GNZBXvmXOWr6nmf7UXAuAbh_7nGEE-K-X1JZw@mail.gmail.com> <50DC1228.2060907@informatik.tu-muenchen.de>*User-agent*: Internet Messaging Program (IMP) H3 (4.0.4)

Hi Jesus and Florian,

definition mat_mult_row where

lemma mat_mult_row_code [code abstract]:

by(simp add: mat_mult_row_def fun_eq_iff) lemma mat_mult [code abstract]: "vec_nth (m ** m') = mat_mult_row m m'" unfolding matrix_matrix_mult_def mat_mult_row_def[abs_def] using vec_lambda_beta by auto export_code "op **" in SML file - So there is no need to wrap all types and do the lifting. Hope this helps, Andreas Zitat von Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

Hi Jesus,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?there is no support for nested abstract datatypes. To achieve abstract matrices, you would need to provide an explicit type for matrices (e.g. using datatype ('a, 'm, 'n) matrix = Matrix "'a ^ 'm ^ 'n" (*)) and then lift all operations you want to that explicit matrix type. When doing this, the recently emerged lifting and transfer infrastructure could be helpful - unfortunately, I have no canonical reference for this at hand and have not used it myself, but others on this mailing list will know better. I hope these meagure hints show the way. Feel free to ask again if you are still lost. Cheers, Florian (*) I am not familiar with the vectors/matrix stuff, so this might be wrong.

**Follow-Ups**:**Re: [isabelle] Code generation from abstract types***From:*Jesus Aransay

- Previous by Date: Re: [isabelle] newbie questions r.e. Isar to Haskell/ML generation
- Next by Date: Re: [isabelle] Happy New Year with Free/Bound Variables
- Previous by Thread: Re: [isabelle] Code generation from abstract types
- Next by Thread: Re: [isabelle] Code generation from abstract types
- Cl-isabelle-users January 2013 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