Cleanup with examples. More commendation.
Another monitor example added (Concept_Example).
This commit is contained in:
parent
0de079cfbb
commit
f1783538bd
16
Isa_DOF.thy
16
Isa_DOF.thy
|
|
@ -1240,7 +1240,7 @@ fun calculate_attr_access_check ctxt attr oid pos = (* template *)
|
|||
| NONE => error "identifier not a docitem reference"
|
||||
|
||||
val _ = Theory.setup
|
||||
(ML_Antiquotation.inline @{binding docitem_attr}
|
||||
(ML_Antiquotation.inline @{binding docitem_attribute}
|
||||
(fn (ctxt,toks) =>
|
||||
(Scan.lift Args.name
|
||||
--| (Scan.lift @{keyword "::"})
|
||||
|
|
@ -1255,20 +1255,20 @@ val _ = Theory.setup
|
|||
)
|
||||
|
||||
fun calculate_trace ctxt oid pos =
|
||||
(* grabs attribute, and converts its HOL-term into (textual) ML representation *)
|
||||
let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
|
||||
val term = calculate_attr_access_check ctxt "trace" oid pos
|
||||
val string_pair_list = map conv (HOLogic.dest_list term)
|
||||
val conv_2_ML = ML_Syntax.print_list(ML_Syntax.print_pair
|
||||
ML_Syntax.print_string
|
||||
ML_Syntax.print_string)
|
||||
in conv_2_ML string_pair_list end
|
||||
val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
|
||||
in ML_Syntax.print_list print_string_pair string_pair_list end
|
||||
|
||||
val _ = Theory.setup
|
||||
(ML_Antiquotation.inline @{binding trace_attribute}
|
||||
(fn (ctxt,toks) =>
|
||||
(Scan.lift (Parse.position Args.name)
|
||||
>> (fn(oid:string,pos) => ML_Syntax.atomic (calculate_trace ctxt oid pos))
|
||||
: string context_parser
|
||||
((Scan.lift (Parse.position Args.name)
|
||||
>>
|
||||
(fn(oid:string,pos) => ML_Syntax.atomic (calculate_trace ctxt oid pos))
|
||||
) : string context_parser
|
||||
)
|
||||
(ctxt, toks))
|
||||
)
|
||||
|
|
|
|||
|
|
@ -1,8 +1,10 @@
|
|||
chapter\<open> Example : Forward and Standard (use-after-define) Referencing\<close>
|
||||
|
||||
theory Example
|
||||
imports "../../ontologies/CENELEC_50126"
|
||||
begin
|
||||
|
||||
section{* Some show-off's of general antiquotations. *}
|
||||
section\<open> Some examples of Isabelle's standard antiquotations. \<close>
|
||||
(* some show-off of standard anti-quotations: *)
|
||||
text \<open>THIS IS A TEXT\<close>
|
||||
|
||||
|
|
@ -19,57 +21,67 @@ text\<open> @{thm refl} of name @{thm [source] refl}
|
|||
|
||||
|
||||
|
||||
section\<open> Core Examples for stating text-elements as doc-items.\<close>
|
||||
|
||||
section{* Example *}
|
||||
text\<open>An "anonymous" text-item, automatically coerced into the top-class "text".\<close>
|
||||
text*[tralala] \<open> Brexit means Brexit \<close>
|
||||
|
||||
text*[tralala] {* Brexit means Brexit *}
|
||||
text\<open>Examples for declaration of typed doc-items "assumption" and "hypothesis",
|
||||
concepts defined in the underlying ontology @{theory "CENELEC_50126"}. \<close>
|
||||
text*[ass1::assumption] \<open> The subsystem Y is safe. \<close>
|
||||
text*[hyp1::hypothesis] \<open> P inequal NP \<close>
|
||||
|
||||
text*[ass1::assumption] {* Brexit means Brexit *}
|
||||
|
||||
text*[hyp1::hypothesis] {* P inequal NP *}
|
||||
|
||||
|
||||
text*[ass122::srac] {* The overall sampling frequence of the odometer
|
||||
text\<open>A real example fragment from a larger project, declaring a text-element as a
|
||||
"safety-related application condition", a concept defined in the @{theory "CENELEC_50126"}
|
||||
ontology:\<close>
|
||||
text*[ass122::srac] \<open> The overall sampling frequence of the odometer
|
||||
subsystem is therefore 14 khz, which includes sampling, computing and
|
||||
result communication times... *}
|
||||
result communication times... \<close>
|
||||
|
||||
text*[t10::test_result] {* This is a meta-test. This could be an ML-command
|
||||
text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command
|
||||
that governs the external test-execution via, eg., a makefile or specific calls
|
||||
to a test-environment or test-engine *}
|
||||
to a test-environment or test-engine \<close>
|
||||
|
||||
|
||||
section\<open> References to doc-items.\<close>
|
||||
text\<open>Finally some examples of references to doc-items, i.e. text-elements with declared
|
||||
meta-information and status. \<close>
|
||||
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||
@{docref (define) \<open>t10\<close>} \<close>
|
||||
text \<open> the @{docref \<open>t10\<close>}
|
||||
as well as the @{docref \<open>ass122\<close>}\<close>
|
||||
text \<open> represent a justification of the safety related applicability
|
||||
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.
|
||||
\<close>
|
||||
condition @{srac \<open>ass122\<close>} aka exported constraint @{ec \<open>ass122\<close>}.\<close>
|
||||
|
||||
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
||||
|
||||
|
||||
|
||||
section\<open> Some Tests for Ontology Framework and its CENELEC Instance \<close>
|
||||
|
||||
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||
|
||||
|
||||
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
|
||||
|
||||
print_doc_classes
|
||||
print_doc_items
|
||||
|
||||
|
||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||
|
||||
|
||||
section{* Text Antiquotation Infrastructure ... *}
|
||||
section\<open> Text Antiquotation Infrastructure ... \<close>
|
||||
|
||||
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
|
||||
text{* @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. *}
|
||||
text\<open> @{docref \<open>lalala\<close>} -- produces warning. \<close>
|
||||
text\<open> @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>
|
||||
|
||||
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
|
||||
text\<open> @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>
|
||||
|
||||
text{* @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
|
||||
text\<open> @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
|
||||
Note that the link is actually a srac, which, according to
|
||||
the ontology, happens to be an "ec". *}
|
||||
the ontology, happens to be an "ec". \<close>
|
||||
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -2,42 +2,43 @@ theory Attributes
|
|||
imports "../../ontologies/Conceptual"
|
||||
begin
|
||||
|
||||
section\<open>Elementary Creation of DocItems and Access of their Attibutes\<close>
|
||||
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
|
||||
|
||||
text\<open>Current status:\<close>
|
||||
print_doc_classes
|
||||
print_doc_items
|
||||
|
||||
(* corresponds to low-level accesses : *)
|
||||
(* this corresponds to low-level accesses : *)
|
||||
ML\<open>
|
||||
val {docobj_tab={tab = x, ...},
|
||||
docclass_tab,
|
||||
ISA_transformer_tab,
|
||||
monitor_tab} = DOF_core.get_data @{context};
|
||||
Symtab.dest x;
|
||||
"==============================================";
|
||||
val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab}
|
||||
= DOF_core.get_data @{context};
|
||||
|
||||
Symtab.dest docitem_tab;
|
||||
Symtab.dest docclass_tab;
|
||||
\<close>
|
||||
|
||||
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
|
||||
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text\<open>document class declarations lead also HOL-type declarations (relevant for ontological links).\<close>
|
||||
typ "C"
|
||||
typ "D"
|
||||
|
||||
text\<open> ... as well as HOL-constant declarations (relevant for monitor rexps and tracres.).\<close>
|
||||
term "C"
|
||||
|
||||
text\<open>Voila what happens on the ML level:\<close>
|
||||
ML\<open>val Type("Conceptual.B.B_ext",[Type("Conceptual.C.C_ext",t)]) = @{typ "C"};
|
||||
val @{typ "D"} = ODL_Command_Parser.cid_2_cidType "Conceptual.D" @{theory};
|
||||
val @{typ "E"}= ODL_Command_Parser.cid_2_cidType "Conceptual.E" @{theory};
|
||||
val @{typ "E"} = ODL_Command_Parser.cid_2_cidType "Conceptual.E" @{theory};
|
||||
\<close>
|
||||
|
||||
text*[dfgdfg2::C, z = "None"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
text*[dfgdfg2::C, z = "None"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text*[omega::E, x = "''def''"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
|
||||
text*[omega::E, x = "''def''"]\<open> Lorem ipsum ... @{thm refl} \<close>
|
||||
|
||||
text\<open> As mentioned in @{docitem_ref \<open>dfgdfg\<close>} \<close>
|
||||
|
||||
|
||||
text\<open>Here is a simulation what happens on the level of the (HOL)-term representation:\<close>
|
||||
term "A.x (undefined\<lparr>A.x := 3\<rparr>)"
|
||||
term "B.x ((undefined::C)\<lparr>B.y := [''sdf'']\<rparr>)"
|
||||
term "C.z ((undefined::C)\<lparr>B.y := [''sdf''], z:= Some undefined\<rparr>)"
|
||||
|
|
@ -69,34 +70,34 @@ text\<open>A not too trivial test: default y -> [].
|
|||
The latter wins at access time.
|
||||
Then @{term "t"}: creation of a multi inheritance object omega,
|
||||
triple updates, the last one wins.\<close>
|
||||
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
|
||||
val t = HOLogic.dest_string (@{docitem_attr x::omega}); \<close>
|
||||
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg});
|
||||
val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \<close>
|
||||
|
||||
|
||||
|
||||
|
||||
section\<open>Mutation of Attibutes in DocItems\<close>
|
||||
|
||||
ML\<open> val Const("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \<close>
|
||||
ML\<open> val Const("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \<close>
|
||||
|
||||
update_instance*[omega::E, a2+="1"]
|
||||
|
||||
ML\<open> val (s as Const("Groups.one_class.one", @{typ "int"}))= @{docitem_attr a2 :: omega} \<close>
|
||||
ML\<open> val (s as Const("Groups.one_class.one", @{typ "int"}))= @{docitem_attribute a2 :: omega} \<close>
|
||||
|
||||
update_instance*[omega::E, a2+="6"]
|
||||
|
||||
ML\<open> @{docitem_attr a2::omega};
|
||||
val s = HOLogic.dest_number @{docitem_attr a2::omega} \<close>
|
||||
ML\<open> @{docitem_attribute a2::omega};
|
||||
val s = HOLogic.dest_number @{docitem_attribute a2::omega} \<close>
|
||||
|
||||
update_instance*[omega::E, x+="''inition''"]
|
||||
|
||||
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
|
||||
ML\<open> val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \<close>
|
||||
|
||||
update_instance*[omega::E, y+="[''defini'',''tion'']"]
|
||||
|
||||
update_instance*[omega::E, y+="[''en'']"]
|
||||
|
||||
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \<close>
|
||||
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \<close>
|
||||
|
||||
section\<open>Simulation of a Monitor\<close>
|
||||
|
||||
|
|
@ -122,17 +123,5 @@ ML\<open>@{trace_attribute figs1}\<close>
|
|||
print_doc_items
|
||||
print_doc_classes
|
||||
|
||||
ML\<open> DOF_core.get_object_global "sdf" @{theory};
|
||||
fold_aterms Term.add_const_names;
|
||||
fold_aterms (fn Const c => insert (op =) c | _ => I);
|
||||
val add_consts = fold_aterms (fn Const(c as (_,@{typ "doc_class rexp"})) => insert (op =) c
|
||||
| _ => I);
|
||||
fun compute_enabled_set cid thy =
|
||||
case DOF_core.get_doc_class_global cid thy of
|
||||
SOME X => map fst (fold add_consts (#rex X) [])
|
||||
| NONE => error("Internal error: class id undefined. ");
|
||||
|
||||
compute_enabled_set "Isa_DOF.figure_group" @{theory}
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
|
@ -55,6 +55,6 @@ a @{typ "C"}-type is required, but a @{typ "G"}-type is offered which is leagal
|
|||
update_instance*[xcv4::F, b+="{(@{docitem ''xcv3''},@{docitem ''xcv5''})}"]
|
||||
|
||||
text\<open>And here is the result on term level:\<close>
|
||||
ML\<open> @{docitem_attr b::xcv4} \<close>
|
||||
ML\<open> @{docitem_attribute b::xcv4} \<close>
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,39 +1,42 @@
|
|||
chapter\<open>Setting and modifying attributes of doc-items\<close>
|
||||
|
||||
theory Concept_Example
|
||||
imports "../../ontologies/Conceptual"
|
||||
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
|
||||
begin
|
||||
|
||||
text\<open>@{theory Conceptual} provides a monitor @{typ M} enforcing a particular document structure.
|
||||
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
|
||||
enabled for.\<close>
|
||||
open_monitor*[struct::M]
|
||||
|
||||
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
|
||||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||
|
||||
|
||||
text*[d::D, a1 = "X3"]
|
||||
\<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... @{docitem_ref \<open>c1\<close>} @{thm "refl"}\<close>
|
||||
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||
... @{docitem \<open>c1\<close>} @{thm "refl"}\<close>
|
||||
|
||||
|
||||
update_instance*[d::D, a1 := X2]
|
||||
|
||||
text{* ... in ut tortor ... @{docitem_ref \<open>a\<close>} ... @{A \<open>a\<close>}*}
|
||||
|
||||
(* text{* ... in ut tortor ... @{docitem_ref \<open>a\<close>} ... @{C \<open>a\<close>}*} *)
|
||||
|
||||
text*[c2::C, x = "''delta''"]
|
||||
\<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
|
||||
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>}\<close>
|
||||
|
||||
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
|
||||
|
||||
section*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
|
||||
|
||||
theorem some_proof : "P" sorry
|
||||
|
||||
|
||||
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
|
||||
update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"]
|
||||
|
||||
text{* ..., mauris amet, id elit aliquam aptent id, ... *}
|
||||
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
|
||||
|
||||
update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C),
|
||||
(@{docitem ''a''}, @{docitem ''c1''})}"]
|
||||
|
||||
close_monitor*[struct]
|
||||
ML\<open>@{trace_attribute struct}\<close>
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
Loading…
Reference in New Issue