forked from Isabelle_DOF/Isabelle_DOF
Fix declarations in traces bug
This commit is contained in:
parent
b96302f676
commit
3670d30ddf
|
@ -141,20 +141,13 @@ close_monitor*[struct]
|
||||||
|
|
||||||
text\<open>And the trace of the monitor is:\<close>
|
text\<open>And the trace of the monitor is:\<close>
|
||||||
ML\<open>val trace = @{trace_attribute struct}\<close>
|
ML\<open>val trace = @{trace_attribute struct}\<close>
|
||||||
ML\<open>@{assert} (trace =
|
|
||||||
[("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 =
|
ML\<open>@{assert} (trace =
|
||||||
[("Conceptual.A", "a0"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
|
[("Conceptual.A", "a0"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
|
||||||
("Conceptual.A", "ac"), ("Conceptual.A", "a1"),
|
("Conceptual.A", "ac"), ("Conceptual.A", "a1"),
|
||||||
("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
|
("Conceptual.C", "c1"), ("Conceptual.D", "d"), ("Conceptual.C", "c4"),
|
||||||
("Conceptual.A", "a2"), ("Conceptual.E", "e5"),
|
("Conceptual.A", "a2"), ("Conceptual.E", "e5"),
|
||||||
("Conceptual.E", "e6"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
|
("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
|
text\<open>Note that the monitor \<^typ>\<open>M\<close> of the ontology \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> does
|
||||||
not observe the common entities of \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>, but just those defined in the
|
not observe the common entities of \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>, but just those defined in the
|
||||||
|
|
|
@ -699,6 +699,13 @@ fun get_value_local oid ctxt =
|
||||||
let val Instance v = get_instance_global oid (Proof_Context.theory_of ctxt)
|
let val Instance v = get_instance_global oid (Proof_Context.theory_of ctxt)
|
||||||
in v |> #value end
|
in v |> #value end
|
||||||
|
|
||||||
|
fun get_defined_global oid thy = let val Instance d = get_instance_global oid thy
|
||||||
|
in d |> #defined end
|
||||||
|
|
||||||
|
fun get_defined_local oid ctxt =
|
||||||
|
let val Instance d = get_instance_global oid (Proof_Context.theory_of ctxt)
|
||||||
|
in d |> #defined end
|
||||||
|
|
||||||
(* missing : setting terms to ground (no type-schema vars, no schema vars. )*)
|
(* missing : setting terms to ground (no type-schema vars, no schema vars. )*)
|
||||||
|
|
||||||
fun binding_from_pos get_objects get_object_name name thy =
|
fun binding_from_pos get_objects get_object_name name thy =
|
||||||
|
@ -1621,7 +1628,10 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
||||||
(Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy)))
|
(Name_Space.dest_table (DOF_core.get_monitor_infos (Proof_Context.init_global thy)))
|
||||||
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
fun conv_attrs (((lhs, pos), opn), rhs) = (markup2string lhs,pos,opn,
|
||||||
Syntax.read_term_global thy rhs)
|
Syntax.read_term_global thy rhs)
|
||||||
val trace_attr = [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
val defined = DOF_core.get_defined_global oid thy
|
||||||
|
val trace_attr = if defined
|
||||||
|
then [((("trace", @{here}), "+="), "[("^cid_long^", ''"^oid^"'')]")]
|
||||||
|
else []
|
||||||
val assns' = map conv_attrs trace_attr
|
val assns' = map conv_attrs trace_attr
|
||||||
fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_instance_global oid thy
|
fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_instance_global oid thy
|
||||||
in #cid params end
|
in #cid params end
|
||||||
|
@ -1631,8 +1641,12 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy =
|
||||||
fun def_trans_value oid =
|
fun def_trans_value oid =
|
||||||
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
(#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns'))
|
||||||
#> value ctxt
|
#> value ctxt
|
||||||
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
|
val _ = if null enabled_monitors
|
||||||
val _ = app (fn (n, _) => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
|
then ()
|
||||||
|
else if defined
|
||||||
|
then (tracing "registrating in monitors ..." ;
|
||||||
|
app (fn (n, _) => tracing (oid^" : "^cid_long^" ==> "^n)) enabled_monitors)
|
||||||
|
else ()
|
||||||
(* check that any transition is possible: *)
|
(* check that any transition is possible: *)
|
||||||
fun class_inv_checks thy =
|
fun class_inv_checks thy =
|
||||||
enabled_monitors
|
enabled_monitors
|
||||||
|
|
Loading…
Reference in New Issue