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

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.


Tobias Nipkow wrote:
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.


Sven Schneider schrieb:
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

*** 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"
  "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"


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