Re: [isabelle] nat_code Equation



On Fri, 30 Nov 2012, René Neumann wrote:

ML {*
 val y : IntInf.int = 70000000;

 (* Tail-recursive approach *)
 val t = Time.now ();
 val _ = @{code nat'} y (@{code nat} 0);
 val nat_tail = Time.- (Time.now (), t);

 (* René Thiemann's approach *)
 val t = Time.now ();
 val _ = @{code nat_th} y;
 val nat_th = Time.- (Time.now() , t);

 (* approach from Code_Integer *)
 val t = Time.now ();
 val _ = @{code nat} y;
 val nat = Time.- (Time.now(), t);
*}

Just some side-remarks about the Isabelle/ML that is quoted above:

  * Type int is always the normal mathematical one, i.e. IntInf and Int
    coincide.  (There are some special tricks to make the different SML
    implementations underlying Isabelle/ML agree on this.)

  * Structure Timing provides some tools for timing, notably the classic
    timeit and timeap combinators.  Since timing on multicore hardware
    is difficult to get right, it currently prints elapsed / CPU / GC time
    to give some starting points for further guessing.  (In any case it is
    the standard library entry for that, so when better timing mechanisms
    become available they will be integrated here.)


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.