Email Gateway (Sep 08 2023 at 23:37): Email Gateway (Sep 08 2023 at 23:37):From: Guilherme Silva <guilhermegfsilva@gmail.com>
I think I might have made a mistake by sending this question to
cl-isabelle-users@lists.cam.ac.uk, so I'm trying this address instead.
Sorry for the inconvenience.
I'm trying to run the following code in Isabelle:
typedecl type_a
typedecl type_b
consts set_a :: "type_a set"
consts set_b :: "type_b set"
consts pairs :: "(type_a \<times> type_b) set"
definition func_1:: "bool" where
"func_1 \<equiv>
\<forall> a b .
((a, b) \<in> pairs \<longrightarrow> (a \<in> set_a \<and> b \<in>
set_b))"
export_code
func_1
in SML module_name SML_func_1
in Haskell module_name Haskell_func_1
in OCaml module_name OCaml_func_1
in Scala module_name Scala_func_1
But I get a "Wellsortedness error: Type type_a/type_b not of sort enum"
error when trying to export code because type_a and type_b are not defined
as enumerable types.
How do I define a new, enumerable type to bypass this? I was under the
impression that this was possible by using Enum.thy (
https://isabelle.in.tum.de/library/HOL/HOL/Enum.html), but I don't know how
exactly to use this theory to do this, or if there's another one than can
be used to do it.
Thanks,
G. Silva
Email Gateway (Sep 09 2023 at 12:04):From: Thomas Sewell <tals4@cam.ac.uk>
I don't think this is going to work.
Isabelle/HOL lets you name types and constants that don't have any definition, as you have done. It also includes some logical operators (e.g. forall) which don't have any standard execution strategy. In these cases, the export mechanism will fail. If you want to generate code for some function, you need to use only the subset of Isabelle's constants and definitional mechanisms which map to concrete code.
There are some extensions, which might be confusing the matter. If your type is enumerable (i.e. if there exists a list of its elements), it's obvious how to implement forall using filter. I guess this is the default strategy for forall, which the system is trying to use, and failing because there's no enumeration known for "type_a". But this is just the first error - nothing else is known about "type_a", so it seems inevitable that the system won't be able to encode any operations on it.
Good luck,
Thomas.
Last updated: Apr 29 2024 at 04:18 UTC