Support invariants on attributes of classes atttributes.
Example:
doc_class inv_test1 =
a :: int
doc_class inv_test2 =
b :: "inv_test1"
c:: int
invariant inv_test2 :: "c σ = 1"
invariant inv_test2' :: "a (b σ) = 2"
doc_class inv_test3 = inv_test1 +
b :: "inv_test1"
c:: int
invariant inv_test3 :: "a σ = 1"
invariant inv_test3' :: "a (b σ) = 2"
To support invariant on attributes in attributes
and invariant on attributes of the superclasses,
we check that the type of the attribute of the subclass is ground:›
ML‹
val Type(st, [ty]) = \<^typ>‹inv_test1›
val Type(st', [ty']) = \<^typ>‹'a inv_test1_scheme›
val t = ty = \<^typ>‹unit›
›
- The current implementation triggers a warning when
rejected classes are find in the monitor,
and an error if monitor_strict_checking is enable.
It follows these rules:
Inside the scope of a monitor,
all instances of classes mentioned in its accepts_clause
(the ∗‹accept-set›) have to appear in the order specified
by the regular expression.
Instances not covered by an accept-set may freely occur.
Monitors may additionally contain a rejects_clause
with a list of class-ids (the reject-list).
This allows specifying ranges of
admissible instances along the class hierarchy:
- a superclass in the reject-list and a subclass in the
accept-expression forbids instances superior to the subclass, and
- a subclass S in the reject-list and a superclass T in the
accept-list allows instances of superclasses of T to occur freely,
instances of T to occur in the specified order and forbids
instances of S.
- No message is triggered for the free classes,
but two theory options, free_class_in_monitor_checking
and free_class_in_monitor_strict_checking,
are added and can be used if we want to trigger warnings or errors,
in the case we do not want free classes inside a monitor.
- Fix the checking warning when defining a monitor,
as the monitor was added to the monitor table and then
the instance of the monitor was added to the theory.
So a monitor had the bad behavior to check itself.
By default invariants checking generates warnings.
If invariants_strict_checking theory option is enabled,
the checking generates errors.
- Update 2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
and 2020-iFM-CSP/paper.thy to pass the checking of
the low level invariant checking function "check"
in scholarly_paper.thy,
which checks that the instances in a sequence of the same class
have a growing level.
For a sequence:
section*[intro::introduction]‹ Introduction ›
text*[introtext::introduction, level = "Some 1"]‹...›
introtext must have a level >= than intro.
- Bypass the checking of high-level invariants
when the class default_cid = "text",
the top (default) document class.
We want the class default_cid to stay abstract
and not have the capability to be defined with attribute,
invariants, etc.
Hence this bypass handles docitem without a class associated,
for example when you just want a document element to be referenceable
without using the burden of ontology classes.
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close>
The functions get_doc_class_global and get_doc_class_local trigger
an error when the class is "text" (default_cid),
then the functions like check_invariants which use it will fail
if the checking is enabled by default for all the theories.
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