This is a problem that I have given quite some thought in the past. The problem is the following: You have a theory A providing certain operations on sets (in this case: Gcd) and a theory B providing implementations for sets (in this case: Containers).
The problem is that the code equations for the operations from A depend on the implementation that is chosen for sets. A cannot give code equations for every possible implementation of sets, while B cannot possibly import every theory that has operations involving sets and give code equations for it. The best possible solution would be to imitate the way it is currently done for setsum, setprod, etc: Define a sufficiently general combinator that iterates over the set and give the code equations in A in terms of this combinator. Then B only has to reimplement this generic combinator. That would be the cleanest solution, but I'm not sure how such a combinator would look like. The folding operation would probably have to satisfy some associativity/commutativity laws and have that information available at the type level (similar to the cfc type in Containers). By the way, my current workaround for this problem is to declare all problematic constants as "code_abort". Cheers, Manuel On 03/10/16 15:21, Thiemann, Rene wrote: > 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 > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
