Stream: Beginner Questions

Topic: About the code generation- Wellsortedness error

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.

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…

Hongjian Jiang (Jul 27 2023 at 13:51):

how to improve such case

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)

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

Hongjian Jiang (Jul 28 2023 at 13:46):

But it is mandatory in my example I think.

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: Apr 27 2024 at 20:14 UTC