Id in instance datatype entry
and name, id and thy_name in onto_class datatype entry are now
useless, as this information is given by the name space.
Remove them
- Use a name space table to store ML inariants objects
- Remove docclass_inv_tab, docclass_eager_inv_tab,
and docclass_lazy_inv_tab tables and accesses
- Name spaces offer the possibility to make reporting
by embedding entries position. Use this possibility
for instances (docitems) reporting
- Position and theory entries in an Instance record are now
useless, as this information is given by the name space.
Remove them
- Use a name space table to store monitor infos objects
- Remove monitor_tab table, as monitor infos were moved
to the name space table
- It offers the possibility to define scoped versions
of monitors
- Use a name space table to store docitem (instance) objects
- Remove docobj table, as instances were moved to the name space table
- It offers the possibility to define scoped versions
of docitems declaration
for text* (and others docitems definition command like value*)
and declare_reference*.
Avoid reporting for meta arguments attributes of isabelle_DOF
commands and for text input of text*
The last reporting duplication not resolved comes
from the document_command command in Isa_DOF,
which parses the meta arguments twice,
one time for the creation of the docitem
with create_and_check_docitem which will add reporting
for the attributes value
(see conv_attrs whichs calls Syntax.read_term_global,
which iwill add reporting)
and the other for the document output
with document_output which also adds reporting
(see meta_args_2_latex which calls
(Syntax.check_term ctxt o Syntax.parse_term ctxt) with
ltx_of_markup and Syntax.parse_term also adds reporting)
- Make optional meta arguments completely optional
- Make meta arguments context of ML* available in its ML context
- Make meta arguments of ML* mandatory to mimic text*.
Without meta arguments, its behavior is already captured by
the ML command
ci/woodpecker/push/build Pipeline was successfulDetails
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›
›
ci/woodpecker/push/build Pipeline was successfulDetails
- 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.
ci/woodpecker/push/build Pipeline was successfulDetails
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.
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
Nicolas Méric
Makarius Wenzel
Achim D. Brucker
Burkhart Wolff