Email Gateway (Aug 18 2022 at 11:01): Email Gateway (Aug 18 2022 at 11:01):From: Sven Schneider <svens@cs.tu-berlin.de>
Dear all,
I am not able to create code from the theory below. Unfortunately I
can't understand the message (see bellow) that I get. I guess it has
something todo with the part 1.5.3 in the manual of the codegeneration
(Concerning operational equality).
All the best
Sven
*** No type arity Label :: eq,
*** for constant eval
*** in defining equations
*** "eval (Obj ?x) º card (dom ?x)"
*** "eval (Var ?n) º ?n",
*** while preprocessing equations for constant(s) eval
*** At command "export_code".
theory Gentest imports Main begin
consts max_label :: nat
typedef Label = "{n :: nat. n <= max_label }" by fastsimp
datatype dB =
Var "nat"
| Obj "Label \<Rightarrow> dB option"
constdefs compare :: "Label \<Rightarrow> Label \<Rightarrow> bool"
"compare k l \<equiv> (Rep_Label k = Rep_Label l)"
consts eval :: "dB \<Rightarrow> nat"
primrec
"eval (Var n) = n"
"eval (Obj x) = card (dom x)"
lemma "eval (Obj(empty(Abs_label (0::nat) \<mapsto>Var 2))) = ?x" by simp
export_code "eval" in "SML" file "gen.ML"
export_code "compare" in "SML" file "gen.ML"
end
Email Gateway (Aug 18 2022 at 11:01):From: Tobias Nipkow <nipkow@in.tum.de>
I'm not sure about the arity problem. But
"eval (Obj x) = card (dom x)"
is unlikely to be executable: dom is defined by set comprehension, which
is not executable, and the definition of card has similar problems.
If you need to compute dom and card, I suspect you need to replace
functions by a special data structure like an association list (see
Library/AssocList.thy) or even search trees.
Tobias
Sven Schneider schrieb:
Email Gateway (Aug 18 2022 at 11:01):From: Amine Chaieb <chaieb@in.tum.de>
Even with Tobias's suggestion, I suspect you wouldn't get executable
code since your labels are "parametrized":
consts max_label :: nat
typedef Label = "{n :: nat. n <= max_label }" by fastsimp
Here you "declare" max_label but not define it. It you were to program
this by yourself in ML, you would need the value max_label either as a
constant or as a parameter.
Amine.
Tobias Nipkow wrote:
Email Gateway (Aug 18 2022 at 11:01):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
The problem indeed is rooted in this declaration:
consts max_label :: nat
typedef Label = "{n :: nat. n <= max_label }" by fastsimp
Beside the problem with the hidden dependency on an unspecified constant
"max_label" pointed out by Amine, for typedefs there is no canonical
code generator setup.
Florian
florian.haftmann.vcf
signature.asc
Email Gateway (Aug 18 2022 at 11:01):From: Sven Schneider <svens@cs.tu-berlin.de>
Hi Amine,
thats a good point.
Defining the max_label is definitely necessary though it is not the source
of 'type arity' problem.
Thanks!
Email Gateway (Aug 18 2022 at 11:01):From: Sven Schneider <svens@cs.tu-berlin.de>
Hello Tobias,
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.
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.
I guess I have to thing about changing everything to lists or similar.
Thanks a lot and have a nice day!
Sven
Email Gateway (Aug 18 2022 at 11:02):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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:
http://www4.in.tum.de/~haftmann/pdf/codegen_isabelle_haftmann_nipkow_16pp.pdf
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
theorems.
Florian
florian.haftmann.vcf
signature.asc
Last updated: May 03 2024 at 04:19 UTC