Hi René and Manuel,
Indeed, for sets, expressing the code equations in terms of a generic iteration operation
on sets would do the job for most of the cases. The comp_fun_commute and comp_fun_idem
types in Containers precisely do this, but they have not been integrated in the HOL
library yet. They should work all kinds of big operators (setsum, setprod, Gcd, etc) and
could be added to the HOL library.
Of course, some special case tricks no longer work if go for a generic iteration
operation. For example, one could prove "Gcd (List.coset xs) = 1" for natural numbers and
declare a code equation. Such things would no longer be possible, but I am not sure
whether they are done at all at the moment.
Manuel's suggestion of code_abort is a bit cleaner than René's use Code.abort, because
Code.abort does not work with normalisation by evaluation whereas code_abort does.
Best,
Andreas
On 03/10/16 15:29, Manuel Eberl wrote:
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
