Skip to content
Towards an extraction of CaPriCon terms to functional programs

CaPriCon is now endowed with a new 'axiom' builtin, which produces an
opaque value of an arbitrary type, meant to represent an external
function (such as an OCaml constructor or type name) which will be
supplied by the runtime after extraction.

Said extraction can then proceed by identifying inductive types within
the term to extract, and defining an axiom for each of those types'
constructors. Then, it can substitute each occurrence of an inductive
value with its equivalent using the now-defined inductive axioms, and
finally erase the extraneous type information to produce an abstract
algebraic functional representation of the initial term.

More in the next release...