[isabelle-dev] NEWS: Computations

[Florian Haftmann]

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

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20170222/9b7a91da/attachment.asc>