Commit Graph

448 Commits

Author SHA1 Message Date
Achim D. Brucker 43ccaf43f7 Refactoring of session setup. 2023-02-19 13:06:00 +00:00
Nicolas Méric 848ce311e2 Re-add name field to onto_class
ci/woodpecker/push/build Pipeline failed Details
To keep the abstract syntax information
of the onto_class name, re-add it to the field
of the onto_class structure
2023-02-17 12:56:45 +01:00
Nicolas Méric 6115f0de4a Some cleanup
ci/woodpecker/push/build Pipeline failed Details
2023-02-17 11:35:51 +01:00
Nicolas Méric bdfea3ddb1 Some cleanup
ci/woodpecker/push/build Pipeline failed Details
2023-02-17 09:08:34 +01:00
Nicolas Méric 9de18b148a Remove some instance and onto_class datatypes entries
ci/woodpecker/push/build Pipeline failed Details
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
2023-02-16 10:41:04 +01:00
Nicolas Méric 1459b8cfc3 Use name space markup for onto_class entries reporting 2023-02-16 10:07:56 +01:00
Nicolas Méric 234ff18ec0 Use a name space for Onto Classes
ci/woodpecker/push/build Pipeline failed Details
- Use a name space table to store ontological class objects
- Remove docclass_tab table and accesses
2023-02-15 17:49:29 +01:00
Nicolas Méric 55690bba33 Homogenize instance getters names
ci/woodpecker/push/build Pipeline failed Details
2023-02-14 09:21:11 +01:00
Nicolas Méric 93509ab17d Update file to match the new name space implementation 2023-02-14 09:20:21 +01:00
Nicolas Méric 1e09598d81 Fix typo 2023-02-14 09:20:21 +01:00
Nicolas Méric e01ec9fc21 Use a name space for ML invariants
- 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
2023-02-14 09:20:13 +01:00
Nicolas Méric 7c16d02979 Use a name space for Isabelle_DOF transformers
ci/woodpecker/push/build Pipeline failed Details
- Use a name space table to store Isabelle_DOF transformers objects
- Remove ISA_transformer_tab table and accesses
2023-02-12 16:49:53 +01:00
Nicolas Méric 4a77347e40 Simplify reporting of monitors
ci/woodpecker/push/build Pipeline failed Details
2023-02-12 11:20:13 +01:00
Nicolas Méric 2398fc579a Use name space markup for instances entries reporting
ci/woodpecker/push/build Pipeline failed Details
- 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
2023-02-11 22:48:11 +01:00
Nicolas Méric 821eefb230 Fix some markups
ci/woodpecker/push/build Pipeline failed Details
2023-02-10 15:23:23 +01:00
Nicolas Méric 9b51844fad Use a name space for monitors infos
ci/woodpecker/push/build Pipeline failed Details
- 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
2023-02-10 13:07:17 +01:00
Nicolas Méric c440f9628f Fix typo
ci/woodpecker/push/build Pipeline failed Details
2023-02-09 16:40:05 +01:00
Nicolas Méric 5b3086bbe5 Use a name space for docitems (instances)
ci/woodpecker/push/build Pipeline failed Details
- 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*.
2023-02-09 16:07:16 +01:00
Nicolas Méric 7c0d2cee55 Add docitem_name text and ML antiquotations
Add the possibility to reference the name of instances
in text and ML code
2023-01-30 07:43:44 +01:00
Nicolas Méric 7c6150affa Make input_term available with theory option
ci/woodpecker/push/build Pipeline failed Details
The raw value term of docitems is now processed and
available when setting the theory attribute object_value_debug
2023-01-27 15:09:34 +01:00
Nicolas Méric ad4ad52b4e Avoid reporting duplication when possible
ci/woodpecker/push/build Pipeline failed Details
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)
2023-01-27 10:32:38 +01:00
Nicolas Méric ba8227e6ab Cleanup and add position to docitem ML antiqutation
ci/woodpecker/push/build Pipeline failed Details
2023-01-26 09:43:51 +01:00
Nicolas Méric 20b0af740d Update meta args syntax and ML* command
ci/woodpecker/push/build Pipeline failed Details
- 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
2023-01-23 09:03:59 +01:00
Nicolas Méric 1379f8a671 Add test of invariants of an inherited attribute of an attribute
ci/woodpecker/push/build Pipeline failed Details
2023-01-20 09:41:19 +01:00
Achim D. Brucker 8fdaafa295 Experimental session with enabled proof objects: Isabelle_DOF-Proofs.
ci/woodpecker/push/build Pipeline failed Details
2023-01-19 22:00:53 +00:00
Nicolas Méric 2b1a9d009e Add support invariants on attributes of attributes
ci/woodpecker/push/build Pipeline was successful Details
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›
›
2023-01-13 08:27:26 +01:00
Nicolas Méric cd758d2c44 Update accepts clause syntax
ci/woodpecker/push/build Pipeline was successful Details
2023-01-12 12:18:58 +01:00
Nicolas Méric 8496963fec Add comment for term_ and value_ ML antiquoatations
ci/woodpecker/push/build Pipeline was successful Details
2023-01-11 14:49:29 +01:00
Nicolas Méric 17ec11b297 Explain evaluator option syntax for value_ text antiquotation
ci/woodpecker/push/build Pipeline was successful Details
2023-01-09 15:13:23 +01:00
Nicolas Méric a96e17abf3 Add term_ and value_ ML antiquotations
ci/woodpecker/push/build Pipeline was successful Details
2023-01-09 11:34:40 +01:00
Nicolas Méric 74b60e47d5 Document term _ and value_ text antiquotations
ci/woodpecker/push/build Pipeline was successful Details
2022-12-22 16:50:53 +01:00
Nicolas Méric a42dd4ea6c Implement term _ and value_ text antiquotations
ci/woodpecker/push/build Pipeline was successful Details
2022-12-22 10:55:03 +01:00
Nicolas Méric b162a24749 Comment out hack for Assumption in scholarly_paper
ci/woodpecker/push/build Pipeline was successful Details
2022-12-22 09:55:46 +01:00
Nicolas Méric a9432c7b52 Add a theory attribute to disable invariants checking 2022-12-22 07:53:42 +01:00
Nicolas Méric 9f28d4949e Limit scope of free class checking in examples 2022-12-22 07:32:37 +01:00
Nicolas Méric 885c23a138 Explain lazy and eager invariants 2022-12-22 07:14:29 +01:00
Nicolas Méric a589d4cd47 Update the position of the default class
The default class must stay abtract and as such
can not have a position.
Set its position to Position.none
2022-12-21 18:32:07 +01:00
Burkhart Wolff e1f143d151 Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline failed Details
2022-12-21 11:35:05 +01:00
Burkhart Wolff fd60cf2312 attempt to add category 'assumption' 2022-12-21 11:34:34 +01:00
Nicolas Méric 73dfcd6c1e Implement rejects clause
ci/woodpecker/push/build Pipeline was successful Details
- 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.
2022-12-21 10:09:17 +01:00
Nicolas Méric c0afe1105e Enable high-level invariants checking everywhere
ci/woodpecker/push/build Pipeline was successful Details
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.
2022-12-20 16:31:09 +01:00
Burkhart Wolff e414b97afb rephrasing invariant for core scholarly_paper classes
ci/woodpecker/push/build Pipeline was successful Details
2022-12-19 12:14:30 +01:00
Nicolas Méric 0b2d28b547 Update error message for invariant checking
ci/woodpecker/push/build Pipeline was successful Details
2022-12-09 16:11:57 +01:00
Nicolas Méric 312734afbd Update Attributes examples
ci/woodpecker/push/build Pipeline was successful Details
2022-12-09 15:12:38 +01:00
Burkhart Wolff 8cee80d78e advanced example on trace-attribute term-antiquotations
ci/woodpecker/push/build Pipeline was successful Details
2022-12-07 16:01:38 +01:00
Makarius Wenzel ec0d525426 Tuned messages, following Isabelle/d6a2a8bc40e1
ci/woodpecker/push/build Pipeline was successful Details
2022-12-05 15:21:26 +01:00
Makarius Wenzel 791990039b Tuned messages and options, following Isabelle/c7f3e94fce7b
ci/woodpecker/push/build Pipeline was successful Details
2022-12-05 12:37:59 +01:00
Makarius Wenzel 78d61390fe Prefer Isar command, instead of its underlying ML implementation 2022-12-05 11:50:12 +01:00
Makarius Wenzel ffcf1f3240 Add missing file (amending 5471d873a9)
ci/woodpecker/push/build Pipeline was successful Details
2022-12-04 19:26:28 +01:00
Makarius Wenzel 5471d873a9 Isabelle/Scala module within session context supports document_build = "dof" without component setup
ci/woodpecker/push/build Pipeline failed Details
2022-12-04 19:13:08 +01:00