[isabelle-dev] Efficient code for Discrete.log
andreas.lochbihler at inf.ethz.ch
Thu Jun 29 19:39:43 CEST 2017
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
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.
On 29/06/17 15:29, Manuel Eberl wrote:
> 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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev