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.



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

isabelle-dev mailing list

Reply via email to