Stream: Beginner Questions

Topic: About the code generation- Wellsortedness error


view this post on Zulip Hongjian Jiang (Jul 27 2023 at 13:47):

When I run my example, I meet below hints:

Wellsortedness error:
Type nat not of sort {enum,equal,order}
No type arity nat :: enum

I am curious about the principal behind this.

The part of snippet could be:

definition check_eqv :: "'a::order rexp ⇒ 'a rexp ⇒ 'a list ⇒ bool" where
"check_eqv r s as =
  (let nr = norm r; ns = norm s
   in case closure as (nr, ns) of
     Some([],_) ⇒ True | _ ⇒ False)"

fun f :: "nat ⇒ bool" where
"f n = (n < 3)"

lemma "check_eqv (Plus One (Times ((Sym (Predicate.Pred f))) (Star (Sym (Predicate.Pred f))))) (Star(Sym (Predicate.Pred f))) [1,2,3,4]"
  by eval

Any helps would be appreciated.

view this post on Zulip Mathias Fleury (Jul 27 2023 at 13:50):

Well the error message basically says that the code generator is not able to generate code, because the only way is to enumerate all solutions…

view this post on Zulip Hongjian Jiang (Jul 27 2023 at 13:51):

how to improve such case

view this post on Zulip Mathias Fleury (Jul 27 2023 at 13:55):

by looking at piece of the code, find out exactly which part is not working (I assume it is closure but I am not sure). Once you know that, you have to replace the code by something executable… (See https://isabelle.in.tum.de/dist/Isabelle2022/doc/codegen.pdf)

view this post on Zulip Hongjian Jiang (Jul 28 2023 at 13:45):

Hi, Mathisas. I thought I found the problem. I use the set comprehension to calculate the value.

Likevalue "{a. f a}"

view this post on Zulip Hongjian Jiang (Jul 28 2023 at 13:46):

But it is mandatory in my example I think.

view this post on Zulip Yong Kiam (Jul 31 2023 at 00:57):

like Mathias said, if you must use sets, you would have to provide rewrites for that in a more "executable" way that doesn't require searching over all numbers a


Last updated: Dec 07 2023 at 20:16 UTC