*To*: Sven Schneider <svens at cs.tu-berlin.de>*Subject*: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Tue, 20 Nov 2007 10:14:53 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <474299DE.8070305@in.tum.de>*References*: <4741A956.6010208@cs.tu-berlin.de> <474299DE.8070305@in.tum.de>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

>> consts max_label :: nat >> typedef Label = "{n :: nat. n <= max_label }" by fastsimp

Amine. 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, whichis not executable, and the definition of card has similar problems.If you need to compute dom and card, I suspect you need to replacefunctions by a special data structure like an association list (seeLibrary/AssocList.thy) or even search trees.Tobias Sven Schneider schrieb:Dear all,I am not able to create code from the theory below. Unfortunately Ican't understand the message (see bellow) that I get. I guess it hassomething 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

**Follow-Ups**:**Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem***From:*Sven Schneider

**References**:**[isabelle] [Code-Generation] 'No type arity (..)' - Problem***From:*Sven Schneider

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

- Previous by Date: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Next by Date: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Previous by Thread: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Next by Thread: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Cl-isabelle-users November 2007 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