ci/woodpecker/push/build Pipeline was successfulDetails
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)
ci/woodpecker/push/build Pipeline was successfulDetails
- 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
ci/woodpecker/push/build Pipeline was successfulDetails
- 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
ci/woodpecker/push/build Pipeline was successfulDetails
When defining low level invariants checking functions,
access to the monitor table might be useful.
So the table should be populated before the checking takes place.
- Isabelle uses eager evaluation, so should the elaboration of terms
which are evaluated.
The value of instances are now registered in the data tables
of Isabelle/DOF when fully elaborated, ie,
term annotation antiquotations proposed by Isabelle/DOF in
an instance value are replaced by its value before registration
in Isabelle/DOF data
A new field, input_term, stores the lazy elaboration
and is used when elaboration is not wished
(to print the original input term declared by the user, for example)
- Clean up the simplication mechanism of the internal trace attribute
(used by monitor classes)
Loosen the dependency of the implementation of value* and term*
on Toplevel.transition.
Toplevel.transition should be avoided as it has specific behaviors
like only allowing atomic transactions.
- 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
- Fix the generation of the record associated with
a class and used for the logic.
The old implementation generated a new attribute
for each attribute defined by a subclass,
even the ones that were overriding ones of the superclass.
The new implementation generates the attributes of the subclass
which are not overriding ones.
Warning:
It implies that overridden attributes in a subclass are not
new attributes added to the theory context.
So the base name of an attribute will refer to the attribute
of the last declared class where it is defined.
If ones wants to refer to atttributes, one should use
long names, even in the invariants of a subclass definition
which overrides the attribute used in the invariant.
For example,
in ~~/src/ontologies/scholarly_paper/scholarly_paper.thy:
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
status :: status <= "description"
formal_results :: "thm list"
invariant L1 :: "λσ::technical. the (level σ) > 0"
type_synonym tc = technical (* technical content *)
doc_class example = text_section +
referentiable :: bool <= True
status :: status <= "description"
short_name :: string <= "''''"
doc_class math_content = tc +
referentiable :: bool <= True
short_name :: string <= "''''"
status :: status <= "semiformal"
mcc :: "math_content_class" <= "thm"
invariant s1 :: "λ σ::math_content. ¬referentiable σ ⟶ short_name σ = ''''"
invariant s2 :: "λ σ::math_content. technical.status σ = semiformal"
The class math_content overrride the attribute status
of the class technical, by using the type synonym tc,
but the base name of this attribute refers
to the attribute of the class example where it is last defined
and not just overridden.
So in the invariant s2 of the class math_content,
we must use the long name of the attribute,
i.e. the base name "status" with its qualifier which refers
to the superclass where it is defined, the class technical.
Type synonyms as qualifiers are not yet supported.
- Qualify classes that only override attributes of their superclass
as vitual classes by adding a virtual attribute.
This attribute is used to discriminate virtual classes and generate
an adequate make function to initialize their associated record.
The implementation uses an hidden attribute (the tag_attribute)
to force the virtual class to be concrete or the logic
by having a full new record definition associated with it.
For example:
doc_class W =
a::"int" <= "1"
doc_class X = W +
a::"int" <= "2"
The class X is tagged as a virtual class and
the record make functions of the classes W and X are:
W.make W_tag_attribute W_a
X.make X_tag_attribute X_a X_tag_attribute
So a record definition is added to the theory context for each class,
even though a virtual class only overrides
attributes of its superclass.
This behavior allows us to support definitions of new default values
for attributes in the subclass, as shown in the example.
- Factorize make name components
- Use Record name components instead of strings to refer to Record
components
- 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
Makarius Wenzel
Nicolas Méric
Achim D. Brucker
Burkhart Wolff
Burkhart Wolff
Nicolas Méric