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›
›
Pierre Derathe
Pierre Derathe
Pierre Derathe
Nicolas Méric
Pierre Derathe
Achim D. Brucker