[isabelle-dev] Efficient code for Discrete.log

[Andreas Lochbihler]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>