Re: [isabelle] Code generation from abstract types



Hi Jesus and Florian,

The code generator does support nested abstract datatypes in this case, although only indirectly. As the abstraction function vec_lambda must not appear in any code equation, you have to promote any such subterm to a proper constant and prove the corresponding code equation. The following works:

definition mat_mult_row where
"mat_mult_row m m' f = vec_lambda (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"

lemma mat_mult_row_code [code abstract]:
"vec_nth (mat_mult_row m m' f) = (%c. setsum (%k. ((m$f)$k) * ((m'$k)$c)) (UNIV :: 'n::finite set))"
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.









This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.