Hi all, I did an experiment with Flyspeck-Tame (on macbroyXY):
Using the Efficient_Nat theory where Isabelle nat is directly represented as PolyML int: > Finished HOL-Flyspeck-Tame (11:50:46 elapsed time, 13:54:35 cpu time, factor > 1.17) Using the Target_Numeral theory where Isabelle nat is an abstract datatype over PolyML int: > Finished HOL-Flyspeck-Tame (10:55:49 elapsed time, 13:57:31 cpu time, factor > 1.27) The reason why this has the same magnitude of runtime is that in PolyML trivial datatypes like > datatype nat = Nat of int > fun int_of (Nat k) = k are optimized away. This is a proof of concept that it is possible in the future to have just *one* type which is mapped onto target language numerals by default, and to refine nat and/or int to use this is implementation if desired, rather than adhoc code_const setups etc. for nat and int. Cf. also https://isabelle.in.tum.de/community/Numerals Cheers, Florian P.S. This his no consequences for the upcoming release. -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
