First draft of the value* command implementation #3
Loading…
Reference in New Issue
No description provided.
Delete Branch "nicolas.meric/Isabelle_DOF:value-star-first-draft"
Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?
Add a command value*
and adds the possibility to evaluate
Term Annotation Antiquotations (TA)
with the help of the DOF_core.transduce_term_global function.
The DOF_core.transduce_term_global function,
in addition to the validation of a term
(also called a second level type checking),
is now able to make a so called elaboration:
it will construct the term referenced by a TA before
passing it to the evaluator.
the "undefined" constant whose evaluation always fails.
(See the code generation documentation).
Furthermore, the instance class generation is updated in such a way
that each of its attributes is initialized with a free variable
whose name shows to the final user that this attribute
is not initialized.
It implies that an instance class evaluation will be pass
to the normalization by evaluation (nbe) evaluator by default
if the final user does not specify a class instance entirely,
i.e. by specifying each attribute of the instance.
This choice is considered a decent compromise, considering
the speed and trustworthiness of the nbe evaluator.
(See the article
A Compiled Implementation of Normalization by Evaluation from 2008)
which is used for the elaboration of the term referenced by the TA.to pass
of the elaboration of the built-ins TA and of an instance class:
as it is;
and expose the limitations of the current implementation
in Evaluation.thy