Trigger error when the attribute is not specified as an argument
of the antiquatation and is not an attribujte of the instance.
(In these case, the position of the attribute is NONE)
- Make doc_class type and constant used by regular expression
in monitors ground
- Make class tag attribute ground (with serial())
- The previous items make possible
the evaluation of the trace attribute
and the definition of the trace-attribute term annotation
- Add an eager and lazy invariants checking functions mechanism
for low level invariants to allow the checking of invariants
only when opening or closing a monitor instance.
The state of the monitor instances traces evolves when declaring
instances between open_monitor* and close_monitor* commands.
This mechanism can capture the changes be defining
invariants before or after traces are populated but not
before and after, with the current mechanism.
Two tables were added: docclass_eager_inv_tab
and docclass_lazy_inv_tab to store these invariants
- Implement CENELEC_50128 Table A.1 using this mechanism
- Warning: the current implementation does yet not support
some use-cases, like invariant on monitors,
or the initialization of docitem without a class associated.
- Add first draft of the checking of invariants.
For now, it is disabled by default because some cases
are not yet supported, like the initialization of docitem
without a class associated.
ex: text*[sdf]‹ Lorem ipsum @{thm refl}›
- To enable the checking, one can use the theory attribute
"invariants_checking" by declaring it in a theory like this:
declare [[invariants_strict_checking = true]]
- A checking using basic tactics (unfolding and auto) can be enable
with the "invariants_checking_with_tactics" theory attribute
for specific use-cases
- The specification of invariants is now automatically abstracted,
so one must define an invariant like this now:
doc_class W =
w::"int"
invariant w :: "w σ ≥ 3"
The old form:
doc_class W =
w::"int"
invariant w :: "λσ. w σ ≥ 3"
is now deprecated.
The specification of the invariant still uses the σ-notation
and is defined globally by the name component "invariantN"
- Update the invariants definition in the theories to match
the new implementation
- Update the manual to explain this new feature
- Add small examples in src/tests/High_Level_Syntax_Invariants.thy
and src/tests/Ontology_Matching_Example.thy
- Add a new Term Annotation Antiquotation (TA)
to allow requests on instances.
Example:
@{C-instances} will return all the instances of the class "C"
defined in the generated theory
- Update ISA_transformers elaborate function signature to
take into account the case where the term argument
of a TA is irrelevant, for example when a TA has no argument.
Example with the TA of the instances of a class:
@{A-instances}
Here the TA has no argument and none second level type checking is
wished, so its associated check function can be the identity function
with respect to the ISA_transformers chek function type.
- Add some request examples in Evaluation.thy
- Fix typos
- Add a first implementation of a referential equivalence
for the built-ins term annotations (TA)
- Some built-ins remain as unspecified constants:
- the docitem TA offers a way to check the reference of
class instances without checking the instances type.
It must be avoided for certification
- the termrepr TA is left as an unspecified constant for now.
A major refactoring of code should be done to enable
referential equivalence for termrepr, by changing the dependency
between the Isa_DOF theory and the Assert theory.
The assert_cmd function in Assert should use the value* command
functions, which make the elaboration of the term
referenced by the TA before passing it to the evaluator
- Update the Evaluation test theory to test the referential equivalence
and expose some of current implementation limitations
- Add a warning about the docitem TA in the TermAntiquotations theory
Add a command value*
- The value* command uses the same code as the value command
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.
- For a term to be evaluated, it must not be contain
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)
- Update the ISA transformer tab to add a function
which is used for the elaboration of the term referenced by the TA.to pass
- Add a first really basic draft of the implementation
of the elaboration of the built-ins TA and of an instance class:
- For the built-ins, the term referenced by the TA is returned
as it is;
- For an instance class, the value of the instance is returned.
- Make the tag attribute global by moving it to DOF_core structure
- Add a first draft for some evaluation tests
and expose the limitations of the current implementation
in Evaluation.thy
Nicolas Méric
Burkhart Wolff
Makarius Wenzel
Burkhart Wolff
Achim D. Brucker
Nicolas Méric