From e01ec9fc21ca8dac01be7701801ed65ccf092d95 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Sun, 12 Feb 2023 17:57:35 +0100 Subject: [PATCH] Use a name space for ML invariants - Use a name space table to store ML inariants objects - Remove docclass_inv_tab, docclass_eager_inv_tab, and docclass_lazy_inv_tab tables and accesses --- .../Isabelle_DOF-Manual/04_RefMan.thy | 4 +- src/DOF/Isa_DOF.thy | 309 ++++++++++-------- .../CENELEC_50128/CENELEC_50128.thy | 27 +- .../scholarly_paper/scholarly_paper.thy | 18 +- src/ontologies/small_math/small_math.thy | 22 +- .../Concept_Example_Low_Level_Invariant.thy | 40 ++- 6 files changed, 261 insertions(+), 159 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy index 189a4578..26819e73 100644 --- a/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/04_RefMan.thy @@ -1218,8 +1218,8 @@ text\ Low-level invariants checking can be set up to be triggered when opening a monitor, when closing a monitor, or both - by using the \<^ML>\DOF_core.update_class_eager_invariant\, - \<^ML>\DOF_core.update_class_lazy_invariant\, or \<^ML>\DOF_core.update_class_invariant\ commands + by using the \<^ML>\DOF_core.add_opening_ml_invariant\, + \<^ML>\DOF_core.add_closing_ml_invariant\, or \<^ML>\DOF_core.add_ml_invariant\ commands respectively, to add the invariants to the theory context (See \<^technical>\sec:low_level_inv\ for an example). \ diff --git a/src/DOF/Isa_DOF.thy b/src/DOF/Isa_DOF.thy index 93a0c1a1..19390723 100644 --- a/src/DOF/Isa_DOF.thy +++ b/src/DOF/Isa_DOF.thy @@ -69,12 +69,13 @@ val def_suffixN = "_" ^ defN val defsN = defN ^ "s" val instances_of_suffixN = "_instances" val invariant_suffixN = "_inv" -val invariantN = "\" +val instance_placeholderN = "\" val makeN = "make" val schemeN = "_scheme" val instanceN = "instance" val monitor_infoN = "monitor_info" val isa_transformerN = "isa_transformer" +val ml_invariantN = "ml_invariant" (* derived from: theory_markup *) fun docref_markup_gen refN def name id pos = @@ -286,16 +287,134 @@ struct | NONE => raise TYPE ("Unknown isa_transformer: " ^ quote i, [], [])); - type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty + type ml_invariant = string -> {is_monitor:bool} -> Context.generic -> bool - type docclass_eager_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_eager_inv_tab : docclass_eager_inv_tab = Symtab.empty + structure ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); - type docclass_lazy_inv_tab = - (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table - val initial_docclass_lazy_inv_tab : docclass_lazy_inv_tab = Symtab.empty + val get_ml_invariants = ML_Invariants.get o Proof_Context.theory_of + + fun get_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_ml_invariants ctxt); + + fun add_ml_invariant name ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, ml_invariant) #> #2); + + fun update_ml_invariant name ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, ml_invariant) #> #2); + + fun update_ml_invariant_entry name new_ml_invariant thy = + thy |> ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_ml_invariant)); + + fun print_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown ml_invariant: " ^ quote i, [], [])); + + + structure Opening_ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_opening_ml_invariants = Opening_ML_Invariants.get o Proof_Context.theory_of + + fun get_opening_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_opening_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_opening_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_opening_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_opening_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_opening_ml_invariants ctxt); + + fun add_opening_ml_invariant name opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, opening_ml_invariant) #> #2); + + fun update_opening_ml_invariant name opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, opening_ml_invariant) #> #2); + + fun update_opening_ml_invariant_entry name new_opening_ml_invariant thy = + thy |> Opening_ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_opening_ml_invariant)); + + fun print_opening_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF Opening_ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_opening_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_opening_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown opening_ml_invariant: " ^ quote i, [], [])); + + structure Closing_ML_Invariants = Theory_Data + ( + type T = ml_invariant Name_Space.table; + val empty : T = Name_Space.empty_table ml_invariantN; + fun merge data : T = Name_Space.merge_tables data; + ); + + val get_closing_ml_invariants = Closing_ML_Invariants.get o Proof_Context.theory_of + + fun get_closing_ml_invariant_global cid thy = + Name_Space.check (Context.Theory thy) + (get_closing_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #2 + + fun get_closing_ml_invariant_name_global cid thy = + Name_Space.check (Context.Theory thy) + (get_closing_ml_invariants (Proof_Context.init_global thy)) (cid, Position.none) |> #1 + + fun check_closing_ml_invariant ctxt = + #1 o Name_Space.check (Context.Proof ctxt) (get_closing_ml_invariants ctxt); + + fun add_closing_ml_invariant name closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.define (Context.Theory thy) true (name, closing_ml_invariant) #> #2); + + fun update_closing_ml_invariant name closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.define (Context.Theory thy) false (name, closing_ml_invariant) #> #2); + + fun update_closing_ml_invariant_entry name new_closing_ml_invariant thy = + thy |> Closing_ML_Invariants.map + (Name_Space.map_table_entry name (fn _ => new_closing_ml_invariant)); + + fun print_closing_ml_invariants verbose ctxt = + Pretty.big_list "Isabelle.DOF Closing_ML_Invariants:" + (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_closing_ml_invariants ctxt))) + |> Pretty.writeln; + + fun the_closing_ml_invariant T i = + (case Name_Space.lookup_key T i of + SOME entry => entry + | NONE => raise TYPE ("Unknown closing_ml_invariant: " ^ quote i, [], [])); datatype monitor_info = Monitor_Info of @@ -349,29 +468,11 @@ struct (* registrating data of the Isa_DOF component *) structure Data = Generic_Data ( - type T = {docclass_tab : docclass_tab, - docclass_inv_tab : docclass_inv_tab, - docclass_eager_inv_tab : docclass_eager_inv_tab, - docclass_lazy_inv_tab : docclass_lazy_inv_tab} - val empty = {docclass_tab = initial_docclass_tab, - docclass_inv_tab = initial_docclass_inv_tab, - docclass_eager_inv_tab = initial_docclass_eager_inv_tab, - docclass_lazy_inv_tab = initial_docclass_lazy_inv_tab - } - fun merge( {docclass_tab = c1, - docclass_inv_tab = n1, - docclass_eager_inv_tab = en1, docclass_lazy_inv_tab = ln1}, - {docclass_tab = c2, - docclass_inv_tab = n2, - docclass_eager_inv_tab = en2, docclass_lazy_inv_tab = ln2}) = - {docclass_tab = merge_docclass_tab (c1,c2), - docclass_inv_tab = override(n1,n2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_eager_inv_tab = override(en1,en2), - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - docclass_lazy_inv_tab = override(ln1,ln2) - (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) - } + type T = {docclass_tab : docclass_tab} + val empty = {docclass_tab = initial_docclass_tab} + fun merge( {docclass_tab = c1}, + {docclass_tab = c2}) = + {docclass_tab = merge_docclass_tab (c1,c2) } ); @@ -381,36 +482,8 @@ val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; -fun upd_docclass_tab f {docclass_tab = y, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = f y, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; -fun upd_docclass_inv_tab f {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_tab, - docclass_inv_tab = f docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; - -fun upd_docclass_eager_inv_tab f {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=f docclass_eager_inv_tab, - docclass_lazy_inv_tab=docclass_lazy_inv_tab}; - -fun upd_docclass_lazy_inv_tab f {docclass_tab, - docclass_inv_tab, - docclass_eager_inv_tab, docclass_lazy_inv_tab} = - {docclass_tab = docclass_tab, - docclass_inv_tab=docclass_inv_tab, - docclass_eager_inv_tab=docclass_eager_inv_tab, - docclass_lazy_inv_tab=f docclass_lazy_inv_tab}; +fun upd_docclass_tab f {docclass_tab = y} = + {docclass_tab = f y}; fun get_accepted_cids (Monitor_Info {accepted_cids, ... }) = accepted_cids fun get_rejected_cids (Monitor_Info {rejected_cids, ... }) = rejected_cids @@ -497,57 +570,6 @@ fun is_virtual cid thy = let val tab = (#docclass_tab(get_data_global thy)) end -fun update_class_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_eager_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_eager_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Eager Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun update_class_lazy_invariant cid_long f thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - in map_data_global (upd_docclass_lazy_inv_tab (Symtab.update (cid_long, - (fn ctxt => ((writeln("Lazy Invariant check of: " ^cid_long); f ctxt )))))) - thy - end - -fun get_class_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_eager_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_eager_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_eager_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - -fun get_class_lazy_invariant cid_long thy = - let val _ = if is_defined_cid_global' cid_long thy then () - else error("undefined class id : " ^cid_long) - val {docclass_lazy_inv_tab, ...} = get_data_global thy - in case Symtab.lookup docclass_lazy_inv_tab cid_long of - NONE => K(K(K true)) - | SOME f => f - end - val SPY = Unsynchronized.ref(Bound 0) fun check_regexps term = @@ -1646,15 +1668,20 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = val assns' = map conv_attrs trace_attr fun cid_of oid = let val DOF_core.Instance params = DOF_core.get_object_global oid thy in #cid params end + val ctxt = Proof_Context.init_global thy fun def_trans_input_term oid = #1 o (calc_update_term {mk_elaboration=false} thy (cid_of oid) assns') fun def_trans_value oid = (#1 o (calc_update_term {mk_elaboration=true} thy (cid_of oid) assns')) - #> value (Proof_Context.init_global thy) + #> value ctxt val _ = if null enabled_monitors then () else writeln "registrating in monitors ..." val _ = app (fn (n, _) => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors; (* check that any transition is possible : *) - fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false} + fun inst_class_inv x = let val invs = DOF_core.get_ml_invariants ctxt + val check_option = Name_Space.lookup invs (cid_of x) + in case check_option of + NONE => (K true) + | SOME check => (check x {is_monitor=false}) end fun class_inv_checks ctxt = map (fn (x, _) => inst_class_inv x ctxt) enabled_monitors val delta_autoS = map is_enabled_for_cid enabled_monitors; fun update_info (n, aS, monitor_info) = @@ -1783,8 +1810,12 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi thy cid_long assns' defaults in (input_term, value_term') end else (\<^term>\()\, value_term') end - val check_inv = (DOF_core.get_class_invariant cid_long thy oid is_monitor) - o Context.Theory + val check_inv = Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid is_monitor) end) in thy |> DOF_core.define_object_global {define = define} ((oid, pos), {defined = false, input_term = fst value_terms, value = value (Proof_Context.init_global thy) @@ -1795,9 +1826,13 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi vcid = vcid}) |> register_oid_cid_in_open_monitors oid pos cid_pos' |> (fn thy => if #is_monitor(is_monitor) - then (((DOF_core.get_class_eager_invariant cid_long thy oid) is_monitor - o Context.Theory) thy; thy) - else thy) + then ((Context.Theory + #> (let val invs = DOF_core.get_opening_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid is_monitor) end)) thy; thy) + else thy) |> (fn thy => (check_inv thy; thy)) (* Bypass checking of high-level invariants when the class default_cid = "text", the top (default) document class. @@ -1992,9 +2027,13 @@ fun update_instance_command (((oid, pos), cid_pos), #1 o (Value_Command.Docitem_Parser.calc_update_term {mk_elaboration=true} thy cid_long assns') #> Value_Command.value (Proof_Context.init_global thy) - fun check_inv thy =((DOF_core.get_class_invariant cid_long thy oid {is_monitor=false} - o Context.Theory ) thy ; - thy) + fun check_inv thy = + ((Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=false}) end) ) thy ; thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug then DOF_core.update_value_input_term_global oid @@ -2062,11 +2101,21 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), val markup = DOF_core.get_object_name_global oid thy |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; - val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true} - o Context.Theory - val check_lazy_inv = (DOF_core.get_class_lazy_invariant cid_long thy oid) {is_monitor=true} - o Context.Theory - in thy |> (fn thy => (check_lazy_inv thy; thy)) + val check_inv = + Context.Theory + #> (let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=true}) end) + val check_closing_inv = + Context.Theory + #> (let val invs = DOF_core.get_closing_ml_invariants (Proof_Context.init_global thy) + val check_option = Name_Space.lookup invs cid_long + in case check_option of + NONE => (K true) + | SOME check => (check oid {is_monitor=true}) end) + in thy |> (fn thy => (check_closing_inv thy; thy)) |> update_instance_command args |> (fn thy => (check_inv thy; thy)) |> (fn thy => if Config.get_global thy DOF_core.invariants_checking @@ -2737,7 +2786,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy = $ (update_attribute_type thy class_scheme_ty cid_long t') | update_attribute_type thy class_scheme_ty cid_long (Abs(s, ty, t)) = Abs(s, ty, update_attribute_type thy class_scheme_ty cid_long t) - | update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = invariantN + | update_attribute_type _ class_scheme_ty _ (Free(s, ty)) = if s = instance_placeholderN then Free (s, class_scheme_ty) else Free (s, ty) | update_attribute_type _ _ _ t = t @@ -2747,7 +2796,7 @@ fun define_inv cid_long ((lbl, pos), inv) thy = current class. *) val inv_term' = update_attribute_type thy inv_ty cid_long inv_term val eq_inv_ty = inv_ty --> HOLogic.boolT - val abs_term = Term.lambda (Free (invariantN, inv_ty)) inv_term' + val abs_term = Term.lambda (Free (instance_placeholderN, inv_ty)) inv_term' in thy |> Named_Target.theory_map (define_cond bdg eq_inv_ty invariant_suffixN abs_term) end fun add_doc_class_cmd overloaded (raw_params, binding) diff --git a/src/ontologies/CENELEC_50128/CENELEC_50128.thy b/src/ontologies/CENELEC_50128/CENELEC_50128.thy index 14edeafd..80c50a1e 100644 --- a/src/ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/src/ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1030,7 +1030,14 @@ fun check_sil oid _ ctxt = in check_sil'' traces end \ -setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil\ +setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_ml_invariant binding check_sil thy end) +\ text\ A more generic example of check_sil which can be generalized: @@ -1066,7 +1073,14 @@ fun check_sil_slow oid _ ctxt = in check_sil' traces end \ -(*setup\DOF_core.update_class_invariant "CENELEC_50128.monitor_SIL0" check_sil_slow\*) +(*setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_ml_invariant binding check_sil_slow thy end) +\*) (* As traces of monitor instances (docitems) are updated each time an instance is declared (with text*, section*, etc.), invariants checking functions which check the full list of traces @@ -1096,7 +1110,14 @@ fun check_required_documents oid _ ctxt = in check_required_documents' accepted_cids end \ -setup\DOF_core.update_class_lazy_invariant "CENELEC_50128.monitor_SIL0" check_required_documents\ +setup\ +(fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "monitor_SIL0" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end + in DOF_core.add_closing_ml_invariant binding check_required_documents thy end) +\ (* Test pattern matching for the records of the current CENELEC implementation classes, and used by checking functions. diff --git a/src/ontologies/scholarly_paper/scholarly_paper.thy b/src/ontologies/scholarly_paper/scholarly_paper.thy index 05a034a6..5a364520 100644 --- a/src/ontologies/scholarly_paper/scholarly_paper.thy +++ b/src/ontologies/scholarly_paper/scholarly_paper.thy @@ -489,15 +489,17 @@ end end \ - -setup\ let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", +setup\ +(fn thy => +let val cidS = ["scholarly_paper.introduction","scholarly_paper.technical", "scholarly_paper.example", "scholarly_paper.conclusion"]; - fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check - ctxt cidS moni_oid NONE; - true) - in DOF_core.update_class_invariant "scholarly_paper.article" body end\ - -ML\ \ + fun body moni_oid _ ctxt = (Scholarly_paper_trace_invariant.check ctxt cidS moni_oid NONE; true) + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "article" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding body thy end) +\ section\Miscelleous\ diff --git a/src/ontologies/small_math/small_math.thy b/src/ontologies/small_math/small_math.thy index fc7cc4fb..5a1020f3 100644 --- a/src/ontologies/small_math/small_math.thy +++ b/src/ontologies/small_math/small_math.thy @@ -64,7 +64,9 @@ doc_class result = technical + -ML\fun check_invariant_invariant oid {is_monitor:bool} ctxt = +ML\ +fn thy => +let fun check_invariant_invariant oid {is_monitor:bool} ctxt = let val kind_term = ISA_core.compute_attr_access ctxt "kind" oid NONE @{here} val property_termS = ISA_core.compute_attr_access ctxt "property" oid NONE @{here} val tS = HOLogic.dest_list property_termS @@ -73,9 +75,14 @@ ML\fun check_invariant_invariant oid {is_monitor:bool} ctxt = else error("class class invariant violation") | _ => false end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "result" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_invariant_invariant thy end \ -setup\DOF_core.update_class_invariant "small_math.result" check_invariant_invariant\ +(*setup\DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\*) doc_class example = technical + @@ -164,10 +171,17 @@ end end \ -setup\ let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"]; +setup\ +fn thy => +let val cidS = ["small_math.introduction","small_math.technical", "small_math.conclusion"]; fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid NONE; true) - in DOF_core.update_class_invariant "small_math.article" body end\ + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "article" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding body thy end +\ end diff --git a/src/tests/Concept_Example_Low_Level_Invariant.thy b/src/tests/Concept_Example_Low_Level_Invariant.thy index de11e0a9..910b52f0 100644 --- a/src/tests/Concept_Example_Low_Level_Invariant.thy +++ b/src/tests/Concept_Example_Low_Level_Invariant.thy @@ -34,24 +34,35 @@ The implementor of an ontology must know what he does ... \ text\Setting a sample invariant, which simply produces some side-effect:\ -setup\DOF_core.update_class_invariant "Conceptual.A" (fn oid => - fn {is_monitor = b} => - fn ctxt => - (writeln ("sample echo : "^oid); true))\ +setup\ +fn thy => +let val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "A" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding (fn oid => + fn {is_monitor = b} => + fn ctxt => + (writeln ("sample echo : "^oid); true)) thy end +\ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ -ML\fun check_A_invariant oid {is_monitor:bool} ctxt = +ML\ +fn thy => +let fun check_A_invariant oid {is_monitor:bool} ctxt = let val term = ISA_core.compute_attr_access ctxt "x" oid NONE @{here} val (@{typ "int"},x_value) = HOLogic.dest_number term - in if x_value > 5 then error("class A invariant violation") else true end + in if x_value > 5 then error("class A invariant violation") else true end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "A" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_A_invariant thy end \ -setup\DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\ - - subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ @@ -79,7 +90,9 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\fun check_M_invariant oid {is_monitor} ctxt = +ML\ +fn thy => +let fun check_M_invariant oid {is_monitor} ctxt = let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} fun conv (\<^Const>\Pair \<^typ>\doc_class rexp\ \<^typ>\string\\ $ (\<^Const>\Atom \<^typ>\doc_class\\ $ (\<^Const>\mk\ $ s)) $ S) = @@ -93,10 +106,13 @@ ML\fun check_M_invariant oid {is_monitor} ctxt = val n = length (filter is_C cid_list) val m = length (filter is_D cid_list) in if m > n then error("class M invariant violation") else true end + val ctxt = Proof_Context.init_global thy + val binding = let val cid = DOF_core.read_cid ctxt "M" + in the ((DOF_core.get_data ctxt |> #docclass_tab |> Symtab.lookup) cid) + |> #name end +in DOF_core.add_ml_invariant binding check_M_invariant thy end \ -setup\DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\ - section\Example: Monitor Class Invariant\