Hi Manuel,
You are not the first to encouter this problem. Here's my experience:
In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of
Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile,
Gcd has become part of Main again.
Conversely, the AFP entry Native_Word sets up serialisation for bit operations, and there
is a specific Code_Target_Bits_Int theory with the relevant adaptations for bit operations
on integers.
I'd suggest that you setup two theories Code_Target_Complex_Int and
Code_Target_Complex_Nat that will collect all the code declarations for constants that are
defined in Complex. I think this is the cleanest approach, even though in the long run, we
might have a huge number of these specific adaptation theories. Your efficient algorithm
can go directly into Discrete.thy.
Best,
Andreas
On 29/06/17 15:29, Manuel Eberl wrote:
Hallo,
I'm considering adding efficient code for Discrete.log (the dual logarithm on natural
numbers). PolyML does provide an IntInf.log2 function that seems reasonably efficient so
that one can set up code printing. However, I am struggling with one detail:
Where would the code that does this actually reside? I cannot really put it into
Discrete.thy, because then that would have to import Code_Target_Numeral. I could put it
into Code_Target_Integer.thy, but then that would have to import Discrete, which does not
sound right to me either.
I attached what I have so far.
Manuel
_______________________________________________
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
