Fix ML invariants bug
ci/woodpecker/push/build Pipeline failed
Details
ci/woodpecker/push/build Pipeline failed
Details
- The ML invariants are not checked anymore. Fix it
This commit is contained in:
Nicolas Méric
parent
9c324fde70
commit
289d47ee56
|
|
@ -1038,8 +1038,10 @@ fun check_sil oid _ ctxt =
|
|||
setup\<open>
|
||||
(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)
|
||||
\<close>
|
||||
|
||||
text\<open>
|
||||
|
|
@ -1114,8 +1116,11 @@ fun check_required_documents oid _ ctxt =
|
|||
setup\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
(* Test pattern matching for the records of the current CENELEC implementation classes,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
\<close>
|
||||
|
||||
(*setup\<open>DOF_core.add_ml_invariant "small_math.result" check_invariant_invariant\<close>*)
|
||||
|
|
@ -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
|
||||
\<close>
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -36,30 +36,32 @@ The implementor of an ontology must know what he does ...
|
|||
\<close>
|
||||
|
||||
text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
|
||||
|
||||
setup\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
ML\<open>DOF_core.binding_from_onto_class_pos "A" @{theory} \<close>
|
||||
text*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
|
||||
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
|
||||
ML\<open>
|
||||
setup\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
|
||||
text*[d0::A, x = "5"]\<open>Lorem ipsum dolor sit amet, ...\<close>
|
||||
|
||||
subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||
|
|
@ -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:
|
||||
\<close>
|
||||
|
||||
ML\<open>
|
||||
setup\<open>
|
||||
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
|
||||
\<close>
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
\<close>
|
||||
|
||||
section\<open>Miscelleous\<close>
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
\<close>
|
||||
|
||||
section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
|
||||
|
|
@ -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>\<open>()\<close>, 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)
|
||||
|
|
|
|||
Loading…
Reference in New Issue