nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Clean up check_invariants

This commit is contained in:
Nicolas Méric 2022-04-07 15:36:01 +02:00
parent 8e1702d2da
commit 74420a932f
1 changed files with 4 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
src/DOF/Isa_DOF.thy
View File

@ -1374,14 +1374,11 @@ fun check_invariants thy oid =
let
val value = the (DOF_core.get_value_global oid thy)
val cid = #cid (the (DOF_core.get_object_global oid thy))
(*val _ = writeln ("cid: " ^ @{make_string} (Long_Name.base_name cid))*)
fun get_all_invariants cid thy =
let val invs = #invs (the (DOF_core.get_doc_class_global cid thy))
in case DOF_core.get_doc_class_global cid thy of
NONE => error("undefined class id for invariants: " ^ cid)
| SOME ({inherits_from=NONE, ...}) => invs
| SOME ({inherits_from=SOME(_,father), ...}) => (invs) @ (get_all_invariants father thy)
end
case DOF_core.get_doc_class_global cid thy of
NONE => error("undefined class id for invariants: " ^ cid)
| SOME ({inherits_from=NONE, invs, ...}) => invs
| SOME ({inherits_from=SOME(_,father), invs, ...}) => (invs) @ (get_all_invariants father thy)
val invariants = get_all_invariants cid thy
val inv_and_apply_list =
let fun mk_inv_and_apply inv value thy =