forked from Isabelle_DOF/Isabelle_DOF
Enable invariants checking everywhere
By default invariants checking generates warnings.
if invariants_strict_checking theory option is enabled,
the checking generates errors.
Errors to resolve:
- Option type in invariant:
See src/ontologies/scholarly_paper/scholarly_paper.thy:133
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
status :: status <= "description"
formal_results :: "thm list"
invariant L1 :: "the (level σ) > 0"
The attribute L1 uses "the" to project the level value
but the default value is None:
See src/ontologies/scholarly_paper/scholarly_paper.thy:69
doc_class text_section = text_element +
main_author :: "author option" <= None
fixme_list :: "string list" <= "[]"
level :: "int option" <= "None"
It generates an error in src/ontologies/CENELEC_50128/CENELEC_50128.thy
for the Definition* commands, for which the level is not defined.
It triggers an error because "the None" triggers an error.
Get rid of the option type?
The value None is used in the check function
in examples/scholarly_paper/2020-iFM-CSP/paper.thy to check
that a subsequent instance of the same class has a level >= than
the previous instance of the same class.
Update this function?
- What to do with the checking done in scholarly_paper (see check function)
which use low level invariant to check the attributes?
Migrate to High level invariant?
If we change the default value of the level attribute in the text_lement
class from "None" to "Some 0" then check function in scholarly_paper
is triggered in examples/scholarly_paper/2020-iFM-CSP/paper.thy
for the introduction instance "introtext" line 55 and generates
a checking error.
It comes from the fact that the previous instance introheader line 54
is a section*, and then has a default value level of 1.
Then, if the default value of the level attribute in the text_element
is put to Some 0, the low level checking invariant function "check" in
scholarly_paper triggers an error, because the "check" function
checks that the instances in a sequence of the same class
have a growing level.
for a sequence: [("scholarly_paper.introduction", "introheader")
, ("scholarly_paper.introduction", "introtext")]
introtext must have a level >= than introheader.
Same issue with
the examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy
theory.
- Bypass 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.
A quick and dirty fix is proposed to pass the compilation, but must be revised.
See the diff.
This commit is contained in:
Nicolas Méric
parent
0b2d28b547
commit
9bc493250f
|
|
@ -74,7 +74,7 @@ abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''I
|
|||
\<close>
|
||||
|
||||
section*[intro::introduction]\<open> Introduction \<close>
|
||||
text*[introtext::introduction]\<open>
|
||||
text*[introtext::introduction, level = "Some 1"]\<open>
|
||||
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
|
||||
most pervasive challenge in the digitization of knowledge and its
|
||||
propagation. This challenge incites numerous research efforts
|
||||
|
|
@ -123,7 +123,7 @@ declare_reference*[ontomod::text_section]
|
|||
declare_reference*[ontopide::text_section]
|
||||
declare_reference*[conclusion::text_section]
|
||||
(*>*)
|
||||
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||
text*[plan::introduction, level="Some 1"]\<open> The plan of the paper is follows: we start by introducing the underlying
|
||||
Isabelle system (@{text_section (unchecked) \<open>bgrnd\<close>}) followed by presenting the
|
||||
essentials of \<^isadof> and its ontology language (@{text_section (unchecked) \<open>isadof\<close>}).
|
||||
It follows @{text_section (unchecked) \<open>ontomod\<close>}, where we present three application
|
||||
|
|
@ -133,7 +133,7 @@ conclusions and discuss related work in @{text_section (unchecked) \<open>conclu
|
|||
|
||||
section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"]
|
||||
\<open> Background: The Isabelle System \<close>
|
||||
text*[background::introduction]\<open>
|
||||
text*[background::introduction, level="Some 1"]\<open>
|
||||
While Isabelle is widely perceived as an interactive theorem prover
|
||||
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
|
||||
would like to emphasize the view that Isabelle is far more than that:
|
||||
|
|
@ -162,7 +162,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
|
|||
asynchronous communication between the Isabelle system and
|
||||
the IDE (right-hand side). \<close>
|
||||
|
||||
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
|
||||
text*[blug::introduction, level="Some 1"]\<open> The Isabelle system architecture shown in @{figure \<open>architecture\<close>}
|
||||
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
|
||||
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
|
||||
resides in the SML structure \<^ML_structure>\<open>Context\<close>. This structure provides a kind of container called
|
||||
|
|
@ -194,7 +194,7 @@ For the antiquotation \inlineisar+\at{value "fac 5"}+ we assume the usual defin
|
|||
\inlineisar+fac+ in HOL.
|
||||
\<close>
|
||||
|
||||
text*[anti]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being
|
||||
text*[anti::introduction, level = "Some 1"]\<open> Thus, antiquotations can refer to formal content, can be type-checked before being
|
||||
displayed and can be used for calculations before actually being typeset. When editing,
|
||||
Isabelle's PIDE offers auto-completion and error-messages while typing the above
|
||||
\<^emph>\<open>semi-formal\<close> content. \<close>
|
||||
|
|
|
|||
|
|
@ -52,7 +52,7 @@ abstract*[abs, keywordlist="[\<open>Shallow Embedding\<close>,\<open>Process-Alg
|
|||
\<close>
|
||||
text\<open>\<close>
|
||||
section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\<open> Introduction \<close>
|
||||
text*[introtext::introduction]\<open>
|
||||
text*[introtext::introduction, level="Some 1"]\<open>
|
||||
Communicating Sequential Processes (\<^csp>) is a language
|
||||
to specify and verify patterns of interaction of concurrent systems.
|
||||
Together with CCS and LOTOS, it belongs to the family of \<^emph>\<open>process algebras\<close>.
|
||||
|
|
@ -154,7 +154,7 @@ processes \<open>Skip\<close> (successful termination) and \<open>Stop\<close> (
|
|||
\<open>\<T>(Skip) = \<T>(Stop) = {[]}\<close>.
|
||||
Note that the trace sets, representing all \<^emph>\<open>partial\<close> history, is in general prefix closed.\<close>
|
||||
|
||||
text*[ex1::math_example, status=semiformal] \<open>
|
||||
text*[ex1::math_example, status=semiformal, level="Some 1"] \<open>
|
||||
Let two processes be defined as follows:
|
||||
|
||||
\<^enum> \<open>P\<^sub>d\<^sub>e\<^sub>t = (a \<rightarrow> Stop) \<box> (b \<rightarrow> Stop)\<close>
|
||||
|
|
@ -354,7 +354,7 @@ Roscoe and Brooks @{cite "Roscoe1992AnAO"} finally proposed another ordering, ca
|
|||
that completeness could at least be assured for read-operations. This more complex ordering
|
||||
is based on the concept \<^emph>\<open>refusals after\<close> a trace \<open>s\<close> and defined by \<open>\<R> P s \<equiv> {X | (s, X) \<in> \<F> P}\<close>.\<close>
|
||||
|
||||
Definition*[process_ordering, short_name="''process ordering''"]\<open>
|
||||
Definition*[process_ordering, level= "Some 2", short_name="''process ordering''"]\<open>
|
||||
We define \<open>P \<sqsubseteq> Q \<equiv> \<psi>\<^sub>\<D> \<and> \<psi>\<^sub>\<R> \<and> \<psi>\<^sub>\<M> \<close>, where
|
||||
\<^enum> \<open>\<psi>\<^sub>\<D> = \<D> P \<supseteq> \<D> Q \<close>
|
||||
\<^enum> \<open>\<psi>\<^sub>\<R> = s \<notin> \<D> P \<Rightarrow> \<R> P s = \<R> Q s\<close>
|
||||
|
|
@ -530,10 +530,10 @@ To handle termination better, we added two new processes \<open>CHAOS\<^sub>S\<^
|
|||
\<close>
|
||||
|
||||
(*<*) (* a test ...*)
|
||||
text*[X22 ::math_content ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||
text*[X32::"definition", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X42]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X52::"definition"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
text*[X22 ::math_content, level="Some 2" ]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||
text*[X32::"definition", level="Some 2", mcc=defn]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X42, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X52::"definition", level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
|
||||
text\<open> The \<open>RUN\<close>-process defined @{math_content X22} represents the process that accepts all
|
||||
events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in two variants shown in
|
||||
|
|
@ -541,11 +541,11 @@ events, but never stops nor deadlocks. The \<open>CHAOS\<close>-process comes in
|
|||
stops or accepts any offered event, whereas \<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\<close> can additionally terminate.\<close>
|
||||
(*>*)
|
||||
|
||||
Definition*[X2]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||
Definition*[X3]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X4]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
|
||||
Definition*[X5]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<close>
|
||||
Definition*[X6]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<close>
|
||||
Definition*[X2, level="Some 2"]\<open>\<open>RUN A \<equiv> \<mu> X. \<box> x \<in> A \<rightarrow> X\<close> \<close>
|
||||
Definition*[X3, level="Some 2"]\<open>\<open>CHAOS A \<equiv> \<mu> X. (STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close> \<close>
|
||||
Definition*[X4, level="Some 2"]\<open>\<open>CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. (SKIP \<sqinter> STOP \<sqinter> (\<box> x \<in> A \<rightarrow> X))\<close>\<close>
|
||||
Definition*[X5, level="Some 2"]\<open>\<open>DF A \<equiv> \<mu> X. (\<sqinter> x \<in> A \<rightarrow> X)\<close> \<close>
|
||||
Definition*[X6, level="Some 2"]\<open>\<open>DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \<equiv> \<mu> X. ((\<sqinter> x \<in> A \<rightarrow> X) \<sqinter> SKIP)\<close> \<close>
|
||||
|
||||
text\<open>In the following, we denote \<open> \<R>\<P> = {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\<close>.
|
||||
All five reference processes are divergence-free.
|
||||
|
|
@ -607,16 +607,16 @@ handled separately. One contribution of our work is establish their precise rela
|
|||
the Failure/Divergence Semantics of \<^csp>.\<close>
|
||||
|
||||
(* bizarre: Definition* does not work for this single case *)
|
||||
text*[X10::"definition"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<close>
|
||||
text*[X10::"definition", level="Some 2"]\<open> \<open>deadlock\<^sub>-free P \<equiv> DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \<sqsubseteq>\<^sub>\<F> P\<close> \<close>
|
||||
|
||||
text\<open>\<^noindent> A process \<open>P\<close> is deadlock-free if and only if after any trace \<open>s\<close> without \<open>\<surd>\<close>, the union of \<open>\<surd>\<close>
|
||||
and all events of \<open>P\<close> can never be a refusal set associated to \<open>s\<close>, which means that \<open>P\<close> cannot
|
||||
be deadlocked after any non-terminating trace.
|
||||
\<close>
|
||||
|
||||
Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>"]
|
||||
Theorem*[T1, short_name="\<open>DF definition captures deadlock-freeness\<close>", level="Some 2"]
|
||||
\<open> \hfill \break \<open>deadlock_free P \<longleftrightarrow> (\<forall>s\<in>\<T> P. tickFree s \<longrightarrow> (s, {\<surd>}\<union>events_of P) \<notin> \<F> P)\<close> \<close>
|
||||
Definition*[X11]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<close>
|
||||
Definition*[X11, level="Some 2"]\<open> \<open>livelock\<^sub>-free P \<equiv> \<D> P = {} \<close> \<close>
|
||||
|
||||
text\<open> Recall that all five reference processes are livelock-free.
|
||||
We also have the following lemmas about the
|
||||
|
|
@ -630,7 +630,7 @@ text\<open>
|
|||
Finally, we proved the following theorem that confirms the relationship between the two vital
|
||||
properties:
|
||||
\<close>
|
||||
Theorem*[T2, short_name="''DF implies LF''"]
|
||||
Theorem*[T2, short_name="''DF implies LF''", level="Some 2"]
|
||||
\<open> \<open>deadlock_free P \<longrightarrow> livelock_free P\<close> \<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -797,7 +797,7 @@ This normal form is closed under deterministic and communication operators.
|
|||
The advantage of this format is that we can mimick the well-known product automata construction
|
||||
for an arbitrary number of synchronized processes under normal form.
|
||||
We only show the case of the synchronous product of two processes: \<close>
|
||||
text*[T3::"theorem", short_name="\<open>Product Construction\<close>"]\<open>
|
||||
text*[T3::"theorem", short_name="\<open>Product Construction\<close>", level="Some 2"]\<open>
|
||||
Parallel composition translates to normal form:
|
||||
@{cartouche [display,indent=5]\<open>(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>1,\<upsilon>\<^sub>1\<rbrakk> \<sigma>\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>\<^sub>2,\<upsilon>\<^sub>2\<rbrakk> \<sigma>\<^sub>2) =
|
||||
P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2). \<tau>\<^sub>1 \<sigma>\<^sub>1 \<inter> \<tau>\<^sub>2 \<sigma>\<^sub>2 , \<lambda>(\<sigma>\<^sub>1,\<sigma>\<^sub>2).\<lambda>e.(\<upsilon>\<^sub>1 \<sigma>\<^sub>1 e, \<upsilon>\<^sub>2 \<sigma>\<^sub>2 e)\<rbrakk> (\<sigma>\<^sub>1,\<sigma>\<^sub>2)\<close>}
|
||||
|
|
@ -817,7 +817,7 @@ states via the closure \<open>\<RR>\<close>, which is defined inductively over:
|
|||
Thus, normalization leads to a new characterization of deadlock-freeness inspired
|
||||
from automata theory. We formally proved the following theorem:\<close>
|
||||
|
||||
text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>"]
|
||||
text*[T4::"theorem", short_name="\<open>DF vs. Reacheability\<close>", level="Some 2"]
|
||||
\<open> If each reachable state \<open>s \<in> (\<RR> \<tau> \<upsilon>)\<close> has outgoing transitions,
|
||||
the \<^csp> process is deadlock-free:
|
||||
@{cartouche [display,indent=10] \<open>\<forall>\<sigma> \<in> (\<RR> \<tau> \<upsilon> \<sigma>\<^sub>0). \<tau> \<sigma> \<noteq> {} \<Longrightarrow> deadlock_free (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\<lbrakk>\<tau>,\<upsilon>\<rbrakk> \<sigma>\<^sub>0)\<close>}
|
||||
|
|
|
|||
|
|
@ -1041,10 +1041,11 @@ text\<open>
|
|||
Ontological classes as described so far are too liberal in many situations.
|
||||
There is a first high-level syntax implementation for class invariants.
|
||||
These invariants can be checked when an instance of the class is defined.
|
||||
To enable the checking of the invariants, the \<^boxed_theory_text>\<open>invariants_checking\<close>
|
||||
To enable the strict checking of the invariants,
|
||||
the \<^boxed_theory_text>\<open>invariants_strict_checking\<close>
|
||||
theory attribute must be set:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
declare[[invariants_checking = true]]\<close>}
|
||||
declare[[invariants_strict_checking = true]]\<close>}
|
||||
|
||||
For example, let's define the following two classes:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
|
|
@ -1104,6 +1105,12 @@ text\<open>
|
|||
All specified constraints are already checked in the IDE of \<^dof> while editing.
|
||||
The invariant \<^boxed_theory_text>\<open>author_finite\<close> enforces that the user sets the
|
||||
\<^boxed_theory_text>\<open>authored_by\<close> set.
|
||||
The invariants \<^theory_text>\<open>author_finite\<close> and \<^theory_text>\<open>establish_defined\<close> can not be checked directly
|
||||
and need a little help.
|
||||
We can set the \<open>invariants_checking_with_tactics\<close> theory attribute to help the checking.
|
||||
It will enable a basic tactic, using unfold and auto:
|
||||
@{boxed_theory_text [display]\<open>
|
||||
declare[[invariants_checking_with_tactics = true]]\<close>}
|
||||
There are still some limitations with this high-level syntax.
|
||||
For now, the high-level syntax does not support monitors (see \<^technical>\<open>sec:monitors\<close>).
|
||||
For example, one would like to delay a final error message till the
|
||||
|
|
|
|||
|
|
@ -813,8 +813,8 @@ fun print_doc_class_tree ctxt P T =
|
|||
val (strict_monitor_checking, strict_monitor_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>strict_monitor_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking, invariants_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking\<close> (K false);
|
||||
val (invariants_strict_checking, invariants_strict_checking_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_strict_checking\<close> (K false);
|
||||
|
||||
val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup)
|
||||
= Attrib.config_bool \<^binding>\<open>invariants_checking_with_tactics\<close> (K false);
|
||||
|
|
@ -825,7 +825,7 @@ end (* struct *)
|
|||
\<close>
|
||||
|
||||
setup\<open>DOF_core.strict_monitor_checking_setup
|
||||
#> DOF_core.invariants_checking_setup
|
||||
#> DOF_core.invariants_strict_checking_setup
|
||||
#> DOF_core.invariants_checking_with_tactics_setup\<close>
|
||||
|
||||
section\<open> Syntax for Term Annotation Antiquotations (TA)\<close>
|
||||
|
|
@ -948,6 +948,7 @@ structure ISA_core =
|
|||
struct
|
||||
|
||||
fun err msg pos = error (msg ^ Position.here pos);
|
||||
fun warn msg pos = warning (msg ^ Position.here pos);
|
||||
|
||||
fun check_path check_file ctxt dir (name, pos) =
|
||||
let
|
||||
|
|
@ -1600,11 +1601,12 @@ fun check_invariants thy oid =
|
|||
end
|
||||
fun check_invariants' ((inv_name, pos), term) =
|
||||
let val ctxt = Proof_Context.init_global thy
|
||||
val trivial_true = \<^term>\<open>True\<close> |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
|
||||
val evaluated_term = value ctxt term
|
||||
handle ERROR e =>
|
||||
if (String.isSubstring "Wellsortedness error" e)
|
||||
andalso (Config.get_global thy DOF_core.invariants_checking_with_tactics)
|
||||
then (warning("Invariants checking uses proof tactics");
|
||||
then (warning("Invariants checking uses proof tactics");
|
||||
let val prop_term = HOLogic.mk_Trueprop term
|
||||
val thms = Proof_Context.get_thms ctxt (inv_name ^ def_suffixN)
|
||||
(* Get the make definition (def(1) of the record) *)
|
||||
|
|
@ -1614,22 +1616,32 @@ fun check_invariants thy oid =
|
|||
(K ((unfold_tac ctxt thms') THEN (auto_tac ctxt)))
|
||||
|> Thm.close_derivation \<^here>
|
||||
handle ERROR e =>
|
||||
ISA_core.err ("Invariant "
|
||||
let
|
||||
val msg_intro = "Invariant "
|
||||
^ inv_name
|
||||
^ " failed to be checked using proof tactics"
|
||||
^ " with error: "
|
||||
^ e) pos
|
||||
^ " with error:\n"
|
||||
in
|
||||
if Config.get_global thy DOF_core.invariants_strict_checking
|
||||
then ISA_core.err (msg_intro ^ e) pos
|
||||
else (ISA_core.warn (msg_intro ^ e) pos; trivial_true) end
|
||||
(* If Goal.prove does not fail, then the evaluation is considered True,
|
||||
else an error is triggered by Goal.prove *)
|
||||
in @{term True} end)
|
||||
else ISA_core.err ("Fail to check invariant "
|
||||
else
|
||||
let val msg_intro = "Fail to check invariant "
|
||||
^ inv_name
|
||||
^ ". Try to activate invariants_checking_with_tactics.") pos
|
||||
^ ". Try to activate invariants_checking_with_tactics\n"
|
||||
in if Config.get_global thy DOF_core.invariants_strict_checking
|
||||
then ISA_core.err (msg_intro ^ e) pos
|
||||
else (ISA_core.warn (msg_intro ^ e) pos; term) end
|
||||
in (if evaluated_term = \<^term>\<open>True\<close>
|
||||
then ((inv_name, pos), term)
|
||||
else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos)
|
||||
else if Config.get_global thy DOF_core.invariants_strict_checking
|
||||
then ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos
|
||||
else ((inv_name, pos), term))
|
||||
end
|
||||
val _ = map check_invariants' inv_and_apply_list
|
||||
val _ = map check_invariants' inv_and_apply_list
|
||||
in thy end
|
||||
|
||||
fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos doc_attrs thy =
|
||||
|
|
@ -1639,20 +1651,19 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
val cid_long = check_classref is_monitor cid_pos thy
|
||||
val default_cid = cid_long = DOF_core.default_cid
|
||||
val vcid = case cid_pos of NONE => NONE
|
||||
| SOME (cid,_) => if (DOF_core.is_virtual cid thy)
|
||||
then SOME (DOF_core.parse_cid_global thy cid)
|
||||
else NONE
|
||||
val value_terms = if (cid_long = DOF_core.default_cid)
|
||||
val value_terms = if default_cid
|
||||
then let
|
||||
val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
|
||||
val undefined_value = Free ("Undefined_Value", \<^Type>\<open>unit\<close>)
|
||||
in (undefined_value, undefined_value) end
|
||||
(*
|
||||
Handle initialization of 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>
|
||||
*)
|
||||
(* Handle initialization of 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> *)
|
||||
else let
|
||||
val defaults_init = create_default_object thy cid_long
|
||||
fun conv (na, _(*ty*), term) =(Binding.name_of na, Binding.pos_of na, "=", term);
|
||||
|
|
@ -1684,9 +1695,15 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do
|
|||
o Context.Theory) thy; thy)
|
||||
else thy)
|
||||
|> (fn thy => (check_inv thy; thy))
|
||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
||||
then check_invariants thy oid
|
||||
else thy)
|
||||
(* Bypass 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> *)
|
||||
|> (fn thy => if default_cid then thy else check_invariants thy oid)
|
||||
end
|
||||
|
||||
end (* structure Docitem_Parser *)
|
||||
|
|
@ -1870,9 +1887,7 @@ fun update_instance_command (((oid:string,pos),cid_pos),
|
|||
in
|
||||
thy |> DOF_core.update_value_global oid def_trans_input_term def_trans_value
|
||||
|> check_inv
|
||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
||||
then Value_Command.Docitem_Parser.check_invariants thy oid
|
||||
else thy)
|
||||
|> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
|
||||
end
|
||||
|
||||
|
||||
|
|
@ -1932,9 +1947,7 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
|
|||
in thy |> (fn thy => (check_lazy_inv thy; thy))
|
||||
|> update_instance_command args
|
||||
|> (fn thy => (check_inv thy; thy))
|
||||
|> (fn thy => if Config.get_global thy DOF_core.invariants_checking = true
|
||||
then Value_Command.Docitem_Parser.check_invariants thy oid
|
||||
else thy)
|
||||
|> (fn thy => Value_Command.Docitem_Parser.check_invariants thy oid)
|
||||
|> delete_monitor_entry
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -69,7 +69,8 @@ which we formalize into:\<close>
|
|||
doc_class text_section = text_element +
|
||||
main_author :: "author option" <= None
|
||||
fixme_list :: "string list" <= "[]"
|
||||
level :: "int option" <= "None"
|
||||
(*level :: "int option" <= "None"*)
|
||||
level :: "int option" <= "Some 0"
|
||||
(* this attribute enables doc-notation support section* etc.
|
||||
we follow LaTeX terminology on levels
|
||||
part = Some -1
|
||||
|
|
@ -134,7 +135,8 @@ doc_class technical = text_section +
|
|||
definition_list :: "string list" <= "[]"
|
||||
status :: status <= "description"
|
||||
formal_results :: "thm list"
|
||||
invariant L1 :: "the (level \<sigma>) > 0"
|
||||
(*invariant L1 :: "(case (level \<sigma>) of None \<Rightarrow> 1 | Some x \<Rightarrow> x) > 0"*)
|
||||
invariant L1 :: " the (level \<sigma>) > 0"
|
||||
|
||||
type_synonym tc = technical (* technical content *)
|
||||
|
||||
|
|
@ -443,6 +445,9 @@ fun group f g cidS [] = []
|
|||
|group f g cidS (a::S) = case find_first (f a) cidS of
|
||||
NONE => [a] :: group f g cidS S
|
||||
| SOME cid => let val (pref,suff) = chop_prefix (g cid) S
|
||||
val _ = writeln("In group a: " ^ \<^make_string> a)
|
||||
val _ = writeln("In group pref: " ^ \<^make_string> pref)
|
||||
val _ = writeln("In group suff: " ^ \<^make_string> suff)
|
||||
in (a::pref)::(group f g cidS suff) end;
|
||||
|
||||
fun partition ctxt cidS trace =
|
||||
|
|
@ -457,13 +462,16 @@ in
|
|||
|
||||
fun check ctxt cidS mon_id pos_opt =
|
||||
let val trace = AttributeAccess.compute_trace_ML ctxt mon_id pos_opt @{here}
|
||||
val _ = writeln("In check trace: " ^ \<^make_string> trace)
|
||||
val _ = writeln("In check cidS: " ^ \<^make_string> cidS)
|
||||
val groups = partition (Context.proof_of ctxt) cidS trace
|
||||
val _ = writeln("In check groups: " ^ \<^make_string> groups)
|
||||
fun get_level_raw oid = ISA_core.compute_attr_access ctxt "level" oid NONE @{here};
|
||||
fun get_level oid = dest_option (snd o HOLogic.dest_number) (get_level_raw (oid));
|
||||
fun check_level_hd a = case (get_level (snd a)) of
|
||||
NONE => error("Invariant violation: leading section" ^ snd a ^
|
||||
" must have lowest level")
|
||||
| SOME X => X
|
||||
| SOME X => (writeln("In check_level level: " ^ \<^make_string> X ^ ", a: " ^ \<^make_string> a);X)
|
||||
fun check_group_elem level_hd a = case (get_level (snd a)) of
|
||||
NONE => true
|
||||
| SOME y => if level_hd <= y then true
|
||||
|
|
@ -489,7 +497,7 @@ setup\<open> let val cidS = ["scholarly_paper.introduction","scholarly_paper.tec
|
|||
ctxt cidS moni_oid NONE;
|
||||
true)
|
||||
in DOF_core.update_class_invariant "scholarly_paper.article" body end\<close>
|
||||
|
||||
|
||||
ML\<open> \<close>
|
||||
|
||||
section\<open>Miscelleous\<close>
|
||||
|
|
|
|||
|
|
@ -12,7 +12,7 @@ text\<open>
|
|||
theory attribute must be set:\<close>
|
||||
|
||||
|
||||
declare[[invariants_checking = true]]
|
||||
declare[[invariants_strict_checking = true]]
|
||||
|
||||
text\<open>For example, let's define the following two classes:\<close>
|
||||
|
||||
|
|
@ -124,7 +124,6 @@ update_instance*[introduction2::introduction
|
|||
|
||||
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
|
||||
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
|
||||
|
||||
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
|
||||
|
||||
text\<open>Then we can evaluate expressions with instances:\<close>
|
||||
|
|
@ -144,6 +143,6 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
|
|||
|
||||
declare[[invariants_checking_with_tactics = false]]
|
||||
|
||||
declare[[invariants_checking = false]]
|
||||
declare[[invariants_strict_checking = false]]
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue