Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem

Sven Schneider wrote:
> Not being able to transform anything to code that involes sets or
> functions seems to be a very strong restriction to me.
> Even though
> "card (dom x)" is just an example and changing it to "0" solves the
> 'type arity'-Problem changing it does not solve my initial problem.

Indeed, adding the following code setup,

lemmas [code func del] = card_def
lemma [code func]:
  "Collect P = project P UNIV"
  unfolding project_def by simp

both card and dom turn executable (the latter only on finite types).
The fact that there is no trivial solution to handle entities involving
"infinity" (like functions and sets) at the same generality as HOL
permits is due to the very nature of code generation.

> Is there a list of what can/can't be executed and what will/will not be
> made executable in the near future? If it is in the manual I missed it.

There is an elaborate technical report on that:

Pragmatically spoken, as long as you restrict to the FP fragment of HOL
(class, datatype, executable constants specified by
functions/definitions only involving datatype constructors or executable
constants), code generation shall be possible.  For specifications
involving inherently logical constructs (set comprehension, ...), it may
be possible to provide an executable model by means of particular code

fn:Florian Haftmann
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =

Attachment: signature.asc
Description: OpenPGP digital signature

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