improved testKit, finished Concept_Example_Low_Level invariant

Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy

@@ -212,16 +212,11 @@ let  val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Co
 in @{assert} (class_ids_so_far = docclass_tab) end\<close>
 
 
+section\<open>For Test and Validation\<close>
 
-section*[test::A]\<open>For Test and Validation\<close>
-
-open_monitor*[aaa::M]
-text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
 text*[sdf]         \<open> Lorem ipsum ... \<close>         \<comment> \<open>anonymous reference\<close>
-text*[sdfg :: F]   \<open> Lorem ipsum ...\<close>          \<comment> \<open>causes just warnings for invariant violations  
-                                                   due to non-strict checking mode\<close>
-close_monitor*[aaa]                            \<comment> \<open>causes warning: accept clause 1 
-                                                   not in final state .\<close>
+text*[sdfg :: F]   \<open> Lorem ipsum ...\<close>          \<comment> \<open>some F instance \<close>  
+
 
 
 

Isabelle_DOF-Unit-Tests/Attributes.thy

@@ -16,6 +16,7 @@ theory
   imports 
   "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual"
+  Concept_MonitorTest1
 begin
 ML\<open>@{assert} (1 = 1)\<close>
 section\<open>Elementar Creation of Doc-items and Access of their Attibutes\<close>
@@ -36,10 +37,7 @@ Name_Space.dest_table docclass_tab;
 
 \<close>
 
-ML\<open>
-val (oid, DOF_core.Instance {value, ...}) =
-    Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)
-\<close>
+
 
 find_theorems (60) name:"Conceptual.M." 
 
@@ -235,12 +233,13 @@ ML  \<open>@{trace_attribute figs1}\<close>
 text\<open>Resulting trace of figs as text antiquotation:\<close>
 text\<open>@{trace_attribute figs1}\<close>
 
+
+section\<open>A Complex Evaluation involving Automatas\<close>
+
 text\<open>Test trace\_attribute term antiquotation:\<close>
 
 term*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
 value*\<open>map snd @{trace-attribute \<open>figs1\<close>}\<close>
-term*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
-value*\<open>map fst @{trace-attribute \<open>aaa\<close>}\<close>
 
 definition example_expression where "example_expression \<equiv> \<lbrace>\<lfloor>''Conceptual.A''\<rfloor> || \<lfloor>''Conceptual.F''\<rfloor>\<rbrace>\<^sup>*"
 value* \<open> DA.accepts (na2da (rexp2na example_expression)) (map fst @{trace-attribute \<open>aaa\<close>}) \<close>

Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy

@@ -11,23 +11,28 @@
  *   SPDX-License-Identifier: BSD-2-Clause
  *************************************************************************)
 
-chapter\<open>Setting and modifying attributes of doc-items\<close>
+chapter\<open>Testing hand-programmed (low-level) Invariants\<close>
 
-theory 
-  Concept_Example_Low_Level_Invariant
+theory   Concept_Example_Low_Level_Invariant
   imports 
   "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
   TestKit
 begin
 
-section\<open>Example: Standard Class Invariant\<close>
+section\<open>Test Purpose.\<close>
+text\<open> Via @{ML "DOF_core.add_ml_invariant"} it is possible to attach user-defined
+      ML-code to classes which is executed at each creation or modification of 
+      class instances. We test exection  of creation  and updates. \<close>
 
 text\<open>Consult the status of the DOF engine:\<close>
 print_doc_classes
 print_doc_items
 
 
+section\<open>Example: Standard Class Invariant\<close>
+
+
 text\<open>Watch out: The current programming interface to document class invariants is pretty low-level:
 \<^item> No inheritance principle
 \<^item> No high-level notation in HOL
@@ -47,7 +52,7 @@ let val ctxt = Proof_Context.init_global thy
 in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (exec, cid_long)) thy end
 \<close>
 
-ML\<open>DOF_core.binding_from_onto_class_pos "A" @{theory} \<close>
+text\<open>The checker \<open>exec\<close> above is set. Just used to provoke output: "sample echo : b"\<close>
 text*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 
 text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
@@ -62,15 +67,16 @@ let fun check_A_invariant oid {is_monitor:bool} ctxt =
 in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (check_A_invariant, cid_long)) thy end
 \<close>
 
-text*[d0::A, x = "5"]\<open>Lorem ipsum dolor sit amet, ...\<close>
+text*[d0::A, x = "5"]            \<open>Lorem ipsum dolor sit amet, ...\<close>
+text-assert-error[d1::A, x = "6"]\<open>Lorem ipsum dolor sit amet, ...\<close>\<open>class A invariant violation\<close>
 
 subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
 
-(* test : update should not fail, invariant still valid *)
+(* invariant still valid *)
 update_instance*[d::A, x += "1"]
 
-(* test : with the next step it should fail : *)
-update_instance*[d::A, x += "1"]
+(* invariant no longer *)
+update_instance-assert-error[d::A, x += "1"]\<open>class A invariant violation\<close>
 
 
 section\<open>Example: Monitor Class Invariant\<close>
@@ -126,9 +132,9 @@ text*[c2:: C, x = "''delta''"]   \<open> ... in ut tortor eleifend augue pretium
 
 subsection*[f::E]                \<open> Lectus accumsan velit ultrices, ... \<close>
 
-(*
-section*[f2::E]                  \<open> Lectus accumsan velit ultrices, ... \<close>
-*)
+
+text-assert-error[f2::E]         \<open> Lectus accumsan velit ultrices, ... \<close>\<open>class M invariant violation\<close>
+
 
 ML\<open>val ctxt = @{context}
    val term = ISA_core.compute_attr_access 

Isabelle_DOF-Unit-Tests/Concept_MonitorTest1.thy

@@ -21,6 +21,8 @@ theory
   TestKit
 begin
 
+section\<open>Test Purpose.\<close>
+text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
 
 open_monitor*[aaa::Conceptual.M]  
 text*[test::A]\<open>For Test and Validation\<close>
@@ -54,7 +56,7 @@ doc_class monitor_M =
   rejects "test_monitor_A"
   accepts "test_monitor_head ~~ test_monitor_B ~~ test_monitor_C"
 
-section\<open>Example: Standard Class Invariant\<close>
+section\<open>A more Complex Monitoring Example \<close>
 
 text\<open>Consult the status of the DOF engine:\<close>
 print_doc_classes

Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy

@@ -85,17 +85,27 @@ text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit r
 
 text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
 
-ML*[ddddd2::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
+ML*[c4::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
 
-lemma*[ddddd3::E] asd: "True" by simp
+lemma*[e5::E] asd: "True" by simp
 
-definition*[dddddd3::E] facu :: "nat \<Rightarrow> nat" where "facu xxxx = undefined"
-
-(* BUG 
-text\<open>As shown in @{E \<open>ddddd3\<close>}\<close>
-text\<open>As shown in @{C \<open>ddddd2\<close>}\<close>
+(* Correct report: "Duplicate instance declaration.. " 
+declare_reference*[c1::C]     \<comment> \<open>forward declaration\<close>
 *)
 
+declare_reference*[e6::E] 
+
+text\<open>This is the answer to the "OutOfOrder Presentation Problem": @{E (unchecked) \<open>e6\<close>} \<close>
+
+definition*[e6::E] facu :: "nat \<Rightarrow> nat" where "facu arg = undefined"
+
+
+text\<open>As shown in @{E [display]\<open>e5\<close>} following from  @{E [display]\<open>e6\<close>}\<close> 
+(* BUG: why is option [display] necessary ? *)
+
+text\<open>As shown in @{C [display]\<open>c4\<close>}\<close>
+
+
 
 text\<open>Ontological information ("class instances") is mutable: \<close>
 
@@ -103,8 +113,8 @@ update_instance*[d::D, a1 := X2]
 
 text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
 
-(* THIS IS A BUG : this should work rather than fail. \<And>\<And>! *)
-text-assert-error[ae::text_element]\<open>the function @{C "ddddd2"} \<close>\<open>referred text-element is macro!\<close>
+(* THIS IS A BUG : this weird option is necessary *)
+text-assert-error[ae::text_element]\<open>the function @{C [display] "c4"} \<close>\<open>referred text-element is macro!\<close>
 
 text*[c2::C, x = "\<open>delta\<close>"]  \<open> ... in ut tortor eleifend augue pretium consectetuer.  \<close>
 
@@ -125,19 +135,21 @@ text\<open>Here we add and maintain a link that is actually modeled as m-to-n re
 update_instance*[f::F,b:="{(@{docitem  \<open>a\<close>}::A,@{docitem  \<open>c1\<close>}::C), 
                            (@{docitem  \<open>a\<close>},   @{docitem  \<open>c2\<close>})}"] 
 
+section\<open>Closing the Monitor and testing the Results.\<close>
+
 close_monitor*[struct]
 
 text\<open>And the trace of the monitor is:\<close>
 ML\<open>val trace = @{trace_attribute struct}\<close>
+ML\<open>@{assert} (trace = 
+   [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), ("Conceptual.A", "abb"),
+    ("Conceptual.C", "c1"), ("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
+    ("Conceptual.E", "e5"), ("Conceptual.E", "e6"), ("Conceptual.E", "e6"), ("Conceptual.C", "c2"),
+    ("Conceptual.F", "f")]) \<close>
+(* BUG : DECLARATIONS SHOULD NOT BE TRACED, JUST DEFINITIONS.
 ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), 
-    ("Conceptual.A", "abb"), ("Conceptual.C", "c1"), ("Conceptual.C", "c1"), ("Conceptual.D", "d"), 
-    ("Conceptual.C", "ddddd2"),("Conceptual.E", "ddddd3"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
-(* BUG : SHOULD BE:
-ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"), ("Conceptual.A", "abb"),
-    ("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "ddddd2"),
-    ("Conceptual.E", "ddddd3"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
-
-   FAILURE DUE TO DUPLICATE DEFINITION BUG 
+    ("Conceptual.A", "abb"), ("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
+    ("Conceptual.E", "e5"), ("Conceptual.E", "e6"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
 *)
 
 text\<open>Note that the monitor \<^typ>\<open>M\<close> of the ontology \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> does

Isabelle_DOF-Unit-Tests/Evaluation.thy

@@ -158,10 +158,10 @@ value*\<open>@{A-instances}\<close>
 text\<open>Warning: If you make a request on attributes that are undefined in some instances,
 you will get a result which includes these unresolved cases.
 In the following example, we request the instances of the @{doc_class A}.
-But we have defined an instance @{docitem \<open>test\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
+But we have defined an instance @{docitem \<open>sdf\<close>} in theory @{theory "Isabelle_DOF-Ontologies.Conceptual"}
 whose our theory inherits from, and this docitem instance does not initialize its attribute \<^emph>\<open>x\<close>.
 So in the request result we get an unresolved case because the evaluator can not get
-the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>test\<close>}:\<close>
+the value of the \<^emph>\<open>x\<close> attribute of the instance @{docitem \<open>sdf\<close>}:\<close>
 value*\<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
 
 section\<open>Limitations\<close>

Isabelle_DOF-Unit-Tests/TermAntiquotations.thy

@@ -95,7 +95,6 @@ text\<open>And here is the results of some ML-term antiquotations:\<close>
 ML\<open> @{docitem_attribute b::xcv4} \<close>
 ML\<open> @{docitem xcv4}              \<close>
 ML\<open> @{docitem_name xcv4}         \<close>
-ML\<open> @{trace_attribute aaa}       \<close>
 
 text\<open>Now we might need to reference a class instance in a term command and we would like
 Isabelle to check that this instance is indeed an instance of this class.

Isabelle_DOF-Unit-Tests/TestKit.thy

@@ -16,8 +16,9 @@ theory
 imports 
   "Isabelle_DOF-Unit-Tests_document"
   "Isabelle_DOF-Ontologies.Conceptual"
-keywords "text-" "text-latex"    :: document_body
-    and  "text-assert-error":: document_body
+keywords "text-" "text-latex"           :: document_body
+    and  "text-assert-error"            :: document_body
+    and  "update_instance-assert-error" :: document_body
 
 begin
 
@@ -117,35 +118,38 @@ fun document_command2 markdown (loc, txt) =
                     | SOME (_, pos) =>(ISA_core.err 
                                            "Illegal target specification -- not a theory context" 
                                            pos))) 
- o 
-  Toplevel.present_local_theory loc                           
-                (fn state =>  (output_document2 state markdown txt));
+  o 
+  Toplevel.present_local_theory loc (fn state => (output_document2 state markdown txt));
 
-fun document_command3 markdown (loc, txt) trns = (document_command2 markdown (loc, txt) trns
-                                                  handle exn => ((writeln "AAA"); trns))
 
-fun gen_enriched_document_command3 assert name body cid_transform attr_transform markdown
-                                  (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t,
-                                     xstring_opt:(xstring * Position.T) option),
-                                    src_list:Input.source list) thy
- = (gen_enriched_document_command2 name body cid_transform attr_transform markdown 
-                                  (((((oid,pos),cid_pos), doc_attrs), xstring_opt), src_list) 
-                                  thy)
+fun gen_enriched_document_command3 assert name body trans at md (margs, src_list) thy
+ = (gen_enriched_document_command2 name body trans at md  (margs, src_list)  thy)
    handle ERROR msg => (if assert src_list msg then (writeln ("Correct error:"^msg^":reported.");thy)
                                                else error"Wrong error reported")
 
-fun  error_match [_, src] msg = (writeln((Input.string_of src));
-                                 String.isPrefix (Input.string_of src) msg )
-   | error_match _ _ = error "Wrong text-assertion-error. Argument format <arg><match> required."
+fun error_match src msg = (writeln((Input.string_of src)); String.isPrefix (Input.string_of src) msg)
+
+fun  error_match2 [_, src] msg = error_match src msg
+   | error_match2 _ _ = error "Wrong text-assertion-error. Argument format <arg><match> required."
 
 
 val _ =
   Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro"
     (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source 
-      >> (Toplevel.theory o (gen_enriched_document_command3 error_match "TTT" {body=true}
+      >> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true}
                                                             I I {markdown = true}) 
                             ));
 
+fun update_instance_command (args,src) thy = 
+    (Monitor_Command_Parser.update_instance_command args thy
+     handle ERROR msg => (if error_match src msg 
+                          then (writeln ("Correct error:"^msg^":reported.");thy)
+                          else error"Wrong error reported"))
+val _ =
+  Outer_Syntax.command \<^command_keyword>\<open>update_instance-assert-error\<close>
+                       "update meta-attributes of an instance of a document class"
+                        (ODL_Meta_Args_Parser.attributes_upd -- Parse.document_source
+                         >> (Toplevel.theory o update_instance_command)); 
 
 val _ =
   Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)"