Dear all, in the following theory, the export-code fails:
(Isabelle 957ba35d1338, AFP 618f04bf906f) theory Problem imports "~~/src/HOL/Library/Polynomial_Factorial" "$AFP/thys/Containers/Set_Impl" begin definition foo :: "'a :: factorial_semiring_gcd ⇒ 'a ⇒ 'a" where "foo x y = gcd y x" definition bar :: "int ⇒ int" where "bar x = foo x (x - 1)" export_code bar in Haskell end The problem arises from two issues: - factorial_semiring_gcd requires code for Gcd :: “Set ‘a => ‘a”, not only for the binary “gcd :: ‘a => ‘a => ‘a”! - the code-equation for Gcd is Gcd_eucl_set: "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs” where “set” is only a constructor if one does not load the container-library. It would be nice, if one can either alter factorial_semiring_gcd so that it does not require “Gcd” anymore, or if the code-equation is modified in a way that permits co-existence with containers. (Of course, similarly for Lcm). With best regards, Akihisa, Sebastiaan, and René PS: We currently solve the problem by disabling Gcd and Lcm as follows: lemma [code]: "(Gcd_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Gcd on sets'') (λ _. Gcd_eucl)" by simp lemma [code]: "(Lcm_eucl :: rat set ⇒ rat) = Code.abort (STR ''no Lcm on sets'') (λ _. Lcm_eucl)" by simp _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
