Computations generated by the code generator can be embedded
directly into ML, alongside with @{code} antiquotations, using
the following antiquotations:
@{computation … terms: … datatypes: …} :
((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a
@{computation_conv … terms: … datatypes: …} :
(Proof.context -> 'ml -> conv) -> Proof.context -> conv
@{computation_check terms: … datatypes: …} :
Proof.context -> conv
See src/HOL/ex/Computations.thy,
src/HOL/Decision_Procs/Commutative_Ring.thy and
src/HOL/Decision_Procs/Reflective_Field.thy for examples and the
tutorial on code generation.
========================================================================
This refers to fd753468786f and is IMHO a remarkable mile stone in the
overall code generation / reflection / proof procedure business after
more than 10 years of previous unsatisfactory attempts in that area.
The details are explained in a dedicated chapter §6 of the tutorial on
code generation.
Cheers,
Florian
--
PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
