added tests with references from and to terms and code
This commit is contained in:
Burkhart Wolff
parent
ef8ffda414
commit
6e5fa2d91b
|
|
@ -37,25 +37,24 @@ text\<open> This uses elements of two ontologies, notably
|
|||
\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> and \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>.\<close>
|
||||
|
||||
(*<*)
|
||||
title*[abbb::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
|
||||
subtitle*[abbbb::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
|
||||
chapter*[abbbbbb::A, x = "3"] \<open> Lorem ipsum dolor sit amet ... \<close>
|
||||
title*[ag::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
|
||||
subtitle*[af::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
|
||||
chapter*[a0::A, x = "3"] \<open> Lorem ipsum dolor sit amet ... \<close>
|
||||
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
subsection*[ab::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
|
||||
As mentioned in the @{title \<open>abbb\<close>}... \<close> \<comment> \<open>old-style and ...\<close>
|
||||
subsubsection*[abb::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
|
||||
As mentioned in the \<^title>\<open>abbb\<close>\<close> \<comment> \<open>new-style references to
|
||||
As mentioned in the @{title \<open>ag\<close>}... \<close> \<comment> \<open>old-style and ...\<close>
|
||||
subsubsection*[ac::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
|
||||
As mentioned in the \<^title>\<open>ag\<close>\<close> \<comment> \<open>new-style references to
|
||||
ontological instances
|
||||
assigned to text
|
||||
elements ...\<close>
|
||||
(*>*)
|
||||
|
||||
|
||||
|
||||
text\<open>Meta-Objects are typed, and references have to respect this : \<close>
|
||||
(*<*)
|
||||
text-assert-error[ac]\<open> \<^title>\<open>a\<close> \<close> \<open>reference ontologically inconsistent\<close>
|
||||
text-assert-error[ad]\<open> \<^title>\<open>abbbb\<close> \<close>\<open>reference ontologically inconsistent\<close>
|
||||
text-assert-error[ad]\<open> \<^title>\<open>a\<close> \<close> \<open>reference ontologically inconsistent\<close>
|
||||
text-assert-error[ae]\<open> \<^title>\<open>af\<close> \<close>\<open>reference ontologically inconsistent\<close>
|
||||
\<comment> \<open>erroneous reference: please consider class hierarchy!\<close>
|
||||
(*>*)
|
||||
|
||||
|
|
@ -69,23 +68,30 @@ text\<open>@{C \<open>c1\<close>} \<close> \<comment> \<open>THIS I
|
|||
|
||||
text\<open>@{C (unchecked) \<open>c1\<close>} \<close> \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
|
||||
|
||||
|
||||
text*[a1::A, level="Some 0", x = 3]\<open>... phasellus amet id massa nunc, ...\<close>
|
||||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
|
||||
text-assert-error[c1::C, x = "''gamma''"]
|
||||
\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
\<open>Duplicate instance declaration\<close>
|
||||
|
||||
\<comment> \<open>Referencing from a text context:\<close>
|
||||
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
... @{C "c1"} or @{C \<open>c1\<close>} or \<^C>\<open>c1\<close>
|
||||
similar to @{thm "refl"} and \<^thm>"refl"\<close> \<comment> \<open>ontological and built-in
|
||||
references\<close>
|
||||
|
||||
|
||||
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
|
||||
references\<close>
|
||||
\<comment> \<open>Referencing from and to a ML-code context:\<close>
|
||||
ML*[c4::C, z = "Some @{A \<open>a1\<close>}"]\<open>
|
||||
fun fac x = if x = 0 then 1 else x * (fac(x-1))
|
||||
val v = \<^value_>\<open>A.x (the (z @{C \<open>c4\<close>}))\<close> |> HOLogic.dest_number |> snd |> fac
|
||||
\<close>
|
||||
|
||||
ML*[c4::C]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
|
||||
definition*[a2::A, x=5, level="Some 1"] xx' where "xx' \<equiv> A.x @{A \<open>a1\<close>}" if "A.x @{A \<open>a1\<close>} = 5"
|
||||
|
||||
lemma*[e5::E] asd: "True" by simp
|
||||
lemma*[e5::E] testtest : "xx + A.x @{A \<open>a1\<close>} = yy + A.x @{A \<open>a1\<close>} \<Longrightarrow> xx = yy" by simp
|
||||
|
||||
declare_reference-assert-error[c1::C]\<open>Duplicate instance declaration\<close> \<comment> \<open>forward declaration\<close>
|
||||
|
||||
|
|
@ -134,18 +140,22 @@ update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1
|
|||
section\<open>Closing the Monitor and testing the Results.\<close>
|
||||
|
||||
close_monitor*[struct]
|
||||
|
||||
text\<open>@{A a0}\<close>
|
||||
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>
|
||||
[("Conceptual.A", "a0"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
|
||||
("Conceptual.A", "ac"), ("Conceptual.C", "c1"), ("Conceptual.A", "a1"),
|
||||
("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
|
||||
("Conceptual.A", "a2"), ("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.D", "d"), ("Conceptual.C", "c4"),
|
||||
("Conceptual.E", "e5"), ("Conceptual.E", "e6"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
|
||||
ML\<open>@{assert} (trace =
|
||||
[("Conceptual.A", "a0"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
|
||||
("Conceptual.A", "ac"), ("Conceptual.A", "a1"),
|
||||
("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
|
||||
("Conceptual.A", "a2"), ("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
|
||||
|
|
|
|||
Loading…
Reference in New Issue