diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index 84f381c1..78ab8653 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -12,16 +12,10 @@ print_doc_items ML\ 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; \ -ML\ -fun fac x = if x = 0 then 1 else x * (fac(x -1)); -fac 3; -open Thm; -\ text\A text item containing standard theorem antiquotations and complex meta-information.\ text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\ Lorem ipsum ... @{thm refl} \ @@ -136,6 +130,6 @@ text\@{trace_attribute figs1}\ text\Final Status:\ print_doc_items print_doc_classes - +check_doc_global end (*>*) diff --git a/test/conceptual/Attributes.thy b/test/conceptual/Attributes.thy deleted file mode 100644 index 451455f9..00000000 --- a/test/conceptual/Attributes.thy +++ /dev/null @@ -1,119 +0,0 @@ -theory Attributes - imports "../../ontologies/Conceptual" -begin - -section\Elementary Creation of DocItems and Access of their Attibutes\ - -text\Current status:\ -print_doc_classes -print_doc_items - -(* corresponds to low-level accesses : *) -ML\ -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; -\ - -text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ - -typ "C" -typ "D" -ML\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}; - \ - -text*[dfgdfg2::C, z = "None"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ - -text*[omega::E, x = "''def''"]\ sdfsdfs sdfsdf sdfsdf @{thm refl} \ - -text\ @{docitem_ref \dfgdfg\} \ - - -term "A.x (undefined\A.x := 3\)" -term "B.x ((undefined::C)\B.y := [''sdf'']\)" -term "C.z ((undefined::C)\B.y := [''sdf''], z:= Some undefined\)" - -ML\ -val SOME {def_occurrence = "Conceptual.A", long_name = "Conceptual.A.x", typ = t, def_pos} - = DOF_core.get_attribute_info "Conceptual.A" "x" @{theory}; -DOF_core.get_attribute_info "Conceptual.B" "x" @{theory}; -DOF_core.get_attribute_info "Conceptual.B" "y" @{theory}; -DOF_core.get_attribute_info "Conceptual.C" "x" @{theory}; -val SOME {def_occurrence = "Conceptual.C", long_name = "Conceptual.B.y", typ = t', def_pos} - = DOF_core.get_attribute_info "Conceptual.C" "y" @{theory}; - (* this is the situation where an attribute is defined in C, but due to inheritance - from B, where it is firstly declared which results in a different long_name. *) -DOF_core.get_attribute_info "Conceptual.C" "z" @{theory}; -\ - - -ML\ -DOF_core.get_value_local "sdf" @{context}; -DOF_core.get_value_local "sdfg" @{context}; -DOF_core.get_value_local "xxxy" @{context}; -DOF_core.get_value_local "dfgdfg" @{context}; -DOF_core.get_value_local "omega" @{context}; -\ - -text\A not too trivial test: default y -> []. - At creation : x -> "f", y -> "sdf". - The latter wins at access time. - Then @{term "t"}: creation of a multi inheritance object omega, - triple updates, the last one wins.\ -ML\val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg}); - val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \ - - - - -section\Mutation of Attibutes in DocItems\ - -ML\ val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \ - -update_instance*[omega::E, a2+="1"] - -ML\ val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attribute a2::omega} \ - -update_instance*[omega::E, a2+="6"] - -ML\ @{docitem_attribute a2::omega} \ -ML\ HOLogic.dest_number @{docitem_attribute a2::omega} \ - -update_instance*[omega::E, x+="''inition''"] - -ML\ val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \ - -update_instance*[omega::E, y+="[''defini'',''tion'']"] - -update_instance*[omega::E, y+="[''en'']"] - -ML\ val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \ - -section\Simulation of a Monitor\ - -open_monitor*[figs1::figure_group, - (* anchor="''fig-demo''", Achim ...*) - caption="''Sample ''"] - -figure*[fig_A::figure, spawn_columns=False,relative_width="90", - src="''figures/A.png''"] - \ The A train \ldots \ - -figure*[fig_B::figure, spawn_columns=False,relative_width="90", - src="''figures/B.png''"] - \ The B train \ldots \ - -close_monitor*[figs1] - -text\Resulting trace in figs1: \ -ML\@{trace_attribute figs1}\ - -print_doc_items - -check_doc_global - -end \ No newline at end of file