diff --git a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy index dec9a27..56f9a19 100644 --- a/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018-cicm-isabelle_dof-applications/IsaDofApplications.thy @@ -74,7 +74,7 @@ abstract*[abs::abstract, keywordlist="[''Ontology'',''Ontological Modeling'',''I \ section*[intro::introduction]\ Introduction \ -text*[introtext::introduction]\ +text*[introtext::introduction, level = "Some 1"]\ The linking of the \<^emph>\formal\ to the \<^emph>\informal\ 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]\ The plan of the paper is follows: we start by introducing the underlying +text*[plan::introduction, level="Some 1"]\ The plan of the paper is follows: we start by introducing the underlying Isabelle system (@{text_section (unchecked) \bgrnd\}) followed by presenting the essentials of \<^isadof> and its ontology language (@{text_section (unchecked) \isadof\}). It follows @{text_section (unchecked) \ontomod\}, where we present three application @@ -133,7 +133,7 @@ conclusions and discuss related work in @{text_section (unchecked) \conclu section*[bgrnd::text_section,main_author="Some(@{docitem ''bu''}::author)"] \ Background: The Isabelle System \ -text*[background::introduction]\ +text*[background::introduction, level="Some 1"]\ 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). \ -text*[blug::introduction]\ The Isabelle system architecture shown in @{figure \architecture\} +text*[blug::introduction, level="Some 1"]\ The Isabelle system architecture shown in @{figure \architecture\} comes with many layers, with Standard ML (SML) at the bottom layer as implementation language. The architecture actually foresees a \<^emph>\Nano-Kernel\ (our terminology) which resides in the SML structure \<^ML_structure>\Context\. 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. \ -text*[anti]\ Thus, antiquotations can refer to formal content, can be type-checked before being +text*[anti::introduction, level = "Some 1"]\ 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>\semi-formal\ content. \ diff --git a/examples/scholarly_paper/2020-iFM-CSP/paper.thy b/examples/scholarly_paper/2020-iFM-CSP/paper.thy index d3f6790..229c48a 100644 --- a/examples/scholarly_paper/2020-iFM-CSP/paper.thy +++ b/examples/scholarly_paper/2020-iFM-CSP/paper.thy @@ -52,7 +52,7 @@ abstract*[abs, keywordlist="[\Shallow Embedding\,\Process-Alg \ text\\ section*[introheader::introduction,main_author="Some(@{docitem ''bu''}::author)"]\ Introduction \ -text*[introtext::introduction]\ +text*[introtext::introduction, level="Some 1"]\ 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>\process algebras\. @@ -154,7 +154,7 @@ processes \Skip\ (successful termination) and \Stop\ ( \\(Skip) = \(Stop) = {[]}\. Note that the trace sets, representing all \<^emph>\partial\ history, is in general prefix closed.\ -text*[ex1::math_example, status=semiformal] \ +text*[ex1::math_example, status=semiformal, level="Some 1"] \ Let two processes be defined as follows: \<^enum> \P\<^sub>d\<^sub>e\<^sub>t = (a \ Stop) \ (b \ Stop)\ @@ -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>\refusals after\ a trace \s\ and defined by \\ P s \ {X | (s, X) \ \ P}\.\ -Definition*[process_ordering, short_name="''process ordering''"]\ +Definition*[process_ordering, level= "Some 2", short_name="''process ordering''"]\ We define \P \ Q \ \\<^sub>\ \ \\<^sub>\ \ \\<^sub>\ \, where \<^enum> \\\<^sub>\ = \ P \ \ Q \ \<^enum> \\\<^sub>\ = s \ \ P \ \ P s = \ Q s\ @@ -530,10 +530,10 @@ To handle termination better, we added two new processes \CHAOS\<^sub>S\<^ \ (*<*) (* a test ...*) -text*[X22 ::math_content ]\\RUN A \ \ X. \ x \ A \ X\ \ -text*[X32::"definition", mcc=defn]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ -Definition*[X42]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ -Definition*[X52::"definition"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ +text*[X22 ::math_content, level="Some 2" ]\\RUN A \ \ X. \ x \ A \ X\ \ +text*[X32::"definition", level="Some 2", mcc=defn]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ +Definition*[X42, level="Some 2"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ +Definition*[X52::"definition", level="Some 2"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\ \ text\ The \RUN\-process defined @{math_content X22} represents the process that accepts all events, but never stops nor deadlocks. The \CHAOS\-process comes in two variants shown in @@ -541,11 +541,11 @@ events, but never stops nor deadlocks. The \CHAOS\-process comes in stops or accepts any offered event, whereas \CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P\ can additionally terminate.\ (*>*) -Definition*[X2]\\RUN A \ \ X. \ x \ A \ X\ \ -Definition*[X3]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ -Definition*[X4]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\\ -Definition*[X5]\\DF A \ \ X. (\ x \ A \ X)\ \ -Definition*[X6]\\DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. ((\ x \ A \ X) \ SKIP)\ \ +Definition*[X2, level="Some 2"]\\RUN A \ \ X. \ x \ A \ X\ \ +Definition*[X3, level="Some 2"]\\CHAOS A \ \ X. (STOP \ (\ x \ A \ X))\ \ +Definition*[X4, level="Some 2"]\\CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. (SKIP \ STOP \ (\ x \ A \ X))\\ +Definition*[X5, level="Some 2"]\\DF A \ \ X. (\ x \ A \ X)\ \ +Definition*[X6, level="Some 2"]\\DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P A \ \ X. ((\ x \ A \ X) \ SKIP)\ \ text\In the following, we denote \ \\

= {DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P, DF, RUN, CHAOS, CHAOS\<^sub>S\<^sub>K\<^sub>I\<^sub>P}\. 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>.\ (* bizarre: Definition* does not work for this single case *) -text*[X10::"definition"]\ \deadlock\<^sub>-free P \ DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \\<^sub>\ P\ \ +text*[X10::"definition", level="Some 2"]\ \deadlock\<^sub>-free P \ DF\<^sub>S\<^sub>K\<^sub>I\<^sub>P UNIV \\<^sub>\ P\ \ text\\<^noindent> A process \P\ is deadlock-free if and only if after any trace \s\ without \\\, the union of \\\ and all events of \P\ can never be a refusal set associated to \s\, which means that \P\ cannot be deadlocked after any non-terminating trace. \ -Theorem*[T1, short_name="\DF definition captures deadlock-freeness\"] +Theorem*[T1, short_name="\DF definition captures deadlock-freeness\", level="Some 2"] \ \hfill \break \deadlock_free P \ (\s\\ P. tickFree s \ (s, {\}\events_of P) \ \ P)\ \ -Definition*[X11]\ \livelock\<^sub>-free P \ \ P = {} \ \ +Definition*[X11, level="Some 2"]\ \livelock\<^sub>-free P \ \ P = {} \ \ text\ Recall that all five reference processes are livelock-free. We also have the following lemmas about the @@ -630,7 +630,7 @@ text\ Finally, we proved the following theorem that confirms the relationship between the two vital properties: \ -Theorem*[T2, short_name="''DF implies LF''"] +Theorem*[T2, short_name="''DF implies LF''", level="Some 2"] \ \deadlock_free P \ livelock_free P\ \ text\ @@ -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: \ -text*[T3::"theorem", short_name="\Product Construction\"]\ +text*[T3::"theorem", short_name="\Product Construction\", level="Some 2"]\ Parallel composition translates to normal form: @{cartouche [display,indent=5]\(P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\\\<^sub>1,\\<^sub>1\ \\<^sub>1) || (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\\\<^sub>2,\\<^sub>2\ \\<^sub>2) = P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\\(\\<^sub>1,\\<^sub>2). \\<^sub>1 \\<^sub>1 \ \\<^sub>2 \\<^sub>2 , \(\\<^sub>1,\\<^sub>2).\e.(\\<^sub>1 \\<^sub>1 e, \\<^sub>2 \\<^sub>2 e)\ (\\<^sub>1,\\<^sub>2)\} @@ -817,7 +817,7 @@ states via the closure \\\, 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:\ -text*[T4::"theorem", short_name="\DF vs. Reacheability\"] +text*[T4::"theorem", short_name="\DF vs. Reacheability\", level="Some 2"] \ If each reachable state \s \ (\ \ \)\ has outgoing transitions, the \<^csp> process is deadlock-free: @{cartouche [display,indent=10] \\\ \ (\ \ \ \\<^sub>0). \ \ \ {} \ deadlock_free (P\<^sub>n\<^sub>o\<^sub>r\<^sub>m\\,\\ \\<^sub>0)\} diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index d12f494..54c271d 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1041,10 +1041,11 @@ text\ 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>\invariants_checking\ + To enable the strict checking of the invariants, + the \<^boxed_theory_text>\invariants_strict_checking\ theory attribute must be set: @{boxed_theory_text [display]\ - declare[[invariants_checking = true]]\} + declare[[invariants_strict_checking = true]]\} For example, let's define the following two classes: @{boxed_theory_text [display]\ @@ -1104,8 +1105,15 @@ text\ All specified constraints are already checked in the IDE of \<^dof> while editing. The invariant \<^boxed_theory_text>\author_finite\ enforces that the user sets the \<^boxed_theory_text>\authored_by\ set. + The invariants \<^theory_text>\author_finite\ and \<^theory_text>\establish_defined\ can not be checked directly + and need a little help. + We can set the \invariants_checking_with_tactics\ theory attribute to help the checking. + It will enable a basic tactic, using unfold and auto: + @{boxed_theory_text [display]\ + declare[[invariants_checking_with_tactics = true]]\} There are still some limitations with this high-level syntax. - For now, the high-level syntax does not support monitors (see \<^technical>\sec:monitors\). + For now, the high-level syntax does not support the checking of + specific monitor behaviors (see \<^technical>\sec:monitors\). For example, one would like to delay a final error message till the closing of a monitor. For this use-case you can use low-level class invariants (see \<^technical>\sec:low_level_inv\). @@ -1147,6 +1155,20 @@ text\ instances of \S\. \ text\ + Should the specified ranges of admissible instances not be observed, warnings will be triggered. + To forbid the violation of the specified ranges, + one can enable the \<^boxed_theory_text>\strict_monitor_checking\ theory attribute: + @{boxed_theory_text [display]\declare[[strict_monitor_checking = true]]\} + It is possible to enable the tracing of free classes occurring inside the scope of a monitor by + enabling the \<^boxed_theory_text>\free_class_in_monitor_checking\ + theory attribute: + @{boxed_theory_text [display]\declare[[free_class_in_monitor_checking = true]]\} + Then a warning will be triggered when defining an instance of a free class + inside the scope of a monitor. + To forbid free classes inside the scope of a monitor, one can enable the + \<^boxed_theory_text>\free_class_in_monitor_strict_checking\ theory attribute: + @{boxed_theory_text [display]\declare[[free_class_in_monitor_strict_checking = true]]\} + Monitored document sections can be nested and overlap; thus, it is possible to combine the effect of different monitors. For example, it would be possible to refine the \<^boxed_theory_text>\example\ section by its own @@ -1164,8 +1186,9 @@ text\ header delimiting the borders of its representation. Class invariants on monitors allow for specifying structural properties on document sections. - For now, the high-level syntax of invariants is not supported for monitors and you must use - the low-level class invariants (see \<^technical>\sec:low_level_inv\.\ + For now, the high-level syntax of invariants does not support the checking of + specific monitor behaviors like the one above and you must use + the low-level class invariants (see \<^technical>\sec:low_level_inv\).\ subsection*["sec:low_level_inv"::technical]\ODL Low-level Class Invariants\ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 5cc5db8..c9693a5 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -346,6 +346,8 @@ fun upd_docclass_lazy_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids +fun get_rejected_cids ({rejected_cids, ... } : open_monitor_info) = rejected_cids +fun get_alphabet monitor_info = (get_accepted_cids monitor_info) @ (get_rejected_cids monitor_info) fun get_automatas ({automatas, ... } : open_monitor_info) = automatas @@ -813,8 +815,14 @@ fun print_doc_class_tree ctxt P T = val (strict_monitor_checking, strict_monitor_checking_setup) = Attrib.config_bool \<^binding>\strict_monitor_checking\ (K false); -val (invariants_checking, invariants_checking_setup) - = Attrib.config_bool \<^binding>\invariants_checking\ (K false); +val (free_class_in_monitor_checking, free_class_in_monitor_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_checking\ (K false); + +val (free_class_in_monitor_strict_checking, free_class_in_monitor_strict_checking_setup) + = Attrib.config_bool \<^binding>\free_class_in_monitor_strict_checking\ (K false); + +val (invariants_strict_checking, invariants_strict_checking_setup) + = Attrib.config_bool \<^binding>\invariants_strict_checking\ (K false); val (invariants_checking_with_tactics, invariants_checking_with_tactics_setup) = Attrib.config_bool \<^binding>\invariants_checking_with_tactics\ (K false); @@ -825,7 +833,9 @@ end (* struct *) \ setup\DOF_core.strict_monitor_checking_setup - #> DOF_core.invariants_checking_setup + #> DOF_core.free_class_in_monitor_checking_setup + #> DOF_core.free_class_in_monitor_strict_checking_setup + #> DOF_core.invariants_strict_checking_setup #> DOF_core.invariants_checking_with_tactics_setup\ section\ Syntax for Term Annotation Antiquotations (TA)\ @@ -948,6 +958,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 @@ -1433,7 +1444,7 @@ fun create_default_object thy class_name = in list_comb (make_const, (tag_attr (serial()))::class_list'') end -fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy = +fun check_classref {is_monitor=is_monitor} (SOME(cid,pos)) thy = let val cid_long = DOF_core.read_cid_global thy cid @@ -1443,10 +1454,10 @@ fun check_classref {is_monitor=is_monitor} (SOME(cid,pos')) thy = else () val markup = docclass_markup false cid id (Binding.pos_of bind_target); val ctxt = Context.Theory thy - val _ = Context_Position.report_generic ctxt pos' markup; - in cid_long + val _ = Context_Position.report_generic ctxt pos markup; + in (cid_long, pos) end - | check_classref _ NONE _ = DOF_core.default_cid + | check_classref _ NONE _ = (DOF_core.default_cid, \<^here>) fun generalize_typ n = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,n),sort)); @@ -1514,67 +1525,104 @@ fun calc_update_term {mk_elaboration=mk_elaboration} thy cid_long end in Sign.certify_term thy (fold read_assn S term) end -fun msg thy txt = if Config.get_global thy DOF_core.strict_monitor_checking - then error txt - else warning txt +fun msg thy txt pos = if Config.get_global thy DOF_core.strict_monitor_checking + then ISA_core.err txt pos + else ISA_core.warn txt pos -fun register_oid_cid_in_open_monitors oid pos cid_long thy = - let val {monitor_tab,...} = DOF_core.get_data_global thy - fun is_enabled (n, info) = - if exists (DOF_core.is_subclass_global thy cid_long) - (DOF_core.get_accepted_cids info) - then SOME n - else NONE - (* filtering those monitors with automata, whose alphabet contains the - cid of this oid. The enabled ones were selected and moved to their successor state - along the super-class id. The evaluation is in parallel, simulating a product - semantics without expanding the subclass relationship. *) - fun is_enabled_for_cid moid = - let val {accepted_cids, automatas, ...} = - the(Symtab.lookup monitor_tab moid) - val indexS= 1 upto (length automatas) - val indexed_autoS = automatas ~~ indexS - fun check_for_cid (A,n) = - let val accS = (RegExpInterface.enabled A accepted_cids) - val is_subclass = DOF_core.is_subclass_global thy - val idx = find_index (is_subclass cid_long) accS - in if idx < 0 - then (msg thy ("monitor "^moid^"(" ^ Int.toString n - ^") not enabled for doc_class: "^cid_long);A) - else RegExpInterface.next A accepted_cids (nth accS idx) +fun register_oid_cid_in_open_monitors oid pos cid_pos thy = + let val {monitor_tab,...} = DOF_core.get_data_global thy + val cid_long= fst cid_pos + val pos' = snd cid_pos + fun is_enabled (n, info) = + if exists (DOF_core.is_subclass_global thy cid_long) + (DOF_core.get_alphabet info) + then SOME n + else if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking + orelse Config.get_global thy DOF_core.free_class_in_monitor_checking + then SOME n + else NONE + (* filtering those monitors with automata, whose alphabet contains the + cid of this oid. The enabled ones were selected and moved to their successor state + along the super-class id. The evaluation is in parallel, simulating a product + semantics without expanding the subclass relationship. *) + fun is_enabled_for_cid moid = + let val {accepted_cids, automatas, rejected_cids, ...} = + the(Symtab.lookup monitor_tab moid) + val indexS= 1 upto (length automatas) + val indexed_autoS = automatas ~~ indexS + fun check_for_cid (A,n) = + let fun direct_super_class _ cid [] = cid + | direct_super_class thy cid (x::xs) = + if DOF_core.is_subclass_global thy cid x + then direct_super_class thy cid xs + else direct_super_class thy x xs + val accS = (RegExpInterface.enabled A accepted_cids) + val accS' = filter (DOF_core.is_subclass_global thy cid_long) accS + fun first_super_class cids = + case List.getItem cids + of SOME (hd,tl) => SOME (direct_super_class thy hd tl) + | NONE => NONE + val first_accepted = first_super_class accS' + val rejectS = filter (DOF_core.is_subclass_global thy cid_long) rejected_cids + val first_rejected = first_super_class rejectS + in + case first_accepted of + NONE => (case first_rejected of + NONE => + let val msg_intro = ("accepts clause " ^ Int.toString n + ^ " of monitor " ^ moid + ^ " not enabled for doc_class: " ^ cid_long) + in + if Config.get_global thy DOF_core.free_class_in_monitor_strict_checking + then ISA_core.err msg_intro pos' + else if Config.get_global thy DOF_core.free_class_in_monitor_checking + then (ISA_core.warn msg_intro pos';A) + else A end - in (moid,map check_for_cid indexed_autoS) end - val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab) - fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, - Syntax.read_term_global thy rhs) - val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] - val assns' = map conv_attrs trace_attr - fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy)) - fun def_trans_input_term oid = - #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') - fun def_trans_value oid = - (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')) - #> value (Proof_Context.init_global thy) - val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." - val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; - (* check that any transition is possible : *) - fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} - fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors - val delta_autoS = map is_enabled_for_cid enabled_monitors; - fun update_info (n, aS) (tab: DOF_core.monitor_tab) = - let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n) - in Symtab.update(n, {accepted_cids=accepted_cids, - rejected_cids=rejected_cids, - automatas=aS}) tab end - fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid) - val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) - in thy |> (* update traces of all enabled monitors *) - fold (update_trace) (enabled_monitors) - |> (* check class invariants of enabled monitors *) - (fn thy => (class_inv_checks (Context.Theory thy); thy)) - |> (* update the automata of enabled monitors *) - DOF_core.map_data_global(update_automatons) - end + | SOME _ => (msg thy ("accepts clause " ^ Int.toString n + ^ " of monitor " ^ moid + ^ " rejected doc_class: " ^ cid_long) pos';A)) + | SOME accepted => (case first_rejected of + NONE => RegExpInterface.next A accepted_cids (accepted) + | SOME rejected => + if DOF_core.is_subclass_global thy accepted rejected + then RegExpInterface.next A accepted_cids (accepted) + else (msg thy ("accepts clause " ^ Int.toString n + ^ " of monitor " ^ moid + ^ " rejected doc_class: " ^ cid_long) pos';A)) + end + in (moid,map check_for_cid indexed_autoS) end + val enabled_monitors = List.mapPartial is_enabled (Symtab.dest monitor_tab) + fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn, + Syntax.read_term_global thy rhs) + val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")] + val assns' = map conv_attrs trace_attr + fun cid_of oid = #cid(the(DOF_core.get_object_global oid thy)) + fun def_trans_input_term oid = + #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') + fun def_trans_value oid = + (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')) + #> value (Proof_Context.init_global thy) + val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." + val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; + (* check that any transition is possible : *) + fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} + fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors + val delta_autoS = map is_enabled_for_cid enabled_monitors; + fun update_info (n, aS) (tab: DOF_core.monitor_tab) = + let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n) + in Symtab.update(n, {accepted_cids=accepted_cids, + rejected_cids=rejected_cids, + automatas=aS}) tab end + fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans_input_term mon_oid) (def_trans_value mon_oid) + val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS) + in thy |> (* update traces of all enabled monitors *) + fold (update_trace) (enabled_monitors) + |> (* check class invariants of enabled monitors *) + (fn thy => (class_inv_checks (Context.Theory thy); thy)) + |> (* update the automata of enabled monitors *) + DOF_core.map_data_global(update_automatons) + end fun check_invariants thy oid = let @@ -1600,11 +1648,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>\True\ |> 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 +1663,37 @@ 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 " - ^ inv_name - ^ ". Try to activate invariants_checking_with_tactics.") pos - in (if evaluated_term = \<^term>\True\ - then ((inv_name, pos), term) - else ISA_core.err ("Invariant " ^ inv_name ^ " violated") pos) + else \<^term>\True \ True\ + in case evaluated_term of + \<^term>\True\ => ((inv_name, pos), term) + | \<^term>\True \ True\ => + let val msg_intro = "Fail to check invariant " + ^ inv_name + ^ ".\nMaybe you can try " + ^ "to activate invariants_checking_with_tactics\n" + ^ "if your invariant is checked against doc_class algebraic " + ^ "types like 'doc_class list' or 'doc_class set'" + in if Config.get_global thy DOF_core.invariants_strict_checking + then ISA_core.err (msg_intro) pos + else (ISA_core.warn (msg_intro) pos; ((inv_name, pos), term)) end + | _ => let val msg_intro = "Invariant " ^ inv_name ^ " violated" + in if Config.get_global thy DOF_core.invariants_strict_checking + then ISA_core.err msg_intro pos + else (ISA_core.warn msg_intro pos; ((inv_name, pos), term)) end 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 = @@ -1638,21 +1702,21 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do val _ = Position.report pos (docref_markup true oid id pos); (* 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 cid_pos' = check_classref is_monitor cid_pos thy + val cid_long = fst cid_pos' + 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>\unit\) + val undefined_value = Free ("Undefined_Value", \<^Type>\unit\) 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]\ Lorem ipsum @{thm refl}\ - *) + (* 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]\ Lorem ipsum @{thm refl}\ *) 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); @@ -1678,15 +1742,21 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} oid pos cid_pos do id = id, cid = cid_long, vcid = vcid}) - |> register_oid_cid_in_open_monitors oid pos cid_long + |> register_oid_cid_in_open_monitors oid pos cid_pos' |> (fn thy => if #is_monitor(is_monitor) then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor 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]\ Lorem ipsum @{thm refl}\ *) + |> (fn thy => if default_cid then thy else check_invariants thy oid) end end (* structure Docitem_Parser *) @@ -1848,8 +1918,9 @@ fun update_instance_command (((oid:string,pos),cid_pos), val _ = Context_Position.report ctxt pos markup; in cid end | NONE => error("undefined doc_class.") - val cid_long = Value_Command.Docitem_Parser.check_classref {is_monitor = false} + val cid_pos' = Value_Command.Docitem_Parser.check_classref {is_monitor = false} cid_pos thy + val cid_long = fst cid_pos' val _ = if cid_long = DOF_core.default_cid orelse cid = cid_long then () else error("incompatible classes:"^cid^":"^cid_long) @@ -1870,9 +1941,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 @@ -1891,31 +1960,33 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Pars in case DOF_core.get_doc_class_global long_cid thy of SOME X => let val ralph = RegExpInterface.alphabet (#rejectS X) - val alph = RegExpInterface.ext_alphabet ralph (#rex X) - in (alph, map (RegExpInterface.rexp_term2da alph)(#rex X)) end + val aalph = RegExpInterface.alphabet (#rex X) + in (aalph, ralph, map (RegExpInterface.rexp_term2da aalph)(#rex X)) end | NONE => error("Internal error: class id undefined. ") end fun create_monitor_entry thy = let val cid = case cid_pos of NONE => ISA_core.err ("You must specified a monitor class.") pos | SOME (cid, _) => cid - val (S, aS) = compute_enabled_set cid thy - val info = {accepted_cids = S, rejected_cids = [], automatas = aS } + val (accS, rejectS, aS) = compute_enabled_set cid thy + val info = {accepted_cids = accS, rejected_cids = rejectS, automatas = aS } in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy) end in - create_monitor_entry #> o_m_c oid pos cid_pos doc_attrs + o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry end; fun close_monitor_command (args as (((oid:string,pos),cid_pos), doc_attrs: (((string*Position.T)*string)*string)list)) thy = let val {monitor_tab,...} = DOF_core.get_data_global thy - fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS - in if i >= 0 + fun check_if_final aS = let val i = (find_index (not o RegExpInterface.final) aS) + 1 + in if i >= 1 then Value_Command.Docitem_Parser.msg thy - ("monitor number "^Int.toString i^" not in final state.") + ("accepts clause " ^ Int.toString i + ^ " of monitor " ^ oid + ^ " not in final state.") pos else () end val _ = case Symtab.lookup monitor_tab oid of @@ -1932,9 +2003,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 diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy index ff9631e..da79817 100644 --- a/src/ontologies/Conceptual/Conceptual.thy +++ b/src/ontologies/Conceptual/Conceptual.thy @@ -177,4 +177,47 @@ text*[ sdfg :: F] \ Lorem ipsum @{thm refl}\ text*[ xxxy ] \ Lorem ipsum @{F \sdfg\} rate @{thm refl}\ close_monitor*[aaa] -end +doc_class test_monitor_free = + tmhd :: int +doc_class test_monitor_head = + tmhd :: int +doc_class test_monitor_A = test_monitor_head + + tmA :: int +doc_class test_monitor_B = test_monitor_A + + tmB :: int +doc_class test_monitor_C = test_monitor_A + + tmC :: int +doc_class test_monitor_D = test_monitor_B + + tmD :: int +doc_class test_monitor_E = test_monitor_D + + tmE :: int + +doc_class monitor_M = + tmM :: int + rejects "test_monitor_A" + accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C" + +declare[[free_class_in_monitor_checking]] + +open_monitor*[test_monitor_M::monitor_M] + +text*[testFree::test_monitor_free]\\ + +open_monitor*[test_monitor_M2::monitor_M] + +text*[test_monitor_A1::test_monitor_A]\\ +text*[testFree2::test_monitor_free]\\ +text*[test_monitor_head1::test_monitor_head]\\ +text*[testFree3::test_monitor_free]\\ +text*[test_monitor_B1::test_monitor_B]\\ +text*[testFree4::test_monitor_free]\\ +text*[test_monitor_D1::test_monitor_D]\\ +text*[testFree5::test_monitor_free]\\ +text*[test_monitor_C1::test_monitor_C]\\ +text*[testFree6::test_monitor_free]\\ + +close_monitor*[test_monitor_M2] + +close_monitor*[test_monitor_M] + +end diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 587365c..05a034a 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -69,7 +69,7 @@ which we formalize into:\ doc_class text_section = text_element + main_author :: "author option" <= None fixme_list :: "string list" <= "[]" - level :: "int option" <= "None" + level :: "int option" <= "None" (* this attribute enables doc-notation support section* etc. we follow LaTeX terminology on levels part = Some -1 diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy index 3467795..762bccf 100644 --- a/src/tests/Attributes.thy +++ b/src/tests/Attributes.thy @@ -173,9 +173,20 @@ text\ @{docitem_attribute y::omega} \ section\Simulation of a Monitor\ +declare[[free_class_in_monitor_checking]] + +ML\ +val thy = \<^theory> +val long_cid = "Isa_COL.figure_group" +val t = DOF_core.get_doc_class_global long_cid thy +\ open_monitor*[figs1::figure_group, caption="''Sample ''"] - +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ +text*[testFreeA::A]\\ figure*[fig_A::figure, spawn_columns=False, relative_width="90", src="''figures/A.png''"] @@ -185,6 +196,47 @@ figure*[fig_B::figure, spawn_columns=False,relative_width="90", src="''figures/B.png''"] \ The B train \ldots \ +open_monitor*[figs2::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ +figure*[fig_C::figure, spawn_columns=False, + relative_width="90", + src="''figures/A.png''"] + \ The C train \ldots \ +open_monitor*[figs3::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ + +figure*[fig_D::figure, + spawn_columns=False,relative_width="90", + src="''figures/B.png''"] + \ The D train \ldots \ +close_monitor*[figs3] + +open_monitor*[figs4::figure_group, + caption="''Sample ''"] +ML\ +val thy = \<^theory> +val {monitor_tab,...} = DOF_core.get_data_global thy +\ + +text*[testRejected1::figure_group, caption="''figures/A.png''"] + \ The A train \ldots \ + +figure*[fig_E::figure, + spawn_columns=False,relative_width="90", + src="''figures/B.png''"] + \ The E train \ldots \ +close_monitor*[figs4] +close_monitor*[figs2] +text*[testRejected2::figure_group, caption="''figures/A.png''"] + \ The A train \ldots \ close_monitor*[figs1] @@ -199,7 +251,8 @@ term*\map snd @{trace-attribute \figs1\}\ value*\map snd @{trace-attribute \figs1\}\ term*\map fst @{trace-attribute \aaa\}\ value*\map fst @{trace-attribute \aaa\}\ -value*\(map fst @{trace-attribute \aaa\}) \ +term*\map fst @{trace-attribute \test_monitor_M\}\ +value*\map fst @{trace-attribute \test_monitor_M\}\ definition example_expression where "example_expression \ \\''Conceptual.A''\ || \''Conceptual.F''\\\<^sup>*" value* \ DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \aaa\}) \ diff --git a/src/tests/High_Level_Syntax_Invariants.thy b/src/tests/High_Level_Syntax_Invariants.thy index 204626f..50fe0f1 100644 --- a/src/tests/High_Level_Syntax_Invariants.thy +++ b/src/tests/High_Level_Syntax_Invariants.thy @@ -12,7 +12,7 @@ text\ theory attribute must be set:\ -declare[[invariants_checking = true]] +declare[[invariants_strict_checking = true]] text\For example, let's define the following two classes:\ @@ -144,6 +144,6 @@ value*\evidence @{result \resultProof\} = evidence @{result \ declare[[invariants_checking_with_tactics = false]] -declare[[invariants_checking = false]] +declare[[invariants_strict_checking = false]] end