From 289d47ee56dcdb7af4c84d2183f7a98bb665722c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Nicolas=20M=C3=A9ric?= Date: Fri, 3 Mar 2023 11:41:48 +0100 Subject: [PATCH] Fix ML invariants bug - The ML invariants are not checked anymore. Fix it --- .../CENELEC_50128/CENELEC_50128.thy | 13 +- .../small_math/small_math.thy | 13 +- .../Concept_Example_Low_Level_Invariant.thy | 23 ++-- .../scholarly_paper/scholarly_paper.thy | 6 +- Isabelle_DOF/thys/Isa_DOF.thy | 118 ++++++++++++------ 5 files changed, 114 insertions(+), 59 deletions(-) diff --git a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy index 3608220..6a7d1e7 100644 --- a/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy +++ b/Isabelle_DOF-Ontologies/CENELEC_50128/CENELEC_50128.thy @@ -1038,8 +1038,10 @@ fun check_sil oid _ ctxt = setup\ (fn thy => let val ctxt = Proof_Context.init_global thy - val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy -in DOF_core.add_ml_invariant binding check_sil thy end) + val cid = "monitor_SIL0" + val binding = DOF_core.binding_from_onto_class_pos cid thy + val cid_long = DOF_core.get_onto_class_name_global cid thy +in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_sil, cid_long)) thy end) \ text\ @@ -1114,8 +1116,11 @@ fun check_required_documents oid _ ctxt = setup\ fn thy => let val ctxt = Proof_Context.init_global thy - val binding = DOF_core.binding_from_onto_class_pos "monitor_SIL0" thy -in DOF_core.add_closing_ml_invariant binding check_required_documents thy end + val cid = "monitor_SIL0" + val binding = DOF_core.binding_from_onto_class_pos cid thy + val cid_long = DOF_core.get_onto_class_name_global cid thy +in DOF_core.add_closing_ml_invariant binding + (DOF_core.make_ml_invariant (check_required_documents, cid_long)) thy end \ (* Test pattern matching for the records of the current CENELEC implementation classes, diff --git a/Isabelle_DOF-Ontologies/small_math/small_math.thy b/Isabelle_DOF-Ontologies/small_math/small_math.thy index 0a68c7d..906bbe6 100644 --- a/Isabelle_DOF-Ontologies/small_math/small_math.thy +++ b/Isabelle_DOF-Ontologies/small_math/small_math.thy @@ -76,8 +76,11 @@ let fun check_invariant_invariant oid {is_monitor:bool} ctxt = else error("class class invariant violation") | _ => false end - val binding = DOF_core.binding_from_onto_class_pos "result" thy -in DOF_core.add_ml_invariant binding check_invariant_invariant thy end + val cid = "result" + val cid_long = DOF_core.get_onto_class_name_global cid thy + val binding = DOF_core.binding_from_onto_class_pos cid thy +in DOF_core.add_ml_invariant binding + (DOF_core.make_ml_invariant (check_invariant_invariant, cid_long)) thy end \ (*setup\DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\*) @@ -175,8 +178,10 @@ let val cidS = ["small_math.introduction","small_math.technical", "small_math.co fun body moni_oid _ ctxt = (Small_Math_trace_invariant.check ctxt cidS moni_oid NONE; true) val ctxt = Proof_Context.init_global thy - val binding = DOF_core.binding_from_onto_class_pos "article" thy -in DOF_core.add_ml_invariant binding body thy end + val cid = "article" + val cid_long = DOF_core.get_onto_class_name_global cid thy + val binding = DOF_core.binding_from_onto_class_pos cid thy +in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end \ end diff --git a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy index 6e71804..61c4a97 100644 --- a/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy +++ b/Isabelle_DOF-Unit-Tests/Concept_Example_Low_Level_Invariant.thy @@ -36,30 +36,32 @@ The implementor of an ontology must know what he does ... \ text\Setting a sample invariant, which simply produces some side-effect:\ + setup\ fn thy => let val ctxt = Proof_Context.init_global thy - val bind = DOF_core.binding_from_onto_class_pos "A" thy + val cid_long = DOF_core.get_onto_class_name_global "A" thy + val bind = Binding.name "Sample_Echo" val exec = (fn oid => fn {is_monitor = b} => fn ctxt => (writeln ("sample echo : "^oid); true)) -in DOF_core.add_ml_invariant bind exec thy end +in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (exec, cid_long)) thy end \ ML\DOF_core.binding_from_onto_class_pos "A" @{theory} \ text*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ -ML\ +setup\ 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 - val binding = DOF_core.binding_from_onto_class_pos "A" thy -in DOF_core.add_ml_invariant binding check_A_invariant thy end + in if x_value > 5 then error("class A invariant violation") else true end + val cid_long = DOF_core.get_onto_class_name_global "A" thy + val bind = Binding.name "Check_A_Invariant" +in DOF_core.add_ml_invariant bind (DOF_core.make_ml_invariant (check_A_invariant, cid_long)) thy end \ - text*[d0::A, x = "5"]\Lorem ipsum dolor sit amet, ...\ subsection*[d::A, x = "4"] \ Lorem ipsum dolor sit amet, ... \ @@ -88,7 +90,7 @@ that instances of class C occur more often as those of class D; note that this i to take sub-classing into account: \ -ML\ +setup\ fn thy => let fun check_M_invariant oid {is_monitor} ctxt = let val term = ISA_core.compute_attr_access ctxt "trace" oid NONE @{here} @@ -104,8 +106,9 @@ let 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 binding = DOF_core.binding_from_onto_class_pos "M" thy -in DOF_core.add_ml_invariant binding check_M_invariant thy end + val cid_long = DOF_core.get_onto_class_name_global "M" thy + val binding = Binding.name "Check_M_Invariant" +in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (check_M_invariant, cid_long)) thy end \ diff --git a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy index e10afb7..4c3ec7c 100644 --- a/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy +++ b/Isabelle_DOF/ontologies/scholarly_paper/scholarly_paper.thy @@ -495,8 +495,10 @@ 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) val ctxt = Proof_Context.init_global thy - val binding = DOF_core.binding_from_onto_class_pos "article" thy -in DOF_core.add_ml_invariant binding body thy end) + val cid = "article" + val binding = DOF_core.binding_from_onto_class_pos cid thy + val cid_long = DOF_core.get_onto_class_name_global cid thy +in DOF_core.add_ml_invariant binding (DOF_core.make_ml_invariant (body, cid_long)) thy end) \ section\Miscelleous\ diff --git a/Isabelle_DOF/thys/Isa_DOF.thy b/Isabelle_DOF/thys/Isa_DOF.thy index bd914f4..572df89 100644 --- a/Isabelle_DOF/thys/Isa_DOF.thy +++ b/Isabelle_DOF/thys/Isa_DOF.thy @@ -142,6 +142,9 @@ fun map_snd f (x,y) = (x,f y) fun map_eq_fst_triple f (x,_,_) (y,_,_) = equal (f x) (f y) +fun lst_and_fun _ [] = true + | lst_and_fun x (f::fs) = (f x) andalso (lst_and_fun x fs) + \ section\ A HomeGrown Document Type Management (the ''Model'') \ @@ -351,7 +354,12 @@ struct | NONE => raise TYPE ("Unknown isa_transformer: " ^ quote i, [], [])); - type ml_invariant = string -> {is_monitor:bool} -> Context.generic -> bool + datatype ml_invariant = ML_Invariant of + {check : string -> {is_monitor:bool} -> Context.generic -> bool + , class : string} + + fun make_ml_invariant (check, class) = + ML_Invariant {check = check, class = class} structure ML_Invariants = Theory_Data ( @@ -486,8 +494,8 @@ struct fun make_monitor_info (accepted_cids, rejected_cids, automatas) = Monitor_Info {accepted_cids = accepted_cids, - rejected_cids = rejected_cids, - automatas = automatas} + rejected_cids = rejected_cids, + automatas = automatas} structure Monitor_Info = Theory_Data ( @@ -1605,11 +1613,17 @@ fun register_oid_cid_in_open_monitors oid pos cid_pos thy = 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 = 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 inst_class_inv x ctxt = + let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal x end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check x {is_monitor=false}) + in (lst_and_fun ctxt check_list') 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) = @@ -1737,12 +1751,18 @@ 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 = 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) + fun check_inv thy = + thy |> Context.Theory + |> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal cid_long end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check oid is_monitor) + in (lst_and_fun ctxt check_list') end) in thy |> DOF_core.define_object_global {define = define} ((oid, pos), DOF_core.make_instance (false, fst value_terms, @@ -1752,13 +1772,18 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi |> register_oid_cid_in_open_monitors oid pos cid_pos' |> (fn thy => if #is_monitor(is_monitor) 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) + #> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal cid_long end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check oid is_monitor) + in (lst_and_fun ctxt check_list') end)) thy; thy) else thy) - |> (fn thy => (check_inv thy; thy)) + |> tap check_inv (* Bypass checking of high-level invariants when the class default_cid = "text", the top (default) document class. We want the class default_cid to stay abstract @@ -1953,12 +1978,17 @@ fun update_instance_command (((oid, pos), cid_pos), thy cid_long assns') #> Value_Command.value (Proof_Context.init_global 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) + ((Context.Theory + #> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal cid_long end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check oid {is_monitor=false}) + in (lst_and_fun ctxt check_list') end) ) thy ; thy) in thy |> (if Config.get_global thy DOF_core.object_value_debug then DOF_core.update_value_input_term_global oid @@ -2023,22 +2053,32 @@ fun close_monitor_command (args as (((oid, pos), cid_pos), |> Name_Space.markup (Name_Space.space_of_table instances) val _ = Context_Position.report ctxt pos markup; 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) + Context.Theory + #> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal cid_long end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check oid {is_monitor=true}) + in (lst_and_fun ctxt check_list') 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) + Context.Theory + #> (fn ctxt => let val invs = DOF_core.get_ml_invariants (Proof_Context.init_global thy) + |> Name_Space.dest_table + val check_list = invs |> filter (fn (_, inv) => + let val DOF_core.ML_Invariant {class, ...} = inv + in class |> equal cid_long end) + |> map (fn (_, inv) => + let val DOF_core.ML_Invariant {check, ...} = inv + in check end) + val check_list' = check_list |> map (fn check => check oid {is_monitor=true}) + in (lst_and_fun ctxt check_list') end) in thy |> (fn thy => (check_closing_inv thy; thy)) |> update_instance_command args - |> (fn thy => (check_inv thy; thy)) + |> tap check_inv |> (fn thy => if Config.get_global thy DOF_core.invariants_checking then Value_Command.Docitem_Parser.check_invariants thy (oid, pos) else thy)