Stream: General

Topic: "not of sort enum" error with code generation

Liangrun Da (Jun 06 2024 at 08:11):

Hi! Considering the following silly definition

theory test
  imports Main
begin

type_synonym graph = ‹(nat × nat) set›

fun has_next_hop :: "nat set ⇒ graph ⇒ bool" where
  "has_next_hop S G = (∀x∈S.∃y.(x, y) ∈ G)"

export_code has_next_hop

end

Isabelle refuses to generate code for this function and gives the following error message:

Wellsortedness error
(in code equation has_next_hop ?s ?g ≡ ∀x∈?s. ∃y. (x, y) ∈ ?g):
Type nat not of sort enum
No type arity nat :: enum

From my understanding, it seems to be an issue related to type classes, specifically that nat does not belong to the enumsort. How can I resolve this error so that I can successfully generate code for my function?

Thanks,
Liangrun

Simon Roßkopf (Jun 06 2024 at 08:27):

You cannot make nat an instance of enum, as it is for explicitly enumerating finite types.

This is also the main problem why code generation fails: You have an unbounded existential quantifier in your definition, so by default the code generator tries to implement this by checking all possible values (this is where the enum comes in), however there are infinitely many of them(and nat therefore can not be an instance of enum), so this does not work.

So your best best is probably changing your definition in a way that only finitely man ys have to be checked

Liangrun Da (Jun 06 2024 at 09:00):

Simon Roßkopf said:

You cannot make nat an instance of enum, as it is for explicitly enumerating finite types.

This is also the main problem why code generation fails: You have an unbounded existential quantifier in your definition, so by default the code generator tries to implement this by checking all possible values (this is where the enum comes in), however there are infinitely many of them(and nat therefore can not be an instance of enum), so this does not work.

So your best best is probably changing your definition in a way that only finitely man ys have to be checked

Thank you! It works after I change it to:

theory test
  imports Main
begin

type_synonym graph = ‹(nat × nat) set›

fun has_next_hop :: "nat set ⇒ graph ⇒ bool" where
  "has_next_hop S G = (∀x∈S.∃(a, _)∈G. (x = a))"

export_code has_next_hop

end

Liangrun Da (Jun 06 2024 at 09:21):

Simon Roßkopf said:

You cannot make nat an instance of enum, as it is for explicitly enumerating finite types.

This is also the main problem why code generation fails: You have an unbounded existential quantifier in your definition, so by default the code generator tries to implement this by checking all possible values (this is where the enum comes in), however there are infinitely many of them(and nat therefore can not be an instance of enum), so this does not work.

So your best best is probably changing your definition in a way that only finitely man ys have to be checked

A follow-up error puzzled me:

I tried to compute the transitive closure of graph using reachable_graph. I used the same pattern to define has_descendant. However this time Isabelle refused to generate code (also gave me the not of sort enum error message).

I thought (∀x∈S.∃(a, _)∈ (reachable_graph G). (x = a)) doesn't need to enumerate nat and should be able to produce code (just like (∀x∈S.∃(a, _)∈ G. (x = a)) does). Could you give me some hint why has_descendant fails?

theory test
  imports Main
begin

type_synonym graph = ‹(nat × nat) set›

fun reachable_graph :: "graph ⇒ graph" where
  "reachable_graph G = rtrancl G"

fun has_next_hop :: "nat set ⇒ graph ⇒ bool" where
  "has_next_hop S G = (∀x∈S.∃(a, _)∈ G. (x = a))"

fun has_descendant :: "nat set ⇒ graph ⇒ bool" where
  "has_descendant S G = (∀x∈S.∃(a, _)∈ (reachable_graph G). (x = a))"

export_code has_descendant

end

Fabian Huch (Jun 06 2024 at 09:25):

Your graph might be infinite

Liangrun Da (Jun 06 2024 at 09:30):

Fabian Huch said:

Your graph might be infinite

If that was the reason, what makes has_next_hop different from hash_descendant? Isabelle can generate code for has_next_hop but G in has_next_hop could also be infinite.

Fabian Huch (Jun 06 2024 at 09:37):

The puzzling thing should be why it can even generate code for has_next_hop, not why it can't generate code for has_descendant.

Fabian Huch (Jun 06 2024 at 09:38):

And the answer is that there is special code setup for dealing with sets, membership, and equality, but not for your custom function

Liangrun Da (Jun 06 2024 at 09:40):

Fabian Huch said:

And the answer is that there is special code setup for dealing with sets, membership, and equality, but not for your custom function

Thanks for your answer!

Last updated: Dec 21 2024 at 12:33 UTC