Email Gateway (Aug 22 2022 at 15:47): Email Gateway (Aug 22 2022 at 15:47):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Hi,
Consider the following silly definition (in Isabelle2016-1):
definition goo :: "bool set" where
"goo ≡ gfp (λx. x ∩ {})"
And the following code generation commands:
export_code goo in Scala
export_code goo in Haskell
export_code goo in SML
export_code goo in OCaml
The first two commands for the Scala and Haskell targets succeed, and
generate code, but the second two do not and instead produce the
following error:
Dependency "ccpo" < "Sup" -> class "Sup" would result in module dependency cycle
The problem appears to be the gfp and lfp constants. How can I work
around this and generate SML code using gfp (and lfp)?
Thanks,
Dominic
Email Gateway (Aug 22 2022 at 15:47):From: Lars Hupel <hupel@in.tum.de>
Hi Dominic,
The problem appears to be the gfp and lfp constants. How can I work
around this and generate SML code using gfp (and lfp)?
in case you don't care about splitting up your generated code into
multiple module, you can instruct the code generator to use just one:
export_code goo in SML module_name exported_code
export_code goo in OCaml module_name exported_code
This avoids cycles between modules.
Cheers
Lars
Email Gateway (Aug 22 2022 at 15:48):From: Peter Lammich <lammich@in.tum.de>
Hi Dominic,
You have to specify a module name to which the code is exported:
export_code goo in SML module_name Goo
export_code goo in OCaml module_name Goo
Email Gateway (Aug 22 2022 at 15:48):From: Dominic Mulligan via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Thanks Lars and Peter!
Last updated: Apr 27 2024 at 01:05 UTC